From 4e6ca7760f801ce5ea16c6ea9be3ad4a86aa3b1d Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 21 Feb 2015 12:15:41 +0100 Subject: [PATCH] Replaced ezDefaultSAT with ezSatPtr --- kernel/register.cc | 14 +++++++ kernel/satgen.h | 32 ++++++++++++++- kernel/yosys.h | 1 + passes/equiv/equiv_induct.cc | 35 +++++++++-------- passes/equiv/equiv_simple.cc | 22 +++++------ passes/memory/memory_share.cc | 14 +++---- passes/opt/share.cc | 26 ++++++------- passes/sat/eval.cc | 20 +++++----- passes/sat/freduce.cc | 54 +++++++++++++------------- passes/sat/sat.cc | 73 ++++++++++++++++++----------------- passes/tests/test_abcloop.cc | 24 ++++++------ passes/tests/test_cell.cc | 10 ++--- 12 files changed, 186 insertions(+), 139 deletions(-) diff --git a/kernel/register.cc b/kernel/register.cc index cdba4c36f..af1cb77b5 100644 --- a/kernel/register.cc +++ b/kernel/register.cc @@ -18,6 +18,8 @@ */ #include "kernel/yosys.h" +#include "kernel/satgen.h" + #include #include #include @@ -691,6 +693,18 @@ struct EchoPass : public Pass { log("echo %s\n", echo_mode ? "on" : "off"); } } EchoPass; + +SatSolver *yosys_satsolver_list; +SatSolver *yosys_satsolver; + +struct MinisatSatSolver : public SatSolver { + MinisatSatSolver() : SatSolver("minisat") { + yosys_satsolver = this; + } + virtual ezSAT *create() YS_OVERRIDE { + return new ezMiniSAT(); + } +} MinisatSatSolver; YOSYS_NAMESPACE_END diff --git a/kernel/satgen.h b/kernel/satgen.h index 2f5efe674..093d248d4 100644 --- a/kernel/satgen.h +++ b/kernel/satgen.h @@ -29,7 +29,37 @@ YOSYS_NAMESPACE_BEGIN -typedef ezMiniSAT ezDefaultSAT; +// defined in kernel/register.cc +extern struct SatSolver *yosys_satsolver_list; +extern struct SatSolver *yosys_satsolver; + +struct SatSolver +{ + string name; + SatSolver *next; + virtual ezSAT *create() = 0; + + SatSolver(string name) : name(name) { + next = yosys_satsolver_list; + yosys_satsolver_list = this; + } + + virtual ~SatSolver() { + auto p = &yosys_satsolver_list; + while (*p) { + if (*p == this) + *p = next; + else + p = &(*p)->next; + } + if (yosys_satsolver == this) + yosys_satsolver = yosys_satsolver_list; + } +}; + +struct ezSatPtr : public std::unique_ptr { + ezSatPtr() : unique_ptr(yosys_satsolver->create()) { } +}; struct SatGen { diff --git a/kernel/yosys.h b/kernel/yosys.h index 47275ecd4..467d2074f 100644 --- a/kernel/yosys.h +++ b/kernel/yosys.h @@ -49,6 +49,7 @@ #include #include #include +#include #include #include diff --git a/passes/equiv/equiv_induct.cc b/passes/equiv/equiv_induct.cc index c5b4eda72..a56730d4d 100644 --- a/passes/equiv/equiv_induct.cc +++ b/passes/equiv/equiv_induct.cc @@ -32,7 +32,7 @@ struct EquivInductWorker vector cells; pool workset; - ezDefaultSAT ez; + ezSatPtr ez; SatGen satgen; int max_seq; @@ -43,7 +43,8 @@ struct EquivInductWorker SigPool undriven_signals; 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) + 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 579877e65..f1b664325 100644 --- a/passes/equiv/equiv_simple.cc +++ b/passes/equiv/equiv_simple.cc @@ -32,7 +32,7 @@ struct EquivSimpleWorker SigMap &sigmap; dict &bit2driver; - ezDefaultSAT ez; + ezSatPtr ez; SatGen satgen; int max_seq; bool verbose; @@ -41,7 +41,7 @@ struct EquivSimpleWorker EquivSimpleWorker(const vector &equiv_cells, SigMap &sigmap, dict &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 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; } diff --git a/passes/memory/memory_share.cc b/passes/memory/memory_share.cc index a2f89f6d9..3d241433a 100644 --- a/passes/memory/memory_share.cc +++ b/passes/memory/memory_share.cc @@ -489,8 +489,8 @@ struct MemoryShareWorker if (wr_ports.size() <= 1) return; - ezDefaultSAT ez; - SatGen satgen(&ez, &modwalker.sigmap); + ezSatPtr ez; + SatGen satgen(ez.get(), &modwalker.sigmap); // find list of considered ports and port pairs @@ -553,7 +553,7 @@ struct MemoryShareWorker if (considered_port_pairs.count(i) || considered_port_pairs.count(i+1)) { RTLIL::SigSpec sig = modwalker.sigmap(wr_ports[i]->getPort("\\EN")); - port_to_sat_variable[i] = ez.expression(ez.OpOr, satgen.importSigSpec(sig)); + port_to_sat_variable[i] = ez->expression(ez->OpOr, satgen.importSigSpec(sig)); std::vector bits = sig; bits_queue.insert(bits.begin(), bits.end()); @@ -582,7 +582,7 @@ struct MemoryShareWorker vector ez_wire_bits = satgen.importSigSpec(wire); for (int i : ez_wire_bits) for (int j : ez_wire_bits) - if (i != j) ez.assume(ez.NOT(i), j); + if (i != j) ez->assume(ez->NOT(i), j); } log(" Common input cone for all EN signals: %d cells.\n", int(sat_cells.size())); @@ -590,7 +590,7 @@ struct MemoryShareWorker for (auto cell : sat_cells) satgen.importCell(cell); - log(" Size of unconstrained SAT problem: %d variables, %d clauses\n", ez.numCnfVariables(), ez.numCnfClauses()); + log(" Size of unconstrained SAT problem: %d variables, %d clauses\n", ez->numCnfVariables(), ez->numCnfClauses()); // merge subsequent ports if possible @@ -599,13 +599,13 @@ struct MemoryShareWorker if (!considered_port_pairs.count(i)) continue; - if (ez.solve(port_to_sat_variable.at(i-1), port_to_sat_variable.at(i))) { + if (ez->solve(port_to_sat_variable.at(i-1), port_to_sat_variable.at(i))) { log(" According to SAT solver sharing of port %d with port %d is not possible.\n", i-1, i); continue; } log(" Merging port %d into port %d.\n", i-1, i); - port_to_sat_variable.at(i) = ez.OR(port_to_sat_variable.at(i-1), port_to_sat_variable.at(i)); + port_to_sat_variable.at(i) = ez->OR(port_to_sat_variable.at(i-1), port_to_sat_variable.at(i)); RTLIL::SigSpec last_addr = wr_ports[i-1]->getPort("\\ADDR"); RTLIL::SigSpec last_data = wr_ports[i-1]->getPort("\\DATA"); diff --git a/passes/opt/share.cc b/passes/opt/share.cc index 9cd0ccc03..bf406bcd8 100644 --- a/passes/opt/share.cc +++ b/passes/opt/share.cc @@ -1180,8 +1180,8 @@ struct ShareWorker optimize_activation_patterns(filtered_cell_activation_patterns); optimize_activation_patterns(filtered_other_cell_activation_patterns); - ezDefaultSAT ez; - SatGen satgen(&ez, &modwalker.sigmap); + ezSatPtr ez; + SatGen satgen(ez.get(), &modwalker.sigmap); pool sat_cells; std::set bits_queue; @@ -1191,13 +1191,13 @@ struct ShareWorker for (auto &p : filtered_cell_activation_patterns) { log(" Activation pattern for cell %s: %s = %s\n", log_id(cell), log_signal(p.first), log_signal(p.second)); - cell_active.push_back(ez.vec_eq(satgen.importSigSpec(p.first), satgen.importSigSpec(p.second))); + cell_active.push_back(ez->vec_eq(satgen.importSigSpec(p.first), satgen.importSigSpec(p.second))); all_ctrl_signals.append(p.first); } for (auto &p : filtered_other_cell_activation_patterns) { log(" Activation pattern for cell %s: %s = %s\n", log_id(other_cell), log_signal(p.first), log_signal(p.second)); - other_cell_active.push_back(ez.vec_eq(satgen.importSigSpec(p.first), satgen.importSigSpec(p.second))); + other_cell_active.push_back(ez->vec_eq(satgen.importSigSpec(p.first), satgen.importSigSpec(p.second))); all_ctrl_signals.append(p.first); } @@ -1232,36 +1232,36 @@ struct ShareWorker log(" Adding exclusive control bits: %s vs. %s\n", log_signal(it.first), log_signal(it.second)); int sub1 = satgen.importSigBit(it.first); int sub2 = satgen.importSigBit(it.second); - ez.assume(ez.NOT(ez.AND(sub1, sub2))); + ez->assume(ez->NOT(ez->AND(sub1, sub2))); } - if (!ez.solve(ez.expression(ez.OpOr, cell_active))) { + if (!ez->solve(ez->expression(ez->OpOr, cell_active))) { log(" According to the SAT solver the cell %s is never active. Sharing is pointless, we simply remove it.\n", log_id(cell)); cells_to_remove.insert(cell); break; } - if (!ez.solve(ez.expression(ez.OpOr, other_cell_active))) { + if (!ez->solve(ez->expression(ez->OpOr, other_cell_active))) { log(" According to the SAT solver the cell %s is never active. Sharing is pointless, we simply remove it.\n", log_id(other_cell)); cells_to_remove.insert(other_cell); shareable_cells.erase(other_cell); continue; } - ez.non_incremental(); + ez->non_incremental(); all_ctrl_signals.sort_and_unify(); std::vector sat_model = satgen.importSigSpec(all_ctrl_signals); std::vector sat_model_values; - int sub1 = ez.expression(ez.OpOr, cell_active); - int sub2 = ez.expression(ez.OpOr, other_cell_active); - ez.assume(ez.AND(sub1, sub2)); + int sub1 = ez->expression(ez->OpOr, cell_active); + int sub2 = ez->expression(ez->OpOr, other_cell_active); + ez->assume(ez->AND(sub1, sub2)); log(" Size of SAT problem: %d cells, %d variables, %d clauses\n", - GetSize(sat_cells), ez.numCnfVariables(), ez.numCnfClauses()); + GetSize(sat_cells), ez->numCnfVariables(), ez->numCnfClauses()); - if (ez.solve(sat_model, sat_model_values)) { + if (ez->solve(sat_model, sat_model_values)) { log(" According to the SAT solver this pair of cells can not be shared.\n"); log(" Model from SAT solver: %s = %d'", log_signal(all_ctrl_signals), GetSize(sat_model_values)); for (int i = GetSize(sat_model_values)-1; i >= 0; i--) diff --git a/passes/sat/eval.cc b/passes/sat/eval.cc index 62534ec0b..01d0e031c 100644 --- a/passes/sat/eval.cc +++ b/passes/sat/eval.cc @@ -143,16 +143,16 @@ struct VlogHammerReporter { log("Verifying SAT model (%s)..\n", model_undef ? "with undef" : "without undef"); - ezDefaultSAT ez; + ezSatPtr ez; SigMap sigmap(module); - SatGen satgen(&ez, &sigmap); + SatGen satgen(ez.get(), &sigmap); satgen.model_undef = model_undef; for (auto &c : module->cells_) if (!satgen.importCell(c.second)) log_error("Failed to import cell %s (type %s) to SAT database.\n", RTLIL::id2cstr(c.first), RTLIL::id2cstr(c.second->type)); - ez.assume(satgen.signals_eq(recorded_set_vars, recorded_set_vals)); + ez->assume(satgen.signals_eq(recorded_set_vars, recorded_set_vals)); std::vector y_vec = satgen.importDefSigSpec(module->wires_.at("\\y")); std::vector y_values; @@ -163,9 +163,9 @@ struct VlogHammerReporter } log(" Created SAT problem with %d variables and %d clauses.\n", - ez.numCnfVariables(), ez.numCnfClauses()); + ez->numCnfVariables(), ez->numCnfClauses()); - if (!ez.solve(y_vec, y_values)) + if (!ez->solve(y_vec, y_values)) log_error("Failed to find solution to SAT problem.\n"); for (int i = 0; i < expected_y.size(); i++) { @@ -204,7 +204,7 @@ struct VlogHammerReporter if (y_undef.at(i)) { log(" Toggling undef bit %d to test undef gating.\n", i); - if (!ez.solve(y_vec, y_values, ez.IFF(y_vec.at(i), y_values.at(i) ? ez.CONST_FALSE : ez.CONST_TRUE))) + if (!ez->solve(y_vec, y_values, ez->IFF(y_vec.at(i), y_values.at(i) ? ez->CONST_FALSE : ez->CONST_TRUE))) log_error("Failed to find solution with toggled bit!\n"); cmp_vars.push_back(y_vec.at(expected_y.size() + i)); @@ -220,15 +220,15 @@ struct VlogHammerReporter } log(" Testing if SAT solution is unique.\n"); - ez.assume(ez.vec_ne(cmp_vars, ez.vec_const(cmp_vals))); - if (ez.solve(y_vec, y_values)) + ez->assume(ez->vec_ne(cmp_vars, ez->vec_const(cmp_vals))); + if (ez->solve(y_vec, y_values)) log_error("Found two distinct solutions to SAT problem.\n"); } else { log(" Testing if SAT solution is unique.\n"); - ez.assume(ez.vec_ne(y_vec, ez.vec_const(y_values))); - if (ez.solve(y_vec, y_values)) + ez->assume(ez->vec_ne(y_vec, ez->vec_const(y_values))); + if (ez->solve(y_vec, y_values)) log_error("Found two distinct solutions to SAT problem.\n"); } diff --git a/passes/sat/freduce.cc b/passes/sat/freduce.cc index fbca35861..8a5301ec3 100644 --- a/passes/sat/freduce.cc +++ b/passes/sat/freduce.cc @@ -73,7 +73,7 @@ struct FindReducedInputs SigMap &sigmap; drivers_t &drivers; - ezDefaultSAT ez; + ezSatPtr ez; std::set ez_cells; SatGen satgen; @@ -81,7 +81,7 @@ struct FindReducedInputs std::vector sat_pi_uniq_bitvec; FindReducedInputs(SigMap &sigmap, drivers_t &drivers) : - sigmap(sigmap), drivers(drivers), satgen(&ez, &sigmap) + sigmap(sigmap), drivers(drivers), satgen(ez.get(), &sigmap) { satgen.model_undef = true; } @@ -104,30 +104,30 @@ struct FindReducedInputs satgen.setContext(&sigmap, "A"); int sat_a = satgen.importSigSpec(bit).front(); - ez.assume(ez.NOT(satgen.importUndefSigSpec(bit).front())); + ez->assume(ez->NOT(satgen.importUndefSigSpec(bit).front())); satgen.setContext(&sigmap, "B"); int sat_b = satgen.importSigSpec(bit).front(); - ez.assume(ez.NOT(satgen.importUndefSigSpec(bit).front())); + ez->assume(ez->NOT(satgen.importUndefSigSpec(bit).front())); int idx = sat_pi.size(); size_t idx_bits = get_bits(idx); if (sat_pi_uniq_bitvec.size() != idx_bits) { - sat_pi_uniq_bitvec.push_back(ez.frozen_literal(stringf("uniq_%d", int(idx_bits)-1))); + sat_pi_uniq_bitvec.push_back(ez->frozen_literal(stringf("uniq_%d", int(idx_bits)-1))); for (auto &it : sat_pi) - ez.assume(ez.OR(ez.NOT(it.second), ez.NOT(sat_pi_uniq_bitvec.back()))); + ez->assume(ez->OR(ez->NOT(it.second), ez->NOT(sat_pi_uniq_bitvec.back()))); } log_assert(sat_pi_uniq_bitvec.size() == idx_bits); - sat_pi[bit] = ez.frozen_literal(stringf("p, falsei_%s", log_signal(bit))); - ez.assume(ez.IFF(ez.XOR(sat_a, sat_b), sat_pi[bit])); + sat_pi[bit] = ez->frozen_literal(stringf("p, falsei_%s", log_signal(bit))); + ez->assume(ez->IFF(ez->XOR(sat_a, sat_b), sat_pi[bit])); for (size_t i = 0; i < idx_bits; i++) if ((idx & (1 << i)) == 0) - ez.assume(ez.OR(ez.NOT(sat_pi[bit]), ez.NOT(sat_pi_uniq_bitvec[i]))); + ez->assume(ez->OR(ez->NOT(sat_pi[bit]), ez->NOT(sat_pi_uniq_bitvec[i]))); else - ez.assume(ez.OR(ez.NOT(sat_pi[bit]), sat_pi_uniq_bitvec[i])); + ez->assume(ez->OR(ez->NOT(sat_pi[bit]), sat_pi_uniq_bitvec[i])); } void register_cone_worker(std::set &pi, std::set &sigdone, RTLIL::SigBit out) @@ -201,7 +201,7 @@ struct FindReducedInputs model_expr.push_back(sat_pi.at(pi[i])); } - if (!ez.solve(model_expr, model, ez.expression(ezSAT::OpOr, model_expr), ez.XOR(output_a, output_b), ez.NOT(output_undef_a), ez.NOT(output_undef_b))) + if (!ez->solve(model_expr, model, ez->expression(ezSAT::OpOr, model_expr), ez->XOR(output_a, output_b), ez->NOT(output_undef_a), ez->NOT(output_undef_b))) break; int found_count = 0; @@ -230,7 +230,7 @@ struct PerformReduction drivers_t &drivers; std::set> &inv_pairs; - ezDefaultSAT ez; + ezSatPtr ez; SatGen satgen; std::vector sat_pi, sat_out, sat_def; @@ -260,7 +260,7 @@ struct PerformReduction } else { pi_bits.push_back(out); sat_pi.push_back(satgen.importSigSpec(out).front()); - ez.assume(ez.NOT(satgen.importUndefSigSpec(out).front())); + ez->assume(ez->NOT(satgen.importUndefSigSpec(out).front())); sigdepth[out] = 0; } @@ -268,7 +268,7 @@ struct PerformReduction } PerformReduction(SigMap &sigmap, drivers_t &drivers, std::set> &inv_pairs, std::vector &bits, int cone_size) : - sigmap(sigmap), drivers(drivers), inv_pairs(inv_pairs), satgen(&ez, &sigmap), out_bits(bits), cone_size(cone_size) + sigmap(sigmap), drivers(drivers), inv_pairs(inv_pairs), satgen(ez.get(), &sigmap), out_bits(bits), cone_size(cone_size) { satgen.model_undef = true; @@ -278,15 +278,15 @@ struct PerformReduction for (auto &bit : bits) { out_depth.push_back(register_cone_worker(celldone, sigdepth, bit)); sat_out.push_back(satgen.importSigSpec(bit).front()); - sat_def.push_back(ez.NOT(satgen.importUndefSigSpec(bit).front())); + sat_def.push_back(ez->NOT(satgen.importUndefSigSpec(bit).front())); } if (inv_mode && cone_size > 0) { - if (!ez.solve(sat_out, out_inverted, ez.expression(ezSAT::OpAnd, sat_def))) + if (!ez->solve(sat_out, out_inverted, ez->expression(ezSAT::OpAnd, sat_def))) log_error("Solving for initial model failed!\n"); for (size_t i = 0; i < sat_out.size(); i++) if (out_inverted.at(i)) - sat_out[i] = ez.NOT(sat_out[i]); + sat_out[i] = ez->NOT(sat_out[i]); } else out_inverted = std::vector(sat_out.size(), false); } @@ -296,8 +296,8 @@ struct PerformReduction if (verbose_level == 1) log(" Finding const value for %s.\n", log_signal(out_bits[idx])); - bool can_be_set = ez.solve(ez.AND(sat_out[idx], sat_def[idx])); - bool can_be_clr = ez.solve(ez.AND(ez.NOT(sat_out[idx]), sat_def[idx])); + bool can_be_set = ez->solve(ez->AND(sat_out[idx], sat_def[idx])); + bool can_be_clr = ez->solve(ez->AND(ez->NOT(sat_out[idx]), sat_def[idx])); log_assert(!can_be_set || !can_be_clr); RTLIL::SigBit value(RTLIL::State::Sx); @@ -355,8 +355,8 @@ struct PerformReduction std::vector sat_set_list, sat_clr_list; for (int idx : bucket) { - sat_set_list.push_back(ez.AND(sat_out[idx], sat_def[idx])); - sat_clr_list.push_back(ez.AND(ez.NOT(sat_out[idx]), sat_def[idx])); + sat_set_list.push_back(ez->AND(sat_out[idx], sat_def[idx])); + sat_clr_list.push_back(ez->AND(ez->NOT(sat_out[idx]), sat_def[idx])); } std::vector modelVars = sat_out; @@ -366,7 +366,7 @@ struct PerformReduction if (verbose_level >= 2) modelVars.insert(modelVars.end(), sat_pi.begin(), sat_pi.end()); - if (ez.solve(modelVars, model, ez.expression(ezSAT::OpOr, sat_set_list), ez.expression(ezSAT::OpOr, sat_clr_list))) + if (ez->solve(modelVars, model, ez->expression(ezSAT::OpOr, sat_set_list), ez->expression(ezSAT::OpOr, sat_clr_list))) { int iter_count = 1; @@ -379,13 +379,13 @@ struct PerformReduction for (int idx : bucket) if (!model[sat_out.size() + idx]) { - sat_set_list.push_back(ez.AND(sat_out[idx], sat_def[idx])); - sat_clr_list.push_back(ez.AND(ez.NOT(sat_out[idx]), sat_def[idx])); + sat_set_list.push_back(ez->AND(sat_out[idx], sat_def[idx])); + sat_clr_list.push_back(ez->AND(ez->NOT(sat_out[idx]), sat_def[idx])); } else { sat_def_list.push_back(sat_def[idx]); } - if (!ez.solve(modelVars, model, ez.expression(ezSAT::OpOr, sat_set_list), ez.expression(ezSAT::OpOr, sat_clr_list), ez.expression(ezSAT::OpAnd, sat_def_list))) + if (!ez->solve(modelVars, model, ez->expression(ezSAT::OpOr, sat_set_list), ez->expression(ezSAT::OpOr, sat_clr_list), ez->expression(ezSAT::OpAnd, sat_def_list))) break; iter_count++; } @@ -431,7 +431,7 @@ struct PerformReduction for (int idx2 : bucket) if (idx != idx2) sat_def_list.push_back(sat_def[idx2]); - if (ez.solve(ez.NOT(sat_def[idx]), ez.expression(ezSAT::OpOr, sat_def_list))) + if (ez->solve(ez->NOT(sat_def[idx]), ez->expression(ezSAT::OpOr, sat_def_list))) undef_slaves.push_back(idx); } @@ -505,7 +505,7 @@ struct PerformReduction for (int idx2 : r) if (idx != idx2) sat_def_list.push_back(sat_def[idx2]); - if (ez.solve(ez.NOT(sat_def[idx]), ez.expression(ezSAT::OpOr, sat_def_list))) + if (ez->solve(ez->NOT(sat_def[idx]), ez->expression(ezSAT::OpOr, sat_def_list))) undef_slaves.push_back(idx); } diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index b9535f49d..ad680b6a2 100644 --- a/passes/sat/sat.cc +++ b/passes/sat/sat.cc @@ -41,9 +41,10 @@ struct SatHelper RTLIL::Design *design; RTLIL::Module *module; - ezDefaultSAT ez; SigMap sigmap; CellTypes ct; + + ezSatPtr ez; SatGen satgen; // additional constraints @@ -65,7 +66,7 @@ struct SatHelper bool gotTimeout; SatHelper(RTLIL::Design *design, RTLIL::Module *module, bool enable_undef) : - design(design), module(module), sigmap(module), ct(design), satgen(&ez, &sigmap) + design(design), module(module), sigmap(module), ct(design), satgen(ez.get(), &sigmap) { this->enable_undef = enable_undef; satgen.model_undef = enable_undef; @@ -155,7 +156,7 @@ struct SatHelper if (set_init_def) { RTLIL::SigSpec rem = satgen.initial_state.export_all(); std::vector undef_rem = satgen.importUndefSigSpec(rem, 1); - ez.assume(ez.NOT(ez.expression(ezSAT::OpOr, undef_rem))); + ez->assume(ez->NOT(ez->expression(ezSAT::OpOr, undef_rem))); } if (set_init_undef) { @@ -179,7 +180,7 @@ struct SatHelper log("Final constraint equation: %s = %s\n\n", log_signal(big_lhs), log_signal(big_rhs)); check_undef_enabled(big_lhs), check_undef_enabled(big_rhs); - ez.assume(satgen.signals_eq(big_lhs, big_rhs, 1)); + ez->assume(satgen.signals_eq(big_lhs, big_rhs, 1)); } void setup(int timestep = -1) @@ -250,7 +251,7 @@ struct SatHelper log("Final constraint equation: %s = %s\n", log_signal(big_lhs), log_signal(big_rhs)); check_undef_enabled(big_lhs), check_undef_enabled(big_rhs); - ez.assume(satgen.signals_eq(big_lhs, big_rhs, timestep)); + ez->assume(satgen.signals_eq(big_lhs, big_rhs, timestep)); // 0 = sets_def // 1 = sets_any_undef @@ -310,11 +311,11 @@ struct SatHelper log("Import %s constraint for this timestep: %s\n", t == 0 ? "def" : t == 1 ? "any_undef" : "all_undef", log_signal(sig)); std::vector undef_sig = satgen.importUndefSigSpec(sig, timestep); if (t == 0) - ez.assume(ez.NOT(ez.expression(ezSAT::OpOr, undef_sig))); + ez->assume(ez->NOT(ez->expression(ezSAT::OpOr, undef_sig))); if (t == 1) - ez.assume(ez.expression(ezSAT::OpOr, undef_sig)); + ez->assume(ez->expression(ezSAT::OpOr, undef_sig)); if (t == 2) - ez.assume(ez.expression(ezSAT::OpAnd, undef_sig)); + ez->assume(ez->expression(ezSAT::OpAnd, undef_sig)); } int import_cell_counter = 0; @@ -401,7 +402,7 @@ struct SatHelper std::vector undef_rhs = satgen.importUndefSigSpec(big_rhs, timestep); for (size_t i = 0; i < value_lhs.size(); i++) - prove_bits.push_back(ez.OR(undef_lhs.at(i), ez.AND(ez.NOT(undef_rhs.at(i)), ez.NOT(ez.XOR(value_lhs.at(i), value_rhs.at(i)))))); + prove_bits.push_back(ez->OR(undef_lhs.at(i), ez->AND(ez->NOT(undef_rhs.at(i)), ez->NOT(ez->XOR(value_lhs.at(i), value_rhs.at(i)))))); } if (prove_asserts) { @@ -412,22 +413,22 @@ struct SatHelper prove_bits.push_back(satgen.importAsserts(timestep)); } - return ez.expression(ezSAT::OpAnd, prove_bits); + return ez->expression(ezSAT::OpAnd, prove_bits); } void force_unique_state(int timestep_from, int timestep_to) { RTLIL::SigSpec state_signals = satgen.initial_state.export_all(); for (int i = timestep_from; i < timestep_to; i++) - ez.assume(ez.NOT(satgen.signals_eq(state_signals, state_signals, i, timestep_to))); + ez->assume(ez->NOT(satgen.signals_eq(state_signals, state_signals, i, timestep_to))); } bool solve(const std::vector &assumptions) { log_assert(gotTimeout == false); - ez.setSolverTimeout(timeout); - bool success = ez.solve(modelExpressions, modelValues, assumptions); - if (ez.getSolverTimoutStatus()) + ez->setSolverTimeout(timeout); + bool success = ez->solve(modelExpressions, modelValues, assumptions); + if (ez->getSolverTimoutStatus()) gotTimeout = true; return success; } @@ -435,9 +436,9 @@ struct SatHelper bool solve(int a = 0, int b = 0, int c = 0, int d = 0, int e = 0, int f = 0) { log_assert(gotTimeout == false); - ez.setSolverTimeout(timeout); - bool success = ez.solve(modelExpressions, modelValues, a, b, c, d, e, f); - if (ez.getSolverTimoutStatus()) + ez->setSolverTimeout(timeout); + bool success = ez->solve(modelExpressions, modelValues, a, b, c, d, e, f); + if (ez->getSolverTimoutStatus()) gotTimeout = true; return success; } @@ -478,7 +479,7 @@ struct SatHelper maybe_undef.push_back(modelExpressions.at(modelExpressions.size()/2 + i)); backupValues.swap(modelValues); - if (!solve(ez.expression(ezSAT::OpAnd, must_undef), ez.expression(ezSAT::OpOr, maybe_undef))) + if (!solve(ez->expression(ezSAT::OpAnd, must_undef), ez->expression(ezSAT::OpOr, maybe_undef))) break; } @@ -832,12 +833,12 @@ struct SatHelper int bit = modelExpressions.at(i), bit_undef = modelExpressions.at(modelExpressions.size()/2 + i); bool val = modelValues.at(i), val_undef = modelValues.at(modelExpressions.size()/2 + i); if (!max_undef || !val_undef) - clause.push_back(val_undef ? ez.NOT(bit_undef) : val ? ez.NOT(bit) : bit); + clause.push_back(val_undef ? ez->NOT(bit_undef) : val ? ez->NOT(bit) : bit); } } else for (size_t i = 0; i < modelExpressions.size(); i++) - clause.push_back(modelValues.at(i) ? ez.NOT(modelExpressions.at(i)) : modelExpressions.at(i)); - ez.assume(ez.expression(ezSAT::OpOr, clause)); + clause.push_back(modelValues.at(i) ? ez->NOT(modelExpressions.at(i)) : modelExpressions.at(i)); + ez->assume(ez->expression(ezSAT::OpOr, clause)); } }; @@ -1319,11 +1320,11 @@ struct SatPass : public Pass { inductstep.ignore_unknown_cells = ignore_unknown_cells; inductstep.setup(1); - inductstep.ez.assume(inductstep.setup_proof(1)); + inductstep.ez->assume(inductstep.setup_proof(1)); if (tempinduct_def) { std::vector undef_state = inductstep.satgen.importUndefSigSpec(inductstep.satgen.initial_state.export_all(), 1); - inductstep.ez.assume(inductstep.ez.NOT(inductstep.ez.expression(ezSAT::OpOr, undef_state))); + inductstep.ez->assume(inductstep.ez->NOT(inductstep.ez->expression(ezSAT::OpOr, undef_state))); } for (int inductlen = 1; inductlen <= maxsteps || maxsteps == 0; inductlen++) @@ -1340,9 +1341,9 @@ struct SatPass : public Pass { basecase.force_unique_state(seq_len + 1, seq_len + inductlen); log("\n[base case] Solving problem with %d variables and %d clauses..\n", - basecase.ez.numCnfVariables(), basecase.ez.numCnfClauses()); + basecase.ez->numCnfVariables(), basecase.ez->numCnfClauses()); - if (basecase.solve(basecase.ez.NOT(property))) { + if (basecase.solve(basecase.ez->NOT(property))) { log("SAT temporal induction proof finished - model found for base case: FAIL!\n"); print_proof_failed(); basecase.print_model(); @@ -1357,7 +1358,7 @@ struct SatPass : public Pass { goto timeout; log("Base case for induction length %d proven.\n", inductlen); - basecase.ez.assume(property); + basecase.ez->assume(property); // phase 2: proving induction step @@ -1371,8 +1372,8 @@ struct SatPass : public Pass { if (inductlen < initsteps) { log("\n[induction step] Skipping problem with %d variables and %d clauses (below initsteps).\n", - inductstep.ez.numCnfVariables(), inductstep.ez.numCnfClauses()); - inductstep.ez.assume(property); + inductstep.ez->numCnfVariables(), inductstep.ez->numCnfClauses()); + inductstep.ez->assume(property); } else { @@ -1385,14 +1386,14 @@ struct SatPass : public Pass { log("Dumping CNF to file `%s'.\n", cnf_file_name.c_str()); cnf_file_name.clear(); - inductstep.ez.printDIMACS(f, false); + inductstep.ez->printDIMACS(f, false); fclose(f); } log("\n[induction step] Solving problem with %d variables and %d clauses..\n", - inductstep.ez.numCnfVariables(), inductstep.ez.numCnfClauses()); + inductstep.ez->numCnfVariables(), inductstep.ez->numCnfClauses()); - if (!inductstep.solve(inductstep.ez.NOT(property))) { + if (!inductstep.solve(inductstep.ez->NOT(property))) { if (inductstep.gotTimeout) goto timeout; log("Induction step proven: SUCCESS!\n"); @@ -1401,7 +1402,7 @@ struct SatPass : public Pass { } log("Induction step failed. Incrementing induction length.\n"); - inductstep.ez.assume(property); + inductstep.ez->assume(property); inductstep.print_model(); } } @@ -1457,7 +1458,7 @@ struct SatPass : public Pass { if (seq_len == 0) { sathelper.setup(); if (sathelper.prove.size() || sathelper.prove_x.size() || sathelper.prove_asserts) - sathelper.ez.assume(sathelper.ez.NOT(sathelper.setup_proof())); + sathelper.ez->assume(sathelper.ez->NOT(sathelper.setup_proof())); } else { std::vector prove_bits; for (int timestep = 1; timestep <= seq_len; timestep++) { @@ -1467,7 +1468,7 @@ struct SatPass : public Pass { prove_bits.push_back(sathelper.setup_proof(timestep)); } if (sathelper.prove.size() || sathelper.prove_x.size() || sathelper.prove_asserts) - sathelper.ez.assume(sathelper.ez.NOT(sathelper.ez.expression(ezSAT::OpAnd, prove_bits))); + sathelper.ez->assume(sathelper.ez->NOT(sathelper.ez->expression(ezSAT::OpAnd, prove_bits))); sathelper.setup_init(); } sathelper.generate_model(); @@ -1481,7 +1482,7 @@ struct SatPass : public Pass { log("Dumping CNF to file `%s'.\n", cnf_file_name.c_str()); cnf_file_name.clear(); - sathelper.ez.printDIMACS(f, false); + sathelper.ez->printDIMACS(f, false); fclose(f); } @@ -1489,7 +1490,7 @@ struct SatPass : public Pass { rerun_solver: log("\nSolving problem with %d variables and %d clauses..\n", - sathelper.ez.numCnfVariables(), sathelper.ez.numCnfClauses()); + sathelper.ez->numCnfVariables(), sathelper.ez->numCnfClauses()); if (sathelper.solve()) { diff --git a/passes/tests/test_abcloop.cc b/passes/tests/test_abcloop.cc index 753fa7bf2..09cb41954 100644 --- a/passes/tests/test_abcloop.cc +++ b/passes/tests/test_abcloop.cc @@ -127,9 +127,9 @@ static void test_abcloop() module->fixup_ports(); Pass::call(design, "clean"); - ezDefaultSAT ez; + ezSatPtr ez; SigMap sigmap(module); - SatGen satgen(&ez, &sigmap); + SatGen satgen(ez.get(), &sigmap); for (auto c : module->cells()) { bool ok YS_ATTRIBUTE(unused) = satgen.importCell(c); @@ -137,7 +137,7 @@ static void test_abcloop() } std::vector in_vec = satgen.importSigSpec(in_sig); - std::vector inverse_in_vec = ez.vec_not(in_vec); + std::vector inverse_in_vec = ez->vec_not(in_vec); std::vector out_vec = satgen.importSigSpec(out_sig); @@ -148,7 +148,7 @@ static void test_abcloop() assumptions.push_back((i & (1 << j)) ? in_vec.at(j) : inverse_in_vec.at(j)); std::vector results; - if (!ez.solve(out_vec, results, assumptions)) { + if (!ez->solve(out_vec, results, assumptions)) { log("No stable solution for input %d found -> recreate module.\n", i); goto recreate_module; } @@ -156,10 +156,10 @@ static void test_abcloop() for (int j = 0; j < 4; j++) truthtab[i][j] = results[j]; - assumptions.push_back(ez.vec_ne(out_vec, ez.vec_const(results))); + assumptions.push_back(ez->vec_ne(out_vec, ez->vec_const(results))); std::vector results2; - if (ez.solve(out_vec, results2, assumptions)) { + if (ez->solve(out_vec, results2, assumptions)) { log("Two stable solutions for input %d found -> recreate module.\n", i); goto recreate_module; } @@ -177,9 +177,9 @@ static void test_abcloop() log("\n"); log("Pre- and post-abc truth table:\n"); - ezDefaultSAT ez; + ezSatPtr ez; SigMap sigmap(module); - SatGen satgen(&ez, &sigmap); + SatGen satgen(ez.get(), &sigmap); for (auto c : module->cells()) { bool ok YS_ATTRIBUTE(unused) = satgen.importCell(c); @@ -187,7 +187,7 @@ static void test_abcloop() } std::vector in_vec = satgen.importSigSpec(in_sig); - std::vector inverse_in_vec = ez.vec_not(in_vec); + std::vector inverse_in_vec = ez->vec_not(in_vec); std::vector out_vec = satgen.importSigSpec(out_sig); @@ -204,7 +204,7 @@ static void test_abcloop() truthtab2[i][j] = truthtab[i][j]; std::vector results; - if (!ez.solve(out_vec, results, assumptions)) { + if (!ez->solve(out_vec, results, assumptions)) { log("No stable solution for input %d found.\n", i); found_error = true; continue; @@ -213,10 +213,10 @@ static void test_abcloop() for (int j = 0; j < 4; j++) truthtab2[i][j] = results[j]; - assumptions.push_back(ez.vec_ne(out_vec, ez.vec_const(results))); + assumptions.push_back(ez->vec_ne(out_vec, ez->vec_const(results))); std::vector results2; - if (ez.solve(out_vec, results2, assumptions)) { + if (ez->solve(out_vec, results2, assumptions)) { log("Two stable solutions for input %d found -> recreate module.\n", i); found_error = true; } diff --git a/passes/tests/test_cell.cc b/passes/tests/test_cell.cc index ea2ab1e65..268f25598 100644 --- a/passes/tests/test_cell.cc +++ b/passes/tests/test_cell.cc @@ -278,10 +278,10 @@ static void run_eval_test(RTLIL::Design *design, bool verbose, bool nosat, std:: RTLIL::Module *gate_mod = design->module("\\gate"); ConstEval gold_ce(gold_mod), gate_ce(gate_mod); - ezDefaultSAT ez1, ez2; + ezSatPtr ez1, ez2; SigMap sigmap(gold_mod); - SatGen satgen1(&ez1, &sigmap); - SatGen satgen2(&ez2, &sigmap); + SatGen satgen1(ez1.get(), &sigmap); + SatGen satgen2(ez2.get(), &sigmap); satgen2.model_undef = true; if (!nosat) @@ -433,7 +433,7 @@ static void run_eval_test(RTLIL::Design *design, bool verbose, bool nosat, std:: std::vector sat1_model = satgen1.importSigSpec(out_sig); std::vector sat1_model_value; - if (!ez1.solve(sat1_model, sat1_model_value, ez1.vec_eq(sat1_in_sig, sat1_in_val))) + if (!ez1->solve(sat1_model, sat1_model_value, ez1->vec_eq(sat1_in_sig, sat1_in_val))) log_error("Evaluating sat model 1 (no undef modeling) failed!\n"); if (verbose) { @@ -468,7 +468,7 @@ static void run_eval_test(RTLIL::Design *design, bool verbose, bool nosat, std:: std::vector sat2_model_value; - if (!ez2.solve(sat2_model, sat2_model_value, ez2.vec_eq(sat2_in_def_sig, sat2_in_def_val), ez2.vec_eq(sat2_in_undef_sig, sat2_in_undef_val))) + if (!ez2->solve(sat2_model, sat2_model_value, ez2->vec_eq(sat2_in_def_sig, sat2_in_def_val), ez2->vec_eq(sat2_in_undef_sig, sat2_in_undef_val))) log_error("Evaluating sat model 2 (undef modeling) failed!\n"); if (verbose) { -- 2.30.2