mirror of
https://github.com/YosysHQ/yosys
synced 2025-06-23 14:23:41 +00:00
Replaced ezDefaultSAT with ezSatPtr
This commit is contained in:
Clifford Wolf
parent
f778a4081c
commit
4e6ca7760f
12 changed files with 186 additions and 139 deletions
|
|
@ -32,7 +32,7 @@ struct EquivInductWorker
|
|||
vector<Cell*> cells;
|
||||
pool<Cell*> workset;
|
||||
|
||||
ezDefaultSAT ez;
|
||||
ezSatPtr ez;
|
||||
SatGen satgen;
|
||||
|
||||
int max_seq;
|
||||
|
|
@ -43,7 +43,8 @@ struct EquivInductWorker
|
|||
SigPool undriven_signals;
|
||||
|
||||
EquivInductWorker(Module *module, const pool<Cell*> &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)
|
||||
cells(module->selected_cells()), workset(unproven_equiv_cells),
|
||||
satgen(ez.get(), &sigmap), max_seq(max_seq), success_counter(0)
|
||||
{
|
||||
satgen.model_undef = model_undef;
|
||||
}
|
||||
|
|
@ -63,9 +64,9 @@ struct EquivInductWorker
|
|||
if (bit_a != bit_b) {
|
||||
int ez_a = satgen.importSigBit(bit_a, step);
|
||||
int ez_b = satgen.importSigBit(bit_b, step);
|
||||
int cond = 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));
|
||||
cond = ez->OR(cond, satgen.importUndefSigBit(bit_a, step));
|
||||
ez_equal_terms.push_back(cond);
|
||||
}
|
||||
}
|
||||
|
|
@ -73,11 +74,11 @@ struct EquivInductWorker
|
|||
|
||||
if (satgen.model_undef) {
|
||||
for (auto bit : undriven_signals.export_all())
|
||||
ez.assume(ez.NOT(satgen.importUndefSigBit(bit, step)));
|
||||
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);
|
||||
ez_step_is_consistent[step] = ez->expression(ez->OpAnd, ez_equal_terms);
|
||||
}
|
||||
|
||||
void run()
|
||||
|
|
@ -101,27 +102,27 @@ struct EquivInductWorker
|
|||
|
||||
if (satgen.model_undef) {
|
||||
for (auto bit : satgen.initial_state.export_all())
|
||||
ez.assume(ez.NOT(satgen.importUndefSigBit(bit, 1)));
|
||||
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]);
|
||||
ez->assume(ez_step_is_consistent[step]);
|
||||
|
||||
log(" Proving existence of base case for step %d. (%d clauses over %d variables)\n", step, ez.numCnfClauses(), ez.numCnfVariables());
|
||||
if (!ez.solve()) {
|
||||
log(" Proving existence of base case for step %d. (%d clauses over %d variables)\n", step, ez->numCnfClauses(), ez->numCnfVariables());
|
||||
if (!ez->solve()) {
|
||||
log(" Proof for base case failed. Circuit inherently diverges!\n");
|
||||
return;
|
||||
}
|
||||
|
||||
create_timestep(step+1);
|
||||
int new_step_not_consistent = ez.NOT(ez_step_is_consistent[step+1]);
|
||||
ez.bind(new_step_not_consistent);
|
||||
int new_step_not_consistent = ez->NOT(ez_step_is_consistent[step+1]);
|
||||
ez->bind(new_step_not_consistent);
|
||||
|
||||
log(" Proving induction step %d. (%d clauses over %d variables)\n", step, ez.numCnfClauses(), ez.numCnfVariables());
|
||||
if (!ez.solve(new_step_not_consistent)) {
|
||||
log(" Proving induction step %d. (%d clauses over %d variables)\n", step, ez->numCnfClauses(), ez->numCnfVariables());
|
||||
if (!ez->solve(new_step_not_consistent)) {
|
||||
log(" Proof for induction step holds. Entire workset of %d cells proven!\n", GetSize(workset));
|
||||
for (auto cell : workset)
|
||||
cell->setPort("\\B", cell->getPort("\\A"));
|
||||
|
|
@ -143,12 +144,12 @@ struct EquivInductWorker
|
|||
|
||||
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);
|
||||
int cond = ez->XOR(ez_a, ez_b);
|
||||
|
||||
if (satgen.model_undef)
|
||||
cond = ez.AND(cond, ez.NOT(satgen.importUndefSigBit(bit_a, max_seq+1)));
|
||||
cond = ez->AND(cond, ez->NOT(satgen.importUndefSigBit(bit_a, max_seq+1)));
|
||||
|
||||
if (!ez.solve(cond)) {
|
||||
if (!ez->solve(cond)) {
|
||||
log(" success!\n");
|
||||
cell->setPort("\\B", cell->getPort("\\A"));
|
||||
success_counter++;
|
||||
|
|
|
|||
|
|
@ -32,7 +32,7 @@ struct EquivSimpleWorker
|
|||
SigMap &sigmap;
|
||||
dict<SigBit, Cell*> &bit2driver;
|
||||
|
||||
ezDefaultSAT ez;
|
||||
ezSatPtr ez;
|
||||
SatGen satgen;
|
||||
int max_seq;
|
||||
bool verbose;
|
||||
|
|
@ -41,7 +41,7 @@ struct EquivSimpleWorker
|
|||
|
||||
EquivSimpleWorker(const vector<Cell*> &equiv_cells, SigMap &sigmap, dict<SigBit, Cell*> &bit2driver, int max_seq, bool verbose, bool model_undef) :
|
||||
module(equiv_cells.front()->module), equiv_cells(equiv_cells), equiv_cell(nullptr),
|
||||
sigmap(sigmap), bit2driver(bit2driver), satgen(&ez, &sigmap), max_seq(max_seq), verbose(verbose)
|
||||
sigmap(sigmap), bit2driver(bit2driver), satgen(ez.get(), &sigmap), max_seq(max_seq), verbose(verbose)
|
||||
{
|
||||
satgen.model_undef = model_undef;
|
||||
}
|
||||
|
|
@ -91,7 +91,7 @@ struct EquivSimpleWorker
|
|||
{
|
||||
SigBit bit_a = sigmap(equiv_cell->getPort("\\A")).to_single_sigbit();
|
||||
SigBit bit_b = sigmap(equiv_cell->getPort("\\B")).to_single_sigbit();
|
||||
int ez_context = ez.frozen_literal();
|
||||
int ez_context = ez->frozen_literal();
|
||||
|
||||
if (satgen.model_undef)
|
||||
{
|
||||
|
|
@ -99,14 +99,14 @@ struct EquivSimpleWorker
|
|||
int ez_b = satgen.importDefSigBit(bit_b, max_seq+1);
|
||||
int ez_undef_a = satgen.importUndefSigBit(bit_a, max_seq+1);
|
||||
|
||||
ez.assume(ez.XOR(ez_a, ez_b), ez_context);
|
||||
ez.assume(ez.NOT(ez_undef_a), ez_context);
|
||||
ez->assume(ez->XOR(ez_a, ez_b), ez_context);
|
||||
ez->assume(ez->NOT(ez_undef_a), ez_context);
|
||||
}
|
||||
else
|
||||
{
|
||||
int ez_a = satgen.importSigBit(bit_a, max_seq+1);
|
||||
int ez_b = satgen.importSigBit(bit_b, max_seq+1);
|
||||
ez.assume(ez.XOR(ez_a, ez_b), ez_context);
|
||||
ez->assume(ez->XOR(ez_a, ez_b), ez_context);
|
||||
}
|
||||
|
||||
pool<SigBit> seed_a = { bit_a };
|
||||
|
|
@ -168,16 +168,16 @@ struct EquivSimpleWorker
|
|||
|
||||
if (satgen.model_undef) {
|
||||
for (auto bit : input_bits)
|
||||
ez.assume(ez.NOT(satgen.importUndefSigBit(bit, step+1)));
|
||||
ez->assume(ez->NOT(satgen.importUndefSigBit(bit, step+1)));
|
||||
}
|
||||
|
||||
if (verbose)
|
||||
log(" Problem size at t=%d: %d literals, %d clauses\n", step, ez.numCnfVariables(), ez.numCnfClauses());
|
||||
log(" Problem size at t=%d: %d literals, %d clauses\n", step, ez->numCnfVariables(), ez->numCnfClauses());
|
||||
|
||||
if (!ez.solve(ez_context)) {
|
||||
if (!ez->solve(ez_context)) {
|
||||
log(verbose ? " Proved equivalence! Marking $equiv cell as proven.\n" : " success!\n");
|
||||
equiv_cell->setPort("\\B", equiv_cell->getPort("\\A"));
|
||||
ez.assume(ez.NOT(ez_context));
|
||||
ez->assume(ez->NOT(ez_context));
|
||||
return true;
|
||||
}
|
||||
|
||||
|
|
@ -224,7 +224,7 @@ struct EquivSimpleWorker
|
|||
if (!verbose)
|
||||
log(" failed.\n");
|
||||
|
||||
ez.assume(ez.NOT(ez_context));
|
||||
ez->assume(ez->NOT(ez_context));
|
||||
return false;
|
||||
}
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue