From bc86b4a7e9c847180e6fd7ed81e0a15d5aee00a0 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 31 Jan 2015 13:58:04 +0100 Subject: [PATCH] Added "equiv_induct -undef" --- kernel/sigtools.h | 2 +- passes/equiv/equiv_induct.cc | 55 ++++++++++++++++++++++++++++++++---- 2 files changed, 51 insertions(+), 6 deletions(-) diff --git a/kernel/sigtools.h b/kernel/sigtools.h index c38736e70..f92a87dbb 100644 --- a/kernel/sigtools.h +++ b/kernel/sigtools.h @@ -129,7 +129,7 @@ struct SigPool return sig; } - size_t size() + size_t size() const { return bits.size(); } diff --git a/passes/equiv/equiv_induct.cc b/passes/equiv/equiv_induct.cc index ff91d11af..c5b4eda72 100644 --- a/passes/equiv/equiv_induct.cc +++ b/passes/equiv/equiv_induct.cc @@ -40,15 +40,18 @@ struct EquivInductWorker dict ez_step_is_consistent; pool cell_warn_cache; + SigPool undriven_signals; - EquivInductWorker(Module *module, const pool &unproven_equiv_cells, int max_seq) : module(module), sigmap(module), + EquivInductWorker(Module *module, const pool &unproven_equiv_cells, bool model_undef, int max_seq) : module(module), sigmap(module), cells(module->selected_cells()), workset(unproven_equiv_cells), satgen(&ez, &sigmap), max_seq(max_seq), success_counter(0) { + satgen.model_undef = model_undef; } void create_timestep(int step) { vector ez_equal_terms; + for (auto cell : cells) { if (!satgen.importCell(cell, step) && !cell_warn_cache.count(cell)) { log_warning("No SAT model available for cell %s (%s).\n", log_id(cell), log_id(cell->type)); @@ -60,11 +63,19 @@ struct EquivInductWorker if (bit_a != bit_b) { int ez_a = satgen.importSigBit(bit_a, step); int ez_b = satgen.importSigBit(bit_b, step); - ez_equal_terms.push_back(ez.IFF(ez_a, ez_b)); + int cond = ez.IFF(ez_a, ez_b); + if (satgen.model_undef) + cond = ez.OR(cond, satgen.importUndefSigBit(bit_a, step)); + ez_equal_terms.push_back(cond); } } } + if (satgen.model_undef) { + for (auto bit : undriven_signals.export_all()) + ez.assume(ez.NOT(satgen.importUndefSigBit(bit, step))); + } + log_assert(!ez_step_is_consistent.count(step)); ez_step_is_consistent[step] = ez.expression(ez.OpAnd, ez_equal_terms); } @@ -73,7 +84,28 @@ struct EquivInductWorker { log("Found %d unproven $equiv cells in module %s:\n", GetSize(workset), log_id(module)); + if (satgen.model_undef) { + for (auto cell : cells) + if (yosys_celltypes.cell_known(cell->type)) + for (auto &conn : cell->connections()) + if (yosys_celltypes.cell_input(cell->type, conn.first)) + undriven_signals.add(sigmap(conn.second)); + for (auto cell : cells) + if (yosys_celltypes.cell_known(cell->type)) + for (auto &conn : cell->connections()) + if (yosys_celltypes.cell_output(cell->type, conn.first)) + undriven_signals.del(sigmap(conn.second)); + } + create_timestep(1); + + if (satgen.model_undef) { + for (auto bit : satgen.initial_state.export_all()) + ez.assume(ez.NOT(satgen.importUndefSigBit(bit, 1))); + log(" Undef modelling: force def on %d initial reg values and %d inputs.\n", + GetSize(satgen.initial_state), GetSize(undriven_signals)); + } + for (int step = 1; step <= max_seq; step++) { ez.assume(ez_step_is_consistent[step]); @@ -107,11 +139,16 @@ struct EquivInductWorker SigBit bit_a = sigmap(cell->getPort("\\A")).to_single_sigbit(); SigBit bit_b = sigmap(cell->getPort("\\B")).to_single_sigbit(); + log(" Trying to prove $equiv for %s:", log_signal(sigmap(cell->getPort("\\Y")))); + int ez_a = satgen.importSigBit(bit_a, max_seq+1); int ez_b = satgen.importSigBit(bit_b, max_seq+1); + int cond = ez.XOR(ez_a, ez_b); - log(" Trying to prove $equiv for %s:", log_signal(sigmap(cell->getPort("\\Y")))); - if (!ez.solve(ez.XOR(ez_a, ez_b))) { + if (satgen.model_undef) + cond = ez.AND(cond, ez.NOT(satgen.importUndefSigBit(bit_a, max_seq+1))); + + if (!ez.solve(cond)) { log(" success!\n"); cell->setPort("\\B", cell->getPort("\\A")); success_counter++; @@ -135,6 +172,9 @@ struct EquivInductPass : public Pass { log("Only selected $equiv cells are proven and only selected cells are used to\n"); log("perform the proof.\n"); log("\n"); + log(" -undef\n"); + log(" enable modelling of undef states\n"); + log("\n"); log(" -seq \n"); log(" the max. number of time steps to be considered (default = 4)\n"); log("\n"); @@ -154,12 +194,17 @@ struct EquivInductPass : public Pass { virtual void execute(std::vector args, Design *design) { int success_counter = 0; + bool model_undef = false; int max_seq = 4; log_header("Executing EQUIV_INDUCT pass.\n"); size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) { + if (args[argidx] == "-undef") { + model_undef = true; + continue; + } if (args[argidx] == "-seq" && argidx+1 < args.size()) { max_seq = atoi(args[++argidx].c_str()); continue; @@ -183,7 +228,7 @@ struct EquivInductPass : public Pass { continue; } - EquivInductWorker worker(module, unproven_equiv_cells, max_seq); + EquivInductWorker worker(module, unproven_equiv_cells, model_undef, max_seq); worker.run(); success_counter += worker.success_counter; }