Skip to content

Commit 3bab967

Browse files
kroeningkroening
committed
LTL/SVA->Buechi: reject error traces early
The Buechi automaton accepts counterexamples to the original property. The Buechi acceptance condition requires a lasso where the loop contains an accepting state. A proof of that requires satisfying the looping condition, which may require a very long counterexample. This adds a shortcut using a sufficient condition for a counterexample: we can reject the property when we reach a state in which the Buechi automaton transitions into an accepting state that has an unconditional self-loop on it. Such traces can always be extended to a lasso as above.
1 parent 78fc96e commit 3bab967

24 files changed

+291
-5
lines changed

‎regression/ebmc-spot/sva-buechi/case1.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
../../verilog/SVA/case1.sv
3+
--buechi --bound 20 --numbered-trace
4+
^\[main\.p0\] always \(case\(main\.x\) 10: 0; endcase\): REFUTED$
5+
^Counterexample with 11 states:$
6+
^EXIT=10$
7+
^SIGNAL=0$
8+
--
9+
^warning: ignoring
10+
--

‎regression/ebmc-spot/sva-buechi/cover1.desc

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
CORE
2+
../../verilog/SVA/cover1.sv
3+
--buechi --bound 10 --numbered-trace
4+
^\[main\.p0\] cover main\.counter == 1: PROVED$
5+
^Trace with 2 states:$
6+
^main\.counter@0 = 0$
7+
^main\.counter@1 = 1$
8+
^\[main\.p1\] cover main\.counter == 100: REFUTED up to bound 10$
9+
^EXIT=10$
10+
^SIGNAL=0$
11+
--
12+
^warning: ignoring
13+
--
14+
Back-end support is missing.

‎regression/ebmc-spot/sva-buechi/cover2.desc

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
../../verilog/SVA/cover2.sv
3+
--buechi --bound 10 --numbered-trace
4+
^\[main\.p0\] cover main\.counter == 1: PROVED$
5+
^Trace with 2 states:$
6+
^main\.counter@0 = 0$
7+
^main\.counter@1 = 1$
8+
^\[main\.p1\] cover main\.counter == 100: REFUTED up to bound 10$
9+
^EXIT=10$
10+
^SIGNAL=0$
11+
--
12+
^warning: ignoring
13+
--

‎regression/ebmc-spot/sva-buechi/cover_sequence1.bmc.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
../../verilog/SVA/cover_sequence1.sv
3+
--buechi --bound 10 --numbered-trace
4+
^\[main\.p0\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 4\): UNSUPPORTED: not convertible to Buechi$
5+
^\[main\.p1\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 5\): UNSUPPORTED: not convertible to Buechi$
6+
^EXIT=10$
7+
^SIGNAL=0$
8+
--
9+
^warning: ignoring
10+
--

‎regression/ebmc-spot/sva-buechi/cover_sequence2.bmc.desc

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
../../verilog/SVA/cover_sequence2.sv
3+
--buechi --bound 5
4+
^\[main\.p0\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 100\): UNSUPPORTED: not convertible to Buechi$
5+
^\[main\.p1\] cover \(main\.x == 98 ##1 main\.x == 99 ##1 main\.x == 100\): UNSUPPORTED: not convertible to Buechi$
6+
^\[main\.p2\] cover \(main\.x == 3 ##1 main\.x == 4 ##1 main\.x == 5\): UNSUPPORTED: not convertible to Buechi$
7+
^\[main\.p3\] cover \(main\.x == 4 ##1 main\.x == 5 ##1 main\.x == 6\): UNSUPPORTED: not convertible to Buechi$
8+
^EXIT=10$
9+
^SIGNAL=0$
10+
--
11+
^warning: ignoring
12+
--

‎regression/ebmc-spot/sva-buechi/cover_sequence3.bmc.desc

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
KNOWNBUG
2+
../../verilog/SVA/cover_sequence3.sv
3+
--buechi --bound 3
4+
^\[main\.p0\] cover \(1 \[\*10\]\): REFUTED up to bound 3$
5+
^\[main\.p1\] cover \(1 \[\*4:10\]\): PROVED$
6+
^\[main\.p2\] cover \(1 \[\*5:10\]\): REFUTED up to bound 3$
7+
^EXIT=10$
8+
^SIGNAL=0$
9+
--
10+
^warning: ignoring
11+
--
12+
Trace one too short.

‎regression/ebmc-spot/sva-buechi/cover_sequence4.bmc.desc

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
KNOWNBUG
2+
../../verilog/SVA/cover_sequence4.sv
3+
--buechi --bound 3
4+
^\[main\.p0\] cover \(1 \[=10\]\): REFUTED up to bound 3$
5+
^\[main\.p1\] cover \(1 \[=4:10\]\): PROVED$
6+
^\[main\.p2\] cover \(1 \[=5:10\]\): REFUTED up to bound 3$
7+
^EXIT=10$
8+
^SIGNAL=0$
9+
--
10+
^warning: ignoring
11+
--
12+
Trace one too short.

‎regression/ebmc-spot/sva-buechi/disable_iff1.bmc.desc

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
../../verilog/SVA/disable_iff1.sv
3+
--buechi --module main --bound 10 --numbered-trace
4+
^\[main\.p0\] always \(disable iff \(main.counter == 0\) main\.counter != 0\): PROVED up to bound 10$
5+
^\[main\.p1\] always \(disable iff \(1\) 0\): PROVED up to bound 10$
6+
^\[main\.p2\] always \(disable iff \(main\.counter == 1\) main\.counter == 0\): REFUTED$
7+
^Counterexample with 3 states:$
8+
^EXIT=10$
9+
^SIGNAL=0$
10+
--
11+
^warning: ignoring
12+
--

‎regression/ebmc-spot/sva-buechi/empty_sequence1.bmc.desc

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
../../verilog/SVA/empty_sequence1.sv
3+
--buechi --bound 5
4+
^\[main\.p0\] 1 \[\*0\]: REFUTED$
5+
^\[main\.p1\] \(1 \[\*0\]\) ##1 main\.x == 0: PROVED up to bound 5$
6+
^\[main\.p2\] main\.x == 0 ##1 \(1 \[\*0\]\): PROVED up to bound 5$
7+
^\[main\.p3\] \(1 \[\*0\]\) ##0 1: REFUTED$
8+
^\[main\.p4\] 1 ##0 \(1 \[\*0\]\): REFUTED$
9+
^EXIT=10$
10+
^SIGNAL=0$
11+
--
12+
^warning: ignoring
13+
--

‎regression/ebmc-spot/sva-buechi/followed-by4.bmc.desc

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
../../verilog/SVA/followed-by4.sv
33
--buechi --bound 3
44
^\[main\.p1\] always \(main\.x == 0 #-# 1\): REFUTED$
@@ -9,4 +9,3 @@ KNOWNBUG
99
--
1010
^warning: ignoring
1111
--
12-
p1 is not refuted.

0 commit comments

Comments
 (0)