From 5ec189a2f5023f72f897f7fa3842fd8cc2a94f25 Mon Sep 17 00:00:00 2001
From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com>
Date: Wed, 16 Jul 2025 21:05:03 +1200
Subject: [PATCH] Tests: Extra equiv_assume tests

---
 tests/various/equiv_assume.ys | 88 +++++++++++++++++++++++++++++++++++
 1 file changed, 88 insertions(+)

diff --git a/tests/various/equiv_assume.ys b/tests/various/equiv_assume.ys
index 0033ac95c..7264e5a29 100644
--- a/tests/various/equiv_assume.ys
+++ b/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