Skip to content

Commit 2e01686

Browse files
authored
Merge pull request #746 from diffblue/eventually4
SVA: KNOWNBUG test for `s_eventually`
2 parents 04b5682 + ac62b1f commit 2e01686

File tree

2 files changed

+15
-0
lines changed

2 files changed

+15
-0
lines changed
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
KNOWNBUG
2+
eventually4.sv
3+
--bound 2
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
^warning: ignoring
8+
--
9+
Property gives counterexample but should pass.

regression/verilog/SVA/eventually4.sv

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
module main(input a);
2+
3+
// should pass for any bound
4+
assert property ((s_eventually !a) or (always a));
5+
6+
endmodule

0 commit comments

Comments
 (0)