Some cleanup, revert sat.cc

diff --git a/passes/opt/opt_rmdff.cc b/passes/opt/opt_rmdff.cc
index c5db344e8aa48058ea03bd0d04ddfda5570e8c98..41bbdcd5735b689fa0c891e09ee6a17020a24bbd 100644 (file)
--- a/passes/opt/opt_rmdff.cc
+++ b/passes/opt/opt_rmdff.cc
@@ -460,15 +460,19 @@ bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff)
        }
 
        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)) {
                        netlists.emplace(mod, Netlist(mod));
                        comb_filters.emplace(mod, comb_cells_filt());
                }
 
+               // Load netlist for the module from the pool
                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) {
                        RTLIL::SigBit q_sigbit = sig_q[position];
                        RTLIL::SigBit d_sigbit = sig_d[position];
@@ -480,6 +484,7 @@ bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff)
                        ezSatPtr ez;
                        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))) {
                                if (!satgen.importCell(cell))
                                        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 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)));
 
-                       if (position == 14) {
-                               counter_example_found = false;
-                       }
-
+                       // If the register bit cannot change, we can replace it with a constant
                        if (!counter_example_found) {
 
                                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));
 
-                               removed_sigbits.push_back(position);
+                               removed_sigbits = true;
                        }
                }
 
-               if (!removed_sigbits.empty()) {
+               if (removed_sigbits) {
                        return true;
                }
        }

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