aboutsummaryrefslogtreecommitdiffstats
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/ff.h46
-rw-r--r--kernel/ffinit.h43
-rw-r--r--kernel/satgen.cc59
-rw-r--r--kernel/satgen.h12
4 files changed, 132 insertions, 28 deletions
diff --git a/kernel/ff.h b/kernel/ff.h
index 8dc83eb49..0aecbaa2a 100644
--- a/kernel/ff.h
+++ b/kernel/ff.h
@@ -323,6 +323,52 @@ struct FfData {
return res;
}
+ void unmap_ce(Module *module) {
+ if (!has_en)
+ return;
+ log_assert(has_clk);
+ if (has_srst && ce_over_srst)
+ unmap_srst(module);
+
+ if (!is_fine) {
+ if (pol_en)
+ sig_d = module->Mux(NEW_ID, sig_q, sig_d, sig_en);
+ else
+ sig_d = module->Mux(NEW_ID, sig_d, sig_q, sig_en);
+ } else {
+ if (pol_en)
+ sig_d = module->MuxGate(NEW_ID, sig_q, sig_d, sig_en);
+ else
+ sig_d = module->MuxGate(NEW_ID, sig_d, sig_q, sig_en);
+ }
+ has_en = false;
+ }
+
+ void unmap_srst(Module *module) {
+ if (!has_srst)
+ return;
+ if (has_en && !ce_over_srst)
+ unmap_ce(module);
+
+ if (!is_fine) {
+ if (pol_srst)
+ sig_d = module->Mux(NEW_ID, sig_d, val_srst, sig_srst);
+ else
+ sig_d = module->Mux(NEW_ID, val_srst, sig_d, sig_srst);
+ } else {
+ if (pol_srst)
+ sig_d = module->MuxGate(NEW_ID, sig_d, val_srst[0], sig_srst);
+ else
+ sig_d = module->MuxGate(NEW_ID, val_srst[0], sig_d, sig_srst);
+ }
+ has_srst = false;
+ }
+
+ void unmap_ce_srst(Module *module) {
+ unmap_ce(module);
+ unmap_srst(module);
+ }
+
Cell *emit(Module *module, IdString name) {
if (!width)
return nullptr;
diff --git a/kernel/ffinit.h b/kernel/ffinit.h
index 49747692f..025b0c862 100644
--- a/kernel/ffinit.h
+++ b/kernel/ffinit.h
@@ -83,22 +83,24 @@ struct FfInitVals
void set_init(RTLIL::SigBit bit, RTLIL::State val)
{
- bit = (*sigmap)(bit);
- auto it = initbits.find(bit);
- if (it != initbits.end()) {
- auto it2 = it->second.second.wire->attributes.find(ID::init);
- it2->second[it->second.second.offset] = val;
- } else {
- log_assert(bit.wire);
- initbits[bit] = std::make_pair(val,bit);
- auto it2 = bit.wire->attributes.find(ID::init);
- if (it2 != bit.wire->attributes.end()) {
- it2->second[bit.offset] = val;
- } else {
- Const cval(State::Sx, GetSize(bit.wire));
- cval[bit.offset] = val;
- bit.wire->attributes[ID::init] = cval;
- }
+ SigBit mbit = (*sigmap)(bit);
+ SigBit abit = bit;
+ auto it = initbits.find(mbit);
+ if (it != initbits.end())
+ abit = it->second.second;
+ else if (val == State::Sx)
+ return;
+ log_assert(abit.wire);
+ initbits[mbit] = std::make_pair(val,abit);
+ auto it2 = abit.wire->attributes.find(ID::init);
+ if (it2 != abit.wire->attributes.end()) {
+ it2->second[abit.offset] = val;
+ if (it2->second.is_fully_undef())
+ abit.wire->attributes.erase(it2);
+ } else if (val != State::Sx) {
+ Const cval(State::Sx, GetSize(abit.wire));
+ cval[abit.offset] = val;
+ abit.wire->attributes[ID::init] = cval;
}
}
@@ -111,14 +113,7 @@ struct FfInitVals
void remove_init(RTLIL::SigBit bit)
{
- auto it = initbits.find((*sigmap)(bit));
- if (it != initbits.end()) {
- auto it2 = it->second.second.wire->attributes.find(ID::init);
- it2->second[it->second.second.offset] = State::Sx;
- if (it2->second.is_fully_undef())
- it->second.second.wire->attributes.erase(it2);
- initbits.erase(it);
- }
+ set_init(bit, State::Sx);
}
void remove_init(const RTLIL::SigSpec &sig)
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<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 bd6259ba1..cf2db733f 100644
--- 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)));
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-27 18:47:47 +0000