mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-06-06 22:23:23 +00:00
Code Activity

Add $bmux and $demux cells.

Browse source
This commit is contained in:
Marcelina Kościelnicka 2022-01-24 16:02:29 +01:00
parent db33b1e535
commit 93508d58da
25 changed files with 694 additions and 49 deletions
Download patch file Download diff file Expand all files Collapse all files

100
kernel/satgen.cc
View file

@ -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);