Skip to content

Commit f5fa309

Browse files
committed
Verilog: $signed(!0) is -1
This fixes the typing of $signed when given a Boolean argument.
1 parent 150f03a commit f5fa309

File tree

3 files changed

+20
-1
lines changed

3 files changed

+20
-1
lines changed
Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
signed2.sv
3+
--bound 0
4+
^\[main\.p0\] always \$signed\(1\) == 1: PROVED up to bound 0$
5+
^\[main\.p1\] always \$signed\(1'b1\) == -1: PROVED up to bound 0$
6+
^\[main\.p2\] always \$signed\(-1\) == -1: PROVED up to bound 0$
7+
^\[main\.p3\] always \$signed\(!0\) == -1: PROVED up to bound 0$
8+
^EXIT=0$
9+
^SIGNAL=0$
10+
--
11+
^warning: ignoring
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
module main;
2+
3+
p0: assert final ($signed(1) == 1);
4+
p1: assert final ($signed(1'b1) == -1);
5+
p2: assert final ($signed(-1) == -1);
6+
p3: assert final ($signed(!0) == -1);
7+
8+
endmodule

src/verilog/verilog_typecheck_expr.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -784,7 +784,7 @@ exprt verilog_typecheck_exprt::convert_system_function(
784784
}
785785
else if(argument.type().id()==ID_bool)
786786
{
787-
expr.type() = signedbv_typet{2};
787+
expr.type() = signedbv_typet{1};
788788
return std::move(expr);
789789
}
790790
else

0 commit comments

Comments
 (0)