Tests: Extra equiv_assume tests

tests/various/equiv_assume.ys

@@ -26,3 +26,91 @@ design -load input
 equiv_make gold gate equiv
 equiv_simple -set-assumes equiv
 equiv_status -assert equiv
+
+# and it works through cells
+design -reset
+read_verilog -sv <<EOT
+module gold (input [1:0] D, output [1:0] Q);
+assign Q = !D;
+endmodule
+
+module gate (input [1:0] D, output [1:0] Q);
+assume property (D == 2'b11);
+wire [1:0] G = ~D;
+assign Q = G;
+endmodule
+EOT
+
+chformal -lower
+async2sync
+design -stash input2
+
+design -load input2
+equiv_make -make_assert gold gate equiv
+prep -top equiv
+sat -set-assumes -prove-asserts -verify
+
+design -load input2
+equiv_make gold gate equiv
+equiv_simple -set-assumes equiv
+equiv_status -assert equiv
+
+# and registers
+design -reset
+read_verilog -sv <<EOT
+module gold (input clk, input [1:0] D, output [1:0] Q);
+assign Q = '0;
+endmodule
+
+module gate (input clk, input [1:0] D, output [1:0] Q);
+reg [1:0] Dreg;
+assume property (Dreg == 2'b11);
+always @(clk) begin
+    Dreg <= D;
+end
+assign Q = ~Dreg;
+endmodule
+EOT
+
+proc
+chformal -lower
+async2sync
+design -stash input3
+
+design -load input3
+equiv_make -make_assert gold gate equiv
+prep -top equiv
+sat -set-assumes -prove-asserts -verify
+
+design -load input3
+equiv_make gold gate equiv
+equiv_simple -set-assumes equiv
+equiv_status -assert equiv
+
+# so long as the assumption doesn't end up after the equiv
+design -reset
+read_verilog -sv <<EOT
+module gold (input [1:0] D, output [1:0] Q);
+assign Q = !D;
+endmodule
+
+module gate (input [1:0] D, output [1:0] Q);
+assume property (G == 2'b00);
+wire [1:0] G = ~D;
+assign Q = G;
+endmodule
+EOT
+
+chformal -lower
+async2sync
+design -stash input4
+
+design -load input4
+equiv_make -make_assert gold gate equiv
+prep -top equiv
+sat -set-assumes -prove-asserts
+
+design -load input4
+equiv_make gold gate equiv
+equiv_simple -set-assumes equiv
+equiv_status equiv