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

This changes the precedence of concatenation and replication when generating
Verilog from expressions such that no additional parentheses are generated.

Author: kroening

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,7 +19,8 @@ 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 parenteses.
 enum class verilog_precedencet
 {
   MAX = 19,
@@ -39,8 +40,7 @@ enum class verilog_precedencet
   IF = 5,          //  ?:
   IMPLIES = 4,     //  ->
   ASSIGN = 3,      //  = += -= etc.
-  CONCAT = 2,      //  { } concatenation
-  REPLICATION = 1, //  {{ }} replication
+  CONCAT = 18,     //  { } concatenation, {{ }} replication
   MIN = 0          //  anything even weaker, e.g., SVA
 };