aboutsummaryrefslogtreecommitdiffstats
path: root/kernel/satgen.cc
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/satgen.cc')
-rw-r--r--kernel/satgen.cc122
1 files changed, 111 insertions, 11 deletions
diff --git a/kernel/satgen.cc b/kernel/satgen.cc
index 2a54e78ec..9c40ec66d 100644
--- a/kernel/satgen.cc
+++ b/kernel/satgen.cc
@@ -1,7 +1,7 @@
/*
* yosys -- Yosys Open SYnthesis Suite
*
- * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
+ * Copyright (C) 2012 Claire Xenia Wolf <claire@yosyshq.com>
*
* Permission to use, copy, modify, and/or distribute this software for any
* purpose with or without fee is hereby granted, provided that the above
@@ -252,6 +252,106 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep)
return true;
}
+ if (cell->type == ID($bmux))
+ {
+ std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> s = importDefSigSpec(cell->getPort(ID::S), timestep);
+ std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
+ std::vector<int> undef_a, undef_s, undef_y;
+
+ if (model_undef)
+ {
+ undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
+ undef_s = importUndefSigSpec(cell->getPort(ID::S), timestep);
+ undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
+ }
+
+ if (GetSize(s) == 0) {
+ ez->vec_set(a, y);
+ if (model_undef)
+ ez->vec_set(undef_a, undef_y);
+ } else {
+ for (int i = GetSize(s)-1; i >= 0; i--)
+ {
+ std::vector<int> out = (i == 0) ? y : ez->vec_var(a.size() / 2);
+ std::vector<int> yy = model_undef ? ez->vec_var(out.size()) : out;
+
+ std::vector<int> a0(a.begin(), a.begin() + a.size() / 2);
+ std::vector<int> a1(a.begin() + a.size() / 2, a.end());
+ ez->assume(ez->vec_eq(ez->vec_ite(s.at(i), a1, a0), yy));
+
+ if (model_undef)
+ {
+ std::vector<int> undef_out = (i == 0) ? undef_y : ez->vec_var(a.size() / 2);
+ std::vector<int> undef_a0(undef_a.begin(), undef_a.begin() + a.size() / 2);
+ std::vector<int> undef_a1(undef_a.begin() + a.size() / 2, undef_a.end());
+ std::vector<int> unequal_ab = ez->vec_not(ez->vec_iff(a0, a1));
+ std::vector<int> undef_ab = ez->vec_or(unequal_ab, ez->vec_or(undef_a0, undef_a1));
+ std::vector<int> yX = ez->vec_ite(undef_s.at(i), undef_ab, ez->vec_ite(s.at(i), undef_a1, undef_a0));
+ ez->assume(ez->vec_eq(yX, undef_out));
+ undefGating(out, yy, undef_out);
+
+ undef_a = undef_out;
+ }
+
+ a = out;
+ }
+ }
+ return true;
+ }
+
+ if (cell->type == ID($demux))
+ {
+ std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
+ std::vector<int> s = importDefSigSpec(cell->getPort(ID::S), timestep);
+ std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
+ std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
+ std::vector<int> undef_a, undef_s, undef_y;
+
+ if (model_undef)
+ {
+ undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
+ undef_s = importUndefSigSpec(cell->getPort(ID::S), timestep);
+ undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
+ }
+
+ if (GetSize(s) == 0) {
+ ez->vec_set(a, y);
+ if (model_undef)
+ ez->vec_set(undef_a, undef_y);
+ } else {
+ for (int i = 0; i < (1 << GetSize(s)); i++)
+ {
+ std::vector<int> ss;
+ for (int j = 0; j < GetSize(s); j++) {
+ if (i & 1 << j)
+ ss.push_back(s[j]);
+ else
+ ss.push_back(ez->NOT(s[j]));
+ }
+ int sss = ez->expression(ezSAT::OpAnd, ss);
+
+ for (int j = 0; j < GetSize(a); j++) {
+ ez->SET(ez->AND(sss, a[j]), yy.at(i * GetSize(a) + j));
+ }
+
+ if (model_undef)
+ {
+ int s0 = ez->expression(ezSAT::OpOr, ez->vec_and(ez->vec_not(ss), ez->vec_not(undef_s)));
+ int us = ez->AND(ez->NOT(s0), ez->expression(ezSAT::OpOr, undef_s));
+ for (int j = 0; j < GetSize(a); j++) {
+ int a0 = ez->AND(ez->NOT(a[j]), ez->NOT(undef_a[j]));
+ int yX = ez->AND(ez->OR(us, undef_a[j]), ez->NOT(ez->OR(s0, a0)));
+ ez->SET(yX, undef_y.at(i * GetSize(a) + j));
+ }
+ }
+ }
+ if (model_undef)
+ undefGating(y, yy, undef_y);
+ }
+ return true;
+ }
+
if (cell->type == ID($pmux))
{
std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
@@ -1081,7 +1181,7 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep)
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))
+ if (ff.has_aload || ff.has_arst || ff.has_sr)
return false;
if (timestep == 1)
@@ -1094,7 +1194,7 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep)
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) {
+ if (ff.has_srst && ff.has_ce && 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;
@@ -1108,21 +1208,21 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep)
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);
+ if (ff.has_ce) {
+ int ce = importDefSigSpec(ff.sig_ce, timestep-1).at(0);
std::vector<int> old_q = importDefSigSpec(ff.sig_q, timestep-1);
- int undef_en;
+ int undef_ce;
std::vector<int> undef_old_q;
if (model_undef) {
- undef_en = importUndefSigSpec(ff.sig_en, timestep-1).at(0);
+ undef_ce = importUndefSigSpec(ff.sig_ce, 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);
+ if (ff.pol_ce)
+ std::tie(d, undef_d) = mux(ce, undef_ce, 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);
+ std::tie(d, undef_d) = mux(ce, undef_ce, d, undef_d, old_q, undef_old_q);
}
- if (ff.has_srst && !(ff.has_en && ff.ce_over_srst)) {
+ if (ff.has_srst && !(ff.has_ce && 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;
generated by cgit v1.2.3 (git 2.25.1) at 2025-02-22 00:16:58 +0000