From 5cbfa76dc35589f11a022e1b07aede5cee4b480c Mon Sep 17 00:00:00 2001 From: agentic-synthesis Date: Sat, 8 Aug 2026 10:21:19 +0200 Subject: [PATCH] lutpack: do not trust an approximate cofactor support in the MUX split `lutpack` aborts on some networks with abc: src/opt/lpk/lpkAbcMux.c:192: Lpk_MuxSplit: Assertion `iVarVac < (int)p->nVars' failed. Reproducer (a 24.7k-LUT `sqrt` netlist produced by `if -K 10 -Z 6`, ~10 s): read_blif sqrt-mapped.blif; lutpack Lpk_MuxSplit() splits one component off a function and stores the new component in a *vacant* fanin slot of the retained one: p->uSupp = Kit_TruthSupport( Pol ? pTruth1 : pTruth0, p->nVars ); p->uSupp |= (1 << Var); iVarVac = Kit_WordFindFirstBit( ~p->uSupp ); assert( iVarVac < (int)p->nVars ); A vacant slot is supposed to be guaranteed by Lpk_MuxAnalize(), which rejects a candidate variable when nSuppSizeL = max(nSuppSize0 + 2*!Polarity, nSuppSize1 + 2*Polarity) > p->nVars but it reads nSuppSize0/nSuppSize1 out of the *cached* p->puSupps[]. When those came from Lpk_ComputeSupports() they are not exact: that routine builds two BDDs of the function in opposite variable orders and stitches the two support estimates together at the cofactoring variable, and the result can be a strict subset of the true cofactor support. Lpk_MuxAnalize() then admits a variable whose split needs one slot more than the function has. On the reproducer this happens for a 12-variable component at Var = 3, Polarity = 1: the cached support of cofactor 1 is 0x3f7 (9 variables) while the truth table's is 0xff7 (11). The guard sees 9 + 2 = 11 <= 12 and accepts; the split then produces uSupp = 0xff7 | (1 << 3) = 0xfff, which is full. Instrumenting the same run shows the estimate differs from the exact support in 484 of 101970 cofactor supports, and is narrower in 352 of them, so this is not a one-off. Rather than change the support estimator or weaken the assertion -- which documents a real invariant of Lpk_MuxSplit() -- re-derive the single support the split depends on, once the candidate has been chosen, and decline the MUX decomposition when it does not fit. That is one cofactor and one support scan per accepted candidate, not per candidate variable. On the reproducer lutpack then completes and yields the same result as recomputing every cached support from the truth table (24694 -> 24635 nodes, 237 levels in both cases). --- src/opt/lpk/lpkAbcDec.c | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/src/opt/lpk/lpkAbcDec.c b/src/opt/lpk/lpkAbcDec.c index b7d4ccb1f..08d1daf30 100644 --- a/src/opt/lpk/lpkAbcDec.c +++ b/src/opt/lpk/lpkAbcDec.c @@ -202,6 +202,24 @@ pMan->timeEvalMuxAn += Abc_Clock() - clk; assert( pResMux == NULL || pResDsd == NULL ); if ( pResMux ) { + // Lpk_MuxAnalize() decides feasibility from the cached cofactor supports in + // p->puSupps. Those may have come from Lpk_ComputeSupports(), which derives + // them from two BDDs built in opposite variable orders and stitches the halves + // together, and that estimate can be a strict SUBSET of the true cofactor + // support. When it is, the component retained by the split below ends up with + // no vacant fanin slot for the component that is split off, and Lpk_MuxSplit() + // fails its assertion `iVarVac < (int)p->nVars'. Re-derive the one support the + // split actually depends on and decline the MUX decomposition if it does not fit. + unsigned * pTruthThis = Lpk_FunTruth( p, 0 ); + unsigned * pTruthCof = Lpk_FunTruth( p, 1 ); + unsigned uSuppExact; + if ( pResMux->Polarity ) + Kit_TruthCofactor1New( pTruthCof, pTruthThis, p->nVars, pResMux->Variable ); + else + Kit_TruthCofactor0New( pTruthCof, pTruthThis, p->nVars, pResMux->Variable ); + uSuppExact = Kit_TruthSupport( pTruthCof, p->nVars ) | ( 1 << pResMux->Variable ); + if ( Kit_WordCountOnes( uSuppExact ) >= (int)p->nVars ) + return 0; clk = Abc_Clock(); p2 = Lpk_MuxSplit( pMan, p, pResMux->Variable, pResMux->Polarity ); pMan->timeEvalMuxSp += Abc_Clock() - clk;