add hierarchy -smtcheck

like -simcheck, but allow smtlib2_module modules.

diff --git a/manual/command-reference-manual.tex b/manual/command-reference-manual.tex
index edc8af6e69a3eab4b86962dc2355c888f566aef5..3a9259867762dc203871aadf0ea777968f615f6c 100644 (file)
--- a/manual/command-reference-manual.tex
+++ b/manual/command-reference-manual.tex
@@ -2379,6 +2379,9 @@ resolves positional module parameters, unrolls array instances, and more.
         like -check, but also throw an error if blackbox modules are
         instantiated, and throw an error if the design has no top module.
 
+    -smtcheck
+        like -simcheck, but allow smtlib2_module modules.
+
     -purge_lib
         by default the hierarchy command will not remove library (blackbox)
         modules. use this option to also remove unused blackbox modules.

diff --git a/passes/hierarchy/hierarchy.cc b/passes/hierarchy/hierarchy.cc
index d40d6e59ff7ef921226b58a4df2e00e965e970b2..d27fddf1cf8830d7a8fb026ff4029aa1761b3f63 100644 (file)
--- a/passes/hierarchy/hierarchy.cc
+++ b/passes/hierarchy/hierarchy.cc
@@ -439,7 +439,8 @@ void check_cell_connections(const RTLIL::Module &module, RTLIL::Cell &cell, RTLI
        }
 }
 
-bool expand_module(RTLIL::Design *design, RTLIL::Module *module, bool flag_check, bool flag_simcheck, std::vector<std::string> &libdirs)
+bool expand_module(RTLIL::Design *design, RTLIL::Module *module, bool flag_check, bool flag_simcheck, bool flag_smtcheck,
+                  std::vector<std::string> &libdirs)
 {
        bool did_something = false;
        std::map<RTLIL::Cell*, std::pair<int, int>> array_cells;
@@ -477,7 +478,7 @@ bool expand_module(RTLIL::Design *design, RTLIL::Module *module, bool flag_check
                RTLIL::Module *mod = design->module(cell->type);
                if (!mod)
                {
-                       mod = get_module(*design, *cell, *module, flag_check || flag_simcheck, libdirs);
+                       mod = get_module(*design, *cell, *module, flag_check || flag_simcheck || flag_smtcheck, libdirs);
 
                        // If we still don't have a module, treat the cell as a black box and skip
                        // it. Otherwise, we either loaded or derived something so should set the
@@ -495,11 +496,11 @@ bool expand_module(RTLIL::Design *design, RTLIL::Module *module, bool flag_check
                // interfaces.
                if_expander.visit_connections(*cell, *mod);
 
-               if (flag_check || flag_simcheck)
+               if (flag_check || flag_simcheck || flag_smtcheck)
                        check_cell_connections(*module, *cell, *mod);
 
                if (mod->get_blackbox_attribute()) {
-                       if (flag_simcheck)
+                       if (flag_simcheck || (flag_smtcheck && !mod->get_bool_attribute(ID::smtlib2_module)))
                                log_error("Module `%s' referenced in module `%s' in cell `%s' is a blackbox/whitebox module.\n",
                                                cell->type.c_str(), module->name.c_str(), cell->name.c_str());
                        continue;
@@ -737,6 +738,9 @@ struct HierarchyPass : public Pass {
                log("        like -check, but also throw an error if blackbox modules are\n");
                log("        instantiated, and throw an error if the design has no top module.\n");
                log("\n");
+               log("    -smtcheck\n");
+               log("        like -simcheck, but allow smtlib2_module modules.\n");
+               log("\n");
                log("    -purge_lib\n");
                log("        by default the hierarchy command will not remove library (blackbox)\n");
                log("        modules. use this option to also remove unused blackbox modules.\n");
@@ -803,6 +807,7 @@ struct HierarchyPass : public Pass {
 
                bool flag_check = false;
                bool flag_simcheck = false;
+               bool flag_smtcheck = false;
                bool purge_lib = false;
                RTLIL::Module *top_mod = NULL;
                std::string load_top_mod;
@@ -821,7 +826,7 @@ struct HierarchyPass : public Pass {
                size_t argidx;
                for (argidx = 1; argidx < args.size(); argidx++)
                {
-                       if (args[argidx] == "-generate" && !flag_check && !flag_simcheck && !top_mod) {
+                       if (args[argidx] == "-generate" && !flag_check && !flag_simcheck && !flag_smtcheck && !top_mod) {
                                generate_mode = true;
                                log("Entering generate mode.\n");
                                while (++argidx < args.size()) {
@@ -868,6 +873,10 @@ struct HierarchyPass : public Pass {
                                flag_simcheck = true;
                                continue;
                        }
+                       if (args[argidx] == "-smtcheck") {
+                               flag_smtcheck = true;
+                               continue;
+                       }
                        if (args[argidx] == "-purge_lib") {
                                purge_lib = true;
                                continue;
@@ -1013,7 +1022,7 @@ struct HierarchyPass : public Pass {
                        }
                }
 
-               if (flag_simcheck && top_mod == nullptr)
+               if ((flag_simcheck || flag_smtcheck) && top_mod == nullptr)
                        log_error("Design has no top module.\n");
 
                if (top_mod != NULL) {
@@ -1039,7 +1048,7 @@ struct HierarchyPass : public Pass {
                        }
 
                        for (auto module : used_modules) {
-                               if (expand_module(design, module, flag_check, flag_simcheck, libdirs))
+                               if (expand_module(design, module, flag_check, flag_simcheck, flag_smtcheck, libdirs))
                                        did_something = true;
                        }