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

Add "fmcombine -fwd -bwd -nop" 

Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
Clifford Wolf 2019-03-15 21:45:37 +01:00
parent 370db33a4c
commit dacaebae35
1 changed files with 59 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

69
passes/sat/fmcombine.cc
View File

@ -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)));