ebmc: add a basic test for CEGAR

diffblue · Dec 1, 2023 · f608044 · f608044
1 parent 78096a2
commit f608044
Show file tree

Hide file tree

Showing 2 changed files with 18 additions and 0 deletions.
diff --git a/regression/ebmc/cegar/basic1.desc b/regression/ebmc/cegar/basic1.desc
@@ -0,0 +1,6 @@
+KNOWNBUG
+basic1.sv
+--cegar
+SUCCESS$
+^EXIT=0$
+^SIGNAL=0$
diff --git a/regression/ebmc/cegar/basic1.sv b/regression/ebmc/cegar/basic1.sv
@@ -0,0 +1,12 @@
+module top(input clk);
+
+  reg important;
+  reg not_important;
+
+  initial important = 1;
+  always @(posedge clk)
+    important = important;
+
+  assert property (important == 1);
+
+endmodule