luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Merge pull request #540 from marcelwa/lpk-mux-split-support-guard 

lutpack: assertion failure in Lpk_MuxSplit from an approximate cofactor support
This commit is contained in:
alanminko 2026-08-16 01:48:22 +09:00 committed by GitHub
parent 25b0e5399c 5cbfa76dc3
commit 1d28820170
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
1 changed files with 18 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
src/opt/lpk/lpkAbcDec.c
View File

@ -202,6 +202,24 @@ pMan->timeEvalMuxAn += Abc_Clock() - clk;
assert( pResMux == NULL || pResDsd == NULL ); assert( pResMux == NULL || pResDsd == NULL );
if ( pResMux ) 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(); clk = Abc_Clock();
p2 = Lpk_MuxSplit( pMan, p, pResMux->Variable, pResMux->Polarity ); p2 = Lpk_MuxSplit( pMan, p, pResMux->Variable, pResMux->Polarity );
pMan->timeEvalMuxSp += Abc_Clock() - clk; pMan->timeEvalMuxSp += Abc_Clock() - clk;