Add "fmcombine -fwd -bwd -nop"

Signed-off-by: Clifford Wolf <clifford@clifford.at>

diff --git a/passes/sat/fmcombine.cc b/passes/sat/fmcombine.cc
index b8a0e94c892694dacf51ca0ceb0e50e3c0d1929e..cd75ca8605579ded2d39f774afb2e848454268a5 100644 (file)
--- a/passes/sat/fmcombine.cc
+++ b/passes/sat/fmcombine.cc
@@ -24,15 +24,23 @@
 USING_YOSYS_NAMESPACE
 PRIVATE_NAMESPACE_BEGIN
 
+struct opts_t
+{
+       bool fwd = false;
+       bool bwd = false;
+       bool nop = false;
+};
+
 struct FmcombineWorker
 {
+       const opts_t &opts;
        Design *design;
        Module *original = nullptr;
        Module *module = nullptr;
        IdString orig_type, combined_type;
 
-       FmcombineWorker(Design *design, IdString orig_type) :
-                       design(design), original(design->module(orig_type)),
+       FmcombineWorker(Design *design, IdString orig_type, const opts_t &opts) :
+                       opts(opts), design(design), original(design->module(orig_type)),
                        orig_type(orig_type), combined_type("$fmcombine" + orig_type.str())
        {
        }
@@ -63,7 +71,7 @@ struct FmcombineWorker
                if (!cell->parameters.empty())
                        log_cmd_error("Cell %s.%s has unresolved instance parameters.\n", log_id(original), log_id(cell));
 
-               FmcombineWorker sub_worker(design, cell->type);
+               FmcombineWorker sub_worker(design, cell->type, opts);
                sub_worker.generate();
 
                Cell *c = module->addCell(cell->name.str() + "_combined", sub_worker.combined_type);
@@ -106,6 +114,9 @@ struct FmcombineWorker
                        module->connect(import_sig(conn.first, "_gate"), import_sig(conn.second, "_gate"));
                }
 
+               if (opts.nop)
+                       return;
+
                CellTypes ct;
                ct.setup_internals_eval();
                ct.setup_stdcells_eval();
@@ -184,15 +195,19 @@ struct FmcombineWorker
                                        consequent = reduce_db.at(consequent);
                                }
 
-                               module->addAssume(NEW_ID, consequent, antecedent);
+                               if (opts.fwd)
+                                       module->addAssume(NEW_ID, consequent, antecedent);
 
-                               if (invert_db.count(antecedent) == 0)
-                                       invert_db[antecedent] = module->Not(NEW_ID, antecedent);
+                               if (opts.bwd)
+                               {
+                                       if (invert_db.count(antecedent) == 0)
+                                               invert_db[antecedent] = module->Not(NEW_ID, antecedent);
 
-                               if (invert_db.count(consequent) == 0)
-                                       invert_db[consequent] = module->Not(NEW_ID, consequent);
+                                       if (invert_db.count(consequent) == 0)
+                                               invert_db[consequent] = module->Not(NEW_ID, consequent);
 
-                               module->addAssume(NEW_ID, invert_db.at(antecedent), invert_db.at(consequent));
+                                       module->addAssume(NEW_ID, invert_db.at(antecedent), invert_db.at(consequent));
+                               }
                        }
                }
        }
@@ -214,9 +229,25 @@ struct FmcombinePass : public Pass {
                log("This is useful for formal test benches that check what differences in behavior\n");
                log("a slight difference in input causes in a module.\n");
                log("\n");
+               log("    -fwd\n");
+               log("        Insert forward hint assumptions into the combined module.\n");
+               log("\n");
+               log("    -bwd\n");
+               log("        Insert backward hint assumptions into the combined module.\n");
+               log("        (Backward hints are logically equivalend to fordward hits, but\n");
+               log("        some solvers are faster with bwd hints, or even both -bwd and -fwd.)\n");
+               log("\n");
+               log("    -nop\n");
+               log("        Don't insert hint assumptions into the combined module.\n");
+               log("        (This should not provide any speedup over the original design, but\n");
+               log("        strangely sometimes it does.)\n");
+               log("\n");
+               log("If none of -fwd, -bwd, and -nop is given, then -fwd is used as default.\n");
+               log("\n");
        }
        void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
        {
+               opts_t opts;
                Module *module = nullptr;
                Cell *gold_cell = nullptr;
                Cell *gate_cell = nullptr;
@@ -230,6 +261,18 @@ struct FmcombinePass : public Pass {
                        //      filename = args[++argidx];
                        //      continue;
                        // }
+                       if (args[argidx] == "-fwd") {
+                               opts.fwd = true;
+                               continue;
+                       }
+                       if (args[argidx] == "-bwd") {
+                               opts.bwd = true;
+                               continue;
+                       }
+                       if (args[argidx] == "-nop") {
+                               opts.nop = true;
+                               continue;
+                       }
                        break;
                }
                if (argidx+2 == args.size())
@@ -262,6 +305,12 @@ struct FmcombinePass : public Pass {
                }
                // extra_args(args, argidx, design);
 
+               if (opts.nop && (opts.fwd || opts.bwd))
+                       log_cmd_error("Option -nop can not be combined with -fwd and/or -bwd.\n");
+
+               if (!opts.nop && !opts.fwd && !opts.bwd)
+                       opts.fwd = true;
+
                if (gold_cell->type != gate_cell->type)
                        log_cmd_error("Types of gold and gate cells do not match.\n");
                if (!gold_cell->parameters.empty())
@@ -269,7 +318,7 @@ struct FmcombinePass : public Pass {
                if (!gate_cell->parameters.empty())
                        log_cmd_error("Gold cell has unresolved instance parameters.\n");
 
-               FmcombineWorker worker(design, gold_cell->type);
+               FmcombineWorker worker(design, gold_cell->type, opts);
                worker.generate();
                IdString combined_cell_name = module->uniquify(stringf("\\%s_%s", log_id(gold_cell), log_id(gate_cell)));