diff --git a/regression/verilog/SVA/immediate3.desc b/regression/verilog/SVA/immediate3.desc index 0dbcfa449..253f0d1f8 100644 --- a/regression/verilog/SVA/immediate3.desc +++ b/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$ -- diff --git a/regression/verilog/SVA/static_final1.desc b/regression/verilog/SVA/static_final1.desc index a8da4ff85..fe052d605 100644 --- a/regression/verilog/SVA/static_final1.desc +++ b/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$ -- diff --git a/regression/verilog/expressions/concatenation3.desc b/regression/verilog/expressions/concatenation3.desc index 3637df6ca..e8b1c033d 100644 --- a/regression/verilog/expressions/concatenation3.desc +++ b/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 diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp index 18e43be22..4855c24d5 100644 --- a/src/verilog/expr2verilog.cpp +++ b/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); diff --git a/src/verilog/expr2verilog_class.h b/src/verilog/expr2verilog_class.h index 5c1b0f205..6228eb5c1 100644 --- a/src/verilog/expr2verilog_class.h +++ b/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