diff --git a/CHANGELOG b/CHANGELOG index d71c5b82e..696faa7d6 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -7,6 +7,7 @@ * Verilog: $isunknown * SystemVerilog: fix for #-# and #=# for empty matches * SystemVerilog: fix for |-> and |=> for empty matches +* SystemVerilog: support 1800-2005 .* wildcard port connections * LTL/SVA to Buechi with --buechi * SMV: abs, bool, count, max, min, toint, word1 * BMC: new encoding for F, avoiding spurious traces diff --git a/regression/verilog/modules/wildcard_port_connection1.desc b/regression/verilog/modules/wildcard_port_connection1.desc new file mode 100644 index 000000000..1eff0fc8d --- /dev/null +++ b/regression/verilog/modules/wildcard_port_connection1.desc @@ -0,0 +1,7 @@ +CORE +wildcard_port_connection1.sv + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/verilog/modules/wildcard_port_connection1.sv b/regression/verilog/modules/wildcard_port_connection1.sv new file mode 100644 index 000000000..27f1947ae --- /dev/null +++ b/regression/verilog/modules/wildcard_port_connection1.sv @@ -0,0 +1,9 @@ +module M(input a, b); + assert final (a); + assert final (!b); +endmodule + +module main; + wire a = 0, b = 1; + M m(.*); +endmodule diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index 3d9fe3aea..472a5e7b4 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -214,7 +214,8 @@ IREP_ID_ONE(verilog_always) IREP_ID_ONE(verilog_always_comb) IREP_ID_ONE(verilog_always_ff) IREP_ID_ONE(verilog_always_latch) -IREP_ID_ONE(named_port_connection) +IREP_ID_ONE(verilog_named_port_connection) +IREP_ID_ONE(verilog_wildcard_port_connection) IREP_ID_ONE(verilog_final) IREP_ID_ONE(initial) IREP_ID_ONE(verilog_label_statement) diff --git a/src/verilog/parser.y b/src/verilog/parser.y index 41cc2f670..ff007822b 100644 --- a/src/verilog/parser.y +++ b/src/verilog/parser.y @@ -405,6 +405,7 @@ int yyverilogerror(const char *error) %token TOK_LSQPLUS "[+" %token TOK_LSQEQUAL "[=" %token TOK_LSQMINUSGREATER "[->" +%token TOK_DOTASTERIC ".*" /* System Verilog Keywords */ %token TOK_ACCEPT_ON "accept_on" @@ -3100,9 +3101,10 @@ named_port_connection_brace: named_port_connection: '.' port_identifier '(' expression_opt ')' - { init($$, ID_named_port_connection); + { init($$, ID_verilog_named_port_connection); mto($$, $2); mto($$, $4); } + | ".*" { init($$, ID_verilog_wildcard_port_connection); } ; // System Verilog standard 1800-2017 @@ -3736,6 +3738,26 @@ open_value_range: value_range; // System Verilog standard 1800-2017 // A.6.7.1 Patterns +pattern: + "." variable_identifier + | ".*" + | constant_expression + | "tagged" member_identifier + | "tagged" member_identifier pattern + | "'{" pattern_list "}" + | "'{" member_pattern_list "}" + ; + +pattern_list: + pattern + | pattern_list "," pattern + ; + +member_pattern_list: + member_identifier ":" pattern + | member_pattern_list "," member_identifier ":" pattern + ; + assignment_pattern: '\'' '{' expression_brace '}' { init($$, ID_verilog_assignment_pattern); swapop($$, $3); } diff --git a/src/verilog/scanner.l b/src/verilog/scanner.l index 14baae647..0dce0842a 100644 --- a/src/verilog/scanner.l +++ b/src/verilog/scanner.l @@ -273,6 +273,8 @@ void verilog_scanner_init() "[+" { SYSTEM_VERILOG_OPERATOR(TOK_LSQPLUS, "[+"); } "[=" { SYSTEM_VERILOG_OPERATOR(TOK_LSQEQUAL, "[="); } "[->" { SYSTEM_VERILOG_OPERATOR(TOK_LSQMINUSGREATER, "[->"); } + /* port connections, patterns */ +".*" { SYSTEM_VERILOG_OPERATOR(TOK_DOTASTERIC, ".*"); } /* Verilog 1364-1995 keywords */ diff --git a/src/verilog/verilog_expr.h b/src/verilog/verilog_expr.h index 02fb0964d..cbfb01b6a 100644 --- a/src/verilog/verilog_expr.h +++ b/src/verilog/verilog_expr.h @@ -799,7 +799,7 @@ class verilog_inst_baset : public verilog_module_itemt named_port_connectiont(exprt _port, exprt _value) : binary_exprt( std::move(_port), - ID_named_port_connection, + ID_verilog_named_port_connection, std::move(_value), typet{}) { @@ -854,6 +854,19 @@ class verilog_inst_baset : public verilog_module_itemt return operands(); } + bool positional_port_connections() const + { + return !named_port_connections(); + } + + bool named_port_connections() const + { + auto &connections = this->connections(); + return connections.empty() || + (connections.front().id() == ID_verilog_named_port_connection || + connections.front().id() == ID_verilog_wildcard_port_connection); + } + protected: using exprt::operands; }; @@ -877,7 +890,7 @@ class verilog_inst_baset : public verilog_module_itemt inline const verilog_inst_baset::named_port_connectiont & to_verilog_named_port_connection(const exprt &expr) { - PRECONDITION(expr.id() == ID_named_port_connection); + PRECONDITION(expr.id() == ID_verilog_named_port_connection); verilog_inst_baset::named_port_connectiont::check(expr); return static_cast(expr); } @@ -885,7 +898,7 @@ to_verilog_named_port_connection(const exprt &expr) inline verilog_inst_baset::named_port_connectiont & to_verilog_named_port_connection(exprt &expr) { - PRECONDITION(expr.id() == ID_named_port_connection); + PRECONDITION(expr.id() == ID_verilog_named_port_connection); verilog_inst_baset::named_port_connectiont::check(expr); return static_cast(expr); } diff --git a/src/verilog/verilog_synthesis.cpp b/src/verilog/verilog_synthesis.cpp index 61416ae2d..23378937d 100644 --- a/src/verilog/verilog_synthesis.cpp +++ b/src/verilog/verilog_synthesis.cpp @@ -1419,7 +1419,7 @@ void verilog_synthesist::instantiate_ports( // named port connection? - if(inst.connections().front().id() == ID_named_port_connection) + if(inst.named_port_connections()) { const irept::subt &ports = symbol.type.find(ID_ports).get_sub(); diff --git a/src/verilog/verilog_typecheck.cpp b/src/verilog/verilog_typecheck.cpp index 904ccc6a3..61f7288fe 100644 --- a/src/verilog/verilog_typecheck.cpp +++ b/src/verilog/verilog_typecheck.cpp @@ -110,17 +110,32 @@ void verilog_typecheckt::typecheck_port_connections( } // named port connection? - if( - inst.connections().empty() || - inst.connections().front().id() == ID_named_port_connection) + if(inst.named_port_connections()) { // We don't require that all ports are connected. std::set assigned_ports; + bool wildcard = false; for(auto &connection : inst.connections()) { - if(connection.id() != ID_named_port_connection) + if(connection.id() == ID_verilog_wildcard_port_connection) + { + // .* + if(wildcard) + { + // .* can only be given once + throw errort{}.with_location(connection.source_location()) + << "wildcard connection given more than once"; + } + else + { + wildcard = true; + continue; + } + } + + if(connection.id() != ID_verilog_named_port_connection) { throw errort().with_location(inst.source_location()) << "expected a named port connection"; @@ -167,7 +182,7 @@ void verilog_typecheckt::typecheck_port_connections( assigned_ports.insert(identifier); } } - else // just a list without names + else // Positional connections, i.e., just a list without port names { if(inst.connections().size() != ports.size()) {