riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Merge pull request #3528 from YosysHQ/claire/crossbits 

Add miter -cross option
This commit is contained in:
Claire Xen 2022-10-25 01:18:30 +02:00 committed by GitHub
parent 408fc60c95 d04c17fd58
commit fdce6c5868
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 32 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

36
passes/sat/miter.cc
View File

@ -31,6 +31,7 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL:
bool flag_make_outcmp = false; bool flag_make_outcmp = false;
bool flag_make_assert = false; bool flag_make_assert = false;
bool flag_flatten = false; bool flag_flatten = false;
bool flag_cross = false;
log_header(design, "Executing MITER pass (creating miter circuit).\n"); log_header(design, "Executing MITER pass (creating miter circuit).\n");
@ -57,6 +58,10 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL:
flag_flatten = true; flag_flatten = true;
continue; continue;
} }
if (args[argidx] == "-cross") {
flag_cross = true;
continue;
}
break; break;
} }
if (argidx+3 != args.size() || args[argidx].compare(0, 1, "-") == 0) if (argidx+3 != args.size() || args[argidx].compare(0, 1, "-") == 0)
@ -75,6 +80,7 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL:
RTLIL::Module *gold_module = design->module(gold_name); RTLIL::Module *gold_module = design->module(gold_name);
RTLIL::Module *gate_module = design->module(gate_name); RTLIL::Module *gate_module = design->module(gate_name);
pool<Wire*> gold_cross_ports;
for (auto gold_wire : gold_module->wires()) { for (auto gold_wire : gold_module->wires()) {
if (gold_wire->port_id == 0) if (gold_wire->port_id == 0)
@ -82,12 +88,17 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL:
RTLIL::Wire *gate_wire = gate_module->wire(gold_wire->name); RTLIL::Wire *gate_wire = gate_module->wire(gold_wire->name);
if (gate_wire == nullptr) if (gate_wire == nullptr)
goto match_gold_port_error; 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) if (gold_wire->port_input != gate_wire->port_input)
goto match_gold_port_error; goto match_gold_port_error;
if (gold_wire->port_output != gate_wire->port_output) if (gold_wire->port_output != gate_wire->port_output)
goto match_gold_port_error; goto match_gold_port_error;
if (gold_wire->width != gate_wire->width)
goto match_gold_port_error;
continue; continue;
match_gold_port_error: match_gold_port_error:
log_cmd_error("No matching port in gate module was found for %s!\n", gold_wire->name.c_str()); 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<std::string> args, RTLIL:
RTLIL::Wire *gold_wire = gold_module->wire(gate_wire->name); RTLIL::Wire *gold_wire = gold_module->wire(gate_wire->name);
if (gold_wire == nullptr) if (gold_wire == nullptr)
goto match_gate_port_error; 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) if (gate_wire->port_input != gold_wire->port_input)
goto match_gate_port_error; goto match_gate_port_error;
if (gate_wire->port_output != gold_wire->port_output) if (gate_wire->port_output != gold_wire->port_output)
goto match_gate_port_error; goto match_gate_port_error;
if (gate_wire->width != gold_wire->width)
goto match_gate_port_error;
continue; continue;
match_gate_port_error: match_gate_port_error:
log_cmd_error("No matching port in gold module was found for %s!\n", gate_wire->name.c_str()); 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<std::string> args, RTLIL:
for (auto gold_wire : gold_module->wires()) 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) if (gold_wire->port_input)
{ {
RTLIL::Wire *w = miter_module->addWire("\\in_" + RTLIL::unescape_id(gold_wire->name), gold_wire->width); 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(" call 'flatten -wb; opt_expr -keepdc -undriven;;' on the miter circuit.\n");
log("\n"); log("\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(" miter -assert [options] module [miter_name]\n");
log("\n"); log("\n");
log("Creates a miter circuit for property checking. All input ports are kept,\n"); log("Creates a miter circuit for property checking. All input ports are kept,\n");