mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-06-03 12:51:23 +00:00
Code Activity

Some cleanup, revert sat.cc

Browse source
This commit is contained in:
Bogdan Vukobratovic 2019-06-14 11:35:45 +02:00
parent 8665f48879
commit 291b36afeb
2 changed files with 11 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

17
passes/opt/opt_rmdff.cc
View file

@ -460,15 +460,19 @@ bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff)
} }
if (sat && has_init) { if (sat && has_init) {
std::vector<int> removed_sigbits; bool removed_sigbits = false;
// Create netlist for the module if not already available
if (!netlists.count(mod)) { if (!netlists.count(mod)) {
netlists.emplace(mod, Netlist(mod)); netlists.emplace(mod, Netlist(mod));
comb_filters.emplace(mod, comb_cells_filt()); comb_filters.emplace(mod, comb_cells_filt());
} }
// Load netlist for the module from the pool
Netlist &net = netlists.at(mod); Netlist &net = netlists.at(mod);
// For each register bit, try to prove that it cannot change from the initial value. If so, remove it
for (int position = 0; position < GetSize(sig_d); position += 1) { for (int position = 0; position < GetSize(sig_d); position += 1) {
RTLIL::SigBit q_sigbit = sig_q[position]; RTLIL::SigBit q_sigbit = sig_q[position];
RTLIL::SigBit d_sigbit = sig_d[position]; RTLIL::SigBit d_sigbit = sig_d[position];
@ -480,6 +484,7 @@ bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff)
ezSatPtr ez; ezSatPtr ez;
SatGen satgen(ez.get(), &net.sigmap); SatGen satgen(ez.get(), &net.sigmap);
// Create SAT instance only for the cells that influence the register bit combinatorially
for (const auto &cell : cell_cone(net, d_sigbit, &comb_filters.at(mod))) { for (const auto &cell : cell_cone(net, d_sigbit, &comb_filters.at(mod))) {
if (!satgen.importCell(cell)) if (!satgen.importCell(cell))
log_error("Can't create SAT model for cell %s (%s)!\n", RTLIL::id2cstr(cell->name), log_error("Can't create SAT model for cell %s (%s)!\n", RTLIL::id2cstr(cell->name),
@ -492,12 +497,10 @@ bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff)
int q_sat_pi = satgen.importSigBit(q_sigbit); int q_sat_pi = satgen.importSigBit(q_sigbit);
int d_sat_pi = satgen.importSigBit(d_sigbit); int d_sat_pi = satgen.importSigBit(d_sigbit);
// Try to find out whether the register bit can change under some circumstances
bool counter_example_found = ez->solve(ez->IFF(q_sat_pi, init_sat_pi), ez->NOT(ez->IFF(d_sat_pi, init_sat_pi))); bool counter_example_found = ez->solve(ez->IFF(q_sat_pi, init_sat_pi), ez->NOT(ez->IFF(d_sat_pi, init_sat_pi)));
if (position == 14) { // If the register bit cannot change, we can replace it with a constant
counter_example_found = false;
}
if (!counter_example_found) { if (!counter_example_found) {
RTLIL::SigBit &driver_port = net.driver_port(q_sigbit); RTLIL::SigBit &driver_port = net.driver_port(q_sigbit);
@ -511,11 +514,11 @@ bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff)
mod->connect(RTLIL::SigSig(q_sigbit, sigbit_init_val)); mod->connect(RTLIL::SigSig(q_sigbit, sigbit_init_val));
removed_sigbits.push_back(position); removed_sigbits = true;
} }
} }
if (!removed_sigbits.empty()) { if (removed_sigbits) {
return true; return true;
} }
} }

7
passes/sat/sat.cc
View file

@ -1548,20 +1548,17 @@ struct SatPass : public Pass {
print_proof_failed(); print_proof_failed();
tip_failed: tip_failed:
design->scratchpad_set_bool("sat.success", false);
if (verify) { if (verify) {
log("\n"); log("\n");
log_error("Called with -verify and proof did fail!\n"); log_error("Called with -verify and proof did fail!\n");
} }
if (0) { if (0)
tip_success: tip_success:
design->scratchpad_set_bool("sat.success", true);
if (falsify) { if (falsify) {
log("\n"); log("\n");
log_error("Called with -falsify and proof did succeed!\n"); log_error("Called with -falsify and proof did succeed!\n");
} }
}
} }
else else
{ {
@ -1631,7 +1628,6 @@ struct SatPass : public Pass {
if (sathelper.solve()) if (sathelper.solve())
{ {
design->scratchpad_set_bool("sat.success", false);
if (max_undef) { if (max_undef) {
log("SAT model found. maximizing number of undefs.\n"); log("SAT model found. maximizing number of undefs.\n");
sathelper.maximize_undefs(); sathelper.maximize_undefs();
@ -1671,7 +1667,6 @@ struct SatPass : public Pass {
} }
else else
{ {
design->scratchpad_set_bool("sat.success", true);
if (sathelper.gotTimeout) if (sathelper.gotTimeout)
goto timeout; goto timeout;
if (rerun_counter) if (rerun_counter)