summaryrefslogtreecommitdiff
path: root/passes/equiv
diff options
context:
space:
mode:
Diffstat (limited to 'passes/equiv')
-rw-r--r--passes/equiv/equiv_induct.cc35
-rw-r--r--passes/equiv/equiv_simple.cc22
2 files changed, 29 insertions, 28 deletions
diff --git a/passes/equiv/equiv_induct.cc b/passes/equiv/equiv_induct.cc
index c5b4eda7..a56730d4 100644
--- a/passes/equiv/equiv_induct.cc
+++ b/passes/equiv/equiv_induct.cc
@@ -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++;
diff --git a/passes/equiv/equiv_simple.cc b/passes/equiv/equiv_simple.cc
index 579877e6..f1b66432 100644
--- a/passes/equiv/equiv_simple.cc
+++ b/passes/equiv/equiv_simple.cc
@@ -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;
}