VCD output: scoped reference names

This implements scoped reference names for $var sections in VCD output,
as defined in 1800-2017.

The --random-trace flow now accepts "-" as filename for VCD output, to
enable checking the VCD output in tests.

regression/ebmc/traces/vcd1.desc

@@ -0,0 +1,25 @@
+CORE
+vcd1.v
+--random-trace --trace-steps 1 --vcd -
+^\$date$
+^\$timescale$
+^  1ns$
+^\$scope module Verilog::main \$end$
+^  \$var wire 32 main\.some_input some_input \[31:0\] \$end$
+^  \$var wire 32 main\.x x \[31:0\] \$end$
+^  \$scope module sub \$end$
+^    \$var wire 32 main\.sub\.x x \[31:0\] \$end$
+^  \$upscope \$end$
+^\$upscope \$end$
+^\$enddefinitions \$end$
+^#0$
+^b\d+ main\.some_input$
+^b\d+ main\.x$
+^b00000000000000000000000001111011 main\.sub\.x$
+^#1$
+^b\d+ main\.some_input$
+^b\d+ main\.x$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/ebmc/traces/vcd1.v

@@ -0,0 +1,13 @@
+module main(input [31:0] some_input);
+
+  wire [31:0] x = 456 + some_input;
+
+  sub sub();
+
+endmodule
+
+module sub;
+
+  wire [31:0] x = 123;
+
+endmodule

src/ebmc/random_traces.cpp

@@ -27,6 +27,7 @@ Author: Daniel Kroening, [email protected]
 #include "waveform.h"
 
 #include <algorithm>
+#include <iostream>
 #include <random>
 
 /*******************************************************************\
@@ -159,6 +160,9 @@ int random_traces(const cmdlinet &cmdline, message_handlert &message_handler)
       return 10; // default
   }();
 
+  if(cmdline.isset("vcd") && cmdline.get_value("vcd") == "-")
+    throw ebmc_errort() << "no stdout output for multiple VCDs";
+
   const auto outfile_prefix = [&cmdline]() -> std::optional<std::string> {
     if(cmdline.isset("vcd"))
       return cmdline.get_value("vcd") + ".";
@@ -285,6 +289,27 @@ int random_trace(const cmdlinet &cmdline, message_handlert &message_handler)
       messaget message(message_handler);
       show_trans_trace_numbered(trace, message, ns, consolet::out());
     }
+    else if(cmdline.isset("vcd"))
+    {
+      auto filename = cmdline.get_value("vcd");
+      messaget message(message_handler);
+
+      if(filename == "-")
+      {
+        show_trans_trace_vcd(trace, message, ns, std::cout);
+      }
+      else
+      {
+        std::ofstream out(widen_if_needed(filename));
+
+        if(!out)
+          throw ebmc_errort() << "failed to write trace to " << filename;
+
+        consolet::out() << "*** Writing " << filename << '\n';
+
+        show_trans_trace_vcd(trace, message, ns, out);
+      }
+    }
     else // default
     {
       messaget message(message_handler);

src/trans-netlist/trans_trace.cpp

@@ -522,7 +522,29 @@ std::string vcd_identifier(const std::string &id)
     result.erase(0, 9);
   else if(has_prefix(result, "smv::"))
     result.erase(0, 5);
-
+
+  return result;
+}
+
+/*******************************************************************\
+
+Function: vcd_reference
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+std::string vcd_reference(const symbolt &symbol, const std::string &prefix)
+{
+  std::string result = id2string(symbol.name);
+
+  if(!prefix.empty() && has_prefix(result, prefix))
+    result.erase(0, prefix.size());
+
   return result;
 }
 
@@ -723,13 +745,10 @@ void vcd_hierarchy_rec(
     std::string suffix=vcd_suffix(symbol.type, ns);
 
     if(width>=1)
-      out << std::string(depth*2, ' ')
-          << "$var " << signal_class << " "
-          << width << " "
-          << vcd_identifier(display_name) << " " 
-          << vcd_identifier(display_name)
-          << (suffix==""?"":" ") << suffix
-          << " $end" << '\n';
+      out << std::string(depth * 2, ' ') << "$var " << signal_class << " "
+          << width << " " << vcd_identifier(display_name) << " "
+          << vcd_reference(symbol, prefix) << (suffix == "" ? "" : " ")
+          << suffix << " $end" << '\n';
   }
 
   // now do sub modules
@@ -777,12 +796,6 @@ void show_trans_trace_vcd(
 
   assert(!state.assignments.empty());
 
-  const symbolt &symbol1=ns.lookup(
-    state.assignments.front().lhs.get(ID_identifier));
-
-  std::string module_name=id2string(symbol1.module);
-  out << "$scope module " << vcd_identifier(module_name) << " $end\n";
-
   // get identifiers
   std::set<irep_idt> ids;
 
@@ -791,10 +804,21 @@ void show_trans_trace_vcd(
     assert(a.lhs.id()==ID_symbol);
     ids.insert(to_symbol_expr(a.lhs).get_identifier());
   }
-
+
+  // determine module
+
+  const symbolt &symbol1 =
+    ns.lookup(state.assignments.front().lhs.get(ID_identifier));
+
+  auto &module_symbol = ns.lookup(symbol1.module);
+
+  // print those in the top module
+
+  out << "$scope module " << vcd_reference(module_symbol, "") << " $end\n";
+
   // split up into hierarchy
-  vcd_hierarchy_rec(ns, ids, module_name+".", out, 1);
-  
+  vcd_hierarchy_rec(ns, ids, id2string(module_symbol.name) + ".", out, 1);
+
   out << "$upscope $end\n";  
 
   out << "$enddefinitions $end\n";