From 9b7f39d1f73fa7f4e52adf6a5c2529089311b942 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 1 Oct 2025 04:19:25 -0700 Subject: [PATCH 1/3] Verilog: cleanup downwards type propagation This cleans up verilog_typecheck_exprt::downwards_type_progatation to handle all the cases in 1800-2017 11.8.2. --- src/verilog/verilog_typecheck_expr.cpp | 203 +++++++++++-------------- 1 file changed, 92 insertions(+), 111 deletions(-) diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index 1c9d3f30e..5db6df015 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/src/verilog/verilog_typecheck_expr.cpp @@ -222,6 +222,39 @@ void verilog_typecheck_exprt::propagate_type( /*******************************************************************\ +Function: zero_extend + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +static exprt zero_extend(const exprt &expr, const typet &type) +{ + auto old_width = expr.type().id() == ID_bool ? 1 + : expr.type().id() == ID_integer + ? 32 + : to_bitvector_type(expr.type()).get_width(); + + // first make unsigned + typet tmp_type; + + if(type.id() == ID_unsignedbv) + tmp_type = unsignedbv_typet{old_width}; + else if(type.id() == ID_verilog_unsignedbv) + tmp_type = verilog_unsignedbv_typet{old_width}; + else + PRECONDITION(false); + + return typecast_exprt::conditional_cast( + typecast_exprt::conditional_cast(expr, tmp_type), type); +} + +/*******************************************************************\ + Function: verilog_typecheck_exprt::downwards_type_progatation Inputs: @@ -241,95 +274,76 @@ void verilog_typecheck_exprt::downwards_type_propagation( // Any context-determined operand of an operator shall be the // same type and size as the result of the operator. - // Exceptions: - // * result type real -- just cast - // * relational operators are always 1 bit unsigned + // As an exception, if the result type is real, the operands + // are just casted. if(expr.type() == type) return; - vtypet vt_from = vtypet(expr.type()); - vtypet vt_to = vtypet(type); - - if(!vt_from.is_other() && !vt_to.is_other() && expr.has_operands()) + if(type.id() == ID_verilog_real || type.id() == ID_verilog_shortreal) { - // arithmetic - - if( - expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_mult || - expr.id() == ID_div || expr.id() == ID_unary_minus || - expr.id() == ID_unary_plus) - { - if(type.id() != ID_bool) - { - Forall_operands(it, expr) - propagate_type(*it, type); - - expr.type() = type; - - return; - } - } - else if( - expr.id() == ID_bitand || expr.id() == ID_bitor || - expr.id() == ID_bitnand || expr.id() == ID_bitnor || - expr.id() == ID_bitxor || expr.id() == ID_bitxnor || - expr.id() == ID_bitnot) - { - Forall_operands(it, expr) - propagate_type(*it, type); - - expr.type() = type; + expr = typecast_exprt{expr, type}; + return; + } - if(type.id() == ID_bool) - { - if(expr.id() == ID_bitand) - expr.id(ID_and); - else if(expr.id() == ID_bitor) - expr.id(ID_or); - else if(expr.id() == ID_bitnand) - expr.id(ID_nand); - else if(expr.id() == ID_bitnor) - expr.id(ID_nor); - else if(expr.id() == ID_bitxor) - expr.id(ID_xor); - else if(expr.id() == ID_bitxnor) - expr.id(ID_xnor); - else if(expr.id() == ID_bitnot) - expr.id(ID_not); - } + // expressions with context-determined width, following + // 1800-2017 Table 11-21 + if( + expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_mult || + expr.id() == ID_div || expr.id() == ID_mod || expr.id() == ID_bitand || + expr.id() == ID_bitor || expr.id() == ID_bitxor || + expr.id() == ID_bitxnor || expr.id() == ID_unary_plus || + expr.id() == ID_unary_minus || expr.id() == ID_bitnot) + { + // All operands are context-determined. + for(auto &op : expr.operands()) + downwards_type_propagation(op, type); + expr.type() = type; + return; + } + else if( + expr.id() == ID_shl || expr.id() == ID_ashr || expr.id() == ID_lshr || + expr.id() == ID_power) + { + // The LHS is context-determined, the RHS is self-determined + auto &binary_expr = to_binary_expr(expr); + downwards_type_propagation(binary_expr.lhs(), type); + expr.type() = type; + return; + } + else if(expr.id() == ID_if) + { + // The first operand is self-determined, the others are context-determined + auto &if_expr = to_if_expr(expr); + downwards_type_propagation(if_expr.op1(), type); + downwards_type_propagation(if_expr.op2(), type); + expr.type() = type; + return; + } - return; - } - else if(expr.id() == ID_if) - { - if(expr.operands().size() == 3) - { - propagate_type(to_if_expr(expr).true_case(), type); - propagate_type(to_if_expr(expr).false_case(), type); + // Just cast the expression, leave any operands as they are. - expr.type() = type; - return; - } - } - else if(expr.id() == ID_shl) // does not work with shr - { - // does not work with boolean - if(type.id() != ID_bool) - { - if(expr.operands().size() == 2) - { - propagate_type(to_binary_expr(expr).op0(), type); - // not applicable to second operand + bool is_constant = expr.is_constant(); - expr.type() = type; - return; - } - } - } + if( + (expr.type().id() == ID_signedbv || + expr.type().id() == ID_verilog_signedbv) && + (type.id() == ID_unsignedbv || type.id() == ID_verilog_unsignedbv) && + get_width(expr.type()) < get_width(type)) + { + // "If the operand shall be extended, then it shall be sign-extended only + // if the propagated type is signed." + // A typecast from signed to a larger unsigned would sign extend. + expr = zero_extend(expr, type); + } + else + { + expr = typecast_exprt{expr, type}; } - implicit_typecast(expr, type); + // fold constants + if(is_constant) + expr = verilog_simplifier(expr, ns); } /*******************************************************************\ @@ -2535,39 +2549,6 @@ void verilog_typecheck_exprt::tc_binary_expr( /*******************************************************************\ -Function: zero_extend - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -static exprt zero_extend(const exprt &expr, const typet &type) -{ - auto old_width = expr.type().id() == ID_bool ? 1 - : expr.type().id() == ID_integer - ? 32 - : to_bitvector_type(expr.type()).get_width(); - - // first make unsigned - typet tmp_type; - - if(type.id() == ID_unsignedbv) - tmp_type = unsignedbv_typet{old_width}; - else if(type.id() == ID_verilog_unsignedbv) - tmp_type = verilog_unsignedbv_typet{old_width}; - else - PRECONDITION(false); - - return typecast_exprt::conditional_cast( - typecast_exprt::conditional_cast(expr, tmp_type), type); -} - -/*******************************************************************\ - Function: verilog_typecheck_exprt::convert_relation Inputs: From 16aa773931e04609ab49383f3df3871505a4ed92 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 2 Oct 2025 13:24:45 -0700 Subject: [PATCH 2/3] Verilog: remove constant folding during downwards type propagation This removes the constant folding during towards type propagation in the Verilog frontend, as this is premature optimisation. --- regression/ebmc/smv-word-level/verilog1.desc | 2 +- src/verilog/verilog_typecheck_expr.cpp | 7 ------- 2 files changed, 1 insertion(+), 8 deletions(-) diff --git a/regression/ebmc/smv-word-level/verilog1.desc b/regression/ebmc/smv-word-level/verilog1.desc index d4dfef295..2c9a6ebca 100644 --- a/regression/ebmc/smv-word-level/verilog1.desc +++ b/regression/ebmc/smv-word-level/verilog1.desc @@ -4,7 +4,7 @@ verilog1.sv ^MODULE main$ ^VAR x : unsigned word\[32\];$ ^INIT main\.x = 0ud32_0$ -^INVAR Verilog::main\.x_aux0 = main\.x \+ 0ud32_1$ +^INVAR Verilog::main\.x_aux0 = main\.x \+ unsigned\(0sd32_1\)$ ^TRANS next\(main\.x\) = Verilog::main\.x_aux0$ ^LTLSPEC F main\.x = unsigned\(0sd32_10\)$ ^EXIT=0$ diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index 5db6df015..ff911c1e5 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/src/verilog/verilog_typecheck_expr.cpp @@ -322,9 +322,6 @@ void verilog_typecheck_exprt::downwards_type_propagation( } // Just cast the expression, leave any operands as they are. - - bool is_constant = expr.is_constant(); - if( (expr.type().id() == ID_signedbv || expr.type().id() == ID_verilog_signedbv) && @@ -340,10 +337,6 @@ void verilog_typecheck_exprt::downwards_type_propagation( { expr = typecast_exprt{expr, type}; } - - // fold constants - if(is_constant) - expr = verilog_simplifier(expr, ns); } /*******************************************************************\ From 4240ae84514fa36da0f48ed786480e4e0f833745 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 2 Oct 2025 13:36:23 -0700 Subject: [PATCH 3/3] Verilog: fix semantics of relations This replaces the custom code for type checking the operands of relations by the code used for other binary expressions. This fixes the downwards type/size propagation. --- .../assignment-with-function-call1.sv | 4 +- regression/verilog/expressions/equality1.desc | 2 +- regression/verilog/expressions/equality2.desc | 2 +- regression/verilog/expressions/shl4.desc | 3 +- .../expressions/wildcard_equality1.desc | 2 +- .../verilog/system-functions/past6.desc | 2 +- src/verilog/verilog_typecheck_expr.cpp | 40 ++----------------- 7 files changed, 11 insertions(+), 44 deletions(-) diff --git a/regression/verilog/assignments/assignment-with-function-call1.sv b/regression/verilog/assignments/assignment-with-function-call1.sv index 5dd9a5857..2f8f431d9 100644 --- a/regression/verilog/assignments/assignment-with-function-call1.sv +++ b/regression/verilog/assignments/assignment-with-function-call1.sv @@ -10,8 +10,8 @@ module top(input [7:0] a, input [7:0] b); wire [7:0] sum_a_b = fn(a, b), sum_1_2 = fn(1, 2), sum_2_3 = fn(2, 3); - - assert property (sum_a_b==a[2:0]+b[2:0]); + + assert property (sum_a_b[2:0]==a[2:0]+b[2:0]); assert property (sum_1_2==3); diff --git a/regression/verilog/expressions/equality1.desc b/regression/verilog/expressions/equality1.desc index e9fed273e..2418f3ee1 100644 --- a/regression/verilog/expressions/equality1.desc +++ b/regression/verilog/expressions/equality1.desc @@ -10,7 +10,7 @@ equality1.v ^\[.*\] always 32'b0000000000000000000000000000000x != 10 === 32'b0000000000000000000000000000000x: PROVED .*$ ^\[.*\] always 32'b0000000000000000000000000000000z != 20 === 32'b0000000000000000000000000000000x: PROVED .*$ ^\[.*\] always 1'sb1 == 2'b11 === 0: PROVED .*$ -^\[.*\] always 2'sb11 == 2'sb11 === 1: PROVED .*$ +^\[.*\] always 1'sb1 == 2'sb11 === 1: PROVED .*$ ^\[.*\] always 1\.1 == 1\.1 == 1: PROVED .*$ ^\[.*\] always 1\.1 == 1 == 0: PROVED .*$ ^EXIT=0$ diff --git a/regression/verilog/expressions/equality2.desc b/regression/verilog/expressions/equality2.desc index f70993dbe..179c844c4 100644 --- a/regression/verilog/expressions/equality2.desc +++ b/regression/verilog/expressions/equality2.desc @@ -12,7 +12,7 @@ equality2.v ^\[.*\] always 32'b0000000000000000000000000000000z === 1 == 0: PROVED .*$ ^\[.*\] always 1 === 1 == 1: PROVED .*$ ^\[.*\] always 3'b011 === 2'sb11 == 1: PROVED .*$ -^\[.*\] always 3'sb111 === 3'sb111 == 1: PROVED .*$ +^\[.*\] always 3'sb111 === 2'sb11 == 1: PROVED .*$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/expressions/shl4.desc b/regression/verilog/expressions/shl4.desc index c467a78ce..7b1140269 100644 --- a/regression/verilog/expressions/shl4.desc +++ b/regression/verilog/expressions/shl4.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE broken-smt-backend shl4.sv --bound 0 ^EXIT=0$ @@ -6,4 +6,3 @@ shl4.sv -- ^warning: ignoring -- -This gives the wrong answer. diff --git a/regression/verilog/expressions/wildcard_equality1.desc b/regression/verilog/expressions/wildcard_equality1.desc index 302a4fdfc..e0457f8b1 100644 --- a/regression/verilog/expressions/wildcard_equality1.desc +++ b/regression/verilog/expressions/wildcard_equality1.desc @@ -10,7 +10,7 @@ wildcard_equality1.sv ^\[main\.property07\] always 2'b00 !=\? 2'b0x === 0: PROVED .*$ ^\[main\.property08\] always 2'b10 !=\? 2'b0x === 1: PROVED .*$ ^\[main\.property09\] always 1'sb1 ==\? 2'b11 === 0: PROVED .*$ -^\[main\.property10\] always 2'sb11 ==\? 2'sb11 === 1: PROVED .*$ +^\[main\.property10\] always 1'sb1 ==\? 2'sb11 === 1: PROVED .*$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/system-functions/past6.desc b/regression/verilog/system-functions/past6.desc index 79d8dc66c..3432b717a 100644 --- a/regression/verilog/system-functions/past6.desc +++ b/regression/verilog/system-functions/past6.desc @@ -1,4 +1,4 @@ -CORE +CORE broken-smt-backend past6.sv ^EXIT=10$ diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index ff911c1e5..9df8862dd 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/src/verilog/verilog_typecheck_expr.cpp @@ -2554,43 +2554,11 @@ Function: verilog_typecheck_exprt::convert_relation void verilog_typecheck_exprt::convert_relation(binary_exprt &expr) { - auto &lhs = expr.lhs(); - auto &rhs = expr.rhs(); - - convert_expr(lhs); - convert_expr(rhs); - - union_decay(lhs); - union_decay(rhs); - - // Relations are special-cased in 1800-2017 11.8.2. - const typet new_type = - max_type(enum_decay(lhs.type()), enum_decay(rhs.type())); - - if(new_type.is_nil()) - { - throw errort().with_location(expr.source_location()) - << "expected operands of compatible type but got:\n" - << " " << to_string(lhs.type()) << '\n' - << " " << to_string(rhs.type()); - } + convert_expr(expr.lhs()); + convert_expr(expr.rhs()); - // If both operands are signed, both are sign-extended to the max width. - // Otherwise, both are zero-extended to the max width. - // In particular, signed operands are then _not_ sign extended, - // which a typecast would do. - if(new_type.id() == ID_verilog_unsignedbv || new_type.id() == ID_unsignedbv) - { - // zero extend both operands - lhs = zero_extend(lhs, new_type); - rhs = zero_extend(rhs, new_type); - } - else - { - // convert - implicit_typecast(lhs, new_type); - implicit_typecast(rhs, new_type); - } + // determine the max of the operand types and propagate it downwards + tc_binary_expr(expr); } /*******************************************************************\