Verilog: ref port type

Author: kroening

regression/verilog/modules/ref1.desc

@@ -0,0 +1,7 @@
+KNOWNBUG
+ref1.sv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

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

src/verilog/verilog_elaborate.cpp

@@ -56,6 +56,13 @@ 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;
+    }
+    else
+      DATA_INVARIANT(false, "unexpected port class");
 
     new_symbol.module = module_identifier;
     new_symbol.value.make_nil();

src/verilog/verilog_interfaces.cpp

@@ -92,13 +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, decl.get_class());
+    ports.emplace_back(identifier, port_symbol->type, direction);
 
     ports.back().set("#name", base_name);
     ports.back().set(ID_C_source_location, declarator.source_location());

src/verilog/verilog_types.h

@@ -193,6 +193,11 @@ class module_typet:public typet
       return direction() == ID_input || direction() == ID_inout;
     }
 
+    bool ref() const
+    {
+      return direction() == ID_verilog_ref;
+    }
+
     const source_locationt &source_location() const
     {
       return (const source_locationt &)find(ID_C_source_location);