Verilog: ref port direction

SystemVerilog adds the ref port direction, usable for passing a reference to
a variable to a module.

Author: kroening

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

regression/verilog/modules/ref1.desc

@@ -0,0 +1,7 @@
+CORE
+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,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();

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_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())

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);