Added "miter -assert"

diff --git a/passes/sat/miter.cc b/passes/sat/miter.cc
index 7c48e5b954486215747cbfd8598500fe8e53034e..24d7e3a08c5ca7aee5d0e9724011d2e539e9ff0c 100644 (file)
--- a/passes/sat/miter.cc
+++ b/passes/sat/miter.cc
@@ -71,7 +71,7 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL:
        if (design->modules_.count(gate_name) == 0)
                log_cmd_error("Can't find gate module %s!\n", gate_name.c_str());
        if (design->modules_.count(miter_name) != 0)
-               log_cmd_error("There is already a module %s!\n", gate_name.c_str());
+               log_cmd_error("There is already a module %s!\n", miter_name.c_str());
 
        RTLIL::Module *gold_module = design->modules_.at(gold_name);
        RTLIL::Module *gate_module = design->modules_.at(gate_name);
@@ -259,6 +259,79 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL:
        }
 }
 
+void create_miter_assert(struct Pass *that, std::vector<std::string> args, RTLIL::Design *design)
+{
+       bool flag_make_outputs = false;
+       bool flag_flatten = false;
+
+       log_header("Executing MITER pass (creating miter circuit).\n");
+
+       size_t argidx;
+       for (argidx = 2; argidx < args.size(); argidx++)
+       {
+               if (args[argidx] == "-make_outputs") {
+                       flag_make_outputs = true;
+                       continue;
+               }
+               if (args[argidx] == "-flatten") {
+                       flag_flatten = true;
+                       continue;
+               }
+               break;
+       }
+       if ((argidx+1 != args.size() && argidx+2 != args.size()) || args[argidx].substr(0, 1) == "-")
+               that->cmd_error(args, argidx, "command argument error");
+
+       IdString module_name = RTLIL::escape_id(args[argidx++]);
+       IdString miter_name = argidx < args.size() ? RTLIL::escape_id(args[argidx++]) : "";
+
+       if (design->modules_.count(module_name) == 0)
+               log_cmd_error("Can't find module %s!\n", module_name.c_str());
+       if (!miter_name.empty() && design->modules_.count(miter_name) != 0)
+               log_cmd_error("There is already a module %s!\n", miter_name.c_str());
+
+       Module *module = design->module(module_name);
+
+       if (!miter_name.empty()) {
+               module = module->clone();
+               module->name = miter_name;
+               design->add(module);
+       }
+
+       if (!flag_make_outputs)
+               for (auto wire : module->wires())
+                       wire->port_output = false;
+
+       Wire *trigger = module->addWire("\\trigger");
+       trigger->port_output = true;
+       module->fixup_ports();
+
+       if (flag_flatten) {
+               log_push();
+               Pass::call_on_module(design, module, "flatten;;");
+               log_pop();
+       }
+
+       SigSpec or_signals;
+       vector<Cell*> cell_list = module->cells();
+       for (auto cell : cell_list) {
+               if (cell->type == "$assert") {
+                       SigBit is_active = module->Nex(NEW_ID, cell->getPort("\\A"), State::S1);
+                       SigBit is_enabled = module->Eqx(NEW_ID, cell->getPort("\\EN"), State::S1);
+                       or_signals.append(module->And(NEW_ID, is_active, is_enabled));
+                       module->remove(cell);
+               }
+       }
+
+       module->addReduceOr(NEW_ID, or_signals, trigger);
+
+       if (flag_flatten) {
+               log_push();
+               Pass::call_on_module(design, module, "opt_const -keepdc -undriven;;");
+               log_pop();
+       }
+}
+
 struct MiterPass : public Pass {
        MiterPass() : Pass("miter", "automatically create a miter circuit") { }
        virtual void help()
@@ -290,6 +363,20 @@ struct MiterPass : public Pass {
                log("    -flatten\n");
                log("        call 'flatten; opt_const -keepdc -undriven;;' on the miter circuit.\n");
                log("\n");
+               log("\n");
+               log("    miter -assert [options] module [miter_name]\n");
+               log("\n");
+               log("Creates a miter circuit for property checking. All input ports are kept,\n");
+               log("output ports are discarded. An additional output 'trigger' is created that\n");
+               log("goes high when an assert is violated. Without a miter_name, the existing\n");
+               log("module is modified.\n");
+               log("\n");
+               log("    -make_outputs\n");
+               log("        keep module output ports.\n");
+               log("\n");
+               log("    -flatten\n");
+               log("        call 'flatten; opt_const -keepdc -undriven;;' on the miter circuit.\n");
+               log("\n");
        }
        virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
        {
@@ -298,6 +385,11 @@ struct MiterPass : public Pass {
                        return;
                }
 
+               if (args.size() > 1 && args[1] == "-assert") {
+                       create_miter_assert(this, args, design);
+                       return;
+               }
+
                log_cmd_error("Missing mode parameter!\n");
        }
 } MiterPass;