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

Various equiv_* improvements

This commit is contained in:
Clifford Wolf 2015-01-24 00:16:17 +01:00
parent 43951099cf
commit 75bbeb828a
4 changed files with 20 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
passes/equiv/equiv_induct.cc
View File

@ -81,7 +81,7 @@ struct EquivInductWorker
log(" Proving existence of base case for step %d. (%d clauses over %d variables)\n", step, ez.numCnfClauses(), ez.numCnfVariables());
if (!ez.solve()) {
log(" Proof for base case failed. Circuit inherently diverges!\n");
break;
return;
}
create_timestep(step+1);

21
passes/equiv/equiv_make.cc
View File

@ -29,16 +29,17 @@ struct EquivMakeWorker
Module *gold_mod, *gate_mod, *equiv_mod;
pool<IdString> wire_names, cell_names;
CellTypes ct;
bool inames;
void copy_to_equiv()
{
Module *gold_clone = gold_mod->clone();
Module *gate_clone = gate_mod->clone();
for (auto it : gold_clone->wires().to_vector()) { if (it->name[0] == '\\') wire_names.insert(it->name); gold_clone->rename(it, it->name.str() + "_gold"); }
for (auto it : gold_clone->cells().to_vector()) { if (it->name[0] == '\\') cell_names.insert(it->name); gold_clone->rename(it, it->name.str() + "_gold"); }
for (auto it : gate_clone->wires().to_vector()) { if (it->name[0] == '\\') wire_names.insert(it->name); gate_clone->rename(it, it->name.str() + "_gate"); }
for (auto it : gate_clone->cells().to_vector()) { if (it->name[0] == '\\') cell_names.insert(it->name); gate_clone->rename(it, it->name.str() + "_gate"); }
for (auto it : gold_clone->wires().to_vector()) { if (it->name[0] == '\\' || inames) wire_names.insert(it->name); gold_clone->rename(it, it->name.str() + "_gold"); }
for (auto it : gold_clone->cells().to_vector()) { if (it->name[0] == '\\' || inames) cell_names.insert(it->name); gold_clone->rename(it, it->name.str() + "_gold"); }
for (auto it : gate_clone->wires().to_vector()) { if (it->name[0] == '\\' || inames) wire_names.insert(it->name); gate_clone->rename(it, it->name.str() + "_gate"); }
for (auto it : gate_clone->cells().to_vector()) { if (it->name[0] == '\\' || inames) cell_names.insert(it->name); gate_clone->rename(it, it->name.str() + "_gate"); }
gold_clone->cloneInto(equiv_mod);
gate_clone->cloneInto(equiv_mod);
@ -230,6 +231,9 @@ struct EquivMakePass : public Pass {
log("equivalent modules. Use commands such as 'equiv_simple' and 'equiv_status'\n");
log("to work with the created equivalent checking module.\n");
log("\n");
log(" -inames\n");
log(" Also match cells and wires with $... names.\n");
log("\n");
log("Note: The circuit created by this command is not a miter (with something like\n");
log("a trigger output), but instead uses $equiv cells to encode the equivalence\n");
log("checking problem. Use 'miter -equiv' if you want to create a miter circuit.\n");
@ -239,14 +243,15 @@ struct EquivMakePass : public Pass {
{
EquivMakeWorker worker;
worker.ct.setup(design);
worker.inames = false;
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++)
{
// if (args[argidx] == "-foo" && argidx+1 < args.size()) {
// log("foo> %s\n", args[++argidx].c_str());
// continue;
// }
if (args[argidx] == "-inames") {
worker.inames = true;
continue;
}
break;
}

9
passes/equiv/equiv_simple.cc
View File

@ -241,11 +241,11 @@ struct EquivSimplePass : public Pass {
for (auto module : design->selected_modules())
{
vector<Cell*> unproven_equiv_cells;
vector<pair<SigBit, Cell*>> unproven_equiv_cells;
for (auto cell : module->selected_cells())
if (cell->type == "$equiv" && cell->getPort("\\A") != cell->getPort("\\B"))
unproven_equiv_cells.push_back(cell);
unproven_equiv_cells.push_back(pair<SigBit, Cell*>(cell->getPort("\\Y").to_single_sigbit(), cell));
if (unproven_equiv_cells.empty())
continue;
@ -264,8 +264,9 @@ struct EquivSimplePass : public Pass {
bit2driver[bit] = cell;
}
for (auto cell : unproven_equiv_cells) {
EquivSimpleWorker worker(cell, sigmap, bit2driver, max_seq, verbose);
std::sort(unproven_equiv_cells.begin(), unproven_equiv_cells.end());
for (auto it : unproven_equiv_cells) {
EquivSimpleWorker worker(it.second, sigmap, bit2driver, max_seq, verbose);
if (worker.run())
success_counter++;
}

2
passes/equiv/equiv_status.cc
View File

@ -71,7 +71,7 @@ struct EquivStatusPass : public Pass {
continue;
}
log("Found %d $equiv cells found in %s:\n", GetSize(unproven_equiv_cells) + proven_equiv_cells, log_id(module));
log("Found %d $equiv cells in %s:\n", GetSize(unproven_equiv_cells) + proven_equiv_cells, log_id(module));
log(" Of those cells %d are proven and %d are unproven.\n", proven_equiv_cells, GetSize(unproven_equiv_cells));
if (unproven_equiv_cells.empty()) {
log(" Equivalence successfully proven!\n");