3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-24 01:25:33 +00:00

Merge pull request #5025 from povik/fix-macc_v2-satgen

satgen: Fix $macc_v2 x-prop
This commit is contained in:
KrystalDelusion 2025-04-22 08:55:28 +12:00 committed by GitHub
commit 1f32f980cd
No known key found for this signature in database
GPG key ID: B5690EEEBB952194

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