From c6d15d0e57cfded62d435896f69279d041ca2ef8 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 3 Oct 2024 18:23:53 -0700 Subject: [PATCH] Verilog: set type of implicit nets 1800 2017 6.10 allows implicit declarations of nets. The type of these nets is to be derived from the LHS of the assignment or the type of the port connection. The warning when a net is declared implicitly is dropped by default; it can be reactivated with --warn-implicit-nets. --- regression/verilog/nets/implicit1.desc | 2 +- regression/verilog/nets/implicit2.desc | 5 +- regression/verilog/nets/implicit3.desc | 2 +- regression/verilog/nets/implicit4.desc | 5 +- regression/verilog/nets/implicit5.desc | 8 ++-- regression/verilog/nets/implicit6.desc | 8 ++++ regression/verilog/nets/implicit6.sv | 10 ++++ regression/verilog/nets/implicit7.desc | 9 ++++ regression/verilog/nets/implicit7.sv | 16 +++++++ src/ebmc/ebmc_parse_options.h | 3 +- src/ebmc/transition_system.cpp | 2 + src/verilog/verilog_language.cpp | 4 +- src/verilog/verilog_language.h | 1 + src/verilog/verilog_parameterize_module.cpp | 2 +- src/verilog/verilog_synthesis.cpp | 2 +- src/verilog/verilog_typecheck.cpp | 51 +++++++++++++++++---- src/verilog/verilog_typecheck.h | 15 ++++-- src/verilog/verilog_typecheck_expr.cpp | 36 +++++++++------ src/verilog/verilog_typecheck_expr.h | 22 ++++++--- 19 files changed, 155 insertions(+), 48 deletions(-) create mode 100644 regression/verilog/nets/implicit6.desc create mode 100644 regression/verilog/nets/implicit6.sv create mode 100644 regression/verilog/nets/implicit7.desc create mode 100644 regression/verilog/nets/implicit7.sv diff --git a/regression/verilog/nets/implicit1.desc b/regression/verilog/nets/implicit1.desc index d562bf059..b6302adda 100644 --- a/regression/verilog/nets/implicit1.desc +++ b/regression/verilog/nets/implicit1.desc @@ -1,6 +1,6 @@ CORE implicit1.sv ---bound 0 +--bound 0 --warn-implicit-nets ^file .* line 4: implicit wire main\.O$ ^file .* line 4: implicit wire main\.A$ ^file .* line 4: implicit wire main\.B$ diff --git a/regression/verilog/nets/implicit2.desc b/regression/verilog/nets/implicit2.desc index f9049b703..caa69518e 100644 --- a/regression/verilog/nets/implicit2.desc +++ b/regression/verilog/nets/implicit2.desc @@ -1,9 +1,8 @@ -KNOWNBUG +CORE implicit2.sv ---bound 0 +--bound 0 --warn-implicit-nets ^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring -- -The width of the implicit net is set incorrectly. diff --git a/regression/verilog/nets/implicit3.desc b/regression/verilog/nets/implicit3.desc index 6fbc330aa..6f4846bd0 100644 --- a/regression/verilog/nets/implicit3.desc +++ b/regression/verilog/nets/implicit3.desc @@ -1,6 +1,6 @@ CORE implicit3.sv ---bound 0 +--bound 0 --warn-implicit-nets ^file .* line 6: implicit wire main\.O$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/verilog/nets/implicit4.desc b/regression/verilog/nets/implicit4.desc index ebe99dfc7..155fba94d 100644 --- a/regression/verilog/nets/implicit4.desc +++ b/regression/verilog/nets/implicit4.desc @@ -1,9 +1,8 @@ -KNOWNBUG +CORE implicit4.sv ---bound 0 +--bound 0 --warn-implicit-nets ^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring -- -The width of the implicit net is set incorrectly. diff --git a/regression/verilog/nets/implicit5.desc b/regression/verilog/nets/implicit5.desc index 2222bba7b..4ca0dfde3 100644 --- a/regression/verilog/nets/implicit5.desc +++ b/regression/verilog/nets/implicit5.desc @@ -1,9 +1,9 @@ -KNOWNBUG +CORE implicit5.sv ---bound 0 -^EXIT=0$ +--bound 0 --warn-implicit-nets +^file .* line 4: unknown identifier A$ +^EXIT=2$ ^SIGNAL=0$ -- ^warning: ignoring -- -This case should be errored. diff --git a/regression/verilog/nets/implicit6.desc b/regression/verilog/nets/implicit6.desc new file mode 100644 index 000000000..472b00703 --- /dev/null +++ b/regression/verilog/nets/implicit6.desc @@ -0,0 +1,8 @@ +CORE +implicit6.sv +--bound 0 --warn-implicit-nets +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/verilog/nets/implicit6.sv b/regression/verilog/nets/implicit6.sv new file mode 100644 index 000000000..ee4e8f086 --- /dev/null +++ b/regression/verilog/nets/implicit6.sv @@ -0,0 +1,10 @@ +module main; + + parameter P = 2; + + // implicit nets are allowed in the port connection list of a module + and [P:0] (O, A, B); + + assert final ($bits(O) == P+1); + +endmodule diff --git a/regression/verilog/nets/implicit7.desc b/regression/verilog/nets/implicit7.desc new file mode 100644 index 000000000..9b625d528 --- /dev/null +++ b/regression/verilog/nets/implicit7.desc @@ -0,0 +1,9 @@ +KNOWNBUG +implicit7.sv +--bound 0 --warn-implicit-nets +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +The implicit net is not known yet when evaluating parameters. diff --git a/regression/verilog/nets/implicit7.sv b/regression/verilog/nets/implicit7.sv new file mode 100644 index 000000000..5fd9553b8 --- /dev/null +++ b/regression/verilog/nets/implicit7.sv @@ -0,0 +1,16 @@ +module main; + + parameter P = 10; + + // implicit nets are allowed in the port connection list of a module + sub #(P) my_sub(x); + + // The type of the implict net could be used to define another parameter + parameter Q = $bits(x); + + assert final (Q == P + 1); + +endmodule + +module sub #(parameter P = 1)(input [P:0] some_input); +endmodule diff --git a/src/ebmc/ebmc_parse_options.h b/src/ebmc/ebmc_parse_options.h index 11f22585d..5929d0866 100644 --- a/src/ebmc/ebmc_parse_options.h +++ b/src/ebmc/ebmc_parse_options.h @@ -47,7 +47,8 @@ class ebmc_parse_optionst:public parse_options_baset "(random-traces)(trace-steps):(random-seed):(traces):" "(random-trace)(random-waveform)" "(liveness-to-safety)" - "I:D:(preprocess)(systemverilog)(vl2smv-extensions)", + "I:D:(preprocess)(systemverilog)(vl2smv-extensions)" + "(warn-implicit-nets)", argc, argv, std::string("EBMC ") + EBMC_VERSION), diff --git a/src/ebmc/transition_system.cpp b/src/ebmc/transition_system.cpp index ead0dbf09..899255db3 100644 --- a/src/ebmc/transition_system.cpp +++ b/src/ebmc/transition_system.cpp @@ -112,6 +112,7 @@ int preprocess(const cmdlinet &cmdline, message_handlert &message_handler) optionst options; options.set_option("force-systemverilog", cmdline.isset("systemverilog")); options.set_option("vl2smv-extensions", cmdline.isset("vl2smv-extensions")); + options.set_option("warn-implicit-nets", cmdline.isset("warn-implicit-nets")); // do -D if(cmdline.isset('D')) @@ -163,6 +164,7 @@ static bool parse( optionst options; options.set_option("force-systemverilog", cmdline.isset("systemverilog")); options.set_option("vl2smv-extensions", cmdline.isset("vl2smv-extensions")); + options.set_option("warn-implicit-nets", cmdline.isset("warn-implicit-nets")); // do -D if(cmdline.isset('D')) diff --git a/src/verilog/verilog_language.cpp b/src/verilog/verilog_language.cpp index bca21c6fc..41d9bb418 100644 --- a/src/verilog/verilog_language.cpp +++ b/src/verilog/verilog_language.cpp @@ -37,6 +37,7 @@ void verilog_languaget::set_language_options( force_systemverilog = options.get_bool_option("force-systemverilog"); vl2smv_extensions = options.get_bool_option("vl2smv-extensions"); initial_defines = options.get_list_option("defines"); + warn_implicit_nets = options.get_bool_option("warn-implicit-nets"); } /*******************************************************************\ @@ -180,7 +181,8 @@ bool verilog_languaget::typecheck( { if(module=="") return false; - if(verilog_typecheck(parse_tree, symbol_table, module, message_handler)) + if(verilog_typecheck( + parse_tree, symbol_table, module, warn_implicit_nets, message_handler)) return true; messaget message(message_handler); diff --git a/src/verilog/verilog_language.h b/src/verilog/verilog_language.h index d7dd5e349..0f566e91e 100644 --- a/src/verilog/verilog_language.h +++ b/src/verilog/verilog_language.h @@ -93,6 +93,7 @@ class verilog_languaget:public languaget protected: bool force_systemverilog = false; bool vl2smv_extensions = false; + bool warn_implicit_nets = false; std::list initial_defines; verilog_parse_treet parse_tree; }; diff --git a/src/verilog/verilog_parameterize_module.cpp b/src/verilog/verilog_parameterize_module.cpp index 2688d4a1b..21d101db1 100644 --- a/src/verilog/verilog_parameterize_module.cpp +++ b/src/verilog/verilog_parameterize_module.cpp @@ -289,7 +289,7 @@ irep_idt verilog_typecheckt::parameterize_module( // recursive call verilog_typecheckt verilog_typecheck( - standard, *new_symbol, symbol_table, get_message_handler()); + standard, false, *new_symbol, symbol_table, get_message_handler()); if(verilog_typecheck.typecheck_main()) throw 0; diff --git a/src/verilog/verilog_synthesis.cpp b/src/verilog/verilog_synthesis.cpp index 6b2e60d86..c3b526a39 100644 --- a/src/verilog/verilog_synthesis.cpp +++ b/src/verilog/verilog_synthesis.cpp @@ -663,7 +663,7 @@ exprt verilog_synthesist::expand_function_call( { // Attempt to constant fold. verilog_typecheck_exprt verilog_typecheck_expr( - standard, ns, get_message_handler()); + standard, false, ns, get_message_handler()); auto result = verilog_typecheck_expr.elaborate_constant_system_function_call(call); if(!result.is_constant()) diff --git a/src/verilog/verilog_typecheck.cpp b/src/verilog/verilog_typecheck.cpp index 6eda9f867..0cf91ee7c 100644 --- a/src/verilog/verilog_typecheck.cpp +++ b/src/verilog/verilog_typecheck.cpp @@ -56,8 +56,17 @@ void verilog_typecheckt::typecheck_port_connection( } else { - convert_expr(op); - + // IEEE 1800 2017 6.10 allows implicit declarations of nets when + // used in a port connection. + if(op.id() == ID_symbol) + { + op = convert_symbol(to_symbol_expr(op), port.type()); + } + else + { + convert_expr(op); + } + if(symbol.is_output) check_lhs(op, A_CONTINUOUS); else @@ -229,7 +238,17 @@ void verilog_typecheckt::typecheck_builtin_port_connections( for(auto &connection : inst.connections()) { - convert_expr(connection); + // IEEE 1800 2017 6.10 allows implicit declarations of nets when + // used in a port connection. + if(connection.id() == ID_symbol) + { + connection = convert_symbol(to_symbol_expr(connection), type); + } + else + { + convert_expr(connection); + } + propagate_type(connection, type); } } @@ -821,8 +840,16 @@ void verilog_typecheckt::convert_continuous_assign( exprt &lhs = to_binary_expr(*it).lhs(); exprt &rhs = to_binary_expr(*it).rhs(); - convert_expr(lhs); + // IEEE 1800 2017 6.10 allows implicit declarations of nets when + // used as the LHS of a continuous assignment. The type is derived + // from the RHS, and hence, we convert that first. convert_expr(rhs); + + if(lhs.id() == ID_symbol) + lhs = convert_symbol(to_symbol_expr(lhs), rhs.type()); + else + convert_expr(lhs); + propagate_type(rhs, lhs.type()); check_lhs(lhs, A_CONTINUOUS); @@ -1761,7 +1788,8 @@ Function: verilog_typecheckt::implicit_wire bool verilog_typecheckt::implicit_wire( const irep_idt &identifier, - const symbolt *&symbol_ptr) + const symbolt *&symbol_ptr, + const typet &net_type) { std::string full_identifier= id2string(module_identifier)+"."+id2string(identifier); @@ -1773,7 +1801,7 @@ bool verilog_typecheckt::implicit_wire( symbol.value.make_nil(); symbol.base_name=identifier; symbol.name=full_identifier; - symbol.type=bool_typet(); // TODO: other types? + symbol.type = net_type; symbol.pretty_name=strip_verilog_prefix(full_identifier); symbolt *new_symbol; @@ -1836,6 +1864,7 @@ bool verilog_typecheck( const verilog_parse_treet &parse_tree, symbol_table_baset &symbol_table, const std::string &module, + bool warn_implicit_nets, message_handlert &message_handler) { verilog_parse_treet::module_mapt::const_iterator it= @@ -1851,7 +1880,11 @@ bool verilog_typecheck( } return verilog_typecheck( - symbol_table, *it->second, parse_tree.standard, message_handler); + symbol_table, + *it->second, + parse_tree.standard, + warn_implicit_nets, + message_handler); } /*******************************************************************\ @@ -1870,6 +1903,7 @@ bool verilog_typecheck( symbol_table_baset &symbol_table, const verilog_module_sourcet &verilog_module_source, verilog_standardt standard, + bool warn_implicit_nets, message_handlert &message_handler) { // create symbol @@ -1898,6 +1932,7 @@ bool verilog_typecheck( } verilog_typecheckt verilog_typecheck( - standard, *new_symbol, symbol_table, message_handler); + standard, warn_implicit_nets, *new_symbol, symbol_table, message_handler); + return verilog_typecheck.typecheck_main(); } diff --git a/src/verilog/verilog_typecheck.h b/src/verilog/verilog_typecheck.h index 05a5bb2d2..589702338 100644 --- a/src/verilog/verilog_typecheck.h +++ b/src/verilog/verilog_typecheck.h @@ -23,12 +23,14 @@ bool verilog_typecheck( const verilog_parse_treet &parse_tree, symbol_table_baset &, const std::string &module, + bool warn_implicit_nets, message_handlert &message_handler); bool verilog_typecheck( symbol_table_baset &, const verilog_module_sourcet &verilog_module_source, verilog_standardt, + bool warn_implicit_nets, message_handlert &message_handler); bool verilog_typecheck( @@ -57,10 +59,15 @@ class verilog_typecheckt: public: verilog_typecheckt( verilog_standardt _standard, + bool warn_implicit_nets, symbolt &_module_symbol, symbol_table_baset &_symbol_table, message_handlert &_message_handler) - : verilog_typecheck_exprt(_standard, ns, _message_handler), + : verilog_typecheck_exprt( + _standard, + warn_implicit_nets, + ns, + _message_handler), verilog_symbol_tablet(_symbol_table), ns(_symbol_table), module_symbol(_module_symbol), @@ -204,8 +211,10 @@ class verilog_typecheckt: virtual void convert_statements(verilog_module_exprt &); // to be overridden - bool implicit_wire(const irep_idt &identifier, - const symbolt *&symbol) override; + bool implicit_wire( + const irep_idt &identifier, + const symbolt *&, + const typet &) override; // generate constructs void elaborate_generate_assign( diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index f8aaabec5..03497cf69 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/src/verilog/verilog_typecheck_expr.cpp @@ -893,7 +893,7 @@ exprt verilog_typecheck_exprt::convert_nullary_expr(nullary_exprt expr) } else if(expr.id()==ID_symbol) { - return convert_symbol(to_symbol_expr(std::move(expr))); + return convert_symbol(to_symbol_expr(std::move(expr)), {}); } else if(expr.id()==ID_verilog_star_event) { @@ -931,7 +931,9 @@ Function: verilog_typecheck_exprt::convert_symbol \*******************************************************************/ -exprt verilog_typecheck_exprt::convert_symbol(symbol_exprt expr) +exprt verilog_typecheck_exprt::convert_symbol( + symbol_exprt expr, + const std::optional &implicit_net_type) { const irep_idt &identifier = expr.get_identifier(); @@ -1018,19 +1020,25 @@ exprt verilog_typecheck_exprt::convert_symbol(symbol_exprt expr) return std::move(expr); } } - else if(!implicit_wire(identifier, symbol)) - { - // this should become an error - warning().source_location=expr.source_location(); - warning() << "implicit wire " << symbol->display_name() << eom; - expr.type()=symbol->type; - expr.set_identifier(symbol->name); - return std::move(expr); - } else { - throw errort().with_location(expr.source_location()) - << "unknown identifier " << identifier; + if(implicit_net_type.has_value()) + { + implicit_wire(identifier, symbol, implicit_net_type.value()); + if(warn_implicit_nets) + { + warning().source_location = expr.source_location(); + warning() << "implicit wire " << symbol->display_name() << eom; + } + expr.type() = symbol->type; + expr.set_identifier(symbol->name); + return std::move(expr); + } + else + { + throw errort().with_location(expr.source_location()) + << "unknown identifier " << identifier; + } } } @@ -3259,7 +3267,7 @@ bool verilog_typecheck( message_handler.get_message_count(messaget::M_ERROR); verilog_typecheck_exprt verilog_typecheck_expr( - standard, ns, module_identifier, message_handler); + standard, true, ns, module_identifier, message_handler); try { diff --git a/src/verilog/verilog_typecheck_expr.h b/src/verilog/verilog_typecheck_expr.h index 3a4bb463d..7d60155f8 100644 --- a/src/verilog/verilog_typecheck_expr.h +++ b/src/verilog/verilog_typecheck_expr.h @@ -26,18 +26,22 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset public: verilog_typecheck_exprt( verilog_standardt _standard, + bool _warn_implicit_nets, const namespacet &_ns, message_handlert &_message_handler) - : verilog_typecheck_baset(_standard, _ns, _message_handler) + : verilog_typecheck_baset(_standard, _ns, _message_handler), + warn_implicit_nets(_warn_implicit_nets) { } verilog_typecheck_exprt( verilog_standardt _standard, + bool _warn_implicit_nets, const namespacet &_ns, const std::string &_module_identifier, message_handlert &_message_handler) : verilog_typecheck_baset(_standard, _ns, _message_handler), - module_identifier(_module_identifier) + module_identifier(_module_identifier), + warn_implicit_nets(_warn_implicit_nets) { } virtual void convert_expr(exprt &expr) @@ -126,11 +130,14 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset PRECONDITION(false); } - virtual bool implicit_wire(const irep_idt &identifier, - const symbolt *&symbol) { + bool warn_implicit_nets = false; + + virtual bool + implicit_wire(const irep_idt &identifier, const symbolt *&, const typet &) + { return true; } - + void typecheck() override { } @@ -156,10 +163,11 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset UNREACHABLE; } -private: +protected: [[nodiscard]] exprt convert_expr_rec(exprt expr); [[nodiscard]] exprt convert_constant(constant_exprt); - [[nodiscard]] exprt convert_symbol(symbol_exprt); + [[nodiscard]] exprt + convert_symbol(symbol_exprt, const std::optional &implicit_net_type); [[nodiscard]] exprt convert_hierarchical_identifier(class hierarchical_identifier_exprt); [[nodiscard]] exprt convert_nullary_expr(nullary_exprt);