Merge pull request #671 from diffblue/paren-concat

Verilog: `{}` and `{{}}` do not need parentheses

Author: tautschnig

regression/verilog/SVA/immediate3.desc

@@ -1,7 +1,7 @@
 CORE
 immediate3.sv
 --bound 0
-^\[full_adder\.assert\.1\] always \(\{ full_adder\.carry, full_adder\.sum \}\) == full_adder\.a \+ full_adder\.b \+ full_adder\.c: PROVED up to bound 0$
+^\[full_adder\.assert\.1\] always \{ full_adder\.carry, full_adder\.sum \} == full_adder\.a \+ full_adder\.b \+ full_adder\.c: PROVED up to bound 0$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/SVA/static_final1.desc

@@ -1,7 +1,7 @@
 CORE
 static_final1.sv
 --bound 0
-^\[full_adder\.p0\] always \(\{ full_adder\.carry, full_adder\.sum \}\) == full_adder\.a \+ full_adder\.b \+ full_adder\.c: PROVED up to bound 0$
+^\[full_adder\.p0\] always \{ full_adder\.carry, full_adder\.sum \} == full_adder\.a \+ full_adder\.b \+ full_adder\.c: PROVED up to bound 0$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/expressions/concatenation3.desc

@@ -3,6 +3,6 @@ concatenation3.sv
 --bound 0
 ^EXIT=0$
 ^SIGNAL=0$
-^\[.*\] always \(\{ 5'bxz01\?, 4'b10zx \}\) === 9'bxz01\?10zx: PROVED up to bound 0$
+^\[.*\] always \{ 5'bxz01\?, 4'b10zx \} === 9'bxz01\?10zx: PROVED up to bound 0$
 --
 ^warning: ignoring

src/verilog/expr2verilog.cpp

@@ -1136,7 +1136,7 @@ expr2verilogt::convert(const exprt &src, verilog_precedencet &precedence)
 
   else if(src.id()==ID_replication)
     return convert_replication(
-      to_replication_expr(src), precedence = verilog_precedencet::REPLICATION);
+      to_replication_expr(src), precedence = verilog_precedencet::CONCAT);
 
   else if(src.id()==ID_array)
     return convert_array(src, precedence);

src/verilog/expr2verilog_class.h

@@ -19,29 +19,29 @@ class sva_ranged_predicate_exprt;
 
 // Precedences (higher means binds more strongly).
 // Follows Table 11-2 in IEEE 1800-2017.
-//
+// We deviate from the table for the precedence of concatenation
+// and replication, which act like parentheses.
 enum class verilog_precedencet
 {
   MAX = 19,
-  MEMBER = 18,     //  [ ]  bit-select  ( )  parenthesis  ::   .
-  NOT = 17,        //  unary !  ~  &  |  ~&  ~|  ^  ~^  ^~  +  -
-  POWER = 16,      //  **  power
-  MULT = 15,       //  *  /  %
-  ADD = 14,        //  + -
-  SHIFT = 13,      //  <<  >>  <<<  >>>
-  RELATION = 12,   //  >  >=  <  <=
-  EQUALITY = 11,   //  ==  !=  ===  !==  ==?  !=?
-  BITAND = 10,     //  &
-  XOR = 9,         //  ^  ~^  ^~ (binary)
-  BITOR = 8,       //  |
-  AND = 7,         //  &&
-  OR = 6,          //  ||
-  IF = 5,          //  ?:
-  IMPLIES = 4,     //  ->
-  ASSIGN = 3,      //  = += -= etc.
-  CONCAT = 2,      //  { } concatenation
-  REPLICATION = 1, //  {{ }} replication
-  MIN = 0          //  anything even weaker, e.g., SVA
+  MEMBER = 18,   //  [ ]  bit-select  ( )  parenthesis  ::   .
+  NOT = 17,      //  unary !  ~  &  |  ~&  ~|  ^  ~^  ^~  +  -
+  POWER = 16,    //  **  power
+  MULT = 15,     //  *  /  %
+  ADD = 14,      //  + -
+  SHIFT = 13,    //  <<  >>  <<<  >>>
+  RELATION = 12, //  >  >=  <  <=
+  EQUALITY = 11, //  ==  !=  ===  !==  ==?  !=?
+  BITAND = 10,   //  &
+  XOR = 9,       //  ^  ~^  ^~ (binary)
+  BITOR = 8,     //  |
+  AND = 7,       //  &&
+  OR = 6,        //  ||
+  IF = 5,        //  ?:
+  IMPLIES = 4,   //  ->
+  ASSIGN = 3,    //  = += -= etc.
+  CONCAT = 18,   //  { } concatenation, {{ }} replication
+  MIN = 0        //  anything even weaker, e.g., SVA
 };
 
 class expr2verilogt