From 02076d464004ed7ff6e2d39fe81e55c98e3af124 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 1 Dec 2025 11:50:46 -0800 Subject: [PATCH] Verilog: fix integral vs. bit vector terminology This changes the naming of methods and error messages. The term 'integral' includes non-integer types, e.g., time variables. Many operators require operands that are integral but exclude time variables. The standard calls these "bit vector types". --- .../verilog/expressions/concatenation5.desc | 2 +- regression/verilog/expressions/equality3.desc | 1 + regression/verilog/expressions/mod2.desc | 2 +- .../verilog/expressions/reduction2.desc | 2 +- .../verilog/expressions/replication3.desc | 2 +- regression/verilog/expressions/shr2.desc | 2 +- .../expressions/streaming_concatenation2.desc | 2 +- .../expressions/wildcard_equality2.desc | 4 +- ...card_equality2.v => wildcard_equality2.sv} | 2 +- src/verilog/verilog_typecheck_expr.cpp | 58 +++++++++++-------- src/verilog/verilog_typecheck_expr.h | 2 +- 11 files changed, 46 insertions(+), 33 deletions(-) rename regression/verilog/expressions/{wildcard_equality2.v => wildcard_equality2.sv} (71%) diff --git a/regression/verilog/expressions/concatenation5.desc b/regression/verilog/expressions/concatenation5.desc index 1c6799eeb..36995a0ff 100644 --- a/regression/verilog/expressions/concatenation5.desc +++ b/regression/verilog/expressions/concatenation5.desc @@ -1,7 +1,7 @@ CORE concatenation5.v -^file .* line 4: operand 1.1 must be integral$ +^file .* line 4: operand 1.1 must have a bit vector type$ ^EXIT=2$ ^SIGNAL=0$ -- diff --git a/regression/verilog/expressions/equality3.desc b/regression/verilog/expressions/equality3.desc index 9b823fb06..6db629d90 100644 --- a/regression/verilog/expressions/equality3.desc +++ b/regression/verilog/expressions/equality3.desc @@ -1,6 +1,7 @@ CORE equality3.v +^file .* line 4: the case equality operator does not allow real or shortreal$ ^EXIT=2$ ^SIGNAL=0$ -- diff --git a/regression/verilog/expressions/mod2.desc b/regression/verilog/expressions/mod2.desc index 329be47ba..a2a7a4294 100644 --- a/regression/verilog/expressions/mod2.desc +++ b/regression/verilog/expressions/mod2.desc @@ -1,7 +1,7 @@ CORE mod2.v -^file .* line 4: operand 1\.1 must be integral$ +^file .* line 4: operand 1\.1 must have a bit vector type$ ^EXIT=2$ ^SIGNAL=0$ -- diff --git a/regression/verilog/expressions/reduction2.desc b/regression/verilog/expressions/reduction2.desc index 740909c3e..fea565df9 100644 --- a/regression/verilog/expressions/reduction2.desc +++ b/regression/verilog/expressions/reduction2.desc @@ -1,7 +1,7 @@ CORE reduction2.v -^file .* line 4: operand 1\.1 must be integral$ +^file .* line 4: operand 1\.1 must have a bit vector type$ ^EXIT=2$ ^SIGNAL=0$ -- diff --git a/regression/verilog/expressions/replication3.desc b/regression/verilog/expressions/replication3.desc index bdf6fde7e..35148a1bb 100644 --- a/regression/verilog/expressions/replication3.desc +++ b/regression/verilog/expressions/replication3.desc @@ -1,7 +1,7 @@ CORE replication3.v -^file .* line 3: operand 1\.1 must be integral$ +^file .* line 3: operand 1\.1 must have a bit vector type$ ^EXIT=2$ ^SIGNAL=0$ -- diff --git a/regression/verilog/expressions/shr2.desc b/regression/verilog/expressions/shr2.desc index e2957ddb1..48a6a5ac6 100644 --- a/regression/verilog/expressions/shr2.desc +++ b/regression/verilog/expressions/shr2.desc @@ -1,7 +1,7 @@ CORE shr2.v -^file .* line 4: operand 1\.1 must be integral$ +^file .* line 4: operand 1\.1 must have a bit vector type$ ^EXIT=2$ ^SIGNAL=0$ -- diff --git a/regression/verilog/expressions/streaming_concatenation2.desc b/regression/verilog/expressions/streaming_concatenation2.desc index ac3c6d7f1..c8a8006d0 100644 --- a/regression/verilog/expressions/streaming_concatenation2.desc +++ b/regression/verilog/expressions/streaming_concatenation2.desc @@ -1,7 +1,7 @@ CORE streaming_concatenation2.sv -^file .* line 4: operand 1\.1 must be integral$ +^file .* line 4: operand 1\.1 must have a bit vector type$ ^EXIT=2$ ^SIGNAL=0$ -- diff --git a/regression/verilog/expressions/wildcard_equality2.desc b/regression/verilog/expressions/wildcard_equality2.desc index ecfe995c4..c653df5c9 100644 --- a/regression/verilog/expressions/wildcard_equality2.desc +++ b/regression/verilog/expressions/wildcard_equality2.desc @@ -1,7 +1,7 @@ CORE -wildcard_equality2.v +wildcard_equality2.sv -^file .* line 4: operand 1\.1 must be integral$ +^file .* line 4: operand 1\.1 must have a bit vector type$ ^EXIT=2$ ^SIGNAL=0$ -- diff --git a/regression/verilog/expressions/wildcard_equality2.v b/regression/verilog/expressions/wildcard_equality2.sv similarity index 71% rename from regression/verilog/expressions/wildcard_equality2.v rename to regression/verilog/expressions/wildcard_equality2.sv index aea237018..b0a3ebde2 100644 --- a/regression/verilog/expressions/wildcard_equality2.v +++ b/regression/verilog/expressions/wildcard_equality2.sv @@ -1,6 +1,6 @@ module main; // ==? only takes integral types - wire x = 1.1 === 1.2; + wire x = 1.1 ==? 1.2; endmodule diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index 9076e7aba..d1478b4c8 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/src/verilog/verilog_typecheck_expr.cpp @@ -426,7 +426,7 @@ void verilog_typecheck_exprt::no_bool_ops(exprt &expr) /*******************************************************************\ -Function: verilog_typecheck_exprt::must_be_integral +Function: verilog_typecheck_exprt::must_be_bit_vector Inputs: @@ -436,9 +436,9 @@ Function: verilog_typecheck_exprt::must_be_integral \*******************************************************************/ -void verilog_typecheck_exprt::must_be_integral(const exprt &expr) +void verilog_typecheck_exprt::must_be_bit_vector(exprt &expr) { - // Throw an error if the given expression doesn't have an integral type. + // Throw an error if the given expression doesn't have a bitvector type. const auto &type = expr.type(); if(type.id() == ID_bool) { @@ -452,7 +452,7 @@ void verilog_typecheck_exprt::must_be_integral(const exprt &expr) } else throw errort().with_location(expr.source_location()) - << "operand " << to_string(expr) << " must be integral"; + << "operand " << to_string(expr) << " must have a bit vector type"; } /*******************************************************************\ @@ -490,7 +490,7 @@ exprt verilog_typecheck_exprt::convert_expr_concatenation( << "unsized literals are not allowed in concatenations"; } - must_be_integral(*it); + must_be_bit_vector(*it); const typet &type = it->type(); @@ -1563,7 +1563,7 @@ exprt verilog_typecheck_exprt::convert_constant(constant_exprt expr) const std::string &value = id2string(expr.get_value()); - // real or integral? + // real or integer? if( value.find('.') != std::string::npos || (value.find('h') == std::string::npos && @@ -2558,10 +2558,11 @@ exprt verilog_typecheck_exprt::convert_unary_expr(unary_exprt expr) { // these may produce an 'x' if the operand is a verilog_bv convert_expr(expr.op()); - must_be_integral(expr.op()); + must_be_bit_vector(expr.op()); - if (expr.op().type().id() == ID_verilog_signedbv || - expr.op().type().id() == ID_verilog_unsignedbv) + if( + expr.op().type().id() == ID_verilog_signedbv || + expr.op().type().id() == ID_verilog_unsignedbv) { expr.type()=verilog_unsignedbv_typet(1); } @@ -2668,7 +2669,7 @@ exprt verilog_typecheck_exprt::convert_unary_expr(unary_exprt expr) // slice_size is defaulted to 1 PRECONDITION(expr.op().operands().size() == 1); convert_expr(expr.op().operands()[0]); - must_be_integral(expr.op().operands()[0]); + must_be_bit_vector(expr.op().operands()[0]); expr.type() = expr.op().operands()[0].type(); return std::move(expr); } @@ -2839,7 +2840,7 @@ exprt verilog_typecheck_exprt::convert_replication_expr(replication_exprt expr) exprt &op1=expr.op1(); convert_expr(op1); - must_be_integral(op1); + must_be_bit_vector(op1); if(op1.type().id()==ID_bool) op1 = typecast_exprt{op1, unsignedbv_typet{1}}; @@ -3069,9 +3070,15 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr) expr.id() == ID_verilog_wildcard_inequality) { // ==? and !=? + // 1800-2017 Table 11-1 says that any integral operands are allowed; + // however, it is unclear how these would apply to types that do not have + // a bit-encoding. convert_relation(expr); - expr.type() = verilog_unsignedbv_typet(1); + must_be_bit_vector(expr.lhs()); + must_be_bit_vector(expr.rhs()); + + expr.type() = verilog_unsignedbv_typet{1}; return std::move(expr); } @@ -3079,15 +3086,20 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr) expr.id()==ID_verilog_case_inequality) { // === and !== + // Take any operand types except real and shortreal (1800-2017 Table 11-1). // The result is always Boolean, and semantically // a proper equality is performed. - expr.type()=bool_typet(); + expr.type() = bool_typet{}; convert_relation(expr); - // integral operands only - must_be_integral(expr.lhs()); - must_be_integral(expr.rhs()); + if( + expr.lhs().type().id() == ID_verilog_real || + expr.lhs().type().id() == ID_verilog_shortreal) + { + throw errort().with_location(expr.source_location()) + << "the case equality operator does not allow real or shortreal"; + } return std::move(expr); } @@ -3120,8 +3132,8 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr) convert_expr(expr.lhs()); convert_expr(expr.rhs()); - must_be_integral(expr.lhs()); - must_be_integral(expr.rhs()); + must_be_bit_vector(expr.lhs()); + must_be_bit_vector(expr.rhs()); no_bool_ops(expr); const typet &lhs_type = expr.lhs().type(); @@ -3157,9 +3169,8 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr) // logical right shift >> convert_expr(expr.lhs()); convert_expr(expr.rhs()); - must_be_integral(expr.lhs()); - must_be_integral(expr.rhs()); - no_bool_ops(expr); + must_be_bit_vector(expr.lhs()); + must_be_bit_vector(expr.rhs()); const typet &lhs_type = expr.lhs().type(); const typet &rhs_type = expr.rhs().type(); @@ -3191,12 +3202,13 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr) { convert_expr(expr.lhs()); convert_expr(expr.rhs()); - must_be_integral(expr.lhs()); - must_be_integral(expr.rhs()); tc_binary_expr(expr); no_bool_ops(expr); + must_be_bit_vector(expr.lhs()); + must_be_bit_vector(expr.rhs()); + expr.type() = expr.lhs().type(); return std::move(expr); diff --git a/src/verilog/verilog_typecheck_expr.h b/src/verilog/verilog_typecheck_expr.h index 59a4fdcc1..0050ef4a5 100644 --- a/src/verilog/verilog_typecheck_expr.h +++ b/src/verilog/verilog_typecheck_expr.h @@ -196,7 +196,7 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset void tc_binary_expr(const exprt &expr, exprt &op0, exprt &op1); void convert_relation(binary_exprt &); void no_bool_ops(exprt &); - void must_be_integral(const exprt &); + void must_be_bit_vector(exprt &); // SVA void convert_sva(exprt &expr)