From fa68299b251127eb8a7375790e8a2a5294a914d1 Mon Sep 17 00:00:00 2001
From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com>
Date: Sat, 14 Jun 2025 11:06:38 +1200
Subject: [PATCH] tests/verific: Add chformal tests

---
 tests/verific/chformal.ys | 74 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 74 insertions(+)
 create mode 100644 tests/verific/chformal.ys

diff --git a/tests/verific/chformal.ys b/tests/verific/chformal.ys
new file mode 100644
index 000000000..0734f7bb7
--- /dev/null
+++ b/tests/verific/chformal.ys
@@ -0,0 +1,74 @@
+verific -formal <<EOT
+
+module top(input clk, a, en);
+    reg a_q = '0;
+    reg en_q = '0;
+
+    always @(posedge clk) begin
+        a_q <= a;
+        en_q <= en;
+    end
+
+    always @(posedge clk)
+        if (en_q)
+            assert(a_q);
+endmodule
+EOT
+
+prep
+
+design -save prep
+
+select -assert-count 1 t:$assert
+
+chformal -assert2assume
+
+select -assert-count 1 t:$assume
+
+chformal -assume2assert
+
+select -assert-count 1 t:$assert
+
+async2sync
+
+chformal -lower
+select -assert-count 1 t:$assert
+
+design -load prep
+
+chformal -assert2cover
+
+select -assert-count 1 t:$cover
+
+design -load prep
+
+chformal -assert2assume
+async2sync
+chformal -lower
+chformal -assume -early
+
+rename -enumerate -pattern assume_% t:$assume
+expose -evert t:$assume
+
+design -save gold
+
+design -load prep
+
+chformal -assert2assume
+chformal -assume -early
+async2sync
+chformal -lower
+
+rename -enumerate -pattern assume_% t:$assume
+expose -evert t:$assume
+
+design -save gate
+
+design -reset
+
+design -copy-from gold -as gold top
+design -copy-from gate -as gate top
+
+miter -equiv -flatten -make_assert gold gate miter
+
+sat -verify -prove-asserts -tempinduct miter