Skip to content

Commit 57f082a

Browse files
committed
ebmc: avoid parentheses in SVA output for unary operators
This removes parentheses when printing unary SVA operators that have operands that are unary.
1 parent 6806280 commit 57f082a

File tree

11 files changed

+13
-12
lines changed

11 files changed

+13
-12
lines changed
Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
counter1.sv
33
--number-of-traces 2 --neural-liveness --neural-engine "echo Candidate: counter\\\\n"
4-
^\[main\.property\.p0\] always \(eventually main.counter == 0\): SUCCESS$
4+
^\[main\.property\.p0\] always eventually main.counter == 0: SUCCESS$
55
^EXIT=0$
66
^SIGNAL=0$
77
--
Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
counter1.sv
33
--ranking-function "(-counter)"
4-
^\[main\.property\.p0\] always \(eventually main.counter == 0\): UNKNOWN$
4+
^\[main\.property\.p0\] always eventually main.counter == 0: UNKNOWN$
55
^EXIT=0$
66
^SIGNAL=0$
77
--
Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
counter1.sv
33
--ranking-function counter
4-
^\[main\.property\.p0\] always \(eventually main.counter == 0\): SUCCESS$
4+
^\[main\.property\.p0\] always eventually main.counter == 0: SUCCESS$
55
^EXIT=0$
66
^SIGNAL=0$
77
--
Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
counter2.sv
33
--ranking-function counter
4-
^\[main\.property\.p0\] always \(eventually main.counter == 10\): UNKNOWN$
4+
^\[main\.property\.p0\] always eventually main.counter == 10: UNKNOWN$
55
^EXIT=0$
66
^SIGNAL=0$
77
--
Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
counter2.sv
33
--ranking-function 10-counter
4-
^\[main\.property\.p0\] always \(eventually main.counter == 10\): SUCCESS$
4+
^\[main\.property\.p0\] always eventually main.counter == 10: SUCCESS$
55
^EXIT=0$
66
^SIGNAL=0$
77
--

regression/ebmc/ranking-function/counter_in_module1.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
counter_in_module1.sv
33
--ranking-function instance.counter
4-
^\[main\.property\.p0\] always \(eventually main.instance.counter == 0\): SUCCESS$
4+
^\[main\.property\.p0\] always eventually main.instance.counter == 0: SUCCESS$
55
^EXIT=0$
66
^SIGNAL=0$
77
--
Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
counter_with_reset1.sv
33
--property main.property.p0 --ranking-function 10-counter
4-
^\[main\.property\.p0\] always \(eventually main.counter == 10\): UNKNOWN$
4+
^\[main\.property\.p0\] always eventually main.counter == 10: UNKNOWN$
55
^EXIT=0$
66
^SIGNAL=0$
77
--
Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
counter_with_reset1.sv
33
--property main.property.p1 --ranking-function 10-counter
4-
^\[main\.property\.p1\] always \(eventually main.reset \|\| main.counter == 10\): SUCCESS$
4+
^\[main\.property\.p1\] always eventually main.reset \|\| main.counter == 10: SUCCESS$
55
^EXIT=0$
66
^SIGNAL=0$
77
--
Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
lexicographic_ranking_function1.sv
33
--ranking-function "{digit1, digit2}"
4-
^\[main\.property\.p0\] always \(eventually main\.digit1 == 0\): SUCCESS$
4+
^\[main\.property\.p0\] always eventually main\.digit1 == 0: SUCCESS$
55
^EXIT=0$
66
^SIGNAL=0$
77
--

regression/verilog/system_verilog_assertion/eventually3.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,6 @@ eventually3.sv
33
--module main --bound 11
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\[main\.property\.p0\] always \(eventually main\.counter <= 5\): FAILURE$
6+
^\[main\.property\.p0\] always eventually main\.counter <= 5: FAILURE$
77
--
88
^warning: ignoring

0 commit comments

Comments
 (0)