mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-20 07:36:39 +00:00
Code Activity

satgen: Fix $macc_v2 x-prop

Browse source
This commit is contained in:
Martin Povišer 2025-04-15 10:31:42 +02:00
parent 05cd1e2942
commit f8e67c7a08
1 changed files with 7 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
kernel/satgen.cc
View file

@ -788,12 +788,18 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep)
{
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_c;
if (cell->type == ID($macc_v2))
undef_c = importUndefSigSpec(cell->getPort(ID::C), timestep);
int undef_any_a = ez->expression(ezSAT::OpOr, undef_a);
int undef_any_b = ez->expression(ezSAT::OpOr, undef_b);
int undef_any_c = ez->expression(ezSAT::OpOr, undef_c);
int undef_any = ez->OR(undef_any_a, ez->OR(undef_any_b, undef_any_c));
std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
ez->assume(ez->vec_eq(undef_y, std::vector<int>(GetSize(y), ez->OR(undef_any_a, undef_any_b))));
ez->assume(ez->vec_eq(undef_y, std::vector<int>(GetSize(y), undef_any)));
undefGating(y, tmp, undef_y);
}