From a57c593c415c07a7849278e5809eeb9ace3c191b Mon Sep 17 00:00:00 2001
From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com>
Date: Wed, 16 Jul 2025 15:32:47 +1200
Subject: [PATCH] tests: Add equiv_assume.ys

---
 tests/various/equiv_assume.ys | 26 ++++++++++++++++++++++++++
 1 file changed, 26 insertions(+)
 create mode 100644 tests/various/equiv_assume.ys

diff --git a/tests/various/equiv_assume.ys b/tests/various/equiv_assume.ys
new file mode 100644
index 000000000..cb7731c29
--- /dev/null
+++ b/tests/various/equiv_assume.ys
@@ -0,0 +1,26 @@
+read_verilog -sv <<EOT
+module gold (input D, output Q);
+assign Q = '0;
+endmodule
+
+module gate (input D, output Q);
+assume property (D == '0);
+assign Q = D;
+endmodule
+EOT
+
+chformal -lower
+async2sync
+design -stash input
+
+# using $assert cells in sat verifies
+design -load input
+equiv_make -make_assert gold gate equiv
+prep -top equiv
+sat -set-assumes -prove-asserts -verify
+
+# so should $equiv
+design -load input
+equiv_make gold gate equiv
+equiv_simple equiv
+equiv_status -assert equiv