KNOWNBUG test for signing cast

Author: kroening

Diff for: 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.

Diff for: 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