diff --git a/regression/verilog/modules/interconnect1.desc b/regression/verilog/modules/interconnect1.desc index 65e4f27d2..8f5f9a52c 100644 --- a/regression/verilog/modules/interconnect1.desc +++ b/regression/verilog/modules/interconnect1.desc @@ -1,8 +1,8 @@ -KNOWNBUG +CORE interconnect1.sv -^EXIT=0$ +^file .* line 2: no support for interconnect nets$ +^EXIT=2$ ^SIGNAL=0$ -- -- -interconnect is not implemented. diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index fcfca60c2..d75254fff 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -123,6 +123,7 @@ IREP_ID_ONE(verilog_associative_array) IREP_ID_ONE(verilog_declarations) IREP_ID_ONE(verilog_default_clocking) IREP_ID_ONE(verilog_default_disable) +IREP_ID_ONE(verilog_interconnect) IREP_ID_ONE(verilog_lifetime) IREP_ID_ONE(verilog_logical_equality) IREP_ID_ONE(verilog_logical_inequality) diff --git a/src/verilog/parser.y b/src/verilog/parser.y index 6e550094c..e2343f7e0 100644 --- a/src/verilog/parser.y +++ b/src/verilog/parser.y @@ -1521,6 +1521,10 @@ net_declaration: addswap($$, ID_class, $1); addswap($$, ID_type, $4); swapop($$, $6); } + | TOK_INTERCONNECT delay3_opt list_of_net_decl_assignments ';' + { init($$, ID_decl); + stack_expr($$).set(ID_class, ID_verilog_interconnect); + swapop($$, $3); } ; // Note that the identifier that is defined using the typedef may be @@ -1790,14 +1794,19 @@ net_type_opt: | net_type ; -net_port_type: net_type_opt signing_opt packed_dimension_brace - { - // The net type is a subtype of the signing. - add_as_subtype(stack_type($2), stack_type($1)); - // That becomes a subtype of the packed dimension. - add_as_subtype(stack_type($3), stack_type($2)); - $$ = $3; - } +net_port_type: + net_type_opt signing_opt packed_dimension_brace + { + // The net type is a subtype of the signing. + add_as_subtype(stack_type($2), stack_type($1)); + // That becomes a subtype of the packed dimension. + add_as_subtype(stack_type($3), stack_type($2)); + $$ = $3; + } + | TOK_INTERCONNECT + { + init($$, ID_verilog_interconnect); + } ; variable_port_type: var_data_type ; diff --git a/src/verilog/verilog_elaborate.cpp b/src/verilog/verilog_elaborate.cpp index 41633f528..69ccd8b6a 100644 --- a/src/verilog/verilog_elaborate.cpp +++ b/src/verilog/verilog_elaborate.cpp @@ -492,8 +492,14 @@ void verilog_typecheckt::collect_symbols(const verilog_declt &decl) symbols_added.push_back(symbol.name); } } - else if(decl_class == ID_reg || decl_class == ID_var) + else if( + decl_class == ID_reg || decl_class == ID_var || + decl_class == ID_verilog_interconnect) { + if(decl_class == ID_verilog_interconnect) + throw errort().with_location(decl.source_location()) + << "no support for interconnect nets"; + symbolt symbol; symbol.mode = mode;