diff options
Diffstat (limited to 'passes/sat')
| -rw-r--r-- | passes/sat/expose.cc | 4 | ||||
| -rw-r--r-- | passes/sat/fmcombine.cc | 41 | ||||
| -rw-r--r-- | passes/sat/sat.cc | 1 |
3 files changed, 41 insertions, 5 deletions
diff --git a/passes/sat/expose.cc b/passes/sat/expose.cc index 3add9a9eb..71ce1683d 100644 --- a/passes/sat/expose.cc +++ b/passes/sat/expose.cc @@ -42,7 +42,7 @@ struct dff_map_bit_info_t { bool consider_wire(RTLIL::Wire *wire, std::map<RTLIL::IdString, dff_map_info_t> &dff_dq_map) { - if (/*wire->name[0] == '$' ||*/ dff_dq_map.count(wire->name)) + if (wire->name[0] == '$' || dff_dq_map.count(wire->name)) return false; if (wire->port_input) return false; @@ -508,7 +508,7 @@ struct ExposePass : public Pass { } for (auto &conn : module->connections_) - conn.first = out_to_in_map(sigmap(conn.first)); + conn.first = out_to_in_map(conn.first); } if (flag_cut) diff --git a/passes/sat/fmcombine.cc b/passes/sat/fmcombine.cc index cd75ca860..f64d99dc2 100644 --- a/passes/sat/fmcombine.cc +++ b/passes/sat/fmcombine.cc @@ -26,6 +26,8 @@ PRIVATE_NAMESPACE_BEGIN struct opts_t { + bool initeq = false; + bool anyeq = false; bool fwd = false; bool bwd = false; bool nop = false; @@ -56,7 +58,7 @@ struct FmcombineWorker return newsig; } - void import_prim_cell(Cell *cell, const string &suffix) + Cell *import_prim_cell(Cell *cell, const string &suffix) { Cell *c = module->addCell(cell->name.str() + suffix, cell->type); c->parameters = cell->parameters; @@ -64,6 +66,8 @@ struct FmcombineWorker for (auto &conn : cell->connections()) c->setPort(conn.first, import_sig(conn.second, suffix)); + + return c; } void import_hier_cell(Cell *cell) @@ -102,8 +106,24 @@ struct FmcombineWorker for (auto cell : original->cells()) { if (design->module(cell->type) == nullptr) { - import_prim_cell(cell, "_gold"); - import_prim_cell(cell, "_gate"); + if (opts.anyeq && cell->type.in("$anyseq", "$anyconst")) { + Cell *gold = import_prim_cell(cell, "_gold"); + for (auto &conn : cell->connections()) + module->connect(import_sig(conn.second, "_gate"), gold->getPort(conn.first)); + } else { + Cell *gold = import_prim_cell(cell, "_gold"); + Cell *gate = import_prim_cell(cell, "_gate"); + if (opts.initeq) { + if (cell->type.in("$ff", "$dff", "$dffe", + "$dffsr", "$adff", "$dlatch", "$dlatchsr")) { + SigSpec gold_q = gold->getPort("\\Q"); + SigSpec gate_q = gate->getPort("\\Q"); + SigSpec en = module->Initstate(NEW_ID); + SigSpec eq = module->Eq(NEW_ID, gold_q, gate_q); + module->addAssume(NEW_ID, eq, en); + } + } + } } else { import_hier_cell(cell); } @@ -229,6 +249,13 @@ 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(" -initeq\n"); + log(" Insert assumptions that initially all FFs in both circuits have the\n"); + log(" same initial values.\n"); + log("\n"); + log(" -anyeq\n"); + log(" Do not duplicate $anyseq/$anyconst cells.\n"); + log("\n"); log(" -fwd\n"); log(" Insert forward hint assumptions into the combined module.\n"); log("\n"); @@ -261,6 +288,14 @@ struct FmcombinePass : public Pass { // filename = args[++argidx]; // continue; // } + if (args[argidx] == "-initeq") { + opts.initeq = true; + continue; + } + if (args[argidx] == "-anyeq") { + opts.anyeq = true; + continue; + } if (args[argidx] == "-fwd") { opts.fwd = true; continue; diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index 695a03e15..cbba738f0 100644 --- a/passes/sat/sat.cc +++ b/passes/sat/sat.cc @@ -1169,6 +1169,7 @@ struct SatPass : public Pass { if (args[argidx] == "-tempinduct-def") { tempinduct = true; tempinduct_def = true; + enable_undef = true; continue; } if (args[argidx] == "-tempinduct-baseonly") { |