Skip to content

Commit 668be19

Browse files
tautschnigtautschnig
authored
Merge pull request #575 from diffblue/assertion-item-namespace
SystemVerilog: concurrent assertion items go into module namespace
2 parents feba5dc + 5cca195 commit 668be19

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

62 files changed

+119
-111
lines changed

‎regression/ebmc/BDD/BDD2.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,6 @@ BDD2.sv
33
--module main --bdd
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\[main.property.my_prop1\] always main.counter < 199: PROVED$
7-
^\[main.property.my_prop2\] always main.counter < 198: REFUTED$
6+
^\[main\.my_prop1\] always main.counter < 199: PROVED$
7+
^\[main\.my_prop2\] always main.counter < 198: REFUTED$
88
--

‎regression/ebmc/BDD/BDD3.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,6 @@ BDD3.sv
33
--module main --bdd
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\[main.property.my_prop1\] always main.counter <= 10: PROVED$
7-
^\[main.property.my_prop2\] always main.counter < 10: REFUTED$
6+
^\[main\.my_prop1\] always main\.counter <= 10: PROVED$
7+
^\[main\.my_prop2\] always main\.counter < 10: REFUTED$
88
--

‎regression/ebmc/BDD/BDD_SVA1.desc

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -3,14 +3,14 @@ BDD_SVA1.sv
33
--bdd
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\[top\.property\.p0\] always top\.my_bit: PROVED$
7-
^\[top\.property\.p1\] always top\.my_bit: PROVED$
8-
^\[top\.property\.p2\] always \(top\.counter == 3 \|-> \(nexttime top\.counter == 4\)\): FAILURE: property not supported by BDD engine$
9-
^\[top\.property\.p3\] always \(top\.counter == 3 \|=> top\.counter == 4\): FAILURE: property not supported by BDD engine$
10-
^\[top\.property\.p4\] always \(top\.counter == 3 \|=> \(nexttime top\.counter == 5\)\): FAILURE: property not supported by BDD engine$
11-
^\[top\.property\.p5\] always s_eventually top\.counter == 8: PROVED$
12-
^\[top\.property\.p6\] always \(top\.counter == 0 \|-> \(s_eventually top\.counter == 8\)\): FAILURE: property not supported by BDD engine$
13-
^\[top\.property\.p7\] always \(top\.counter == 0 \|-> \(top\.counter <= 5 until top\.counter == 6\)\): FAILURE: property not supported by BDD engine$
14-
^\[top\.property\.p8\] always \(top\.counter == 0 \|-> \(top\.counter <= 5 until_with top\.counter == 5\)\): FAILURE: property not supported by BDD engine$
6+
^\[top\.p0\] always top\.my_bit: PROVED$
7+
^\[top\.p1\] always top\.my_bit: PROVED$
8+
^\[top\.p2\] always \(top\.counter == 3 \|-> \(nexttime top\.counter == 4\)\): FAILURE: property not supported by BDD engine$
9+
^\[top\.p3\] always \(top\.counter == 3 \|=> top\.counter == 4\): FAILURE: property not supported by BDD engine$
10+
^\[top\.p4\] always \(top\.counter == 3 \|=> \(nexttime top\.counter == 5\)\): FAILURE: property not supported by BDD engine$
11+
^\[top\.p5\] always s_eventually top\.counter == 8: PROVED$
12+
^\[top\.p6\] always \(top\.counter == 0 \|-> \(s_eventually top\.counter == 8\)\): FAILURE: property not supported by BDD engine$
13+
^\[top\.p7\] always \(top\.counter == 0 \|-> \(top\.counter <= 5 until top\.counter == 6\)\): FAILURE: property not supported by BDD engine$
14+
^\[top\.p8\] always \(top\.counter == 0 \|-> \(top\.counter <= 5 until_with top\.counter == 5\)\): FAILURE: property not supported by BDD engine$
1515
--
1616
^warning: ignoring

‎regression/ebmc/Next-in-Property1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,5 +3,5 @@ main.sv
33
--module top --bound 10
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[top.property.p1\] always \(top.counter\[0\] |-> \(##1 top.counter <= 5\)\): SUCCESS$
6+
^\[top\.p1\] always \(top\.counter\[0\] |-> \(##1 top\.counter <= 5\)\): SUCCESS$
77
--

‎regression/ebmc/SVA-LTL/freeze.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
CORE
22
freeze.sv
33
--bound 1
4-
^\[main\.property\.p1\] always s_eventually main\.w: REFUTED$
5-
^\[main\.property\.p2\] always s_eventually !main\.w: REFUTED$
4+
^\[main\.p1\] always s_eventually main\.w: REFUTED$
5+
^\[main\.p2\] always s_eventually !main\.w: REFUTED$
66
^EXIT=10$
77
^SIGNAL=0$
88
--

‎regression/ebmc/SVA-LTL/lasso1-counterexample.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ lasso1.sv
33
--bound 10 --waveform
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\[top\.property\.p0\] .* REFUTED$
6+
^\[top\.p0\] .* REFUTED$
77
^ 0 1 2 3 4 5 6 7 8 9 10$
88
^top\.counter 0 1 2 3 4 5 6 7 8 9 3$
99
--

‎regression/ebmc/SVA-LTL/lasso1-small-bound.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,6 @@ lasso1.sv
33
--bound 5
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[top\.property\.p0\] .* PROVED up to bound 5$
6+
^\[top\.p0\] .* PROVED up to bound 5$
77
--
88
--

‎regression/ebmc/SVA-LTL/simple_counterexamples_to_Fp.p0.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
CORE
22
simple_counterexamples_to_Fp.sv
3-
--bound 10 --property top.property.p0
3+
--bound 10 --property top.p0
44
^Adding lasso constraints$
55
^EXIT=10$
66
^SIGNAL=0$
7-
^\[top\.property\.p0\] .* REFUTED$
7+
^\[top\.p0\] .* REFUTED$
88
--

‎regression/ebmc/SVA-LTL/simple_counterexamples_to_Fp.p1.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
CORE
22
simple_counterexamples_to_Fp.sv
3-
--bound 10 --property top.property.p1
3+
--bound 10 --property top.p1
44
^Adding lasso constraints$
55
^EXIT=10$
66
^SIGNAL=0$
7-
^\[top\.property\.p1\] .* REFUTED$
7+
^\[top\.p1\] .* REFUTED$
88
--

‎regression/ebmc/SVA-LTL/simple_counterexamples_to_Fp.p2.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
CORE
22
simple_counterexamples_to_Fp.sv
3-
--bound 10 --property top.property.p2
3+
--bound 10 --property top.p2
44
^Adding lasso constraints$
55
^EXIT=10$
66
^SIGNAL=0$
7-
^\[top\.property\.p2\] .* REFUTED$
7+
^\[top\.p2\] .* REFUTED$
88
--

0 commit comments

Comments
 (0)