From 75bbeb828ad266a7614eff2e33d0a8f9fab75ed2 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 24 Jan 2015 00:16:17 +0100 Subject: [PATCH] Various equiv_* improvements --- passes/equiv/equiv_induct.cc | 2 +- passes/equiv/equiv_make.cc | 21 +++++++++++++-------- passes/equiv/equiv_simple.cc | 9 +++++---- passes/equiv/equiv_status.cc | 2 +- 4 files changed, 20 insertions(+), 14 deletions(-) diff --git a/passes/equiv/equiv_induct.cc b/passes/equiv/equiv_induct.cc index 01b922043..ff91d11af 100644 --- a/passes/equiv/equiv_induct.cc +++ b/passes/equiv/equiv_induct.cc @@ -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); diff --git a/passes/equiv/equiv_make.cc b/passes/equiv/equiv_make.cc index be1480e94..310d85f32 100644 --- a/passes/equiv/equiv_make.cc +++ b/passes/equiv/equiv_make.cc @@ -29,16 +29,17 @@ struct EquivMakeWorker Module *gold_mod, *gate_mod, *equiv_mod; pool 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; } diff --git a/passes/equiv/equiv_simple.cc b/passes/equiv/equiv_simple.cc index f0ab6da61..d50b5abad 100644 --- a/passes/equiv/equiv_simple.cc +++ b/passes/equiv/equiv_simple.cc @@ -241,11 +241,11 @@ struct EquivSimplePass : public Pass { for (auto module : design->selected_modules()) { - vector unproven_equiv_cells; + vector> 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(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++; } diff --git a/passes/equiv/equiv_status.cc b/passes/equiv/equiv_status.cc index bcd09cd9c..8ca1aacd5 100644 --- a/passes/equiv/equiv_status.cc +++ b/passes/equiv/equiv_status.cc @@ -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"); -- 2.30.2