diff --git a/CHANGELOG b/CHANGELOG index d71c5b82e..b137b209d 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: ref module port direction * 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/ref1.desc b/regression/verilog/modules/ref1.desc new file mode 100644 index 000000000..52e3beb57 --- /dev/null +++ b/regression/verilog/modules/ref1.desc @@ -0,0 +1,7 @@ +CORE +ref1.sv + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/verilog/modules/ref1.sv b/regression/verilog/modules/ref1.sv new file mode 100644 index 000000000..f35bac51f --- /dev/null +++ b/regression/verilog/modules/ref1.sv @@ -0,0 +1,9 @@ +module M(ref [31:0] some_ref); + initial some_ref = 123; +endmodule + +module main; + bit [31:0] some_var; + M m(some_var); + assert final (some_var == 123); +endmodule diff --git a/src/ebmc/output_verilog.cpp b/src/ebmc/output_verilog.cpp index 3ce5a0dd1..f3e1894f6 100644 --- a/src/ebmc/output_verilog.cpp +++ b/src/ebmc/output_verilog.cpp @@ -16,6 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include "output_verilog.h" @@ -585,17 +586,17 @@ void output_verilog_baset::module_header(const symbolt &symbol) { out << "module " << symbol.base_name; - const irept &ports=symbol.type.find(ID_ports); - + const auto &ports = to_module_type(symbol.type).ports(); + // // print port in module statement // - if(!ports.get_sub().empty()) + if(!ports.empty()) { out << '('; bool first = true; - for(auto &port : ports.get_sub()) + for(auto &port : ports) { if(first) first = false; @@ -615,10 +616,10 @@ void output_verilog_baset::module_header(const symbolt &symbol) // // port declarations // - for(auto &port : ports.get_sub()) + for(auto &port : ports) { - bool is_input = port.get_bool(ID_input); - bool is_output = port.get_bool(ID_output); + bool is_input = port.input(); + bool is_output = port.output(); out << " "; @@ -629,7 +630,7 @@ void output_verilog_baset::module_header(const symbolt &symbol) else out << "output"; - const typet &type = static_cast(port.find(ID_type)); + const typet &type = port.type(); if(type.id()==ID_named_block) continue; diff --git a/src/ebmc/transition_system.cpp b/src/ebmc/transition_system.cpp index 1aca22783..1157912fb 100644 --- a/src/ebmc/transition_system.cpp +++ b/src/ebmc/transition_system.cpp @@ -22,6 +22,7 @@ Author: Daniel Kroening, dkr@amazon.com #include #include #include +#include #include "ebmc_error.h" #include "ebmc_version.h" @@ -424,17 +425,14 @@ std::vector transition_systemt::inputs() const DATA_INVARIANT( module_symbol.type.id() == ID_module, "main_symbol must be module"); - const auto &ports_irep = module_symbol.type.find(ID_ports); - // filter out the inputs - auto &ports = static_cast(ports_irep).operands(); + auto &ports = to_module_type(module_symbol.type).ports(); for(auto &port : ports) { DATA_INVARIANT(port.id() == ID_symbol, "port must be a symbol"); - if(port.get_bool(ID_input) && !port.get_bool(ID_output)) + if(port.input() && !port.output()) { - symbol_exprt input_symbol( - to_symbol_expr(port).get_identifier(), port.type()); + symbol_exprt input_symbol(port.identifier(), port.type()); input_symbol.add_source_location() = port.source_location(); inputs.push_back(std::move(input_symbol)); } diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index 3d9fe3aea..0dc8b8301 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -107,6 +107,7 @@ IREP_ID_ONE(module_instance) IREP_ID_TWO(C_const, #const) IREP_ID_TWO(C_offset, #offset) IREP_ID_TWO(C_increasing, #increasing) +IREP_ID_ONE(direction) IREP_ID_ONE(ports) IREP_ID_ONE(inst) IREP_ID_ONE(Verilog) diff --git a/src/verilog/verilog_elaborate.cpp b/src/verilog/verilog_elaborate.cpp index d26214121..8df68d742 100644 --- a/src/verilog/verilog_elaborate.cpp +++ b/src/verilog/verilog_elaborate.cpp @@ -56,6 +56,14 @@ void verilog_typecheckt::collect_port_symbols(const verilog_declt &decl) new_symbol.is_input = true; new_symbol.is_output = true; } + else if(port_class == ID_verilog_ref) + { + new_symbol.is_input = false; + new_symbol.is_output = false; + new_symbol.is_state_var = true; + } + else + DATA_INVARIANT(false, "unexpected port class"); new_symbol.module = module_identifier; new_symbol.value.make_nil(); diff --git a/src/verilog/verilog_interfaces.cpp b/src/verilog/verilog_interfaces.cpp index e4871c79e..535832ecb 100644 --- a/src/verilog/verilog_interfaces.cpp +++ b/src/verilog/verilog_interfaces.cpp @@ -92,17 +92,24 @@ void verilog_typecheckt::check_module_ports( << "port `" << base_name << "' not declared"; } - if(!port_symbol->is_input && !port_symbol->is_output) + irep_idt direction = decl.get_class(); + + if(direction.empty()) { - throw errort().with_location(declarator.source_location()) - << "port `" << base_name << "' not declared as input or output"; + if(!port_symbol->is_input && !port_symbol->is_output) + { + throw errort().with_location(declarator.source_location()) + << "port `" << base_name << "' not declared as input or output"; + } + else if(port_symbol->is_input && !port_symbol->is_output) + direction = ID_input; + else if(!port_symbol->is_input && port_symbol->is_output) + direction = ID_output; + else + direction = ID_inout; } - ports.emplace_back( - identifier, - port_symbol->type, - port_symbol->is_input, - port_symbol->is_output); + ports.emplace_back(identifier, port_symbol->type, direction); ports.back().set("#name", base_name); ports.back().set(ID_C_source_location, declarator.source_location()); diff --git a/src/verilog/verilog_typecheck.cpp b/src/verilog/verilog_typecheck.cpp index 13695e907..6023fa1cc 100644 --- a/src/verilog/verilog_typecheck.cpp +++ b/src/verilog/verilog_typecheck.cpp @@ -43,10 +43,13 @@ void verilog_typecheckt::typecheck_port_connection( { const symbolt &symbol = ns.lookup(port.identifier()); - if(!symbol.is_input && !symbol.is_output) + if(port.direction() != ID_verilog_ref) { - throw errort().with_location(op.source_location()) - << "port `" << symbol.name << "' is neither input nor output"; + if(!symbol.is_input && !symbol.is_output) + { + throw errort().with_location(op.source_location()) + << "port `" << symbol.name << "' is neither input nor output"; + } } if(op.is_nil()) diff --git a/src/verilog/verilog_types.h b/src/verilog/verilog_types.h index 71424d7bb..08940b284 100644 --- a/src/verilog/verilog_types.h +++ b/src/verilog/verilog_types.h @@ -145,13 +145,12 @@ class module_typet:public typet class portt : public irept { public: - portt(irep_idt _identifier, typet _type, bool _input, bool _output) + portt(irep_idt _identifier, typet _type, irep_idt _direction) : irept(ID_symbol) { - type() = std::move(_type); identifier(_identifier); - input(_input); - output(_output); + type() = std::move(_type); + direction(_direction); } typet &type() @@ -174,24 +173,34 @@ class module_typet:public typet set(ID_identifier, _identifier); } - bool output() const + irep_idt direction() const { - return get_bool(ID_output); + return get(ID_direction); } - void output(bool _output) + void direction(irep_idt _direction) { - set(ID_output, _output); + set(ID_direction, _direction); + } + + bool output() const + { + return direction() == ID_output || direction() == ID_inout; } bool input() const { - return get_bool(ID_input); + return direction() == ID_input || direction() == ID_inout; } - void input(bool _input) + bool ref() const + { + return direction() == ID_verilog_ref; + } + + const source_locationt &source_location() const { - set(ID_input, _input); + return (const source_locationt &)find(ID_C_source_location); } };