From b98c14974437cd306f84c23ca5b37ccf43c7ad47 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 3 Dec 2025 08:31:27 -0800 Subject: [PATCH] Verilog system tasks and functions are always base names Verilog system tasks and functions are never qualified or decorated, hence use verilog_identifier_exprt for their name. --- src/verilog/expr2verilog.cpp | 21 +++++ src/verilog/expr2verilog_class.h | 3 + src/verilog/parser.y | 2 +- src/verilog/verilog_expr.cpp | 5 +- src/verilog/verilog_lowering.cpp | 34 ++++---- src/verilog/verilog_synthesis.cpp | 36 ++++----- src/verilog/verilog_typecheck_expr.cpp | 107 ++++++++++++------------- src/verilog/verilog_typecheck_expr.h | 3 +- 8 files changed, 113 insertions(+), 98 deletions(-) diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp index 1d03ba284..8674feba9 100644 --- a/src/verilog/expr2verilog.cpp +++ b/src/verilog/expr2verilog.cpp @@ -1178,6 +1178,24 @@ expr2verilogt::resultt expr2verilogt::convert_symbol(const exprt &src) /*******************************************************************\ +Function: expr2verilogt::convert_verilog_identifier + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +expr2verilogt::resultt +expr2verilogt::convert_verilog_identifier(const verilog_identifier_exprt &src) +{ + return {verilog_precedencet::MAX, id2string(src.base_name())}; +} + +/*******************************************************************\ + Function: expr2verilogt::convert_nondet_symbol Inputs: @@ -1809,6 +1827,9 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src) else if(src.id()==ID_symbol) return convert_symbol(src); + else if(src.id() == ID_verilog_identifier) + return convert_symbol(to_verilog_identifier_expr(src)); + else if(src.id()==ID_nondet_symbol) return convert_nondet_symbol(src); diff --git a/src/verilog/expr2verilog_class.h b/src/verilog/expr2verilog_class.h index 3a32e13d6..f06989bf6 100644 --- a/src/verilog/expr2verilog_class.h +++ b/src/verilog/expr2verilog_class.h @@ -19,6 +19,7 @@ class sva_cycle_delay_exprt; class sva_sequence_first_match_exprt; class sva_sequence_property_instance_exprt; class sva_sequence_repetition_exprt; +class verilog_identifier_exprt; // Precedences (higher means binds more strongly). // Follows Table 11-2 in IEEE 1800-2017. @@ -98,6 +99,8 @@ class expr2verilogt resultt convert_symbol(const exprt &); + resultt convert_verilog_identifier(const verilog_identifier_exprt &); + resultt convert_hierarchical_identifier(const class hierarchical_identifier_exprt &); diff --git a/src/verilog/parser.y b/src/verilog/parser.y index 9f1de4eee..fe0efcfc3 100644 --- a/src/verilog/parser.y +++ b/src/verilog/parser.y @@ -3718,7 +3718,7 @@ function_statement: statement ; system_task_name: TOK_SYSIDENT - { new_symbol($$, $1); } + { new_symbol($$, $1); stack_expr($$).id(ID_verilog_identifier); } ; // System Verilog standard 1800-2017 diff --git a/src/verilog/verilog_expr.cpp b/src/verilog/verilog_expr.cpp index 05431cd4d..c85d92c56 100644 --- a/src/verilog/verilog_expr.cpp +++ b/src/verilog/verilog_expr.cpp @@ -52,8 +52,9 @@ typet verilog_declaratort::merged_type(const typet &declaration_type) const static bool is_system_function_identifier(const exprt &function) { - return function.id() == ID_symbol && - has_prefix(id2string(to_symbol_expr(function).get_identifier()), "$"); + return function.id() == ID_verilog_identifier && + has_prefix( + id2string(to_verilog_identifier_expr(function).base_name()), "$"); } bool function_call_exprt::is_system_function_call() const diff --git a/src/verilog/verilog_lowering.cpp b/src/verilog/verilog_lowering.cpp index 141723f0d..1e7633c27 100644 --- a/src/verilog/verilog_lowering.cpp +++ b/src/verilog/verilog_lowering.cpp @@ -176,20 +176,20 @@ exprt to_bitvector(const exprt &src) exprt verilog_lowering_system_function(const function_call_exprt &call) { - auto identifier = to_symbol_expr(call.function()).get_identifier(); + auto base_name = to_verilog_identifier_expr(call.function()).base_name(); auto &arguments = call.arguments(); - if(identifier == "$signed" || identifier == "$unsigned") + if(base_name == "$signed" || base_name == "$unsigned") { // lower to typecast DATA_INVARIANT( - arguments.size() == 1, id2string(identifier) + " takes one argument"); + arguments.size() == 1, id2string(base_name) + " takes one argument"); return typecast_exprt{arguments[0], call.type()}; } - else if(identifier == "$rtoi") + else if(base_name == "$rtoi") { DATA_INVARIANT( - arguments.size(), id2string(identifier) + " takes one argument"); + arguments.size(), id2string(base_name) + " takes one argument"); // These truncate, and do not round. return floatbv_typecast_exprt{ arguments[0], @@ -197,10 +197,10 @@ exprt verilog_lowering_system_function(const function_call_exprt &call) ieee_floatt::rounding_modet::ROUND_TO_ZERO), verilog_lowering(call.type())}; } - else if(identifier == "$itor") + else if(base_name == "$itor") { DATA_INVARIANT( - arguments.size(), id2string(identifier) + " takes one argument"); + arguments.size(), id2string(base_name) + " takes one argument"); // No rounding required, any 32-bit integer will fit into double. return floatbv_typecast_exprt{ arguments[0], @@ -208,36 +208,36 @@ exprt verilog_lowering_system_function(const function_call_exprt &call) ieee_floatt::rounding_modet::ROUND_TO_ZERO), verilog_lowering(call.type())}; } - else if(identifier == "$bitstoreal") + else if(base_name == "$bitstoreal") { DATA_INVARIANT( - arguments.size(), id2string(identifier) + " takes one argument"); + arguments.size(), id2string(base_name) + " takes one argument"); // not a conversion -- this returns the given bit-pattern as a real return typecast_exprt{ zero_extend_exprt{arguments[0], bv_typet{64}}, verilog_lowering(call.type())}; } - else if(identifier == "$bitstoshortreal") + else if(base_name == "$bitstoshortreal") { DATA_INVARIANT( - arguments.size(), id2string(identifier) + " takes one argument"); + arguments.size(), id2string(base_name) + " takes one argument"); // not a conversion -- this returns the given bit-pattern as a real return typecast_exprt{ zero_extend_exprt{arguments[0], bv_typet{32}}, verilog_lowering(call.type())}; } - else if(identifier == "$realtobits") + else if(base_name == "$realtobits") { DATA_INVARIANT( - arguments.size(), id2string(identifier) + " takes one argument"); + arguments.size(), id2string(base_name) + " takes one argument"); // not a conversion -- this returns the given floating-point bit-pattern as [63:0] return zero_extend_exprt{ typecast_exprt{arguments[0], bv_typet{64}}, call.type()}; } - else if(identifier == "$shortrealtobits") + else if(base_name == "$shortrealtobits") { DATA_INVARIANT( - arguments.size(), id2string(identifier) + " takes one argument"); + arguments.size(), id2string(base_name) + " takes one argument"); // not a conversion -- this returns the given floating-point bit-pattern as [31:0] return zero_extend_exprt{ typecast_exprt{arguments[0], bv_typet{32}}, call.type()}; @@ -350,8 +350,8 @@ exprt verilog_lowering(exprt expr) auto &call = to_function_call_expr(expr); if(call.is_system_function_call()) { - auto identifier = to_symbol_expr(call.function()).get_identifier(); - if(identifier == "$typename") + auto base_name = to_verilog_identifier_expr(call.function()).base_name(); + if(base_name == "$typename") { // Don't touch. // Will be expanded by elaborate_constant_system_function_call, diff --git a/src/verilog/verilog_synthesis.cpp b/src/verilog/verilog_synthesis.cpp index 39fed49a0..5b694dbab 100644 --- a/src/verilog/verilog_synthesis.cpp +++ b/src/verilog/verilog_synthesis.cpp @@ -342,8 +342,8 @@ exprt verilog_synthesist::expand_function_call( // Is it a 'system function call'? if(call.is_system_function_call()) { - auto identifier = to_symbol_expr(call.function()).get_identifier(); - if(identifier == "$ND") + auto base_name = to_verilog_identifier_expr(call.function()).base_name(); + if(base_name == "$ND") { std::string identifier = id2string(module) + "::nondet::" + std::to_string(nondet_count++); @@ -354,7 +354,7 @@ exprt verilog_synthesist::expand_function_call( select_one.set(ID_identifier, identifier); return select_one.with_source_location(call); } - else if(identifier == "$past") + else if(base_name == "$past") { auto what = call.arguments()[0]; auto ticks = call.arguments().size() < 2 @@ -363,8 +363,8 @@ exprt verilog_synthesist::expand_function_call( return verilog_past_exprt{what, ticks}.with_source_location(call); } else if( - identifier == "$stable" || identifier == "$rose" || - identifier == "$fell" || identifier == "$changed") + base_name == "$stable" || base_name == "$rose" || base_name == "$fell" || + base_name == "$changed") { DATA_INVARIANT(call.arguments().size() >= 1, "must have argument"); auto what = call.arguments()[0]; @@ -376,18 +376,18 @@ exprt verilog_synthesist::expand_function_call( std::move(expr), from_integer(0, integer_typet{})}; }; - if(identifier == "$stable") + if(base_name == "$stable") return equal_exprt{what, past}; - else if(identifier == "$changed") + else if(base_name == "$changed") return notequal_exprt{what, past}; - else if(identifier == "$rose") + else if(base_name == "$rose") return and_exprt{not_exprt{lsb(past)}, lsb(what)}; - else if(identifier == "$fell") + else if(base_name == "$fell") return and_exprt{lsb(past), not_exprt{lsb(what)}}; else DATA_INVARIANT(false, "all cases covered"); } - else if(identifier == "$countones") + else if(base_name == "$countones") { // lower to popcount DATA_INVARIANT( @@ -3094,21 +3094,15 @@ Function: verilog_synthesist::synth_function_call_or_task_enable void verilog_synthesist::synth_function_call_or_task_enable( const verilog_function_callt &statement) { - // this is essentially inlined - const symbol_exprt &function=to_symbol_expr(statement.function()); - - irep_idt identifier=function.get_identifier(); - - // We ignore everyting that starts with a '$', - // e.g., $display etc - - if(!identifier.empty() && identifier[0]=='$') + if(statement.is_system_function_call()) { - // ignore + // ignore system functions } else { - const symbolt &symbol=ns.lookup(identifier); + // this is essentially inlined + const symbol_exprt &function = to_symbol_expr(statement.function()); + const symbolt &symbol = ns.lookup(function); if(symbol.type.id()!=ID_code) { diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index 0ce66721a..9ed0218e3 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/src/verilog/verilog_typecheck_expr.cpp @@ -624,20 +624,20 @@ exprt verilog_typecheck_exprt::convert_expr_function_call( Forall_expr(it, arguments) convert_expr(*it); - + + // built-in functions + if(expr.is_system_function_call()) + return convert_system_function(expr); + if(expr.function().id()!=ID_symbol) { throw errort().with_location(expr.source_location()) << "expected symbol as function argument"; } - - // built-in functions + symbol_exprt &f_op=to_symbol_expr(expr.function()); - - const irep_idt &identifier=f_op.get_identifier(); - - if(expr.is_system_function_call()) - return convert_system_function(identifier, expr); + + const irep_idt &identifier = f_op.get_identifier(); std::string full_identifier= id2string(module_identifier)+"."+id2string(identifier); @@ -901,13 +901,13 @@ Function: verilog_typecheck_exprt::convert_system_function \*******************************************************************/ -exprt verilog_typecheck_exprt::convert_system_function( - const irep_idt &identifier, - function_call_exprt expr) +exprt verilog_typecheck_exprt::convert_system_function(function_call_exprt expr) { + auto base_name = to_verilog_identifier_expr(expr.function()).base_name(); + exprt::operandst &arguments=expr.arguments(); - if(identifier=="$signed") + if(base_name == "$signed") { // this is an explicit type cast if(arguments.size()!=1) @@ -942,7 +942,7 @@ exprt verilog_typecheck_exprt::convert_system_function( << to_string(argument.type()) << '\''; } } - else if(identifier=="$unsigned") + else if(base_name == "$unsigned") { // this is an explicit type cast if(arguments.size()!=1) @@ -977,7 +977,7 @@ exprt verilog_typecheck_exprt::convert_system_function( << to_string(argument.type()) << '\''; } } - else if(identifier=="$ND") + else if(base_name == "$ND") { // this is something from VIS @@ -991,13 +991,13 @@ exprt verilog_typecheck_exprt::convert_system_function( return std::move(expr); } else if( - identifier == "$bits" || identifier == "$left" || identifier == "$right" || - identifier == "$increment" || identifier == "$low" || identifier == "$high") + base_name == "$bits" || base_name == "$left" || base_name == "$right" || + base_name == "$increment" || base_name == "$low" || base_name == "$high") { if(arguments.size() != 1) { throw errort().with_location(expr.source_location()) - << identifier << " takes one argument"; + << base_name << " takes one argument"; } // The return type is integer. @@ -1005,7 +1005,7 @@ exprt verilog_typecheck_exprt::convert_system_function( return std::move(expr); } - else if(identifier == "$countones") // SystemVerilog + else if(base_name == "$countones") // SystemVerilog { if(arguments.size() != 1) { @@ -1018,7 +1018,7 @@ exprt verilog_typecheck_exprt::convert_system_function( return std::move(expr); } - else if(identifier=="$onehot") // SystemVerilog + else if(base_name == "$onehot") // SystemVerilog { if(arguments.size()!=1) { @@ -1032,7 +1032,7 @@ exprt verilog_typecheck_exprt::convert_system_function( return std::move(onehot); } - else if(identifier=="$onehot0") // SystemVerilog + else if(base_name == "$onehot0") // SystemVerilog { if(arguments.size()!=1) { @@ -1046,7 +1046,7 @@ exprt verilog_typecheck_exprt::convert_system_function( return std::move(onehot0); } - else if(identifier == "$clog2") // Verilog-2005 + else if(base_name == "$clog2") // Verilog-2005 { if(arguments.size() != 1) { @@ -1058,7 +1058,7 @@ exprt verilog_typecheck_exprt::convert_system_function( return std::move(expr); } - else if(identifier == "$isunknown") + else if(base_name == "$isunknown") { if(arguments.size() != 1) { @@ -1070,7 +1070,7 @@ exprt verilog_typecheck_exprt::convert_system_function( return std::move(expr); } - else if(identifier == "$past") + else if(base_name == "$past") { if(arguments.size() == 0 || arguments.size() >= 4) { @@ -1089,73 +1089,73 @@ exprt verilog_typecheck_exprt::convert_system_function( return std::move(expr); } else if( - identifier == "$stable" || identifier == "$rose" || identifier == "$fell" || - identifier == "$changed") + base_name == "$stable" || base_name == "$rose" || base_name == "$fell" || + base_name == "$changed") { if(arguments.size() != 1 && arguments.size() != 2) { throw errort().with_location(expr.source_location()) - << identifier << " takes one or two arguments"; + << base_name << " takes one or two arguments"; } expr.type() = bool_typet(); return std::move(expr); } - else if(identifier == "$rtoi") + else if(base_name == "$rtoi") { if(arguments.size() != 1) { throw errort().with_location(expr.source_location()) - << identifier << " takes one argument"; + << base_name << " takes one argument"; } expr.type() = verilog_integer_typet(); return std::move(expr); } - else if(identifier == "$itor") + else if(base_name == "$itor") { if(arguments.size() != 1) { throw errort().with_location(expr.source_location()) - << identifier << " takes one argument"; + << base_name << " takes one argument"; } expr.type() = verilog_real_typet(); return std::move(expr); } - else if(identifier == "$bitstoreal") + else if(base_name == "$bitstoreal") { if(arguments.size() != 1) { throw errort().with_location(expr.source_location()) - << identifier << " takes one argument"; + << base_name << " takes one argument"; } expr.type() = verilog_real_typet(); return std::move(expr); } - else if(identifier == "$bitstoshortreal") + else if(base_name == "$bitstoshortreal") { if(arguments.size() != 1) { throw errort().with_location(expr.source_location()) - << identifier << " takes one argument"; + << base_name << " takes one argument"; } expr.type() = verilog_shortreal_typet(); return std::move(expr); } - else if(identifier == "$realtobits") + else if(base_name == "$realtobits") { if(arguments.size() != 1) { throw errort().with_location(expr.source_location()) - << identifier << " takes one argument"; + << base_name << " takes one argument"; } arguments[0] = @@ -1165,12 +1165,12 @@ exprt verilog_typecheck_exprt::convert_system_function( return std::move(expr); } - else if(identifier == "$shortrealtobits") + else if(base_name == "$shortrealtobits") { if(arguments.size() != 1) { throw errort().with_location(expr.source_location()) - << identifier << " takes one argument"; + << base_name << " takes one argument"; } arguments[0] = @@ -1180,7 +1180,7 @@ exprt verilog_typecheck_exprt::convert_system_function( return std::move(expr); } - else if(identifier == "$typename") + else if(base_name == "$typename") { if(arguments.size() != 1) { @@ -1198,7 +1198,7 @@ exprt verilog_typecheck_exprt::convert_system_function( else { throw errort().with_location(expr.function().source_location()) - << "unknown system function `" << identifier << "'"; + << "unknown system function `" << base_name << "'"; } } @@ -1821,44 +1821,41 @@ exprt verilog_typecheck_exprt::elaborate_constant_system_function_call( // This performs constant-folding on a type-checked function // call expression according to Section 11.2.1 IEEE 1800-2017. auto &function = expr.function(); - if(function.id() != ID_symbol) - return std::move(expr); // give up - - auto &identifier = to_symbol_expr(function).get_identifier(); - + PRECONDITION(function.id() == ID_verilog_identifier); + auto &base_name = to_verilog_identifier_expr(function).base_name(); auto &arguments = expr.arguments(); - if(identifier == "$bits") + if(base_name == "$bits") { DATA_INVARIANT(arguments.size() == 1, "$bits has one argument"); return bits(arguments[0]); } - else if(identifier == "$low") + else if(base_name == "$low") { DATA_INVARIANT(arguments.size() == 1, "$low has one argument"); return low(arguments[0]); } - else if(identifier == "$high") + else if(base_name == "$high") { DATA_INVARIANT(arguments.size() == 1, "$high has one argument"); return high(arguments[0]); } - else if(identifier == "$left") + else if(base_name == "$left") { DATA_INVARIANT(arguments.size() == 1, "$left has one argument"); return left(arguments[0]); } - else if(identifier == "$right") + else if(base_name == "$right") { DATA_INVARIANT(arguments.size() == 1, "$right has one argument"); return right(arguments[0]); } - else if(identifier == "$increment") + else if(base_name == "$increment") { DATA_INVARIANT(arguments.size() == 1, "$increment has one argument"); return increment(arguments[0]); } - else if(identifier == "$countones") + else if(base_name == "$countones") { DATA_INVARIANT(arguments.size() == 1, "$countones has one argument"); @@ -1869,7 +1866,7 @@ exprt verilog_typecheck_exprt::elaborate_constant_system_function_call( return countones(to_constant_expr(op)); } - else if(identifier == "$clog2") + else if(base_name == "$clog2") { // the ceiling of the log with base 2 of the argument DATA_INVARIANT(arguments.size() == 1, "$clog2 has one argument"); @@ -1895,12 +1892,12 @@ exprt verilog_typecheck_exprt::elaborate_constant_system_function_call( return from_integer(result, integer_typet()); } } - else if(identifier == "$typename") + else if(base_name == "$typename") { DATA_INVARIANT(arguments.size() == 1, "$typename takes one argument"); return typename_string(arguments[0]); } - else if(identifier == "$isunknown") + else if(base_name == "$isunknown") { DATA_INVARIANT(arguments.size() == 1, "$isunknown takes one argument"); diff --git a/src/verilog/verilog_typecheck_expr.h b/src/verilog/verilog_typecheck_expr.h index 0050ef4a5..59612f619 100644 --- a/src/verilog/verilog_typecheck_expr.h +++ b/src/verilog/verilog_typecheck_expr.h @@ -185,8 +185,7 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset [[nodiscard]] exprt convert_trinary_expr(ternary_exprt); [[nodiscard]] exprt convert_expr_concatenation(concatenation_exprt); [[nodiscard]] exprt convert_expr_function_call(function_call_exprt); - [[nodiscard]] exprt - convert_system_function(const irep_idt &identifier, function_call_exprt); + [[nodiscard]] exprt convert_system_function(function_call_exprt); [[nodiscard]] exprt convert_bit_select_expr(binary_exprt); [[nodiscard]] exprt convert_replication_expr(replication_exprt); [[nodiscard]] exprt convert_power_expr(power_exprt);