diff --git a/regression/verilog/nets/implicit1.desc b/regression/verilog/nets/implicit1.desc index d562bf05..b6302add 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 f9049b70..caa69518 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 6fbc330a..6f4846bd 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 ebe99dfc..155fba94 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 2222bba7..4ca0dfde 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 00000000..472b0070 --- /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 00000000..ee4e8f08 --- /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 00000000..9b625d52 --- /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 00000000..5fd9553b --- /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 11f22585..5929d086 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 ead0dbf0..899255db 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 bca21c6f..41d9bb41 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 d7dd5e34..0f566e91 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 2688d4a1..21d101db 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 6b2e60d8..c3b526a3 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 6eda9f86..0cf91ee7 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 05a5bb2d..58970233 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 f8aaabec..03497cf6 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 3a4bb463..7d60155f 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);