From 06c409ae0183df3b7cb859eb4cc2d90c44bbb377 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 17 Apr 2026 09:37:18 -0700 Subject: [PATCH] Verilog: multiple top-level modules This extends the Verilog language to support multiple top-level modules, following SystemVerilog 1800-2017 23.3.1. --- src/verilog/verilog_ebmc_language.cpp | 114 +++++++++++++++++--------- src/verilog/verilog_ebmc_language.h | 10 ++- 2 files changed, 79 insertions(+), 45 deletions(-) diff --git a/src/verilog/verilog_ebmc_language.cpp b/src/verilog/verilog_ebmc_language.cpp index d06013680..7dc9a6f5f 100644 --- a/src/verilog/verilog_ebmc_language.cpp +++ b/src/verilog/verilog_ebmc_language.cpp @@ -180,7 +180,7 @@ void verilog_ebmc_languaget::typecheck_module( transition_systemt verilog_ebmc_languaget::typecheck( const parse_treest &parse_trees, - irep_idt top_level_module, + const std::vector top_level_modules, symbol_tablet &&symbol_table) { std::map module_map; @@ -198,13 +198,17 @@ transition_systemt verilog_ebmc_languaget::typecheck( } } - // now type check the top-level module - auto m_it = module_map.find(verilog_module_symbol(top_level_module)); - CHECK_RETURN(m_it != module_map.end()); - + // now type check the given top-level modules transition_systemt transition_system; transition_system.symbol_table = std::move(symbol_table); - typecheck_module(m_it->second, transition_system.symbol_table); + + for(auto top_level_module : top_level_modules) + { + auto m_it = module_map.find(verilog_module_symbol(top_level_module)); + CHECK_RETURN(m_it != module_map.end()); + + typecheck_module(m_it->second, transition_system.symbol_table); + } return transition_system; } @@ -244,8 +248,10 @@ static void module_dependencies( module_dependencies_rec(item, action); } -irep_idt -verilog_ebmc_languaget::top_level_module(const parse_treest &parse_trees) const +/// Determine the set of top-level modules following 1800 2017 23.3.1, +/// given via their base names. Sorted alphabetically. +std::vector +verilog_ebmc_languaget::top_level_modules(const parse_treest &parse_trees) const { // start with a set of all modules, from all the files std::set all_modules; @@ -260,29 +266,47 @@ verilog_ebmc_languaget::top_level_module(const parse_treest &parse_trees) const } } - // Did the user specify one? - irep_idt given_module; + // Did the user specify a set of top level modules? + std::vector given_modules; if(cmdline.isset("module")) - given_module = cmdline.get_value("module"); + { + for(auto &value : cmdline.get_values("module")) + given_modules.push_back(value); + } else if(cmdline.isset("top")) - given_module = cmdline.get_value("top"); + { + for(auto &value : cmdline.get_values("top")) + given_modules.push_back(value); + } - if(given_module != irep_idt{}) + if(!given_modules.empty()) { - if(all_modules.find(given_module) == all_modules.end()) + // first check that all the given modules exist + for(const auto &given_module : given_modules) { - messaget log{message_handler}; - log.error() << "module '" << given_module << "' not found" - << messaget::eom; - throw ebmc_errort{}.with_exit_code(2); + if(all_modules.find(given_module) == all_modules.end()) + { + messaget log{message_handler}; + log.error() << "module '" << given_module << "' not found" + << messaget::eom; + throw ebmc_errort{}.with_exit_code(2); + } } - else - return given_module; // done + + // now sort alphabetically + std::sort( + given_modules.begin(), + given_modules.end(), + [](const irep_idt &a, const irep_idt &b) + { return id2string(a) < id2string(b); }); + + return given_modules; // done } - // start with all modules, and then erase the ones that are - // used as a dependency + // No modules given. Find all modules that are not used + // as a submodule. Start with all modules, and then erase + // the ones that are used as a submodule. std::set top_level_modules = all_modules; for(auto &parse_tree : parse_trees) @@ -304,33 +328,41 @@ verilog_ebmc_languaget::top_level_module(const parse_treest &parse_trees) const log.error() << "no module found" << messaget::eom; throw ebmc_errort{}.with_exit_code(1); } - else if(top_level_modules.size() >= 2) - { - // sorted alphabetically - std::set modules; - for(const auto &base_name : top_level_modules) - modules.insert(id2string(base_name)); + // sort alphabetically into a vector + std::vector result; + for(auto &module : top_level_modules) + result.push_back(module); + + std::sort( + result.begin(), + result.end(), + [](const irep_idt &a, const irep_idt &b) + { return id2string(a) < id2string(b); }); + + return result; // done +} + +static bool get_main( + const std::vector top_level_modules, + message_handlert &message_handler, + transition_systemt &transition_system) +{ + if(top_level_modules.size() >= 2) + { messaget log{message_handler}; log.error() << "multiple modules found, please select one:\n"; - for(const auto &module : modules) + for(const auto &module : top_level_modules) log.error() << " " << module << '\n'; log.error() << messaget::eom; throw ebmc_errort{}.with_exit_code(1); } - // we have exactly one top-level module - return *top_level_modules.begin(); -} + auto top_level_module = top_level_modules.front(); -static bool get_main( - irep_idt top_level_module, - message_handlert &message_handler, - transition_systemt &transition_system) -{ try { auto identifier = verilog_module_symbol(top_level_module); @@ -448,9 +480,9 @@ std::optional verilog_ebmc_languaget::transition_system() symbol_tablet symbol_table = elaborate_compilation_units(parse_trees); // - // determine the top-level module + // determine the top-level modules // - auto top_level_module = this->top_level_module(parse_trees); + auto top_level_modules = this->top_level_modules(parse_trees); // // type checking @@ -459,7 +491,7 @@ std::optional verilog_ebmc_languaget::transition_system() message.status() << "Converting" << messaget::eom; auto transition_system = - typecheck(parse_trees, top_level_module, std::move(symbol_table)); + typecheck(parse_trees, top_level_modules, std::move(symbol_table)); if(cmdline.isset("show-symbol-table")) { @@ -467,7 +499,7 @@ std::optional verilog_ebmc_languaget::transition_system() return {}; } - if(get_main(top_level_module, message_handler, transition_system)) + if(get_main(top_level_modules, message_handler, transition_system)) throw ebmc_errort{}.with_exit_code(1); if(cmdline.isset("show-module-hierarchy")) diff --git a/src/verilog/verilog_ebmc_language.h b/src/verilog/verilog_ebmc_language.h index 1f3822d35..bfeacff3c 100644 --- a/src/verilog/verilog_ebmc_language.h +++ b/src/verilog/verilog_ebmc_language.h @@ -51,8 +51,8 @@ class verilog_ebmc_languaget : public ebmc_languaget void copy_parse_tree(const parse_treet &, symbol_tablet &); - // base_name of the top-level module - irep_idt top_level_module(const parse_treest &) const; + // base_names of the top-level modules, alphabetical order + std::vector top_level_modules(const parse_treest &) const; class modulet { @@ -66,8 +66,10 @@ class verilog_ebmc_languaget : public ebmc_languaget }; symbol_tablet elaborate_compilation_units(const parse_treest &); - transition_systemt - typecheck(const parse_treest &, irep_idt top_level_module, symbol_tablet &&); + transition_systemt typecheck( + const parse_treest &, + const std::vector top_level_modules, + symbol_tablet &&); void typecheck_module(modulet &, symbol_tablet &); };