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

Fixed combo loop in choice computation.

This commit is contained in:
Alan Mishchenko 2025-08-10 11:04:20 -07:00
parent 15151c58ed
commit e7d360811f
2 changed files with 48 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

48
src/aig/gia/giaDup.c
View File

@ -6272,6 +6272,40 @@ Gia_Man_t * Gia_ManDupFanouts( Gia_Man_t * p )
return pNew;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManDupChoicesMarkTfi_rec( Gia_Man_t * pGia, int iObj )
{
if ( Gia_ObjIsTravIdCurrentId(pGia, iObj) )
return;
Gia_ObjSetTravIdCurrentId(pGia, iObj);
Gia_Obj_t * pObj = Gia_ManObj(pGia, iObj);
if ( !Gia_ObjIsAnd(pObj) )
return;
Gia_ManDupChoicesMarkTfi_rec( pGia, Gia_ObjFaninId0(pObj, iObj) );
Gia_ManDupChoicesMarkTfi_rec( pGia, Gia_ObjFaninId1(pObj, iObj) );
Gia_Obj_t * pSibl = Gia_ObjSiblObj( pGia, iObj );
if ( pSibl ) Gia_ManDupChoicesMarkTfi_rec( pGia, Gia_ObjId(pGia, pSibl) );
}
int Gia_ManDupChoicesCheckOverlap( Gia_Man_t * pGia, int iObj, int iFan0, int iFan1 )
{
Gia_ManIncrementTravId( pGia );
Gia_ManDupChoicesMarkTfi_rec( pGia, Gia_ObjFaninId0(Gia_ManObj(pGia, iObj), iObj) );
Gia_ManDupChoicesMarkTfi_rec( pGia, Gia_ObjFaninId1(Gia_ManObj(pGia, iObj), iObj) );
if ( Gia_ObjIsTravIdCurrentId(pGia, iFan0) || Gia_ObjIsTravIdCurrentId(pGia, iFan1) )
return 1;
return 0;
}
/**Function*************************************************************
Synopsis [Reorders choice nodes.]
@ -6288,14 +6322,24 @@ void Gia_ManPrintChoices( Gia_Man_t * p )
Gia_Obj_t * pObj; int i;
Gia_ManForEachAnd( p, pObj, i )
if ( p->pSibls[i] )
printf( "%d -> %d\n", i, p->pSibls[i] );
printf( "%d -> %d ", i, p->pSibls[i] );
}
void Gia_ManReorderChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
{
if ( ~pObj->Value )
return;
assert( Gia_ObjIsAnd(pObj) );
Gia_Obj_t * pSibl = Gia_ObjSiblObj(p, Gia_ObjId(p, pObj));
int ObjId = Gia_ObjId(p, pObj);
Gia_Obj_t * pSibl = Gia_ObjSiblObj(p, ObjId);
if ( pSibl ) {
int SiblId = Gia_ObjId(p, pSibl);
if ( Gia_ManDupChoicesCheckOverlap( p, SiblId, Gia_ObjFaninId0(pObj, ObjId), Gia_ObjFaninId1(pObj, ObjId) ) ) {
assert( p->pSibls[ObjId] == SiblId );
p->pSibls[ObjId] = p->pSibls[SiblId];
Gia_ManReorderChoices_rec( pNew, p, pObj );
return;
}
}
Gia_ManReorderChoices_rec( pNew, p, Gia_ObjFanin0(pObj) );
Gia_ManReorderChoices_rec( pNew, p, Gia_ObjFanin1(pObj) );
if ( pSibl ) Gia_ManReorderChoices_rec( pNew, p, pSibl );

4
src/base/abci/abc.c
View File

@ -47482,8 +47482,8 @@ usage:
Abc_Print( -2, "\t-f : toggle using lighter logic synthesis [default = %s]\n", pPars->fLightSynth? "yes": "no" );
Abc_Print( -2, "\t-r : toggle skipping choices with redundant support [default = %s]\n", pPars->fSkipRedSupp? "yes": "no" );
Abc_Print( -2, "\t-e : toggle computing and merging equivalences [default = %s]\n", fEquiv? "yes": "no" );
Abc_Print( -2, "\t-m : toggle minimizing logic level after merging equivalences [default = %s]\n", fRandom? "yes": "no" );
Abc_Print( -2, "\t-n : toggle selecting random choices while merging equivalences [default = %s]\n", fMinLevel? "yes": "no" );
Abc_Print( -2, "\t-m : toggle minimizing logic level after merging equivalences [default = %s]\n", fMinLevel? "yes": "no" );
Abc_Print( -2, "\t-n : toggle selecting random choices while merging equivalences [default = %s]\n", fRandom? "yes": "no" );
Abc_Print( -2, "\t-g : toggle using GIA to prove equivalences [default = %s]\n", pPars->fUseGia? "yes": "no" );
Abc_Print( -2, "\t-c : toggle using circuit-based SAT vs. MiniSat [default = %s]\n", pPars->fUseCSat? "yes": "no" );
Abc_Print( -2, "\t-x : toggle using new choice computation [default = %s]\n", pPars->fUseNew? "yes": "no" );