diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2015-09-04 11:52:27 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2015-09-04 11:52:27 -0700 |
commit | a207f6c07117fc577076f924984a0cbad1c0b0b0 (patch) | |
tree | fe67f782b9d8664befb6d18595f94cdd94da58ff /src/base/abci/abcCollapse.c | |
parent | 1ffd9aad766b3d980b8d8a030d03e8f17371f673 (diff) | |
download | abc-a207f6c07117fc577076f924984a0cbad1c0b0b0.tar.gz abc-a207f6c07117fc577076f924984a0cbad1c0b0b0.tar.bz2 abc-a207f6c07117fc577076f924984a0cbad1c0b0b0.zip |
Experiments with SAT-based collapsing.
Diffstat (limited to 'src/base/abci/abcCollapse.c')
-rw-r--r-- | src/base/abci/abcCollapse.c | 293 |
1 files changed, 206 insertions, 87 deletions
diff --git a/src/base/abci/abcCollapse.c b/src/base/abci/abcCollapse.c index e0f80c60..e8ab3f7a 100644 --- a/src/base/abci/abcCollapse.c +++ b/src/base/abci/abcCollapse.c @@ -19,6 +19,7 @@ ***********************************************************************/ #include "base/abc/abc.h" +#include "aig/gia/gia.h" #ifdef ABC_USE_CUDD #include "bdd/extrab/extraBdd.h" @@ -32,9 +33,6 @@ ABC_NAMESPACE_IMPL_START #ifdef ABC_USE_CUDD -static Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk ); -static Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode * bFunc ); - extern int Abc_NodeSupport( DdNode * bFunc, Vec_Str_t * vSupport, int nVars ); //////////////////////////////////////////////////////////////////////// @@ -117,74 +115,24 @@ int Abc_NtkMinimumBase2( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fVerbose ) +Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode * bFunc ) { - Abc_Ntk_t * pNtkNew; - abctime clk = Abc_Clock(); - - assert( Abc_NtkIsStrash(pNtk) ); - // compute the global BDDs - if ( Abc_NtkBuildGlobalBdds(pNtk, fBddSizeMax, 1, fReorder, fVerbose) == NULL ) - return NULL; - if ( fVerbose ) - { - DdManager * dd = (DdManager *)Abc_NtkGlobalBddMan( pNtk ); - printf( "Shared BDD size = %6d nodes. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) ); - ABC_PRT( "BDD construction time", Abc_Clock() - clk ); - } - - // create the new network - pNtkNew = Abc_NtkFromGlobalBdds( pNtk ); -// Abc_NtkFreeGlobalBdds( pNtk ); - Abc_NtkFreeGlobalBdds( pNtk, 1 ); - if ( pNtkNew == NULL ) - { -// Cudd_Quit( pNtk->pManGlob ); -// pNtk->pManGlob = NULL; - return NULL; - } -// Extra_StopManager( pNtk->pManGlob ); -// pNtk->pManGlob = NULL; - - // make the network minimum base - Abc_NtkMinimumBase2( pNtkNew ); - - if ( pNtk->pExdc ) - pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc ); - - // make sure that everything is okay - if ( !Abc_NtkCheck( pNtkNew ) ) - { - printf( "Abc_NtkCollapse: The network check has failed.\n" ); - Abc_NtkDelete( pNtkNew ); - return NULL; - } - return pNtkNew; + Abc_Obj_t * pNodeNew, * pTemp; + int i; + // create a new node + pNodeNew = Abc_NtkCreateNode( pNtkNew ); + // add the fanins in the order, in which they appear in the reordered manager + Abc_NtkForEachCi( pNtkNew, pTemp, i ) + Abc_ObjAddFanin( pNodeNew, Abc_NtkCi(pNtkNew, dd->invperm[i]) ); + // transfer the function + pNodeNew->pData = Extra_TransferLevelByLevel( dd, (DdManager *)pNtkNew->pManFunc, bFunc ); Cudd_Ref( (DdNode *)pNodeNew->pData ); + return pNodeNew; } - - -//int runtime1, runtime2; - -/**Function************************************************************* - - Synopsis [Derives the network with the given global BDD.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk ) { -// extern void Extra_ShuffleTest( reo_man * p, DdManager * dd, DdNode * Func ); -// reo_man * pReo; - ProgressBar * pProgress; Abc_Ntk_t * pNtkNew; Abc_Obj_t * pNode, * pDriver, * pNodeNew; -// DdManager * dd = pNtk->pManGlob; DdManager * dd = (DdManager *)Abc_NtkGlobalBddMan( pNtk ); int i; @@ -222,9 +170,6 @@ Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk ) Cudd_RecursiveDeref( dd, bBddDc ); } -// pReo = Extra_ReorderInit( Abc_NtkCiNum(pNtk), 1000 ); -// runtime1 = runtime2 = 0; - // start the new network pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD ); // make sure the new manager has the same number of inputs @@ -240,25 +185,66 @@ Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk ) Abc_ObjAddFanin( pNode->pCopy, pDriver->pCopy ); continue; } -// pNodeNew = Abc_NodeFromGlobalBdds( pNtkNew, dd, Vec_PtrEntry(pNtk->vFuncsGlob, i) ); pNodeNew = Abc_NodeFromGlobalBdds( pNtkNew, dd, (DdNode *)Abc_ObjGlobalBdd(pNode) ); Abc_ObjAddFanin( pNode->pCopy, pNodeNew ); -// Extra_ShuffleTest( pReo, dd, Abc_ObjGlobalBdd(pNode) ); - } Extra_ProgressBarStop( pProgress ); + return pNtkNew; +} +Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fVerbose ) +{ + Abc_Ntk_t * pNtkNew; + abctime clk = Abc_Clock(); -// Extra_ReorderQuit( pReo ); -//ABC_PRT( "Reo ", runtime1 ); -//ABC_PRT( "Cudd", runtime2 ); + assert( Abc_NtkIsStrash(pNtk) ); + // compute the global BDDs + if ( Abc_NtkBuildGlobalBdds(pNtk, fBddSizeMax, 1, fReorder, fVerbose) == NULL ) + return NULL; + if ( fVerbose ) + { + DdManager * dd = (DdManager *)Abc_NtkGlobalBddMan( pNtk ); + printf( "Shared BDD size = %6d nodes. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) ); + ABC_PRT( "BDD construction time", Abc_Clock() - clk ); + } + // create the new network + pNtkNew = Abc_NtkFromGlobalBdds( pNtk ); + Abc_NtkFreeGlobalBdds( pNtk, 1 ); + if ( pNtkNew == NULL ) + return NULL; + + // make the network minimum base + Abc_NtkMinimumBase2( pNtkNew ); + + if ( pNtk->pExdc ) + pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc ); + + // make sure that everything is okay + if ( !Abc_NtkCheck( pNtkNew ) ) + { + printf( "Abc_NtkCollapse: The network check has failed.\n" ); + Abc_NtkDelete( pNtkNew ); + return NULL; + } return pNtkNew; } + +#else + +Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fVerbose ) +{ + return NULL; +} + +#endif + + + /**Function************************************************************* - Synopsis [Derives the network with the given global BDD.] + Synopsis [Derives GIA for the cone of one output and computes its SOP.] Description [] @@ -267,28 +253,161 @@ Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode * bFunc ) +int Abc_NtkClpOneGia_rec( Gia_Man_t * pNew, Abc_Obj_t * pNode ) { - Abc_Obj_t * pNodeNew, * pTemp; - int i; + int iLit0, iLit1; + if ( Abc_NodeIsTravIdCurrent(pNode) || Abc_ObjFaninNum(pNode) == 0 ) + return pNode->iTemp; + assert( Abc_ObjIsNode( pNode ) ); + Abc_NodeSetTravIdCurrent( pNode ); + iLit0 = Abc_NtkClpOneGia_rec( pNew, Abc_ObjFanin0(pNode) ); + iLit1 = Abc_NtkClpOneGia_rec( pNew, Abc_ObjFanin1(pNode) ); + iLit0 = Abc_LitNotCond( iLit0, Abc_ObjFaninC0(pNode) ); + iLit1 = Abc_LitNotCond( iLit1, Abc_ObjFaninC1(pNode) ); + return (pNode->iTemp = Gia_ManHashAnd(pNew, iLit0, iLit1)); +} +Gia_Man_t * Abc_NtkClpOneGia( Abc_Ntk_t * pNtk, int iCo, Vec_Int_t * vSupp ) +{ + int i, iCi, iLit; + Abc_Obj_t * pNode; + Gia_Man_t * pNew, * pTemp; + pNew = Gia_ManStart( 1000 ); + pNew->pName = Abc_UtilStrsav( pNtk->pName ); + pNew->pSpec = Abc_UtilStrsav( pNtk->pSpec ); + Gia_ManHashStart( pNew ); + // primary inputs + Abc_AigConst1(pNtk)->iTemp = 1; + Vec_IntForEachEntry( vSupp, iCi, i ) + Abc_NtkCi(pNtk, iCi)->iTemp = Gia_ManAppendCi(pNew); + // create the first cone + Abc_NtkIncrementTravId( pNtk ); + pNode = Abc_NtkCo( pNtk, iCo ); + iLit = Abc_NtkClpOneGia_rec( pNew, Abc_ObjFanin0(pNode) ); + iLit = Abc_LitNotCond( iLit, Abc_ObjFaninC0(pNode) ); + Gia_ManAppendCo( pNew, iLit ); + // perform cleanup + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; +} +Vec_Str_t * Abc_NtkClpOne( Abc_Ntk_t * pNtk, int iCo, int nCubeLim, int nBTLimit, int fVerbose, int fCanon, Vec_Int_t ** pvSupp ) +{ + extern Vec_Int_t * Abc_NtkNodeSupportInt( Abc_Ntk_t * pNtk, int iCo ); + extern Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fVerbose ); + Vec_Int_t * vSupp = Abc_NtkNodeSupportInt( pNtk, iCo ); + Gia_Man_t * pGia = Abc_NtkClpOneGia( pNtk, iCo, vSupp ); + Vec_Str_t * vSop; + if ( fVerbose ) + printf( "Output %d:\n", iCo ); + vSop = Bmc_CollapseOne( pGia, nCubeLim, nBTLimit, fCanon, fVerbose ); + Gia_ManStop( pGia ); + *pvSupp = vSupp; + if ( vSop == NULL ) + Vec_IntFree(vSupp); + else if ( Vec_StrSize(vSop) == 4 ) // constant + Vec_IntClear(vSupp); + return vSop; +} + +/**Function************************************************************* + + Synopsis [SAT-based collapsing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Abc_NtkFromSopsOne( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, int iCo, int nCubeLim, int nBTLimit, int fCanon, int fVerbose ) +{ + Abc_Obj_t * pNodeNew; + Vec_Int_t * vSupp; + Vec_Str_t * vSop; + int i, iCi; + // compute SOP of the node + vSop = Abc_NtkClpOne( pNtk, iCo, nCubeLim, nBTLimit, fVerbose, fCanon, &vSupp ); + if ( vSop == NULL ) + return NULL; // create a new node pNodeNew = Abc_NtkCreateNode( pNtkNew ); - // add the fanins in the order, in which they appear in the reordered manager - Abc_NtkForEachCi( pNtkNew, pTemp, i ) - Abc_ObjAddFanin( pNodeNew, Abc_NtkCi(pNtkNew, dd->invperm[i]) ); + // add fanins + Vec_IntForEachEntry( vSupp, iCi, i ) + Abc_ObjAddFanin( pNodeNew, Abc_NtkCi(pNtkNew, iCi) ); + Vec_IntFree( vSupp ); // transfer the function - pNodeNew->pData = Extra_TransferLevelByLevel( dd, (DdManager *)pNtkNew->pManFunc, bFunc ); Cudd_Ref( (DdNode *)pNodeNew->pData ); + pNodeNew->pData = Abc_SopRegister( (Mem_Flex_t *)pNtkNew->pManFunc, Vec_StrArray(vSop) ); + Vec_StrFree( vSop ); return pNodeNew; } - -#else - -Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fVerbose ) +Abc_Ntk_t * Abc_NtkFromSops( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int fCanon, int fVerbose ) { - return NULL; + ProgressBar * pProgress; + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pNode, * pDriver, * pNodeNew; + int i; + // start the new network + pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP ); + // process the POs + pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) ); + Abc_NtkForEachCo( pNtk, pNode, i ) + { + Extra_ProgressBarUpdate( pProgress, i, NULL ); + pDriver = Abc_ObjFanin0(pNode); + if ( Abc_ObjIsCi(pDriver) && !strcmp(Abc_ObjName(pNode), Abc_ObjName(pDriver)) ) + { + Abc_ObjAddFanin( pNode->pCopy, pDriver->pCopy ); + continue; + } +/* + if ( Abc_ObjIsCi(pDriver) ) + { + pNodeNew = Abc_NtkCreateNode( pNtkNew ); + Abc_ObjAddFanin( pNodeNew, pDriver->pCopy ); // pDriver->pCopy is removed by GIA construction... + pNodeNew->pData = Abc_SopRegister( (Mem_Flex_t *)pNtkNew->pManFunc, Abc_ObjFaninC0(pNode) ? "0 1\n" : "1 1\n" ); + continue; + } +*/ + if ( pDriver == Abc_AigConst1(pNtk) ) + { + pNodeNew = Abc_NtkCreateNode( pNtkNew ); + pNodeNew->pData = Abc_SopRegister( (Mem_Flex_t *)pNtkNew->pManFunc, Abc_ObjFaninC0(pNode) ? " 0\n" : " 1\n" ); + Abc_ObjAddFanin( pNode->pCopy, pNodeNew ); + continue; + } + pNodeNew = Abc_NtkFromSopsOne( pNtkNew, pNtk, i, nCubeLim, nBTLimit, fCanon, fVerbose ); + if ( pNodeNew == NULL ) + { + Abc_NtkDelete( pNtkNew ); + pNtkNew = NULL; + break; + } + Abc_ObjAddFanin( pNode->pCopy, pNodeNew ); + } + Extra_ProgressBarStop( pProgress ); + return pNtkNew; +} +Abc_Ntk_t * Abc_NtkCollapseSat( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int fCanon, int fVerbose ) +{ + Abc_Ntk_t * pNtkNew; + assert( Abc_NtkIsStrash(pNtk) ); + // create the new network + pNtkNew = Abc_NtkFromSops( pNtk, nCubeLim, nBTLimit, fCanon, fVerbose ); + if ( pNtkNew == NULL ) + return NULL; + if ( pNtk->pExdc ) + pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc ); + // make sure that everything is okay + if ( !Abc_NtkCheck( pNtkNew ) ) + { + printf( "Abc_NtkCollapseSat: The network check has failed.\n" ); + Abc_NtkDelete( pNtkNew ); + return NULL; + } + return pNtkNew; } -#endif //////////////////////////////////////////////////////////////////////// /// END OF FILE /// |