Verilog: elaborate starting from top-level module

Author: kroening

regression/verilog/modules/module_not_found1.desc

@@ -1,7 +1,7 @@
 CORE
 module_not_found1.v
 --bound 1 --top main
-^found no file that provides module Verilog::some_module_that_does_not_exist$
+^file .* line 3: module not found$
 ^EXIT=2$
 ^SIGNAL=0$
 --

src/verilog/verilog_ebmc_language.cpp

@@ -150,6 +150,7 @@ void verilog_ebmc_languaget::typecheck_module(
 
   module.in_progress = true;
 
+#if 0
   // first get dependencies of current module
   const auto dependency_set = module.parse_tree.dependencies(module.identifier);
 
@@ -169,6 +170,7 @@ void verilog_ebmc_languaget::typecheck_module(
 
     typecheck_module(dependency_it->second, symbol_table);
   }
+#endif
 
   // type check the module
   log.status() << "Type-checking " << module.identifier << messaget::eom;
@@ -208,8 +210,11 @@ void verilog_ebmc_languaget::typecheck_module(
   module.in_progress = false;
 }
 
+#include <iostream>
+
 transition_systemt verilog_ebmc_languaget::typecheck(
   const parse_treest &parse_trees,
+  irep_idt top_level_module,
   symbol_tablet &&symbol_table)
 {
   // set up the module map
@@ -230,9 +235,12 @@ transition_systemt verilog_ebmc_languaget::typecheck(
 
   transition_system.symbol_table = std::move(symbol_table);
 
-  for(auto &[_, module] : module_map)
+  for(auto &[id, module] : module_map)
   {
-    typecheck_module(module, transition_system.symbol_table);
+    if(id == verilog_module_symbol(top_level_module))
+    {
+      typecheck_module(module, transition_system.symbol_table);
+    }
   }
 
   return transition_system;
@@ -486,25 +494,25 @@ std::optional<transition_systemt> verilog_ebmc_languaget::transition_system()
   for(auto &parse_tree : parse_trees)
     copy_parse_tree(parse_tree, symbol_table);
 
+  //
+  // determine the top-level module
+  //
+  auto top_level_module = this->top_level_module(parse_trees);
+
   //
   // type checking
   //
 
   message.status() << "Converting" << messaget::eom;
 
-  auto transition_system = typecheck(parse_trees, std::move(symbol_table));
+  auto transition_system = typecheck(parse_trees, top_level_module, std::move(symbol_table));
 
   if(cmdline.isset("show-symbol-table"))
   {
     std::cout << transition_system.symbol_table;
     return {};
   }
 
-  //
-  // determine the top-level module
-  //
-  auto top_level_module = this->top_level_module(parse_trees);
-
   if(get_main(top_level_module, message_handler, transition_system))
     throw ebmc_errort{}.with_exit_code(1);
 

src/verilog/verilog_ebmc_language.h

@@ -67,7 +67,7 @@ class verilog_ebmc_languaget : public ebmc_languaget
 
   std::map<irep_idt, modulet> module_map;
 
-  transition_systemt typecheck(const parse_treest &, symbol_tablet &&);
+  transition_systemt typecheck(const parse_treest &, irep_idt top_level_module, symbol_tablet &&);
   void typecheck_module(modulet &, symbol_tablet &);
 };