clk2fflogic: work for bit-level $_DFF_* and $_DFFSR_*

diff --git a/passes/sat/clk2fflogic.cc b/passes/sat/clk2fflogic.cc
index 4bb4aa04762ec646d7736abd8ce15b3a5cec8585..f9e7783a906e64ddf424eb0abe3c11f1142eb3f6 100644 (file)
--- a/passes/sat/clk2fflogic.cc
+++ b/passes/sat/clk2fflogic.cc
@@ -214,14 +214,38 @@ struct Clk2fflogicPass : public Pass {
                                        continue;
                                }
 
-                               if (cell->type.in("$dff", "$adff", "$dffsr"))
+                               bool word_dff = cell->type.in("$dff", "$adff", "$dffsr");
+                               if (word_dff || cell->type.in(ID($_DFF_N_), ID($_DFF_P_),
+                                               ID($_DFF_NN0_), ID($_DFF_NN1_), ID($_DFF_NP0_), ID($_DFF_NP1_),
+                                               ID($_DFF_PP0_), ID($_DFF_PP1_), ID($_DFF_PN0_), ID($_DFF_PN1_),
+                                               ID($_DFFSR_NNN_), ID($_DFFSR_NNP_), ID($_DFFSR_NPN_), ID($_DFFSR_NPP_),
+                                               ID($_DFFSR_PNN_), ID($_DFFSR_PNP_), ID($_DFFSR_PPN_), ID($_DFFSR_PPP_)))
                                {
-                                       bool clkpol = cell->parameters["\\CLK_POLARITY"].as_bool();
+                                       bool clkpol;
+                                       SigSpec clk;
+                                       if (word_dff) {
+                                               clkpol = cell->parameters["\\CLK_POLARITY"].as_bool();
+                                               clk = cell->getPort("\\CLK");
+                                       }
+                                       else {
+                                               if (cell->type.in(ID($_DFF_P_), ID($_DFF_N_),
+                                                                       ID($_DFF_NN0_), ID($_DFF_NN1_), ID($_DFF_NP0_), ID($_DFF_NP1_),
+                                                                       ID($_DFF_PP0_), ID($_DFF_PP1_), ID($_DFF_PN0_), ID($_DFF_PN1_)))
+                                                       clkpol = cell->type[6] == 'P';
+                                               else if (cell->type.in(ID($_DFFSR_NNN_), ID($_DFFSR_NNP_), ID($_DFFSR_NPN_), ID($_DFFSR_NPP_),
+                                                                       ID($_DFFSR_PNN_), ID($_DFFSR_PNP_), ID($_DFFSR_PPN_), ID($_DFFSR_PPP_)))
+                                                       clkpol = cell->type[8] == 'P';
+                                               else log_abort();
+                                               clk = cell->getPort("\\C");
+                                       }
 
-                                       SigSpec clk = cell->getPort("\\CLK");
                                        Wire *past_clk = module->addWire(NEW_ID);
                                        past_clk->attributes["\\init"] = clkpol ? State::S1 : State::S0;
-                                       module->addFf(NEW_ID, clk, past_clk);
+
+                                       if (word_dff)
+                                               module->addFf(NEW_ID, clk, past_clk);
+                                       else
+                                               module->addFfGate(NEW_ID, clk, past_clk);
 
                                        SigSpec sig_d = cell->getPort("\\D");
                                        SigSpec sig_q = cell->getPort("\\Q");
@@ -244,8 +268,14 @@ struct Clk2fflogicPass : public Pass {
 
                                        Wire *past_d = module->addWire(NEW_ID, GetSize(sig_d));
                                        Wire *past_q = module->addWire(NEW_ID, GetSize(sig_q));
-                                       module->addFf(NEW_ID, sig_d, past_d);
-                                       module->addFf(NEW_ID, sig_q, past_q);
+                                       if (word_dff) {
+                                               module->addFf(NEW_ID, sig_d, past_d);
+                                               module->addFf(NEW_ID, sig_q, past_q);
+                                       }
+                                       else {
+                                               module->addFfGate(NEW_ID, sig_d, past_d);
+                                               module->addFfGate(NEW_ID, sig_q, past_q);
+                                       }
 
                                        if (cell->type == "$adff")
                                        {
@@ -266,6 +296,26 @@ struct Clk2fflogicPass : public Pass {
                                                        module->addMux(NEW_ID, rstval, qval, arst, sig_q);
                                        }
                                        else
+                                       if (cell->type.in(ID($_DFF_NN0_), ID($_DFF_NN1_), ID($_DFF_NP0_), ID($_DFF_NP1_),
+                                               ID($_DFF_PP0_), ID($_DFF_PP1_), ID($_DFF_PN0_), ID($_DFF_PN1_)))
+                                       {
+                                               SigSpec arst = cell->getPort("\\R");
+                                               SigSpec qval = module->MuxGate(NEW_ID, past_q, past_d, clock_edge);
+                                               SigBit rstval = (cell->type[8] == '1');
+
+                                               Wire *past_arst = module->addWire(NEW_ID);
+                                               module->addFfGate(NEW_ID, arst, past_arst);
+                                               if (cell->type[7] == 'P')
+                                                       arst = module->OrGate(NEW_ID, arst, past_arst);
+                                               else
+                                                       arst = module->AndGate(NEW_ID, arst, past_arst);
+
+                                               if (cell->type[7] == 'P')
+                                                       module->addMuxGate(NEW_ID, qval, rstval, arst, sig_q);
+                                               else
+                                                       module->addMuxGate(NEW_ID, rstval, qval, arst, sig_q);
+                                       }
+                                       else
                                        if (cell->type == "$dffsr")
                                        {
                                                SigSpec qval = module->Mux(NEW_ID, past_q, past_d, clock_edge);
@@ -282,9 +332,30 @@ struct Clk2fflogicPass : public Pass {
                                                module->addAnd(NEW_ID, qval, clrval, sig_q);
                                        }
                                        else
+                                       if (cell->type.in(ID($_DFFSR_NNN_), ID($_DFFSR_NNP_), ID($_DFFSR_NPN_), ID($_DFFSR_NPP_),
+                                               ID($_DFFSR_PNN_), ID($_DFFSR_PNP_), ID($_DFFSR_PPN_), ID($_DFFSR_PPP_)))
+                                       {
+                                               SigSpec qval = module->MuxGate(NEW_ID, past_q, past_d, clock_edge);
+                                               SigSpec setval = cell->getPort("\\S");
+                                               SigSpec clrval = cell->getPort("\\R");
+
+                                               if (cell->type[9] != 'P')
+                                                       setval = module->Not(NEW_ID, setval);
+
+                                               if (cell->type[10] == 'P')
+                                                       clrval = module->Not(NEW_ID, clrval);
+
+                                               qval = module->OrGate(NEW_ID, qval, setval);
+                                               module->addAndGate(NEW_ID, qval, clrval, sig_q);
+                                       }
+                                       else if (cell->type == "$dff")
                                        {
                                                module->addMux(NEW_ID, past_q, past_d, clock_edge, sig_q);
                                        }
+                                       else
+                                       {
+                                               module->addMuxGate(NEW_ID, past_q, past_d, clock_edge, sig_q);
+                                       }
 
                                        Const initval;
                                        bool assign_initval = false;

diff --git a/tests/sat/clk2fflogic.ys b/tests/sat/clk2fflogic.ys
new file mode 100644 (file)
index 0000000..cdbeb02
--- /dev/null
+++ b/tests/sat/clk2fflogic.ys
@@ -0,0 +1,39 @@
+read_verilog <<EOT
+module top(input clk, d, s, r, output reg [17:0] q);
+always @(posedge clk or posedge s) if ( s) q[ 0] <= 1'b1; else q[ 0] <= d;
+always @(posedge clk or negedge s) if (!s) q[ 1] <= 1'b1; else q[ 1] <= d;
+always @(posedge clk or posedge r) if ( r) q[ 2] <= 1'b0; else q[ 2] <= d;
+always @(posedge clk or negedge r) if (!r) q[ 3] <= 1'b0; else q[ 3] <= d;
+always @(negedge clk or posedge s) if ( s) q[ 4] <= 1'b1; else q[ 4] <= d;
+always @(negedge clk or negedge s) if (!s) q[ 5] <= 1'b1; else q[ 5] <= d;
+always @(negedge clk or posedge r) if ( r) q[ 6] <= 1'b0; else q[ 6] <= d;
+always @(negedge clk or negedge r) if (!r) q[ 7] <= 1'b0; else q[ 7] <= d;
+
+always @(posedge clk or posedge s or posedge r) if ( r) q[ 8] <= 1'b0; else if ( s) q[ 8] <= 1'b1; else q[ 8] <= d;
+always @(posedge clk or posedge s or negedge r) if (!r) q[ 9] <= 1'b0; else if ( s) q[ 9] <= 1'b1; else q[ 9] <= d;
+always @(posedge clk or negedge s or posedge r) if ( r) q[10] <= 1'b0; else if (!s) q[10] <= 1'b1; else q[10] <= d;
+always @(posedge clk or negedge s or negedge r) if (!r) q[11] <= 1'b0; else if (!s) q[11] <= 1'b1; else q[11] <= d;
+always @(negedge clk or posedge s or posedge r) if ( r) q[12] <= 1'b0; else if ( s) q[12] <= 1'b1; else q[12] <= d;
+always @(negedge clk or posedge s or negedge r) if (!r) q[13] <= 1'b0; else if ( s) q[13] <= 1'b1; else q[13] <= d;
+always @(negedge clk or negedge s or posedge r) if ( r) q[14] <= 1'b0; else if (!s) q[14] <= 1'b1; else q[14] <= d;
+always @(negedge clk or negedge s or negedge r) if (!r) q[15] <= 1'b0; else if (!s) q[15] <= 1'b1; else q[15] <= d;
+
+always @(posedge clk) q[16] <= d;
+always @(negedge clk) q[17] <= d;
+endmodule
+EOT
+proc
+select -assert-count 8 t:$adff
+select -assert-count 8 t:$dffsr
+select -assert-count 2 t:$dff
+design -save gold
+
+simplemap
+design -stash gate
+
+design -import gold -as gold
+design -import gate -as gate
+clk2fflogic
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports -set-init-undef -seq 10 miter