From 435509bd7ea8afcd87c79a7c8182da478c47c1ff Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 19 Oct 2025 10:44:32 -0700 Subject: [PATCH] Verilog: explicit casts are assignments Explicit casts, such as size casts, act like assignments, and hence, use the assignment conversion. --- CHANGELOG | 3 ++- .../verilog/expressions/size_cast3.desc | 3 +-- .../verilog/expressions/static_cast3.desc | 3 +-- .../verilog/expressions/static_cast4.desc | 8 ++++++++ .../verilog/expressions/static_cast4.sv | 17 ++++++++++++++++ src/verilog/verilog_expr.h | 11 ---------- src/verilog/verilog_lowering.cpp | 17 +++++++++++++--- src/verilog/verilog_typecheck_expr.cpp | 20 ++++++++++++++++++- 8 files changed, 62 insertions(+), 20 deletions(-) create mode 100644 regression/verilog/expressions/static_cast4.desc create mode 100644 regression/verilog/expressions/static_cast4.sv diff --git a/CHANGELOG b/CHANGELOG index dac3a2f3c..608287b9c 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -1,7 +1,8 @@ # EBMC 5.8 -* SystemVerilog: cover sequence * Verilog: semantic fix for output register ports +* SystemVerilog: cover sequence +* SystemVerilog: semantics fix for explicit casts # EBMC 5.7 diff --git a/regression/verilog/expressions/size_cast3.desc b/regression/verilog/expressions/size_cast3.desc index 9a0e097c3..cf828778e 100644 --- a/regression/verilog/expressions/size_cast3.desc +++ b/regression/verilog/expressions/size_cast3.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE size_cast3.sv --module main ^EXIT=0$ @@ -6,4 +6,3 @@ size_cast3.sv -- ^warning: ignoring -- -This is not yet implemented. diff --git a/regression/verilog/expressions/static_cast3.desc b/regression/verilog/expressions/static_cast3.desc index 4ff7e48ae..f6c7f68c3 100644 --- a/regression/verilog/expressions/static_cast3.desc +++ b/regression/verilog/expressions/static_cast3.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE static_cast3.sv --module main ^EXIT=0$ @@ -6,4 +6,3 @@ static_cast3.sv -- ^warning: ignoring -- -This is not yet implemented. diff --git a/regression/verilog/expressions/static_cast4.desc b/regression/verilog/expressions/static_cast4.desc new file mode 100644 index 000000000..8a353d973 --- /dev/null +++ b/regression/verilog/expressions/static_cast4.desc @@ -0,0 +1,8 @@ +CORE +static_cast4.sv +--module main +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/verilog/expressions/static_cast4.sv b/regression/verilog/expressions/static_cast4.sv new file mode 100644 index 000000000..cd7fc02a2 --- /dev/null +++ b/regression/verilog/expressions/static_cast4.sv @@ -0,0 +1,17 @@ +module main; + + // The standard suggests that casts can be applied to assignment patterns. + // VCS, Icarus Verilog and Xcelium error this. + // Questa allows it. + // Riviera throws an internal error. + + typedef struct packed { int a, b; } S; + + initial begin + S some_struct; + some_struct.a = 1; + some_struct.b = 2; + assert ((S'('{a: 1, b: 2})) == some_struct); + end + +endmodule diff --git a/src/verilog/verilog_expr.h b/src/verilog/verilog_expr.h index 0ce9ecca2..e87912694 100644 --- a/src/verilog/verilog_expr.h +++ b/src/verilog/verilog_expr.h @@ -2558,12 +2558,6 @@ class verilog_explicit_size_cast_exprt : public binary_exprt { return op1(); } - - // lower to typecast - exprt lower() const - { - return typecast_exprt{op(), type()}; - } }; inline const verilog_explicit_size_cast_exprt & @@ -2659,11 +2653,6 @@ class verilog_explicit_type_cast_exprt : public unary_exprt std::move(__type)) { } - - exprt lower() const - { - return typecast_exprt{op(), type()}; - } }; inline const verilog_explicit_type_cast_exprt & diff --git a/src/verilog/verilog_lowering.cpp b/src/verilog/verilog_lowering.cpp index 9bb6dab9f..510644d1b 100644 --- a/src/verilog/verilog_lowering.cpp +++ b/src/verilog/verilog_lowering.cpp @@ -471,8 +471,13 @@ exprt verilog_lowering(exprt expr) } else if(expr.id() == ID_verilog_explicit_type_cast) { - return verilog_lowering_cast( - to_typecast_expr(to_verilog_explicit_type_cast_expr(expr).lower())); + // These act like an assignment, and hence, the type checker + // has already converted the argument to the target type. + auto &type_cast = to_verilog_explicit_type_cast_expr(expr); + expr.type() = verilog_lowering(expr.type()); + DATA_INVARIANT( + type_cast.op().type() == type_cast.type(), "type cast type consistency"); + return type_cast.op(); } else if(expr.id() == ID_verilog_explicit_signing_cast) { @@ -480,7 +485,13 @@ exprt verilog_lowering(exprt expr) } else if(expr.id() == ID_verilog_explicit_size_cast) { - return verilog_lowering(to_verilog_explicit_size_cast_expr(expr).lower()); + // These act like an assignment, and hence, the type checker + // has already converted the argument to the target type. + auto &size_cast = to_verilog_explicit_size_cast_expr(expr); + expr.type() = verilog_lowering(expr.type()); + DATA_INVARIANT( + size_cast.op().type() == size_cast.type(), "size cast type consistency"); + return size_cast.op(); } else if( expr.id() == ID_verilog_streaming_concatenation_left_to_right || diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index 9bb189316..1e01aee9c 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/src/verilog/verilog_typecheck_expr.cpp @@ -2694,9 +2694,22 @@ exprt verilog_typecheck_exprt::convert_unary_expr(unary_exprt expr) else if(expr.id() == ID_verilog_explicit_type_cast) { // SystemVerilog has got type'(expr). This is an explicit - // type cast. + // type cast. These are assignment contexts. convert_expr(expr.op()); expr.type() = elaborate_type(expr.type()); + + // In contrast to assignments, these can turn integers into enums + // (1800-2017 6.19.3). + if(expr.type().get(ID_C_verilog_type) == ID_verilog_enum) + { + expr.op() = typecast_exprt::conditional_cast(expr.op(), expr.type()); + } + else + { + assignment_conversion(expr.op(), expr.type()); + } + + CHECK_RETURN(expr.op().type() == expr.type()); } else if(expr.id() == ID_verilog_explicit_signing_cast) { @@ -3327,6 +3340,11 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr) << "cannot perform size cast on " << to_string(op_type); } + // These act like an assignment (1800-2017 6.24.1) + assignment_conversion(expr.rhs(), expr.type()); + + CHECK_RETURN(expr.rhs().type() == expr.type()); + return std::move(expr); } else if(