From 0c6d0d4b5dc7c0b19bcca3f63a95b97a9df703d9 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Marcelina=20Ko=C5=9Bcielnicka?= Date: Mon, 20 Jul 2020 22:49:30 +0200 Subject: [PATCH] satgen: Add support for dffe, sdff, sdffe, sdffce cells. --- kernel/satgen.cc | 59 +++++++++++++++++++++++++-- kernel/satgen.h | 12 ++++++ tests/arch/xilinx/pmgen_xilinx_srl.ys | 2 - tests/sat/dff.ys | 21 ++++++++++ 4 files changed, 88 insertions(+), 6 deletions(-) create mode 100644 tests/sat/dff.ys diff --git a/kernel/satgen.cc b/kernel/satgen.cc index b90b43fb7..73839d37a 100644 --- 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 d = importDefSigSpec(cell->getPort(ID::D), timestep-1); + std::vector 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 rval = importDefSigSpec(ff.val_srst, timestep-1); + int undef_srst; + std::vector 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 old_q = importDefSigSpec(ff.sig_q, timestep-1); + int undef_en; + std::vector 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 rval = importDefSigSpec(ff.val_srst, timestep-1); + int undef_srst; + std::vector 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 q = importDefSigSpec(cell->getPort(ID::Q), timestep); std::vector 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 undef_d = importUndefSigSpec(cell->getPort(ID::D), timestep-1); std::vector 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 bd6259ba1..cf2db733f 100644 --- a/kernel/satgen.h +++ b/kernel/satgen.h @@ -262,6 +262,18 @@ struct SatGen } } + std::pair, std::vector> mux(int s, int undef_s, const std::vector &a, const std::vector &undef_a, const std::vector &b, const std::vector &undef_b) { + std::vector res; + std::vector undef_res; + res = ez->vec_ite(s, b, a); + if (model_undef) { + std::vector unequal_ab = ez->vec_not(ez->vec_iff(a, b)); + std::vector 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 e76fb20ab..9a5e70ea9 100644 --- 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 index 000000000..ba3625871 --- /dev/null +++ b/tests/sat/dff.ys @@ -0,0 +1,21 @@ +# Ensure all sync-only DFFs have usable SAT models. + +read_verilog -icells <