Skip to content

Commit 8fe0551

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 ad2f8ba commit 8fe0551

20 files changed

+245
-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/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.

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

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
../../verilog/SVA/if1.sv
3+
--buechi --bound 2
4+
^\[main\.p0\] always \(if\(main\.counter == 0\) nexttime main\.counter == 1\): PROVED up to bound 2$
5+
^\[main\.p1\] always \(if\(main\.counter == 0\) nexttime main\.counter == 1 else nexttime main\.counter == 3\): REFUTED$
6+
^EXIT=10$
7+
^SIGNAL=0$
8+
--
9+
^warning: ignoring
10+
--
11+
SMT-back end doesn't do cast from bool to bool.

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

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

‎regression/ebmc-spot/sva-buechi/s_always1.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/s_always1.sv
33
--buechi --bound 20
44
^\[main\.p0\] s_always \[0:9\] main\.x < 10: PROVED up to bound 20$
@@ -8,4 +8,3 @@ KNOWNBUG
88
--
99
^warning: ignoring
1010
--
11-
main.p1 is not refuted.

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

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

0 commit comments

Comments
 (0)