aboutsummaryrefslogtreecommitdiffstats
path: root/passes/sat/miter.cc
diff options
context:
space:
mode:
Diffstat (limited to 'passes/sat/miter.cc')
-rw-r--r--passes/sat/miter.cc110
1 files changed, 101 insertions, 9 deletions
diff --git a/passes/sat/miter.cc b/passes/sat/miter.cc
index 9853cd0c6..4854e19bf 100644
--- a/passes/sat/miter.cc
+++ b/passes/sat/miter.cc
@@ -2,11 +2,11 @@
* yosys -- Yosys Open SYnthesis Suite
*
* Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
- *
+ *
* Permission to use, copy, modify, and/or distribute this software for any
* purpose with or without fee is hereby granted, provided that the above
* copyright notice and this permission notice appear in all copies.
- *
+ *
* THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
* WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
* MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
@@ -32,7 +32,7 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL:
bool flag_make_assert = false;
bool flag_flatten = false;
- log_header("Executing MITER pass (creating miter circuit).\n");
+ log_header(design, "Executing MITER pass (creating miter circuit).\n");
size_t argidx;
for (argidx = 2; argidx < args.size(); argidx++)
@@ -61,7 +61,7 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL:
}
if (argidx+3 != args.size() || args[argidx].substr(0, 1) == "-")
that->cmd_error(args, argidx, "command argument error");
-
+
RTLIL::IdString gold_name = RTLIL::escape_id(args[argidx++]);
RTLIL::IdString gate_name = RTLIL::escape_id(args[argidx++]);
RTLIL::IdString miter_name = RTLIL::escape_id(args[argidx++]);
@@ -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);
@@ -254,7 +254,80 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL:
if (flag_flatten) {
log_push();
- Pass::call_on_module(design, miter_module, "flatten; opt_const -keepdc -undriven;;");
+ Pass::call_on_module(design, miter_module, "flatten; opt_expr -keepdc -undriven;;");
+ log_pop();
+ }
+}
+
+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(design, "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_expr -keepdc -undriven;;");
log_pop();
}
}
@@ -267,7 +340,7 @@ struct MiterPass : public Pass {
log("\n");
log(" miter -equiv [options] gold_name gate_name miter_name\n");
log("\n");
- log("Creates a miter circuit for equivialence checking. The gold- and gate- modules\n");
+ log("Creates a miter circuit for equivalence checking. The gold- and gate- modules\n");
log("must have the same interfaces. The miter circuit will have all inputs of the\n");
log("two source modules, prefixed with 'in_'. The miter circuit has a 'trigger'\n");
log("output that goes high if an output mismatch between the two source modules is\n");
@@ -288,7 +361,21 @@ struct MiterPass : public Pass {
log(" also create an 'assert' cell that checks if trigger is always low.\n");
log("\n");
log(" -flatten\n");
- log(" call 'flatten; opt_const -keepdc -undriven;;' on the miter circuit.\n");
+ log(" call 'flatten; opt_expr -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_expr -keepdc -undriven;;' on the miter circuit.\n");
log("\n");
}
virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
@@ -298,8 +385,13 @@ 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;
-
+
PRIVATE_NAMESPACE_END
generated by cgit v1.2.3 (git 2.25.1) at 2025-06-05 14:28:34 +0000