mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-08-08 12:11:24 +00:00
Code Activity

Add bitwise $bweqx and $bwmux cells

Browse source 
The new bitwise case equality (`$bweqx`) and bitwise mux (`$bwmux`)
cells enable compact encoding and decoding of 3-valued logic signals
using multiple 2-valued signals.
This commit is contained in:
Jannis Harder 2022-11-02 17:12:51 +01:00
parent f2c531e65f
commit 7203ba7bc1
9 changed files with 179 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

36
kernel/satgen.cc
View file

@ -223,7 +223,33 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep)
return true;
}
if (cell->type.in(ID($_MUX_), ID($mux), ID($_NMUX_)))
if (cell->type == ID($bweqx))
{
std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
std::vector<int> b = importDefSigSpec(cell->getPort(ID::B), timestep);
std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
std::vector<int> bweqx = ez->vec_not(ez->vec_xor(a, b));
if (model_undef)
{
std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
std::vector<int> undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep);
std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
std::vector<int> both_undef = ez->vec_and(undef_a, undef_b);
std::vector<int> both_def = ez->vec_and(ez->vec_not(undef_a), ez->vec_not(undef_b));
bweqx = ez->vec_or(both_undef, ez->vec_and(both_def, bweqx));
for (int yx : undef_y)
ez->assume(ez->NOT(yx));
}
ez->assume(ez->vec_eq(bweqx, y));
return true;
}
if (cell->type.in(ID($_MUX_), ID($mux), ID($_NMUX_), ID($bwmux)))
{
std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
std::vector<int> b = importDefSigSpec(cell->getPort(ID::B), timestep);
@ -233,6 +259,8 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep)
std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
if (cell->type == ID($_NMUX_))
ez->assume(ez->vec_eq(ez->vec_not(ez->vec_ite(s.at(0), b, a)), yy));
else if (cell->type == ID($bwmux))
ez->assume(ez->vec_eq(ez->vec_ite(s, b, a), yy));
else
ez->assume(ez->vec_eq(ez->vec_ite(s.at(0), b, a), yy));
@ -245,7 +273,11 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep)
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));
std::vector<int> yX = ez->vec_ite(undef_s.at(0), undef_ab, ez->vec_ite(s.at(0), undef_b, undef_a));
std::vector<int> yX;
if (cell->type == ID($bwmux))
yX = ez->vec_ite(undef_s, undef_ab, ez->vec_ite(s, undef_b, undef_a));
else
yX = ez->vec_ite(undef_s.at(0), undef_ab, ez->vec_ite(s.at(0), undef_b, undef_a));
ez->assume(ez->vec_eq(yX, undef_y));
undefGating(y, yy, undef_y);
}