diff --git a/passes/sat/miter.cc b/passes/sat/miter.cc index 37efadfbd..bf33c9ce3 100644 --- a/passes/sat/miter.cc +++ b/passes/sat/miter.cc @@ -31,6 +31,7 @@ void create_miter_equiv(struct Pass *that, std::vector args, RTLIL: bool flag_make_outcmp = false; bool flag_make_assert = false; bool flag_flatten = false; + bool flag_cross = false; log_header(design, "Executing MITER pass (creating miter circuit).\n"); @@ -57,6 +58,10 @@ void create_miter_equiv(struct Pass *that, std::vector args, RTLIL: flag_flatten = true; continue; } + if (args[argidx] == "-cross") { + flag_cross = true; + continue; + } break; } if (argidx+3 != args.size() || args[argidx].compare(0, 1, "-") == 0) @@ -75,6 +80,7 @@ void create_miter_equiv(struct Pass *that, std::vector args, RTLIL: RTLIL::Module *gold_module = design->module(gold_name); RTLIL::Module *gate_module = design->module(gate_name); + pool gold_cross_ports; for (auto gold_wire : gold_module->wires()) { if (gold_wire->port_id == 0) @@ -82,12 +88,17 @@ void create_miter_equiv(struct Pass *that, std::vector args, RTLIL: RTLIL::Wire *gate_wire = gate_module->wire(gold_wire->name); if (gate_wire == nullptr) goto match_gold_port_error; + if (gold_wire->width != gate_wire->width) + goto match_gold_port_error; + if (flag_cross && !gold_wire->port_input && gold_wire->port_output && + gate_wire->port_input && !gate_wire->port_output) { + gold_cross_ports.insert(gold_wire); + continue; + } if (gold_wire->port_input != gate_wire->port_input) goto match_gold_port_error; if (gold_wire->port_output != gate_wire->port_output) goto match_gold_port_error; - if (gold_wire->width != gate_wire->width) - goto match_gold_port_error; continue; match_gold_port_error: log_cmd_error("No matching port in gate module was found for %s!\n", gold_wire->name.c_str()); @@ -99,12 +110,15 @@ void create_miter_equiv(struct Pass *that, std::vector args, RTLIL: RTLIL::Wire *gold_wire = gold_module->wire(gate_wire->name); if (gold_wire == nullptr) goto match_gate_port_error; + if (gate_wire->width != gold_wire->width) + goto match_gate_port_error; + if (flag_cross && !gold_wire->port_input && gold_wire->port_output && + gate_wire->port_input && !gate_wire->port_output) + continue; if (gate_wire->port_input != gold_wire->port_input) goto match_gate_port_error; if (gate_wire->port_output != gold_wire->port_output) goto match_gate_port_error; - if (gate_wire->width != gold_wire->width) - goto match_gate_port_error; continue; match_gate_port_error: log_cmd_error("No matching port in gold module was found for %s!\n", gate_wire->name.c_str()); @@ -123,6 +137,14 @@ void create_miter_equiv(struct Pass *that, std::vector args, RTLIL: for (auto gold_wire : gold_module->wires()) { + if (gold_cross_ports.count(gold_wire)) + { + RTLIL::Wire *w = miter_module->addWire("\\cross_" + RTLIL::unescape_id(gold_wire->name), gold_wire->width); + gold_cell->setPort(gold_wire->name, w); + gate_cell->setPort(gold_wire->name, w); + continue; + } + if (gold_wire->port_input) { RTLIL::Wire *w = miter_module->addWire("\\in_" + RTLIL::unescape_id(gold_wire->name), gold_wire->width); @@ -384,6 +406,12 @@ struct MiterPass : public Pass { log(" call 'flatten -wb; opt_expr -keepdc -undriven;;' on the miter circuit.\n"); log("\n"); log("\n"); + log(" -cross\n"); + log(" allow output ports on the gold module to match input ports on the\n"); + log(" gate module. This is useful when the gold module contains additional\n"); + log(" logic to drive some of the gate module inputs.\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");