Various equiv_* improvements

diff --git a/passes/equiv/equiv_induct.cc b/passes/equiv/equiv_induct.cc
index 01b9220430fb2436c7b6fd35275011320fa9be88..ff91d11aff79a25629288630c3369af869445b5e 100644 (file)
--- 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 be1480e9425825f72763fb6207eef21cada48817..310d85f32494784a334980b10a1596e8efe0f56e 100644 (file)
--- 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<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;
                }
 

diff --git a/passes/equiv/equiv_simple.cc b/passes/equiv/equiv_simple.cc
index f0ab6da614853949a66431192a58d1ea8f2038f2..d50b5abad9be0bbbf1a6fce54bfc84d8105627a1 100644 (file)
--- 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<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++;
                        }

diff --git a/passes/equiv/equiv_status.cc b/passes/equiv/equiv_status.cc
index bcd09cd9c45eb635d0c354e2663ad8c8a4b26946..8ca1aacd53e53510f9b41d70f1bf05f4da525807 100644 (file)
--- 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");