From badc5f7eb9f438e66797c12352b6798c27384960 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Sat, 25 Jul 2015 11:23:45 +0200
Subject: Added "miter -assert"
---
passes/sat/miter.cc | 94 ++++++++++++++++++++++++++++++++++++++++++++++++++++-
1 file changed, 93 insertions(+), 1 deletion(-)
(limited to 'passes/sat')
diff --git a/passes/sat/miter.cc b/passes/sat/miter.cc
index 7c48e5b95..24d7e3a08 100644
--- 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;
--
cgit v1.2.3