Merge pull request #872 from diffblue/fix-signed-on-bool

Fix `$signed` on bool

Author: tautschnig

regression/verilog/expressions/signing_cast1.desc

@@ -0,0 +1,15 @@
+KNOWNBUG
+signing_cast1.sv
+--module main --bound 0
+^\[main\.p0\] always signed \[0:0\]'\(1'b1\) == -1: PROVED up to bound 0$
+^\[main\.p1\] always signed \[0:0\]'\(4'b1110\) == -2: PROVED up to bound 0$
+^\[main\.p2\] always signed \[0:0\]'\(4'b0111\) == 7: PROVED up to bound 0$
+^\[main\.p3\] always signed \[0:0\]'\(!0\) == -1: PROVED up to bound 0$
+^\[main\.p4\] always \[0:0\]'\(!0\) == 1: PROVED up to bound 0$
+^\[main\.p5\] always \[0:0\]'\(-1\) == 32'hFFFFFFFF: PROVED up to bound 0$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The width of the operand is not preserved.

regression/verilog/expressions/signing_cast1.sv

@@ -0,0 +1,14 @@
+module main;
+
+  // 1800-2017 6.24.1
+  p0: assert final (signed'(1'b1) == -1);
+  p1: assert final (signed'(4'b1110) == -2);
+  p2: assert final (signed'(4'b0111) == 7);
+  p3: assert final (signed'(!0) == -1);
+  p4: assert final (unsigned'(!0) == 1);
+  p5: assert final (unsigned'(-1) == 32'hffff_ffff);
+
+  // signing casts yield constants
+  parameter Q = signed'(1);
+
+endmodule

regression/verilog/system-functions/signed2.desc

@@ -0,0 +1,11 @@
+CORE
+signed2.sv
+--bound 0
+^\[main\.p0\] always \$signed\(1\) == 1: PROVED up to bound 0$
+^\[main\.p1\] always \$signed\(1'b1\) == -1: PROVED up to bound 0$
+^\[main\.p2\] always \$signed\(-1\) == -1: PROVED up to bound 0$
+^\[main\.p3\] always \$signed\(!0\) == -1: PROVED up to bound 0$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/system-functions/signed2.sv

@@ -0,0 +1,8 @@
+module main;
+
+  p0: assert final ($signed(1) == 1);
+  p1: assert final ($signed(1'b1) == -1);
+  p2: assert final ($signed(-1) == -1);
+  p3: assert final ($signed(!0) == -1);
+
+endmodule

src/verilog/verilog_typecheck_expr.cpp

@@ -784,7 +784,7 @@ exprt verilog_typecheck_exprt::convert_system_function(
     }
     else if(argument.type().id()==ID_bool)
     {
-      expr.type() = signedbv_typet{2};
+      expr.type() = signedbv_typet{1};
       return std::move(expr);
     }
     else