Skip to content

Commit 921e331

Browse files
tautschnigtautschnig
authored
Merge pull request #576 from diffblue/assertion-statement-namespace
SystemVerilog: assertion statements use hierarchical identifiers
2 parents 7232740 + 840b233 commit 921e331

File tree

13 files changed

+43
-27
lines changed

13 files changed

+43
-27
lines changed

‎regression/verilog/Memory2/test.desc‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,6 @@ main.v
33
--module main --bound 1
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.property.property1\] .* PROVED up to bound 1$
6+
^\[main\.property\.property1\] .* PROVED up to bound 1$
77
--
88
^warning: ignoring

‎regression/verilog/SVA/always_with_range1.desc‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
CORE
22
always_with_range1.sv
33
--bound 20
4-
^\[main\.property\.p0\] always \[0:9\] main\.x < 10: PROVED up to bound 20$
5-
^\[main\.property\.p1\] always \[0:\$\] main\.x < 10: REFUTED$
6-
^\[main\.property\.p2\] s_always \[0:9\] main\.x < 10: PROVED up to bound 20$
4+
^\[main\.p0\] always \[0:9\] main\.x < 10: PROVED up to bound 20$
5+
^\[main\.p1\] always \[0:\$\] main\.x < 10: REFUTED$
6+
^\[main\.p2\] s_always \[0:9\] main\.x < 10: PROVED up to bound 20$
77
^EXIT=10$
88
^SIGNAL=0$
99
--

‎regression/verilog/SVA/cover2.desc‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,11 @@
11
CORE
22
cover2.sv
33
--bound 10 --numbered-trace
4-
^\[main\.property\.p0\] cover main\.counter == 1: PROVED$
4+
^\[main\.p0\] cover main\.counter == 1: PROVED$
55
^Trace with 2 states:$
66
^main\.counter@0 = 0$
77
^main\.counter@1 = 1$
8-
^\[main\.property\.p1\] cover main\.counter == 100: REFUTED up to bound 10$
8+
^\[main\.p1\] cover main\.counter == 100: REFUTED up to bound 10$
99
^EXIT=10$
1010
^SIGNAL=0$
1111
--

‎regression/verilog/SVA/immediate2.desc‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
CORE broken-smt-backend
22
immediate2.sv
33
--bound 0
4-
^\[main\.property\.1\] assume always \(main\.index >= 10 |-> 0\): ASSUMED$
5-
^\[main\.property\.2\] always main\.index < 10: PROVED up to bound 0$
6-
^\[main\.property\.3\] always 0: REFUTED$
4+
^\[main\.assert\.1\] assume always \(main\.index >= 10 |-> 0\): ASSUMED$
5+
^\[main\.assert\.2\] always main\.index < 10: PROVED up to bound 0$
6+
^\[main\.assert\.3\] always 0: REFUTED$
77
^EXIT=10$
88
^SIGNAL=0$
99
--

‎regression/verilog/SVA/initial1.desc‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,11 @@
11
CORE
22
initial1.sv
33
--module main --bound 1
4-
^\[main\.property\.p0\] main\.counter == 0: PROVED up to bound 1$
5-
^\[main\.property\.p1\] main\.counter == 100: REFUTED$
6-
^\[main\.property\.p2\] ##1 main\.counter == 1: PROVED up to bound 1$
7-
^\[main\.property\.p3\] ##1 main\.counter == 100: REFUTED$
8-
^\[main\.property\.p4\] s_nexttime main\.counter == 1: PROVED up to bound 1$
4+
^\[main\.p0\] main\.counter == 0: PROVED up to bound 1$
5+
^\[main\.p1\] main\.counter == 100: REFUTED$
6+
^\[main\.p2\] ##1 main\.counter == 1: PROVED up to bound 1$
7+
^\[main\.p3\] ##1 main\.counter == 100: REFUTED$
8+
^\[main\.p4\] s_nexttime main\.counter == 1: PROVED up to bound 1$
99
^EXIT=10$
1010
^SIGNAL=0$
1111
--

‎regression/verilog/SVA/initial2.desc‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
CORE
22
initial2.sv
33
--module main --bound 1
4-
^\[main\.property\.1\] 1 == 1: PROVED up to bound 1
5-
^\[main\.property\.2\] main\.counter == 2: PROVED up to bound 1
4+
^\[main\.assert\.1\] 1 == 1: PROVED up to bound 1
5+
^\[main\.assert\.2\] main\.counter == 2: PROVED up to bound 1
66
^EXIT=0$
77
^SIGNAL=0$
88
--

‎regression/verilog/SVA/sequence1.desc‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
sequence1.sv
33
--bound 20 --numbered-trace
4-
^\[main\.property\.p0\] ##\[0:9\] main\.x == 100: REFUTED$
4+
^\[main\.p0\] ##\[0:9\] main\.x == 100: REFUTED$
55
^Counterexample with 10 states:$
66
^main\.x@0 = 0$
77
^main\.x@9 = 9$

‎regression/verilog/SVA/sequence2.desc‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
sequence2.sv
33
--bound 10 --numbered-trace
4-
^\[main\.property\.p0] ##\[0:\$\] main\.x == 10: REFUTED$
4+
^\[main\.p0] ##\[0:\$\] main\.x == 10: REFUTED$
55
^Counterexample with 7 states:$
66
^main\.x@0 = 0$
77
^main\.x@1 = 1$

‎regression/verilog/SVA/sequence3.desc‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
CORE
22
sequence3.sv
33
--bound 20 --numbered-trace
4-
^\[main\.property\.p0\] ##\[\*\] main\.x == 6: REFUTED$
4+
^\[main\.p0\] ##\[\*\] main\.x == 6: REFUTED$
55
^Counterexample with 2 states:$
6-
^\[main\.property\.p1\] ##\[\+\] main\.x == 0: REFUTED$
6+
^\[main\.p1\] ##\[\+\] main\.x == 0: REFUTED$
77
^Counterexample with 7 states:$
88
^EXIT=10$
99
^SIGNAL=0$

‎regression/verilog/SVA/sequence_followed_by1.desc‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
CORE
22
sequence_followed_by1.sv
33
--bound 20 --numbered-trace
4-
^\[main\.property\.p0\] main\.x == 0 #=# \(main\.x == 1 #=# main\.x == 2\): FAILURE: property not supported by BMC engine$
5-
^\[main\.property\.p1\] main\.x == 0 #-# \(\(##1 main\.x == 1\) #-# \(##1 main\.x == 2\)\): FAILURE: property not supported by BMC engine$
4+
^\[main\.p0\] main\.x == 0 #=# \(main\.x == 1 #=# main\.x == 2\): FAILURE: property not supported by BMC engine$
5+
^\[main\.p1\] main\.x == 0 #-# \(\(##1 main\.x == 1\) #-# \(##1 main\.x == 2\)\): FAILURE: property not supported by BMC engine$
66
^EXIT=10$
77
^SIGNAL=0$
88
--

0 commit comments

Comments
 (0)