Skip to content

Commit e32bd10

Browse files
authored
Merge pull request #269 from diffblue/verilog-string
Verilog: fix string literals
2 parents 89ae7ce + 943cdbb commit e32bd10

File tree

3 files changed

+31
-14
lines changed

3 files changed

+31
-14
lines changed
Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
string_literals1.v
3+
--bound 0
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
^warning: ignoring
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
module main;
2+
3+
// padded from left with zeros
4+
wire [6*8-1:0] hello = "hello";
5+
always assert p0: hello[0*8+7:0*8] == "o";
6+
always assert p1: hello[1*8+7:1*8] == "l";
7+
always assert p2: hello[2*8+7:2*8] == "l";
8+
always assert p3: hello[3*8+7:3*8] == "e";
9+
always assert p4: hello[4*8+7:4*8] == "h";
10+
always assert p5: hello[5*8+7:5*8] == 0;
11+
12+
endmodule

src/verilog/verilog_typecheck_expr.cpp

Lines changed: 12 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -900,23 +900,21 @@ void verilog_typecheck_exprt::convert_constant(constant_exprt &expr)
900900
{
901901
if(expr.type().id()==ID_string)
902902
{
903-
exprt new_expr;
903+
// These are unsigned integer vectors with 8 bits per character.
904+
// The first character is the most significant one.
904905
const std::string &value=expr.get_string(ID_value);
906+
auto type = unsignedbv_typet(value.size() * 8);
905907

906-
new_expr.type()=unsignedbv_typet(value.size()*8);
907-
908-
std::string new_value;
909-
910-
for(unsigned i=0; i<value.size(); i++)
911-
for(unsigned bit=0; bit<8; bit++)
912-
{
913-
bool b=(value[i]&(1<<bit))!=0;
914-
new_value=(b?"1":"0")+new_value;
915-
}
908+
// The below is quadratic, and should be made linear.
909+
mp_integer new_value = 0;
910+
for(std::size_t i = 0; i < value.size(); i++)
911+
{
912+
unsigned char character = value[i];
913+
new_value += mp_integer(character) << ((value.size() - i - 1) * 8);
914+
}
916915

917-
new_expr.set(ID_value, new_value);
918-
919-
expr.swap(new_expr);
916+
expr =
917+
from_integer(new_value, type).with_source_location<constant_exprt>(expr);
920918
return;
921919
}
922920
else if(expr.type().id()==ID_unsignedbv ||

0 commit comments

Comments
 (0)