From f8e67c7a081f2eaf3500b13e6f071e463da5bf8f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Tue, 15 Apr 2025 10:31:42 +0200 Subject: [PATCH] satgen: Fix $macc_v2 x-prop --- kernel/satgen.cc | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/kernel/satgen.cc b/kernel/satgen.cc index 9e5fa9111..a161adb5b 100644 --- a/kernel/satgen.cc +++ b/kernel/satgen.cc @@ -788,12 +788,18 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep) { std::vector undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep); std::vector undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep); + std::vector 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 undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep); - ez->assume(ez->vec_eq(undef_y, std::vector(GetSize(y), ez->OR(undef_any_a, undef_any_b)))); + ez->assume(ez->vec_eq(undef_y, std::vector(GetSize(y), undef_any))); undefGating(y, tmp, undef_y); }