Skip to content

Commit f2736e5

Browse files
committed
Verilog: fix for signed constants
Verilog allows constants to be marked as signed (e.g., 'sb1). When using base 2, 8 and 16, these need to be sign extended to 32 bits unless the number of bits is given.
1 parent a52c32b commit f2736e5

File tree

5 files changed

+82
-27
lines changed

5 files changed

+82
-27
lines changed

regression/verilog/expressions/equality1.desc

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -5,10 +5,10 @@ equality1.v
55
^\[.*\] always 10 == 20 === 0: PROVED up to bound 0$
66
^\[.*\] always 10 != 20 === 1: PROVED up to bound 0$
77
^\[.*\] always 10 == 20 === 0: PROVED up to bound 0$
8-
^\[.*\] always 1'bx == 10 === 1'bx: PROVED up to bound 0$
9-
^\[.*\] always 1'bz == 20 === 1'bx: PROVED up to bound 0$
10-
^\[.*\] always 1'bx != 10 === 1'bx: PROVED up to bound 0$
11-
^\[.*\] always 1'bz != 20 === 1'bx: PROVED up to bound 0$
8+
^\[.*\] always 32'b0000000000000000000000000000000x == 10 === 32'b0000000000000000000000000000000x: PROVED up to bound 0$
9+
^\[.*\] always 32'b0000000000000000000000000000000z == 20 === 32'b0000000000000000000000000000000x: PROVED up to bound 0$
10+
^\[.*\] always 32'b0000000000000000000000000000000x != 10 === 32'b0000000000000000000000000000000x: PROVED up to bound 0$
11+
^\[.*\] always 32'b0000000000000000000000000000000z != 20 === 32'b0000000000000000000000000000000x: PROVED up to bound 0$
1212
^\[.*\] always 2'b11 == 2'b11 === 0: REFUTED$
1313
^\[.*\] always 2'sb11 == 2'sb11 === 1: PROVED up to bound 0$
1414
^EXIT=10$

regression/verilog/expressions/equality2.desc

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -5,11 +5,11 @@ equality2.v
55
^\[.*\] always 10 === 20 == 0: PROVED up to bound 0$
66
^\[.*\] always 10 !== 10 == 0: PROVED up to bound 0$
77
^\[.*\] always 10 !== 20 == 1: PROVED up to bound 0$
8-
^\[.*\] always 1'bx === 1'bx == 1: PROVED up to bound 0$
9-
^\[.*\] always 1'bz === 1'bz == 1: PROVED up to bound 0$
10-
^\[.*\] always 1'bx === 1'bz == 0: PROVED up to bound 0$
11-
^\[.*\] always 1'bx === 1 == 0: PROVED up to bound 0$
12-
^\[.*\] always 1'bz === 1 == 0: PROVED up to bound 0$
8+
^\[.*\] always 32'b0000000000000000000000000000000x === 32'b0000000000000000000000000000000x == 1: PROVED up to bound 0$
9+
^\[.*\] always 32'b0000000000000000000000000000000z === 32'b0000000000000000000000000000000z == 1: PROVED up to bound 0$
10+
^\[.*\] always 32'b0000000000000000000000000000000x === 32'b0000000000000000000000000000000z == 0: PROVED up to bound 0$
11+
^\[.*\] always 32'b0000000000000000000000000000000x === 1 == 0: PROVED up to bound 0$
12+
^\[.*\] always 32'b0000000000000000000000000000000z === 1 == 0: PROVED up to bound 0$
1313
^\[.*\] always 1 === 1 == 1: PROVED up to bound 0$
1414
^\[.*\] always 3'b011 === 3'b111 == 1: REFUTED$
1515
^\[.*\] always 3'sb111 === 3'sb111 == 1: PROVED up to bound 0$
Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,8 @@
1-
KNOWNBUG
1+
CORE
22
signed2.sv
33
--bound 0
44
^EXIT=0$
55
^SIGNAL=0$
66
--
77
^warning: ignoring
88
--
9-
The signed base 2 literal should be sign-extended.
Lines changed: 26 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,30 @@
11
module main;
22

3-
p0: assert final ('sb1 == -1);
4-
p1: assert final ('sb11 == -1);
5-
p2: assert final (4'sb111 == 7);
3+
// base 2
4+
pA0: assert final ('sb1 == -1);
5+
pA1: assert final ('sb01 == 1);
6+
pA2: assert final ('sb1x === 'sb1111111111111111111111111111111x);
7+
pA3: assert final ($bits('sb1) == 32);
8+
pA4: assert final ('sb11 == -1);
9+
pA5: assert final (4'sb111 == 7);
10+
pA6: assert final ($bits(4'sb111) == 4);
11+
12+
// base 8
13+
pB0: assert final ('so7 == -1);
14+
pB1: assert final ('so1 == 1);
15+
pB2: assert final ('so7x === 'so3777777777x);
16+
pB3: assert final ($bits('so1) == 32);
17+
pB4: assert final ('so77 == -1);
18+
pB5: assert final (4'so7 == 7);
19+
pB6: assert final ($bits(4'so7) == 4);
20+
21+
// base 16
22+
pC0: assert final ('shf == -1);
23+
pC1: assert final ('sh1 == 1);
24+
pC2: assert final ('shfx === 'shfffffffx);
25+
pC3: assert final ($bits('sh1) == 32);
26+
pC4: assert final ('shff == -1);
27+
pC5: assert final (8'shf == 15);
28+
pC6: assert final ($bits(8'shf) == 8);
629

730
endmodule

src/verilog/verilog_typecheck_expr.cpp

Lines changed: 46 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -1223,14 +1223,14 @@ exprt verilog_typecheck_exprt::convert_constant(constant_exprt expr)
12231223
// check representation
12241224

12251225
std::string::size_type pos=rest.find('\'');
1226-
unsigned bits=0;
1226+
std::size_t bits = 0;
12271227
bool bits_given=false;
12281228

12291229
if(pos!=std::string::npos) // size given?
12301230
{
12311231
if(rest[0]!='\'')
12321232
{
1233-
bits=atoi(rest.c_str());
1233+
bits = atol(rest.c_str());
12341234
bits_given=true;
12351235

12361236
if(bits==0)
@@ -1273,14 +1273,13 @@ exprt verilog_typecheck_exprt::convert_constant(constant_exprt expr)
12731273
bool is_signed=!based || s_flag_given;
12741274

12751275
// check for z/x
1276-
1277-
bool other=false;
1276+
bool four_valued = false;
12781277

12791278
for(unsigned i=0; i<rest.size(); i++)
12801279
if(rest[i]=='?' || rest[i]=='z' || rest[i]=='x')
1281-
other=true;
1280+
four_valued = true;
12821281

1283-
if(other) // z/x/? found
1282+
if(base != 10)
12841283
{
12851284
// expand bits
12861285

@@ -1370,17 +1369,51 @@ exprt verilog_typecheck_exprt::convert_constant(constant_exprt expr)
13701369
bits=fvalue.size();
13711370
}
13721371

1373-
if(is_signed)
1374-
expr.type()=verilog_signedbv_typet(bits);
1375-
else
1376-
expr.type()=verilog_unsignedbv_typet(bits);
1372+
if(four_valued)
1373+
{
1374+
// we do a 32-bit minimum if the number of bits isn't given
1375+
if(!bits_given)
1376+
{
1377+
if(bits < 32)
1378+
{
1379+
// do sign extension
1380+
char extension = is_signed ? fvalue.front() : '0';
1381+
fvalue = std::string(32 - bits, extension) + fvalue;
1382+
bits = 32;
1383+
}
1384+
}
1385+
1386+
if(is_signed)
1387+
expr.type() = verilog_signedbv_typet(bits);
1388+
else
1389+
expr.type() = verilog_unsignedbv_typet(bits);
13771390

1378-
expr.set(ID_value, fvalue);
1391+
// stored as individual bits
1392+
expr.set_value(fvalue);
1393+
}
1394+
else // two valued
1395+
{
1396+
mp_integer int_value = binary2integer(fvalue, is_signed);
1397+
1398+
// we do a 32-bit minimum if the number of bits isn't given
1399+
if(!bits_given)
1400+
if(bits < 32)
1401+
bits = 32;
1402+
1403+
if(is_signed)
1404+
expr.type() = signedbv_typet(bits);
1405+
else
1406+
expr.type() = unsignedbv_typet(bits);
1407+
1408+
// stored as bvrep
1409+
expr.set_value(integer2bvrep(int_value, bits));
1410+
}
13791411
}
13801412
else
13811413
{
1414+
// base 10, never negative
13821415
mp_integer int_value=string2integer(rest, base);
1383-
1416+
13841417
if(!bits_given)
13851418
{
13861419
bits = address_bits(int_value + 1);
@@ -1393,7 +1426,7 @@ exprt verilog_typecheck_exprt::convert_constant(constant_exprt expr)
13931426
else
13941427
expr.type()=unsignedbv_typet(bits);
13951428

1396-
expr.set(ID_value, integer2bvrep(int_value, bits));
1429+
expr.set_value(integer2bvrep(int_value, bits));
13971430
}
13981431

13991432
return std::move(expr);

0 commit comments

Comments
 (0)