Verilog: create $root module instance

Create a $root module instance that contains an instance of the
top-level module, per IEEE 1800-2017. The $root module is synthesized
via verilog_synthesis, which expands the top-level module into $root's
namespace. The main_symbol now points to $root.

The $root module's type is copied from the top-level module (including
ports), and its module field is set to the instance identifier for
expression resolution (used by -p, --reset, etc.).

Pretty names and expression output strip the $root prefix since it is
implicit in SystemVerilog.

Author: kroening

regression/ebmc/netlist/netlist-output1.desc

@@ -3,10 +3,10 @@ netlist-output1.v
 --show-netlist
 activate-multi-line-match
 ^Variable map:
-  Verilog::main\.clk=0->false \(input\)
-  Verilog::main\.data=1->false \(input\)
-  Verilog::main\.some_register=2->!3 \(latch\)
-  Verilog::main\.some_register_aux0=!3->false \(wire\)
+  Verilog::\$root.main\.clk=0->false \(input\)
+  Verilog::\$root.main\.data=1->false \(input\)
+  Verilog::\$root.main\.some_register=2->!3 \(latch\)
+  Verilog::\$root.main\.some_register_aux0=!3->false \(wire\)
 
 Total no. of variable bits: 3
 Total no. of latch bits: 1
@@ -15,10 +15,10 @@ Total no. of input bits: 2
 Total no. of output bits: 0
 
 Next state functions:
-  NEXT\(Verilog::main\.some_register\)=!\(!\(Verilog::main\.data\) & !\(Verilog::main\.some_register\)\)
+  NEXT\(Verilog::\$root.main\.some_register\)=!\(!\(Verilog::\$root.main\.data\) & !\(Verilog::\$root.main\.some_register\)\)
 
 Initial state: 
-  !\(Verilog::main\.some_register\)
+  !\(Verilog::\$root.main\.some_register\)
 
 State invariant constraints: 
 

regression/ebmc/smv-netlist/array_assignment.desc

@@ -1,8 +1,8 @@
 CORE
 array_assignment.sv
 --reset rst --smv-netlist --simple-netlist
-^ASSIGN next\(Verilog\.main\.data\[0\]\):=nondet\[1\];$
-^ASSIGN next\(Verilog\.main\.data\[1\]\):=nondet\[2\];$
+^ASSIGN next\(Verilog\.\$36\$root\.main\.data\[0\]\):=nondet\[1\];$
+^ASSIGN next\(Verilog\.\$36\$root\.main\.data\[1\]\):=nondet\[2\];$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/ebmc/smv-netlist/verilog1.desc

@@ -2,12 +2,12 @@ CORE
 verilog1.sv
 --smv-netlist
 ^MODULE main$
-^VAR Verilog\.main\.x: boolean;$
-^ASSIGN next\(Verilog\.main\.x\):=\!Verilog\.main\.x;$
-^INIT !Verilog\.main\.x$
-^-- Verilog::main.assert.1$
-^LTLSPEC G F Verilog\.main\.x$
-^-- Verilog::main.assert.2$
+^VAR Verilog\.\$36\$root\.main\.x: boolean;$
+^ASSIGN next\(Verilog\.\$36\$root\.main\.x\):=\!Verilog\.\$36\$root\.main\.x;$
+^INIT !Verilog\.\$36\$root\.main\.x$
+^-- Verilog::\$root\.main\.assert\.1$
+^LTLSPEC G F Verilog\.\$36\$root\.main\.x$
+^-- Verilog::\$root\.main\.assert\.2$
 ^-- not translated$
 ^EXIT=0$
 ^SIGNAL=0$

regression/ebmc/traces/json1.desc

@@ -1,7 +1,7 @@
 CORE
 json1.v
 --bound 10 --json-result -
-^      "identifier": "Verilog::main\.property\.p1",$
+^      "identifier": "Verilog::\$root\.main\.property\.p1",$
 ^      "status": "REFUTED",$
 ^      "trace": \{$
 ^        "states": \[ \[$

regression/smv/smv-netlist/smv_netlist1.desc

@@ -1,10 +1,10 @@
 CORE
 smv_netlist1.v
 --smv-netlist
-^VAR Verilog\.main\.my-bit: boolean;$
-^VAR Verilog\.main\.clk: boolean;$
-^ASSIGN next\(Verilog\.main\.my-bit\):=!Verilog\.main\.my-bit;$
-^INIT !Verilog\.main\.my-bit$
+^VAR Verilog\.\$36\$root\.main\.my-bit: boolean;$
+^VAR Verilog\.\$36\$root\.main\.clk: boolean;$
+^ASSIGN next\(Verilog\.\$36\$root\.main\.my-bit\):=!Verilog\.\$36\$root\.main\.my-bit;$
+^INIT !Verilog\.\$36\$root\.main\.my-bit$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/modules/show-module-hierarchy1.desc

@@ -1,13 +1,14 @@
 CORE
 show-module-hierarchy1.v
 --show-module-hierarchy
-^main:$
-^  inner main\.inner_instance1$
-^    leaf1 main\.inner_instance1\.leaf1_instance$
-^    leaf2 main\.inner_instance1\.leaf2_instance$
-^  inner main\.inner_instance2$
-^    leaf1 main\.inner_instance2\.leaf1_instance$
-^    leaf2 main\.inner_instance2\.leaf2_instance$
+^\$root:$
+^  main main$
+^    inner main\.inner_instance1$
+^      leaf1 main\.inner_instance1\.leaf1_instance$
+^      leaf2 main\.inner_instance1\.leaf2_instance$
+^    inner main\.inner_instance2$
+^      leaf1 main\.inner_instance2\.leaf1_instance$
+^      leaf2 main\.inner_instance2\.leaf2_instance$
 ^EXIT=0$
 ^SIGNAL=0$
 --

src/ebmc/instrument_past.cpp

@@ -97,7 +97,7 @@ model_past(const past_sett &past_set, transition_systemt &transition_system)
         symbolt symbol{
           identifier, past_expr.type(), transition_system.main_symbol->mode};
         symbol.is_state_var = true;
-        symbol.module = transition_system.main_symbol->module;
+        symbol.module = transition_system.main_symbol->name;
         transition_system.symbol_table.add(std::move(symbol));
       }
 

src/ebmc/live_signal.cpp

@@ -23,7 +23,7 @@ void set_live_signal(transition_systemt &transition_system, exprt property)
     symbolt live_symbol{
       identifier, bool_typet(), transition_system.main_symbol->mode};
 
-    live_symbol.module = transition_system.main_symbol->module;
+    live_symbol.module = transition_system.main_symbol->name;
     live_symbol.base_name = "live";
 
     const auto symbol_expr = live_symbol.symbol_expr();

src/ebmc/liveness_to_safety.cpp

@@ -170,7 +170,7 @@ void liveness_to_safetyt::operator()()
       transition_system.main_symbol->mode};
 
     save_symbol.is_input = true;
-    save_symbol.module = transition_system.main_symbol->module;
+    save_symbol.module = transition_system.main_symbol->name;
     save_symbol.base_name = "save";
 
     auto result = transition_system.symbol_table.insert(std::move(save_symbol));
@@ -185,7 +185,7 @@ void liveness_to_safetyt::operator()()
       transition_system.main_symbol->mode};
 
     saved_symbol.is_state_var = true;
-    saved_symbol.module = transition_system.main_symbol->module;
+    saved_symbol.module = transition_system.main_symbol->name;
     saved_symbol.base_name = "saved";
 
     auto result =
@@ -223,7 +223,7 @@ void liveness_to_safetyt::operator()()
       transition_system.main_symbol->mode};
 
     looped_symbol.is_state_var = false;
-    looped_symbol.module = transition_system.main_symbol->module;
+    looped_symbol.module = transition_system.main_symbol->name;
 
     auto result =
       transition_system.symbol_table.insert(std::move(looped_symbol));
@@ -278,7 +278,7 @@ void liveness_to_safetyt::translate_GFp(propertyt &property)
       transition_system.main_symbol->mode};
 
     live_symbol.is_state_var = true;
-    live_symbol.module = transition_system.main_symbol->module;
+    live_symbol.module = transition_system.main_symbol->name;
 
     auto result = transition_system.symbol_table.insert(std::move(live_symbol));
     CHECK_RETURN(result.second);

src/trans-netlist/trans_trace.cpp

@@ -817,14 +817,17 @@ void show_trans_trace_vcd(
 
   auto &module_symbol = ns.lookup(symbol1.module);
 
-  // print those in the top module
-
-  out << "$scope module " << module_symbol.display_name() << " $end\n";
-
-  // split up into hierarchy
-  vcd_hierarchy_rec(ns, ids, id2string(module_symbol.name) + ".", out, 1);
-
-  out << "$upscope $end\n";  
+  // print those in the top module -- skip $root scope in VCD output
+  if(module_symbol.base_name == "$root")
+  {
+    vcd_hierarchy_rec(ns, ids, id2string(module_symbol.name) + ".", out, 0);
+  }
+  else
+  {
+    out << "$scope module " << module_symbol.display_name() << " $end\n";
+    vcd_hierarchy_rec(ns, ids, id2string(module_symbol.name) + ".", out, 1);
+    out << "$upscope $end\n";
+  }  
 
   out << "$enddefinitions $end\n";