Merge pull request #272 from diffblue/expr2verilog-sva-precedence

ebmc: avoid parentheses in SVA output for unary operators

Author: tautschnig

regression/ebmc/neural-liveness/counter1.desc

@@ -1,7 +1,7 @@
 CORE
 counter1.sv
 --number-of-traces 2 --neural-liveness --neural-engine "echo Candidate: counter\\\\n"
-^\[main\.property\.p0\] always \(eventually main.counter == 0\): PROVED$
+^\[main\.property\.p0\] always eventually main.counter == 0: PROVED$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/ebmc/ranking-function/counter1.fail.desc

@@ -1,7 +1,7 @@
 CORE
 counter1.sv
 --ranking-function "(-counter)"
-^\[main\.property\.p0\] always \(eventually main.counter == 0\): INCONCLUSIVE$
+^\[main\.property\.p0\] always eventually main.counter == 0: INCONCLUSIVE$
 ^EXIT=10$
 ^SIGNAL=0$
 --

regression/ebmc/ranking-function/counter1.pass.desc

@@ -1,7 +1,7 @@
 CORE
 counter1.sv
 --ranking-function counter
-^\[main\.property\.p0\] always \(eventually main.counter == 0\): PROVED$
+^\[main\.property\.p0\] always eventually main.counter == 0: PROVED$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/ebmc/ranking-function/counter2.fail.desc

@@ -1,7 +1,7 @@
 CORE
 counter2.sv
 --ranking-function counter
-^\[main\.property\.p0\] always \(eventually main.counter == 10\): INCONCLUSIVE$
+^\[main\.property\.p0\] always eventually main.counter == 10: INCONCLUSIVE$
 ^EXIT=10$
 ^SIGNAL=0$
 --

regression/ebmc/ranking-function/counter2.pass.desc

@@ -1,7 +1,7 @@
 CORE
 counter2.sv
 --ranking-function 10-counter
-^\[main\.property\.p0\] always \(eventually main.counter == 10\): PROVED$
+^\[main\.property\.p0\] always eventually main.counter == 10: PROVED$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/ebmc/ranking-function/counter_in_module1.desc

@@ -1,7 +1,7 @@
 CORE
 counter_in_module1.sv
 --ranking-function instance.counter
-^\[main\.property\.p0\] always \(eventually main.instance.counter == 0\): PROVED$
+^\[main\.property\.p0\] always eventually main.instance.counter == 0: PROVED$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/ebmc/ranking-function/counter_with_reset1.fail.desc

@@ -1,7 +1,7 @@
 CORE
 counter_with_reset1.sv
 --property main.property.p0 --ranking-function 10-counter
-^\[main\.property\.p0\] always \(eventually main.counter == 10\): INCONCLUSIVE$
+^\[main\.property\.p0\] always eventually main.counter == 10: INCONCLUSIVE$
 ^EXIT=10$
 ^SIGNAL=0$
 --

regression/ebmc/ranking-function/counter_with_reset1.pass.desc

@@ -1,7 +1,7 @@
 CORE
 counter_with_reset1.sv
 --property main.property.p1 --ranking-function 10-counter
-^\[main\.property\.p1\] always \(eventually main.reset \|\| main.counter == 10\): PROVED$
+^\[main\.property\.p1\] always eventually main.reset \|\| main.counter == 10: PROVED$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/ebmc/ranking-function/lexicographic_ranking_function1.desc

@@ -1,7 +1,7 @@
 CORE
 lexicographic_ranking_function1.sv
 --ranking-function "{digit1, digit2}"
-^\[main\.property\.p0\] always \(eventually main\.digit1 == 0\): PROVED$
+^\[main\.property\.p0\] always eventually main\.digit1 == 0: PROVED$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/system_verilog_assertion/eventually3.desc

@@ -3,6 +3,6 @@ eventually3.sv
 --module main --bound 11
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main\.property\.p0\] always \(eventually main\.counter <= 5\): REFUTED$
+^\[main\.property\.p0\] always eventually main\.counter <= 5: REFUTED$
 --
 ^warning: ignoring

src/verilog/expr2verilog.cpp

@@ -386,9 +386,10 @@ std::string expr2verilogt::convert_sva(
 {
   if(src.operands().size()==1)
   {
+    auto &op = to_unary_expr(src).op();
     unsigned p;
-    auto s = convert(to_unary_expr(src).op(), p);
-    if(p == 0)
+    auto s = convert(op, p);
+    if(p == 0 && op.operands().size() >= 2)
       s = "(" + s + ")";
     return name + " " + s;
   }