From 4640fa72f85ab5ba46a5de7ef33e30e7605ad218 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 28 Sep 2025 01:10:27 -0700 Subject: [PATCH 1/2] Verilog: test verilog/asic-world-operators/shift.desc works PR #1277 has moved the failing test case out of this file. --- regression/verilog/asic-world-operators/shift.desc | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/regression/verilog/asic-world-operators/shift.desc b/regression/verilog/asic-world-operators/shift.desc index 82422e73a..519152ad8 100644 --- a/regression/verilog/asic-world-operators/shift.desc +++ b/regression/verilog/asic-world-operators/shift.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE shift.sv --module main --bound 0 ^EXIT=0$ @@ -6,4 +6,3 @@ shift.sv -- ^warning: ignoring -- -The test shift_p7 fails. From 18504a41a75c8fb85df9beb3f3c1c80dab82cdee Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 26 Sep 2025 07:10:06 -0700 Subject: [PATCH 2/2] Verilog: assignment conversion The conversion done to the RHS of an assignment differs from the downwards propagation done when adjusting the type of the operand of expressions. This introduces a new method assignment_conversion, different from propagate_type, to implement these differences. Three tests are changed to restore the previous circuit, as the circuit without the downward propagation pass is too large for BDDs. --- .../verilog/SVA/sequence_repetition1.sv | 4 +- .../verilog/SVA/sequence_repetition2.sv | 4 +- .../verilog/SVA/sequence_repetition3.sv | 4 +- regression/verilog/modules/ports2.desc | 2 +- src/verilog/verilog_typecheck.cpp | 51 ++++++++++++++++--- src/verilog/verilog_typecheck.h | 2 + 6 files changed, 52 insertions(+), 15 deletions(-) diff --git a/regression/verilog/SVA/sequence_repetition1.sv b/regression/verilog/SVA/sequence_repetition1.sv index 7973497c5..a2d03292b 100644 --- a/regression/verilog/SVA/sequence_repetition1.sv +++ b/regression/verilog/SVA/sequence_repetition1.sv @@ -4,10 +4,10 @@ module main(input clk); // 0 1 2 3 4 ... always_ff @(posedge clk) - x<=x+1; + x<=x+8'd1; // 0 0 1 1 2 2 3 3 ... - wire [7:0] half_x = x/2; + wire [7:0] half_x = x/8'd2; // should pass initial p0: assert property (half_x==0[*2]); diff --git a/regression/verilog/SVA/sequence_repetition2.sv b/regression/verilog/SVA/sequence_repetition2.sv index 9d848f495..d6efc708f 100644 --- a/regression/verilog/SVA/sequence_repetition2.sv +++ b/regression/verilog/SVA/sequence_repetition2.sv @@ -4,10 +4,10 @@ module main(input clk); // 0 1 2 3 4 ... always_ff @(posedge clk) - x<=x+1; + x<=x+8'd1; // 0 0 1 1 2 2 3 3 ... - wire [7:0] half_x = x/2; + wire [7:0] half_x = x/8'd2; // should pass initial p0: assert property (x==0[*]); diff --git a/regression/verilog/SVA/sequence_repetition3.sv b/regression/verilog/SVA/sequence_repetition3.sv index e0ab91765..aa383c2ec 100644 --- a/regression/verilog/SVA/sequence_repetition3.sv +++ b/regression/verilog/SVA/sequence_repetition3.sv @@ -4,10 +4,10 @@ module main(input clk); // 0 1 2 3 4 ... always_ff @(posedge clk) - x<=x+1; + x<=x+8'd1; // 0 0 1 1 2 2 3 3 ... - wire [7:0] half_x = x/2; + wire [7:0] half_x = x/8'd2; // should pass initial p0: assert property (x==0[*1] #=# x==1[*1]); diff --git a/regression/verilog/modules/ports2.desc b/regression/verilog/modules/ports2.desc index b4938fc43..2c640a8a2 100644 --- a/regression/verilog/modules/ports2.desc +++ b/regression/verilog/modules/ports2.desc @@ -1,4 +1,4 @@ -CORE +CORE broken-smt-backend ports2.v --module main --bound 1 ^EXIT=0$ diff --git a/src/verilog/verilog_typecheck.cpp b/src/verilog/verilog_typecheck.cpp index 6023fa1cc..b328b2f37 100644 --- a/src/verilog/verilog_typecheck.cpp +++ b/src/verilog/verilog_typecheck.cpp @@ -27,6 +27,34 @@ Author: Daniel Kroening, kroening@kroening.com /*******************************************************************\ +Function: verilog_typecheckt::assignment_conversion + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void verilog_typecheckt::assignment_conversion( + exprt &rhs, + const typet &lhs_type) +{ + // Implements 1800-2017 10.7 + // If the RHS is smaller than the LHS: + // * if the RHS is unsigned, it is zero-padded + // * if the RHS is signed, it is sign-extended + // If the RHS is larger than the LHS, it is truncated. + + // This matches our typecast, but differs from the steps taken + // when evaluating binary expressions (11.8.2), where sign + // extension only happens when the propagated type is signed. + implicit_typecast(rhs, lhs_type); +} + +/*******************************************************************\ + Function: verilog_typecheckt::typecheck_port_connection Inputs: @@ -74,7 +102,10 @@ void verilog_typecheckt::typecheck_port_connection( if(symbol.is_output) check_lhs(op, A_CONTINUOUS); else - propagate_type(op, port.type()); + { + // This is an assignment to the input + assignment_conversion(op, port.type()); + } } } @@ -239,7 +270,8 @@ void verilog_typecheckt::typecheck_builtin_port_connections( convert_expr(connection); } - propagate_type(connection, type); + // like an assignment + assignment_conversion(connection, type); } } @@ -427,7 +459,7 @@ void verilog_typecheckt::convert_decl(verilog_declt &decl) { auto &rhs = declarator.value(); convert_expr(rhs); - propagate_type(rhs, symbol.type); + assignment_conversion(rhs, symbol.type); } } } @@ -795,7 +827,7 @@ void verilog_typecheckt::convert_procedural_continuous_assign( convert_expr(lhs); convert_expr(rhs); - propagate_type(rhs, lhs.type()); + assignment_conversion(rhs, lhs.type()); check_lhs(lhs, A_PROCEDURAL_CONTINUOUS); } @@ -839,7 +871,7 @@ void verilog_typecheckt::convert_continuous_assign( else convert_expr(lhs); - propagate_type(rhs, lhs.type()); + assignment_conversion(rhs, lhs.type()); check_lhs(lhs, A_CONTINUOUS); } @@ -903,7 +935,7 @@ void verilog_typecheckt::convert_function_call_or_task_enable( for(unsigned i=0; itype; @@ -983,7 +1015,8 @@ void verilog_typecheckt::convert_force(verilog_forcet &statement) convert_expr(lhs); convert_expr(rhs); - propagate_type(rhs, lhs.type()); + + assignment_conversion(rhs, lhs.type()); //check_lhs(lhs, blocking?A_BLOCKING:A_NON_BLOCKING); } @@ -1014,7 +1047,7 @@ void verilog_typecheckt::convert_assign( convert_expr(lhs); convert_expr(rhs); - propagate_type(rhs, lhs.type()); + assignment_conversion(rhs, lhs.type()); check_lhs(lhs, blocking?A_BLOCKING:A_NON_BLOCKING); } @@ -1199,6 +1232,8 @@ void verilog_typecheckt::convert_case_values( Forall_operands(it, values) { convert_expr(*it); + + // This works like a relational operator, not like an assignment typet t=max_type(it->type(), case_operand.type()); propagate_type(*it, t); } diff --git a/src/verilog/verilog_typecheck.h b/src/verilog/verilog_typecheck.h index 4d0ce747b..ffa6cd276 100644 --- a/src/verilog/verilog_typecheck.h +++ b/src/verilog/verilog_typecheck.h @@ -168,6 +168,8 @@ class verilog_typecheckt: void convert_assert_assume_cover(verilog_assert_assume_cover_statementt &); void convert_assume(verilog_assume_statementt &); + void assignment_conversion(exprt &rhs, const typet &lhs_type); + // module items void convert_decl(class verilog_declt &); void convert_function_or_task(class verilog_function_or_task_declt &);