Verilog: register-transfer level IR layer

src/ebmc/ebmc_parse_options.cpp

@@ -578,6 +578,7 @@ void ebmc_parse_optionst::help()
     " {y--show-parse}                \t show parse trees\n"
     " {y--show-modules}              \t show a list of the modules\n"
     " {y--show-module-hierarchy}     \t show the hierarchy of module instantiations\n"
+    " {y--show-rtl}                  \t show the register-transfer level representation\n"
     " {y--show-varmap}               \t show variable map\n"
     " {y--show-netlist}              \t show netlist\n"
     " {y--aiger}                     \t output netlist in AIGER format\n"

src/ebmc/ebmc_parse_options.h

@@ -26,6 +26,7 @@ class ebmc_parse_optionst:public parse_options_baset
         "(diatest)(statebits):(bound):(max-bound):"
         "(show-parse)(show-varmap)(show-symbol-table)(show-netlist)"
         "(show-ldg)(show-modules)(show-module-hierarchy)"
+        "(show-rtl)"
         "(show-trans)(show-bdds)(show-formula)"
         "(show-traces)"
         "(modules-xml):"

src/verilog/Makefile

@@ -24,6 +24,7 @@ SRC = aval_bval_encoding.cpp \
       verilog_preprocessor.cpp \
       verilog_preprocessor_lex.yy.cpp \
       verilog_preprocessor_tokenizer.cpp \
+      verilog_rtl.cpp \
       verilog_scope.cpp \
       verilog_simplifier.cpp \
       verilog_standard.cpp \

src/verilog/verilog_ebmc_language.cpp

@@ -28,6 +28,7 @@ Author: Daniel Kroening, dkr@amazon.com
 #include "verilog_lowering.h"
 #include "verilog_parser.h"
 #include "verilog_preprocessor.h"
+#include "verilog_rtl.h"
 #include "verilog_synthesis.h"
 #include "verilog_typecheck.h"
 #include "verilog_types.h"
@@ -186,6 +187,22 @@ void verilog_ebmc_languaget::typecheck_module(
     throw ebmc_errort{}.with_exit_code(2);
   }
 
+  // The RTL representation follows type checking and
+  // precedes synthesis.
+  if(cmdline.isset("show-rtl"))
+  {
+    auto rtl = verilog_rtl(
+      symbol_table,
+      module.identifier,
+      module.parse_tree.standard,
+      message_handler);
+
+    const namespacet ns(symbol_table);
+    rtl.output(ns, std::cout);
+
+    return; // no synthesis
+  }
+
   messaget message(message_handler);
   log.status() << "Synthesis " << module.identifier << messaget::eom;
 
@@ -638,6 +655,10 @@ std::optional<transition_systemt> verilog_ebmc_languaget::transition_system()
   auto transition_system =
     typecheck(parse_trees, top_level_modules, std::move(symbol_table));
 
+  // --show-rtl is handled between type checking and synthesis
+  if(cmdline.isset("show-rtl"))
+    return {};
+
   // Create the $root module instance and synthesize it
   create_root_module(
     top_level_modules, parse_trees.front().standard, transition_system);