Optimizing DFFs whose initial value prevents their value from changing

This is a proof of concept implementation that invokes SAT solver via Pass::call
method.

diff --git a/passes/opt/opt_rmdff.cc b/passes/opt/opt_rmdff.cc
index 2abffa2a9d40a9ee9d07ece33efb878c9fc8f2d8..72eac9111ebe90ab4a5c03cf7bd4f0ea502fb71b 100644 (file)
--- a/passes/opt/opt_rmdff.cc
+++ b/passes/opt/opt_rmdff.cc
@@ -30,6 +30,7 @@ SigMap assign_map, dff_init_map;
 SigSet<RTLIL::Cell*> mux_drivers;
 dict<SigBit, pool<SigBit>> init_attributes;
 bool keepdc;
+bool sat;
 
 void remove_init_attr(SigSpec sig)
 {
@@ -258,7 +259,7 @@ delete_dlatch:
        return true;
 }
 
-bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff)
+bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff, Pass *pass)
 {
        RTLIL::SigSpec sig_d, sig_q, sig_c, sig_r, sig_e;
        RTLIL::Const val_cp, val_rp, val_rv, val_ep;
@@ -452,6 +453,52 @@ bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff)
                dff->unsetPort("\\E");
        }
 
+       if (sat && has_init) {
+               std::vector<int> removed_sigbits;
+
+               // for (auto &sigbit : sig_q.bits()) {
+               for (int position =0; position < GetSize(sig_d); position += 1) {
+                       RTLIL::SigBit q_sigbit = sig_q[position];
+                       RTLIL::SigBit d_sigbit = sig_d[position];
+                       RTLIL::Const  sigbit_init_val = val_init.extract(position);
+
+                       if ((!q_sigbit.wire) || (!d_sigbit.wire)) {
+                               continue;
+                       }
+
+                       char str[1024];
+                       sprintf(str, "sat -ignore_unknown_cells -prove %s[%d] %s -set %s[%d] %s",
+                                                       log_id(d_sigbit.wire),
+                                                       d_sigbit.offset,
+                                                       sigbit_init_val.as_string().c_str(),
+                                                       log_id(q_sigbit.wire),
+                                                       q_sigbit.offset,
+                                                       sigbit_init_val.as_string().c_str()
+                                                       );
+                       log("Running: %s\n", str);
+
+                       log_flush();
+
+                       pass->call(mod->design, str);
+                       if (mod->design->scratchpad_get_bool("sat.success", false)) {
+                               sprintf(str, "connect -set %s[%d] %s",
+                                                               log_id(q_sigbit.wire),
+                                                               q_sigbit.offset,
+                                                               sigbit_init_val.as_string().c_str()
+                                                               );
+                               log("Running: %s\n", str);
+                               log_flush();
+                               pass->call(mod->design, str);
+                               // mod->connect(q_sigbit, sigbit_init_val);
+                               removed_sigbits.push_back(position);
+                       }
+               }
+
+               if (!removed_sigbits.empty()) {
+                       return true;
+               }
+       }
+
        return false;
 
 delete_dff:
@@ -467,7 +514,7 @@ struct OptRmdffPass : public Pass {
        {
                //   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
                log("\n");
-               log("    opt_rmdff [-keepdc] [selection]\n");
+               log("    opt_rmdff [-keepdc] [-sat] [selection]\n");
                log("\n");
                log("This pass identifies flip-flops with constant inputs and replaces them with\n");
                log("a constant driver.\n");
@@ -479,6 +526,7 @@ struct OptRmdffPass : public Pass {
                log_header(design, "Executing OPT_RMDFF pass (remove dff with constant values).\n");
 
                keepdc = false;
+               sat = false;
 
                size_t argidx;
                for (argidx = 1; argidx < args.size(); argidx++) {
@@ -486,6 +534,10 @@ struct OptRmdffPass : public Pass {
                                keepdc = true;
                                continue;
                        }
+                       if (args[argidx] == "-sat") {
+                               sat = true;
+                               continue;
+                       }
                        break;
                }
                extra_args(args, argidx, design);
@@ -568,7 +620,7 @@ struct OptRmdffPass : public Pass {
 
                        for (auto &id : dff_list) {
                                if (module->cell(id) != nullptr &&
-                                               handle_dff(module, module->cells_[id]))
+                                               handle_dff(module, module->cells_[id], this))
                                        total_count++;
                        }
 

diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index cbba738f06b70cf1a5832fead05034bd8970484b..453ae8cca7f55cf9e10712c5399f2550358e0d50 100644 (file)
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -1548,6 +1548,7 @@ 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");
@@ -1555,6 +1556,7 @@ struct SatPass : public Pass {
 
                        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");
@@ -1628,6 +1630,7 @@ 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();
@@ -1667,6 +1670,7 @@ struct SatPass : public Pass {
                        }
                        else
                        {
+                               design->scratchpad_set_bool("sat.success", true);
                                if (sathelper.gotTimeout)
                                        goto timeout;
                                if (rerun_counter)

diff --git a/tests/opt/opt_ff_sat.v b/tests/opt/opt_ff_sat.v
new file mode 100644 (file)
index 0000000..fc1e619
--- /dev/null
+++ b/tests/opt/opt_ff_sat.v
@@ -0,0 +1,15 @@
+module top(
+                                        input  clk,
+                                        input  a,
+                                        output b
+                                        );
+  reg                                          b_reg;
+  initial begin
+    b_reg <= 0;
+  end
+
+  assign b = b_reg;
+  always @(posedge clk) begin
+    b_reg <= a && b_reg;
+  end
+endmodule

diff --git a/tests/opt/opt_ff_sat.ys b/tests/opt/opt_ff_sat.ys
new file mode 100644 (file)
index 0000000..13e4ad2
--- /dev/null
+++ b/tests/opt/opt_ff_sat.ys
@@ -0,0 +1,4 @@
+read_verilog opt_ff_sat.v
+prep -flatten
+opt_rmdff -sat
+synth