diff options
author | Clifford Wolf <clifford@clifford.at> | 2015-07-25 11:23:45 +0200 |
---|---|---|
committer | Clifford Wolf <clifford@clifford.at> | 2015-07-25 12:09:57 +0200 |
commit | badc5f7eb9f438e66797c12352b6798c27384960 (patch) | |
tree | c06cc10e234c2aded66b57cc11cca907eb90c35d /passes/sat | |
parent | 2397078485aca763453e019fd980ced992b0abed (diff) | |
download | yosys-badc5f7eb9f438e66797c12352b6798c27384960.tar.gz yosys-badc5f7eb9f438e66797c12352b6798c27384960.tar.bz2 yosys-badc5f7eb9f438e66797c12352b6798c27384960.zip |
Added "miter -assert"
Diffstat (limited to 'passes/sat')
-rw-r--r-- | passes/sat/miter.cc | 94 |
1 files changed, 93 insertions, 1 deletions
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; |