mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-11-04 13:29:12 +00:00
Code Activity

equiv_induct: Add -set-assumes option

Browse source 
Uses mostly the same code as equiv_simple, but the assumes are already being imported so long as they're in the selection, so it's even easier.
This commit is contained in:
Krystine Sherwin 2025-08-06 15:12:48 +12:00
parent 5ec189a2f5
commit 93b39ad9b3
No known key found for this signature in database
1 changed files with 21 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

25
passes/equiv/equiv_induct.cc
View file

@ -37,14 +37,15 @@ struct EquivInductWorker
int max_seq;
int success_counter;
bool set_assumes;
dict<int, int> ez_step_is_consistent;
pool<Cell*> cell_warn_cache;
SigPool undriven_signals;
EquivInductWorker(Module *module, const pool<Cell*> &unproven_equiv_cells, bool model_undef, int max_seq) : module(module), sigmap(module),
EquivInductWorker(Module *module, const pool<Cell*> &unproven_equiv_cells, bool model_undef, int max_seq, bool set_assumes) : module(module), sigmap(module),
cells(module->selected_cells()), workset(unproven_equiv_cells),
satgen(ez.get(), &sigmap), max_seq(max_seq), success_counter(0)
satgen(ez.get(), &sigmap), max_seq(max_seq), success_counter(0), set_assumes(set_assumes)
{
satgen.model_undef = model_undef;
}
@ -77,6 +78,14 @@ struct EquivInductWorker
}
}
if (set_assumes) {
RTLIL::SigSpec assumes_a, assumes_en;
satgen.getAssumes(assumes_a, assumes_en, step);
for (int i = 0; i < GetSize(assumes_a); i++)
log("Import constraint from assume cell: %s when %s.\n", log_signal(assumes_a[i]), log_signal(assumes_en[i]));
ez->assume(satgen.importAssumes(step));
}
if (satgen.model_undef) {
for (auto bit : undriven_signals.export_all())
ez->assume(ez->NOT(satgen.importUndefSigBit(bit, step)));
@ -184,6 +193,9 @@ struct EquivInductPass : public Pass {
log(" -seq <N>\n");
log(" the max. number of time steps to be considered (default = 4)\n");
log("\n");
log(" -set-assumes\n");
log(" set all assumptions provided via $assume cells\n");
log("\n");
log("This command is very effective in proving complex sequential circuits, when\n");
log("the internal state of the circuit quickly propagates to $equiv cells.\n");
log("\n");
@ -200,7 +212,7 @@ struct EquivInductPass : public Pass {
void execute(std::vector<std::string> args, Design *design) override
{
int success_counter = 0;
bool model_undef = false;
bool model_undef = false, set_assumes = false;
int max_seq = 4;
log_header(design, "Executing EQUIV_INDUCT pass.\n");
@ -215,6 +227,10 @@ struct EquivInductPass : public Pass {
max_seq = atoi(args[++argidx].c_str());
continue;
}
if (args[argidx] == "-set-assumes") {
set_assumes = true;
continue;
}
break;
}
extra_args(args, argidx, design);
@ -222,6 +238,7 @@ struct EquivInductPass : public Pass {
for (auto module : design->selected_modules())
{
pool<Cell*> unproven_equiv_cells;
vector<Cell*> assume_cells;
for (auto cell : module->selected_cells())
if (cell->type == ID($equiv)) {
@ -234,7 +251,7 @@ struct EquivInductPass : public Pass {
continue;
}
EquivInductWorker worker(module, unproven_equiv_cells, model_undef, max_seq);
EquivInductWorker worker(module, unproven_equiv_cells, model_undef, max_seq, set_assumes);
worker.run();
success_counter += worker.success_counter;
}