Merge pull request #746 from diffblue/eventually4

SVA: KNOWNBUG test for `s_eventually`
diffblue · Oct 1, 2024 · 2e01686 · 2e01686
2 parents 04b5682 + ac62b1f
commit 2e01686
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 0 deletions.
diff --git a/regression/verilog/SVA/eventually4.desc b/regression/verilog/SVA/eventually4.desc
@@ -0,0 +1,9 @@
+KNOWNBUG
+eventually4.sv
+--bound 2
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Property gives counterexample but should pass.
diff --git a/regression/verilog/SVA/eventually4.sv b/regression/verilog/SVA/eventually4.sv
@@ -0,0 +1,6 @@
+module main(input a);
+
+  // should pass for any bound
+  assert property ((s_eventually !a) or (always a));
+
+endmodule