Merge pull request #869 from diffblue/verilog-retain-explicit-casts

SystemVerilog: retain explicit casts

Author: tautschnig

regression/verilog/case/riscv-alu.desc

@@ -4,11 +4,11 @@ riscv-alu.sv
 ^\[alu\.pADD\] always alu\.op == \{ 7'b0000000, 3'b000 \} -> alu\.out == alu\.a \+ alu\.b: PROVED up to bound 0$
 ^\[alu\.pSUB\] always alu\.op == \{ 7'b0100000, 3'b000 \} -> alu\.out == alu\.a - alu\.b: PROVED up to bound 0$
 ^\[alu\.pSLL\] always alu\.op == \{ 7'b0000000, 3'b001 \} -> alu\.out == alu\.a << alu\.b\[4:0\]: PROVED up to bound 0$
-^\[alu\.pSLT\] always alu\.op == \{ 7'b0000000, 3'b010 \} -> alu\.out == alu\.a < alu\.b: PROVED up to bound 0$
+^\[alu\.pSLT\] always alu\.op == \{ 7'b0000000, 3'b010 \} -> alu\.out == \$signed\(alu\.a\) < \$signed\(alu\.b\): PROVED up to bound 0$
 ^\[alu\.pSLTU\] always alu\.op == \{ 7'b0000000, 3'b011 \} -> alu\.out == alu\.a < alu\.b: PROVED up to bound 0$
 ^\[alu\.pXOR\] always alu\.op == \{ 7'b0000000, 3'b100 \} -> alu\.out == \(alu\.a \^ alu\.b\): PROVED up to bound 0$
 ^\[alu\.pSRL\] always alu\.op == \{ 7'b0000000, 3'b101 \} -> alu\.out == alu\.a >> alu\.b\[4:0\]: PROVED up to bound 0$
-^\[alu\.pSRA\] always alu\.op == \{ 7'b0100000, 3'b101 \} -> alu\.out == alu\.a >>> alu\.b\[4:0\]: PROVED up to bound 0$
+^\[alu\.pSRA\] always alu\.op == \{ 7'b0100000, 3'b101 \} -> alu\.out == \$signed\(alu\.a\) >>> alu\.b\[4:0\]: PROVED up to bound 0$
 ^\[alu\.pOR\] always alu\.op == \{ 7'b0000000, 3'b110 \} -> alu\.out == \(alu\.a | alu\.b\): PROVED up to bound 0$
 ^\[alu\.pAND\] always alu\.op == \{ 7'b0000000, 3'b111 \} -> alu\.out == \(alu\.a & alu\.b\): PROVED up to bound 0$
 ^EXIT=0$

regression/verilog/enums/enum4.desc

@@ -3,5 +3,5 @@ enum4.sv
 --bound 0
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main\.p1\] always main\.A == 1: PROVED up to bound 0$
+^\[main\.p1\] always main\.A == \[7:0\]'\(1\): PROVED up to bound 0$
 --

regression/verilog/enums/enum_cast1.desc

@@ -3,6 +3,6 @@ enum_cast1.sv
 --bound 0
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main\.p1\] always main.A == 1: PROVED up to bound 0$
-^\[main\.p2\] always main.B == 2: PROVED up to bound 0$
+^\[main\.p1\] always main.A == signed \[31:0\]'\(1\): PROVED up to bound 0$
+^\[main\.p2\] always main.B == signed \[31:0\]'\(2\): PROVED up to bound 0$
 --

regression/verilog/expressions/signed1.desc

@@ -1,6 +1,14 @@
 CORE
 signed1.sv
 --module main --bound 0
+^\[main\.p1\] always main\.wire1 == main.wire2: PROVED up to bound 0$
+^\[main\.p2\] always main\.wire1 >>> 1 == -1: PROVED up to bound 0$
+^\[main\.p3\] always main\.wire2 >> 1 != -1: PROVED up to bound 0$
+^\[main\.p4\] always main\.wire1\[31:0\] >> 1 != -1: PROVED up to bound 0$
+^\[main\.p5\] always \$unsigned\(main\.wire1\) >> 1 != -1: PROVED up to bound 0$
+^\[main\.p6\] always \$signed\(main\.wire2\) >>> 1 == -1: PROVED up to bound 0$
+^\[main\.p7\] always -1 >> 1 != -1: PROVED up to bound 0$
+^\[main\.p8\] always -1 >>> 1 == -1: PROVED up to bound 0$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/expressions/size_cast1.desc

@@ -1,6 +1,10 @@
 CORE
 size_cast1.sv
 --module main --bound 0
+^\[main\.p0\] always \$bits\(10'\(1\)\) == 10: PROVED up to bound 0$
+^\[main\.p1\] always \$bits\(20'\(1\)\) == 20: PROVED up to bound 0$
+^\[main\.p2\] always 10'\(-1\) == -1: PROVED up to bound 0$
+^\[main\.p3\] always 2'\(1 == 1\) == 1: PROVED up to bound 0$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/expressions/size_cast1.sv

@@ -7,4 +7,7 @@ module main;
   p2: assert final (10'(-1) == -1);
   p3: assert final (2'(1==1) == 1);
 
+  // size-casts yield constants
+  parameter Q = 10'(1);
+
 endmodule

regression/verilog/expressions/static_cast1.desc

@@ -1,8 +1,8 @@
 CORE
 static_cast1.sv
 --module main --bound 0
+^\[main\.p0\] always \[7:0\]'\(32'hFFFF\) == 255: PROVED up to bound 0$
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main\.p0\] always 32'hFFFF == 255: PROVED up to bound 0$
 --
 ^warning: ignoring

regression/verilog/expressions/static_cast1.sv

@@ -4,4 +4,7 @@ module main;
 
   p0: assert final (eight_bits'('hffff) == 'hff);
 
+  // static casts yield constants
+  parameter Q = eight_bits'('hffff);
+
 endmodule

regression/verilog/system-functions/signed1.desc

@@ -0,0 +1,7 @@
+CORE
+signed1.v
+--bound 0
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/system-functions/signed1.v

@@ -0,0 +1,5 @@
+module main;
+
+  parameter Q = $signed(123);
+
+endmodule