satgen: Add support for dffe, sdff, sdffe, sdffce cells.

diff --git a/kernel/satgen.cc b/kernel/satgen.cc
index b90b43fb790861a3809eb766e792044bb367bcda..73839d37a58a36b918a6b6b48997b38febdab519 100644 (file)
--- a/kernel/satgen.cc
+++ b/kernel/satgen.cc
@@ -18,6 +18,7 @@
  */
 
 #include "kernel/satgen.h"
+#include "kernel/ff.h"
 
 USING_YOSYS_NAMESPACE
 
@@ -1075,8 +1076,14 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep)
                return true;
        }
 
-       if (timestep > 0 && cell->type.in(ID($ff), ID($dff), ID($_FF_), ID($_DFF_N_), ID($_DFF_P_)))
+       if (timestep > 0 && RTLIL::builtin_ff_cell_types().count(cell->type))
        {
+               FfData ff(nullptr, cell);
+
+               // Latches and FFs with async inputs are not supported — use clk2fflogic or async2sync first.
+               if (!ff.has_d || ff.has_arst || ff.has_sr || (ff.has_en && !ff.has_clk))
+                       return false;
+
                if (timestep == 1)
                {
                        initial_state.add((*sigmap)(cell->getPort(ID::Q)));
@@ -1084,6 +1091,51 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep)
                else
                {
                        std::vector<int> d = importDefSigSpec(cell->getPort(ID::D), timestep-1);
+                       std::vector<int> undef_d;
+                       if (model_undef)
+                               undef_d = importUndefSigSpec(cell->getPort(ID::D), timestep-1);
+                       if (ff.has_srst && ff.has_en && ff.ce_over_srst) {
+                               int srst = importDefSigSpec(ff.sig_srst, timestep-1).at(0);
+                               std::vector<int> rval = importDefSigSpec(ff.val_srst, timestep-1);
+                               int undef_srst;
+                               std::vector<int> undef_rval;
+                               if (model_undef) {
+                                       undef_srst = importUndefSigSpec(ff.sig_srst, timestep-1).at(0);
+                                       undef_rval = importUndefSigSpec(ff.val_srst, timestep-1);
+                               }
+                               if (ff.pol_srst)
+                                       std::tie(d, undef_d) = mux(srst, undef_srst, d, undef_d, rval, undef_rval);
+                               else
+                                       std::tie(d, undef_d) = mux(srst, undef_srst, rval, undef_rval, d, undef_d);
+                       }
+                       if (ff.has_en) {
+                               int en = importDefSigSpec(ff.sig_en, timestep-1).at(0);
+                               std::vector<int> old_q = importDefSigSpec(ff.sig_q, timestep-1);
+                               int undef_en;
+                               std::vector<int> undef_old_q;
+                               if (model_undef) {
+                                       undef_en = importUndefSigSpec(ff.sig_en, timestep-1).at(0);
+                                       undef_old_q = importUndefSigSpec(ff.sig_q, timestep-1);
+                               }
+                               if (ff.pol_en)
+                                       std::tie(d, undef_d) = mux(en, undef_en, old_q, undef_old_q, d, undef_d);
+                               else
+                                       std::tie(d, undef_d) = mux(en, undef_en, d, undef_d, old_q, undef_old_q);
+                       }
+                       if (ff.has_srst && !(ff.has_en && ff.ce_over_srst)) {
+                               int srst = importDefSigSpec(ff.sig_srst, timestep-1).at(0);
+                               std::vector<int> rval = importDefSigSpec(ff.val_srst, timestep-1);
+                               int undef_srst;
+                               std::vector<int> undef_rval;
+                               if (model_undef) {
+                                       undef_srst = importUndefSigSpec(ff.sig_srst, timestep-1).at(0);
+                                       undef_rval = importUndefSigSpec(ff.val_srst, timestep-1);
+                               }
+                               if (ff.pol_srst)
+                                       std::tie(d, undef_d) = mux(srst, undef_srst, d, undef_d, rval, undef_rval);
+                               else
+                                       std::tie(d, undef_d) = mux(srst, undef_srst, rval, undef_rval, d, undef_d);
+                       }
                        std::vector<int> q = importDefSigSpec(cell->getPort(ID::Q), timestep);
 
                        std::vector<int> qq = model_undef ? ez->vec_var(q.size()) : q;
@@ -1091,7 +1143,6 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep)
 
                        if (model_undef)
                        {
-                               std::vector<int> undef_d = importUndefSigSpec(cell->getPort(ID::D), timestep-1);
                                std::vector<int> undef_q = importUndefSigSpec(cell->getPort(ID::Q), timestep);
 
                                ez->assume(ez->vec_eq(undef_d, undef_q));
@@ -1182,7 +1233,7 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep)
                return true;
        }
 
-       // Unsupported internal cell types: $pow $lut
-       // .. and all sequential cells except $dff and $_DFF_[NP]_
+       // Unsupported internal cell types: $pow $fsm $mem*
+       // .. and all sequential cells with asynchronous inputs
        return false;
 }

diff --git a/kernel/satgen.h b/kernel/satgen.h
index bd6259ba145a92b994d5e16f50d4294d6efc11cd..cf2db733f8727053d3cce9ceb0fff4f1737a64f8 100644 (file)
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -262,6 +262,18 @@ struct SatGen
                }
        }
 
+       std::pair<std::vector<int>, std::vector<int>> mux(int s, int undef_s, const std::vector<int> &a, const std::vector<int> &undef_a, const std::vector<int> &b, const std::vector<int> &undef_b) {
+               std::vector<int> res;
+               std::vector<int> undef_res;
+               res = ez->vec_ite(s, b, a);
+               if (model_undef) {
+                       std::vector<int> unequal_ab = ez->vec_not(ez->vec_iff(a, b));
+                       std::vector<int> undef_ab = ez->vec_or(unequal_ab, ez->vec_or(undef_a, undef_b));
+                       undef_res = ez->vec_ite(undef_s, undef_ab, ez->vec_ite(s, undef_b, undef_a));
+               }
+               return std::make_pair(res, undef_res);
+       }
+
        void undefGating(int y, int yy, int undef)
        {
                ez->assume(ez->OR(undef, ez->IFF(y, yy)));

diff --git a/tests/arch/xilinx/pmgen_xilinx_srl.ys b/tests/arch/xilinx/pmgen_xilinx_srl.ys
index e76fb20ab3d2c84ae90c481dcc7c69165b0f9c2b..9a5e70ea9ef61206b88f97bf1db9841e4e2a897e 100644 (file)
--- a/tests/arch/xilinx/pmgen_xilinx_srl.ys
+++ b/tests/arch/xilinx/pmgen_xilinx_srl.ys
@@ -35,7 +35,6 @@ design -stash gate
 
 design -copy-from gold -as gold pmtest_xilinx_srl_pm_fixed
 design -copy-from gate -as gate pmtest_xilinx_srl_pm_fixed
-dff2dffe -unmap # sat does not support flops-with-enable yet
 miter -equiv -flatten -make_assert gold gate miter
 sat -set-init-zero -seq 5 -verify -prove-asserts miter
 
@@ -52,6 +51,5 @@ design -stash gate
 
 design -copy-from gold -as gold pmtest_xilinx_srl_pm_variable
 design -copy-from gate -as gate pmtest_xilinx_srl_pm_variable
-dff2dffe -unmap # sat does not support flops-with-enable yet
 miter -equiv -flatten -make_assert gold gate miter
 sat -set-init-zero -seq 5 -verify -prove-asserts miter

diff --git a/tests/sat/dff.ys b/tests/sat/dff.ys
new file mode 100644 (file)
index 0000000..ba36258
--- /dev/null
+++ b/tests/sat/dff.ys
@@ -0,0 +1,21 @@
+# Ensure all sync-only DFFs have usable SAT models.
+
+read_verilog -icells <<EOT
+
+module top(...);
+
+input C, D, R, E;
+output [4:0] Q;
+
+\$dff #(.WIDTH(1), .CLK_POLARITY(1'b1)) ff0 (.CLK(C), .D(D), .Q(Q[0]));
+\$dffe #(.WIDTH(1), .CLK_POLARITY(1'b1), .EN_POLARITY(1'b1)) ff1 (.CLK(C), .D(D), .EN(E), .Q(Q[1]));
+\$sdff #(.WIDTH(1), .CLK_POLARITY(1'b1), .SRST_POLARITY(1'b1), .SRST_VALUE(1'b0)) ff2 (.CLK(C), .D(D), .SRST(R), .Q(Q[2]));
+\$sdffe #(.WIDTH(1), .CLK_POLARITY(1'b1), .SRST_POLARITY(1'b1), .SRST_VALUE(1'b0), .EN_POLARITY(1'b1)) ff3 (.CLK(C), .D(D), .EN(E), .SRST(R), .Q(Q[3]));
+\$sdffce #(.WIDTH(1), .CLK_POLARITY(1'b1), .SRST_POLARITY(1'b1), .SRST_VALUE(1'b0), .EN_POLARITY(1'b1)) ff4 (.CLK(C), .D(D), .EN(E), .SRST(R), .Q(Q[4]));
+
+endmodule
+
+EOT
+
+# This ensures that 1) coarse cells have SAT models, 2) fine cells have SAT models, 3) they're equivalent
+equiv_opt -assert simplemap