/**CFile**************************************************************** FileName [abcCollapse.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [Network and node package.] Synopsis [Collapsing the network into two-levels.] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - June 20, 2005.] Revision [$Id: abcCollapse.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ #include "base/abc/abc.h" #include "aig/gia/gia.h" #include "misc/vec/vecWec.h" #include "sat/cnf/cnf.h" #include "sat/bsat/satStore.h" #ifdef ABC_USE_CUDD #include "bdd/extrab/extraBdd.h" #endif ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// #ifdef ABC_USE_CUDD extern int Abc_NodeSupport( DdNode * bFunc, Vec_Str_t * vSupport, int nVars ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* Synopsis [Makes nodes minimum base.] Description [Returns the number of changed nodes.] SideEffects [] SeeAlso [] ***********************************************************************/ int Abc_NodeMinimumBase2( Abc_Obj_t * pNode ) { Vec_Str_t * vSupport; Vec_Ptr_t * vFanins; DdNode * bTemp; int i, nVars; assert( Abc_NtkIsBddLogic(pNode->pNtk) ); assert( Abc_ObjIsNode(pNode) ); // compute support vSupport = Vec_StrAlloc( 10 ); nVars = Abc_NodeSupport( Cudd_Regular(pNode->pData), vSupport, Abc_ObjFaninNum(pNode) ); if ( nVars == Abc_ObjFaninNum(pNode) ) { Vec_StrFree( vSupport ); return 0; } // add fanins vFanins = Vec_PtrAlloc( Abc_ObjFaninNum(pNode) ); Abc_NodeCollectFanins( pNode, vFanins ); Vec_IntClear( &pNode->vFanins ); for ( i = 0; i < vFanins->nSize; i++ ) if ( vSupport->pArray[i] != 0 ) // useful Vec_IntPush( &pNode->vFanins, Abc_ObjId((Abc_Obj_t *)vFanins->pArray[i]) ); assert( nVars == Abc_ObjFaninNum(pNode) ); // update the function of the node pNode->pData = Extra_bddRemapUp( (DdManager *)pNode->pNtk->pManFunc, bTemp = (DdNode *)pNode->pData ); Cudd_Ref( (DdNode *)pNode->pData ); Cudd_RecursiveDeref( (DdManager *)pNode->pNtk->pManFunc, bTemp ); Vec_PtrFree( vFanins ); Vec_StrFree( vSupport ); return 1; } int Abc_NtkMinimumBase2( Abc_Ntk_t * pNtk ) { Abc_Obj_t * pNode, * pFanin; int i, k, Counter; assert( Abc_NtkIsBddLogic(pNtk) ); // remove all fanouts Abc_NtkForEachObj( pNtk, pNode, i ) Vec_IntClear( &pNode->vFanouts ); // add useful fanins Counter = 0; Abc_NtkForEachNode( pNtk, pNode, i ) Counter += Abc_NodeMinimumBase2( pNode ); // add fanouts Abc_NtkForEachObj( pNtk, pNode, i ) Abc_ObjForEachFanin( pNode, pFanin, k ) Vec_IntPush( &pFanin->vFanouts, Abc_ObjId(pNode) ); return Counter; } /**Function************************************************************* Synopsis [Collapses the network.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode * bFunc, int fReverse ) { 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, fReverse ? Abc_NtkCiNum(pNtkNew)-1-dd->invperm[i] : dd->invperm[i]) ); // transfer the function pNodeNew->pData = Extra_TransferLevelByLevel( dd, (DdManager *)pNtkNew->pManFunc, bFunc ); Cudd_Ref( (DdNode *)pNodeNew->pData ); return pNodeNew; } Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk, int fReverse ) { ProgressBar * pProgress; Abc_Ntk_t * pNtkNew; Abc_Obj_t * pNode, * pDriver, * pNodeNew; DdManager * dd = (DdManager *)Abc_NtkGlobalBddMan( pNtk ); int i; // extract don't-care and compute ISOP if ( pNtk->pExdc ) { DdManager * ddExdc = NULL; DdNode * bBddMin, * bBddDc, * bBddL, * bBddU; assert( Abc_NtkIsStrash(pNtk->pExdc) ); assert( Abc_NtkCoNum(pNtk->pExdc) == 1 ); // compute the global BDDs if ( Abc_NtkBuildGlobalBdds(pNtk->pExdc, 10000000, 1, 1, 0, 0) == NULL ) return NULL; // transfer tot the same manager ddExdc = (DdManager *)Abc_NtkGlobalBddMan( pNtk->pExdc ); bBddDc = (DdNode *)Abc_ObjGlobalBdd(Abc_NtkCo(pNtk->pExdc, 0)); bBddDc = Cudd_bddTransfer( ddExdc, dd, bBddDc ); Cudd_Ref( bBddDc ); Abc_NtkFreeGlobalBdds( pNtk->pExdc, 1 ); // minimize the output Abc_NtkForEachCo( pNtk, pNode, i ) { bBddMin = (DdNode *)Abc_ObjGlobalBdd(pNode); // derive lower and uppwer bound bBddL = Cudd_bddAnd( dd, bBddMin, Cudd_Not(bBddDc) ); Cudd_Ref( bBddL ); bBddU = Cudd_bddAnd( dd, Cudd_Not(bBddMin), Cudd_Not(bBddDc) ); Cudd_Ref( bBddU ); Cudd_RecursiveDeref( dd, bBddMin ); // compute new one bBddMin = Cudd_bddIsop( dd, bBddL, Cudd_Not(bBddU) ); Cudd_Ref( bBddMin ); Cudd_RecursiveDeref( dd, bBddL ); Cudd_RecursiveDeref( dd, bBddU ); // update global BDD Abc_ObjSetGlobalBdd( pNode, bBddMin ); //Extra_bddPrint( dd, bBddMin ); printf( "\n" ); } Cudd_RecursiveDeref( dd, bBddDc ); } // 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 Cudd_bddIthVar( (DdManager *)pNtkNew->pManFunc, dd->size-1 ); // 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; } pNodeNew = Abc_NodeFromGlobalBdds( pNtkNew, dd, (DdNode *)Abc_ObjGlobalBdd(pNode), fReverse ); Abc_ObjAddFanin( pNode->pCopy, pNodeNew ); } Extra_ProgressBarStop( pProgress ); return pNtkNew; } void Abc_NtkDumpVariableOrder( Abc_Ntk_t * pNtk ) { DdManager * dd = (DdManager *)Abc_NtkGlobalBddMan( pNtk ); FILE * pFile = fopen( "order.txt", "wb" ); int i; for ( i = 0; i < dd->size; i++ ) fprintf( pFile, "%d ", dd->invperm[i] ); fprintf( pFile, "\n" ); fclose( pFile ); } Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fReverse, int fDumpOrder, int fVerbose ) { Abc_Ntk_t * pNtkNew; abctime clk = Abc_Clock(); assert( Abc_NtkIsStrash(pNtk) ); // compute the global BDDs if ( Abc_NtkBuildGlobalBdds(pNtk, fBddSizeMax, 1, fReorder, fReverse, 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 ); } if ( fDumpOrder ) Abc_NtkDumpVariableOrder( pNtk ); // create the new network pNtkNew = Abc_NtkFromGlobalBdds( pNtk, fReverse ); 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 fReverse, int fDumpOrder, int fVerbose ) { return NULL; } #endif #if 0 /**Function************************************************************* Synopsis [Derives GIA for the cone of one output and computes its SOP.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Abc_NtkClpOneGia_rec( Gia_Man_t * pNew, Abc_Obj_t * pNode ) { int iLit0, iLit1; if ( Abc_NodeIsTravIdCurrent(pNode) || Abc_ObjFaninNum(pNode) == 0 || Abc_ObjIsCi(pNode) ) 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, int fReverse, Vec_Int_t * vSupp ) { Vec_Str_t * vSop; abctime clk = Abc_Clock(); extern Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ); Gia_Man_t * pGia = Abc_NtkClpOneGia( pNtk, iCo, vSupp ); if ( fVerbose ) printf( "Output %4d: Supp = %4d. Cone =%6d.\n", iCo, Vec_IntSize(vSupp), Gia_ManAndNum(pGia) ); vSop = Bmc_CollapseOne( pGia, nCubeLim, nBTLimit, fCanon, fReverse, fVerbose ); Gia_ManStop( pGia ); if ( vSop == NULL ) return NULL; if ( Vec_StrSize(vSop) == 4 ) // constant Vec_IntClear(vSupp); if ( fVerbose ) Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); return vSop; } /**Function************************************************************* Synopsis [Collect structural support for all nodes.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Vec_Wec_t * Abc_NtkCreateCoSupps( Abc_Ntk_t * pNtk, int fVerbose ) { abctime clk = Abc_Clock(); Abc_Obj_t * pNode; int i; Vec_Wec_t * vSupps = Vec_WecStart( Abc_NtkObjNumMax(pNtk) ); Abc_NtkForEachCi( pNtk, pNode, i ) Vec_IntPush( Vec_WecEntry(vSupps, pNode->Id), i ); Abc_NtkForEachNode( pNtk, pNode, i ) Vec_IntTwoMerge2( Vec_WecEntry(vSupps, Abc_ObjFanin0(pNode)->Id), Vec_WecEntry(vSupps, Abc_ObjFanin1(pNode)->Id), Vec_WecEntry(vSupps, pNode->Id) ); if ( fVerbose ) Abc_PrintTime( 1, "Support computation", Abc_Clock() - clk ); return vSupps; } /**Function************************************************************* Synopsis [Derive array of COs sorted by cone size in the reverse order.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Abc_NodeCompareByTemp( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 ) { int Diff = (*pp2)->iTemp - (*pp1)->iTemp; if ( Diff < 0 ) return -1; if ( Diff > 0 ) return 1; Diff = strcmp( Abc_ObjName(*pp1), Abc_ObjName(*pp2) ); if ( Diff < 0 ) return -1; if ( Diff > 0 ) return 1; return 0; } Vec_Ptr_t * Abc_NtkCreateCoOrder( Abc_Ntk_t * pNtk, Vec_Wec_t * vSupps ) { Abc_Obj_t * pNode; int i; Vec_Ptr_t * vNodes = Vec_PtrAlloc( Abc_NtkCoNum(pNtk) ); Abc_NtkForEachCo( pNtk, pNode, i ) { pNode->iTemp = Vec_IntSize( Vec_WecEntry(vSupps, Abc_ObjFaninId0(pNode)) ); Vec_PtrPush( vNodes, pNode ); } // order objects alphabetically qsort( (void *)Vec_PtrArray(vNodes), (size_t)Vec_PtrSize(vNodes), sizeof(Abc_Obj_t *), (int (*)(const void *, const void *)) Abc_NodeCompareByTemp ); // cleanup // Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i ) // printf( "%s %d ", Abc_ObjName(pNode), pNode->iTemp ); // printf( "\n" ); return vNodes; } /**Function************************************************************* Synopsis [SAT-based collapsing.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Abc_Obj_t * Abc_NtkFromSopsOne( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, int iCo, Vec_Int_t * vSupp, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ) { Abc_Obj_t * pNodeNew; Vec_Str_t * vSop; int i, iCi; // compute SOP of the node vSop = Abc_NtkClpOne( pNtk, iCo, nCubeLim, nBTLimit, fVerbose, fCanon, fReverse, vSupp ); if ( vSop == NULL ) return NULL; // create a new node pNodeNew = Abc_NtkCreateNode( pNtkNew ); // add fanins if ( Vec_StrSize(vSop) > 4 ) // non-constant SOP Vec_IntForEachEntry( vSupp, iCi, i ) Abc_ObjAddFanin( pNodeNew, Abc_NtkCi(pNtkNew, iCi) ); // transfer the function pNodeNew->pData = Abc_SopRegister( (Mem_Flex_t *)pNtkNew->pManFunc, Vec_StrArray(vSop) ); Vec_StrFree( vSop ); return pNodeNew; } Abc_Ntk_t * Abc_NtkFromSops( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int nCostMax, int fCanon, int fReverse, int fVerbose ) { ProgressBar * pProgress; Abc_Ntk_t * pNtkNew; Abc_Obj_t * pNode, * pDriver, * pNodeNew; Vec_Ptr_t * vDriverCopy, * vCoNodes, * vDfsNodes; Vec_Int_t * vNodeCoIds, * vLevel; Vec_Wec_t * vSupps; int i; // Abc_NtkForEachCi( pNtk, pNode, i ) // printf( "%d ", Abc_ObjFanoutNum(pNode) ); // printf( "\n" ); // compute structural supports vSupps = Abc_NtkCreateCoSupps( pNtk, fVerbose ); // order CO nodes by support size vCoNodes = Abc_NtkCreateCoOrder( pNtk, vSupps ); // compute cost of the largest node if ( nCubeLim > 0 ) { word Cost; pNode = (Abc_Obj_t *)Vec_PtrEntry( vCoNodes, 0 ); vDfsNodes = Abc_NtkDfsNodes( pNtk, &pNode, 1 ); vLevel = Vec_WecEntry( vSupps, Abc_ObjFaninId0(pNode) ); Cost = (word)Vec_PtrSize(vDfsNodes) * (word)Vec_IntSize(vLevel) * (word)nCubeLim; if ( Cost > (word)nCostMax ) { printf( "Cost of the largest output cone exceeded the limit (%d * %d * %d > %d).\n", Vec_PtrSize(vDfsNodes), Vec_IntSize(vLevel), nCubeLim, nCostMax ); Vec_PtrFree( vDfsNodes ); Vec_PtrFree( vCoNodes ); Vec_WecFree( vSupps ); return NULL; } Vec_PtrFree( vDfsNodes ); } // collect CO IDs in this order vNodeCoIds = Vec_IntAlloc( Abc_NtkCoNum(pNtk) ); Abc_NtkForEachCo( pNtk, pNode, i ) pNode->iTemp = i; Vec_PtrForEachEntry( Abc_Obj_t *, vCoNodes, pNode, i ) Vec_IntPush( vNodeCoIds, pNode->iTemp ); // start the new network pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP ); // collect driver copies vDriverCopy = Vec_PtrAlloc( Abc_NtkCoNum(pNtk) ); // Abc_NtkForEachCo( pNtk, pNode, i ) Vec_PtrForEachEntry( Abc_Obj_t *, vCoNodes, pNode, i ) Vec_PtrPush( vDriverCopy, Abc_ObjFanin0(pNode)->pCopy ); // process the POs pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) ); // Abc_NtkForEachCo( pNtk, pNode, i ) Vec_PtrForEachEntry( Abc_Obj_t *, vCoNodes, 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, (Abc_Obj_t *)Vec_PtrEntry(vDriverCopy, i) ); continue; } if ( Abc_ObjIsCi(pDriver) ) { pNodeNew = Abc_NtkCreateNode( pNtkNew ); Abc_ObjAddFanin( pNodeNew, (Abc_Obj_t *)Vec_PtrEntry(vDriverCopy, i) ); pNodeNew->pData = Abc_SopRegister( (Mem_Flex_t *)pNtkNew->pManFunc, Abc_ObjFaninC0(pNode) ? "0 1\n" : "1 1\n" ); Abc_ObjAddFanin( pNode->pCopy, pNodeNew ); 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, Vec_IntEntry(vNodeCoIds, i), Vec_WecEntry(vSupps, Abc_ObjFanin0(pNode)->Id), nCubeLim, nBTLimit, fCanon, fReverse, i ? 0 : fVerbose ); if ( pNodeNew == NULL ) { Abc_NtkDelete( pNtkNew ); pNtkNew = NULL; break; } Abc_ObjAddFanin( pNode->pCopy, pNodeNew ); } Vec_PtrFree( vDriverCopy ); Vec_PtrFree( vCoNodes ); Vec_IntFree( vNodeCoIds ); Vec_WecFree( vSupps ); Extra_ProgressBarStop( pProgress ); return pNtkNew; } Abc_Ntk_t * Abc_NtkCollapseSat( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int nCostMax, int fCanon, int fReverse, int fVerbose ) { Abc_Ntk_t * pNtkNew; assert( Abc_NtkIsStrash(pNtk) ); // create the new network pNtkNew = Abc_NtkFromSops( pNtk, nCubeLim, nBTLimit, nCostMax, fCanon, fReverse, 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 extern Vec_Wec_t * Gia_ManCreateCoSupps( Gia_Man_t * p, int fVerbose ); extern int Gia_ManCoLargestSupp( Gia_Man_t * p, Vec_Wec_t * vSupps ); extern Vec_Wec_t * Gia_ManIsoStrashReduceInt( Gia_Man_t * p, Vec_Wec_t * vSupps, int fVerbose ); /**Function************************************************************* Synopsis [Derives GIA for the network.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Abc_NtkClpGia_rec( Gia_Man_t * pNew, Abc_Obj_t * pNode ) { int iLit0, iLit1; if ( pNode->iTemp >= 0 ) return pNode->iTemp; assert( Abc_ObjIsNode( pNode ) ); iLit0 = Abc_NtkClpGia_rec( pNew, Abc_ObjFanin0(pNode) ); iLit1 = Abc_NtkClpGia_rec( pNew, Abc_ObjFanin1(pNode) ); iLit0 = Abc_LitNotCond( iLit0, Abc_ObjFaninC0(pNode) ); iLit1 = Abc_LitNotCond( iLit1, Abc_ObjFaninC1(pNode) ); return (pNode->iTemp = Gia_ManAppendAnd(pNew, iLit0, iLit1)); } Gia_Man_t * Abc_NtkClpGia( Abc_Ntk_t * pNtk ) { int i, iLit; Gia_Man_t * pNew; Abc_Obj_t * pNode; assert( Abc_NtkIsStrash(pNtk) ); pNew = Gia_ManStart( 1000 ); pNew->pName = Abc_UtilStrsav( pNtk->pName ); pNew->pSpec = Abc_UtilStrsav( pNtk->pSpec ); Abc_NtkForEachObj( pNtk, pNode, i ) pNode->iTemp = -1; Abc_AigConst1(pNtk)->iTemp = 1; Abc_NtkForEachCi( pNtk, pNode, i ) pNode->iTemp = Gia_ManAppendCi(pNew); Abc_NtkForEachCo( pNtk, pNode, i ) { iLit = Abc_NtkClpGia_rec( pNew, Abc_ObjFanin0(pNode) ); iLit = Abc_LitNotCond( iLit, Abc_ObjFaninC0(pNode) ); Gia_ManAppendCo( pNew, iLit ); } return pNew; } /**Function************************************************************* Synopsis [Minimize SOP by removing redundant variables.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ #define Abc_NtkSopForEachCube( pSop, nVars, pCube ) for ( pCube = (pSop); *pCube; pCube += (nVars) + 3 ) int Abc_NtkCollapseReduce( Vec_Str_t * vSop, Vec_Int_t * vSupp, Vec_Int_t * vClass, Vec_Wec_t * vSupps ) { int j = 0, i, k, iCo, iVar, nVars = Vec_IntSize(vSupp); char * pCube, * pSop = Vec_StrArray(vSop); Vec_Int_t * vPres; if ( Vec_StrSize(vSop) == 4 ) // constant { Vec_IntForEachEntry( vClass, iCo, i ) Vec_IntClear( Vec_WecEntry(vSupps, iCo) ); return 1; } vPres = Vec_IntStart( nVars ); Abc_NtkSopForEachCube( pSop, nVars, pCube ) for ( k = 0; k < nVars; k++ ) if ( pCube[k] != '-' ) Vec_IntWriteEntry( vPres, k, 1 ); if ( Vec_IntCountZero(vPres) == 0 ) { Vec_IntFree( vPres ); return 0; } // reduce cubes Abc_NtkSopForEachCube( pSop, nVars, pCube ) for ( k = 0; k < nVars + 3; k++ ) if ( k >= nVars || Vec_IntEntry(vPres, k) ) Vec_StrWriteEntry( vSop, j++, pCube[k] ); Vec_StrWriteEntry( vSop, j++, '\0' ); Vec_StrShrink( vSop, j ); // reduce support Vec_IntForEachEntry( vClass, iCo, i ) { j = 0; vSupp = Vec_WecEntry( vSupps, iCo ); Vec_IntForEachEntry( vSupp, iVar, k ) if ( Vec_IntEntry(vPres, k) ) Vec_IntWriteEntry( vSupp, j++, iVar ); Vec_IntShrink( vSupp, j ); } Vec_IntFree( vPres ); // if ( Vec_IntSize(vSupp) != Abc_SopGetVarNum(Vec_StrArray(vSop)) ) // printf( "Mismatch!!!\n" ); return 1; } /**Function************************************************************* Synopsis [Derives SAT solver for one output from the shared CNF.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ sat_solver * Abc_NtkClpDeriveSatSolver( Cnf_Dat_t * pCnf, int iCoObjId, Vec_Int_t * vSupp, Vec_Int_t * vAnds, Vec_Int_t * vMap, sat_solver ** ppSat1, sat_solver ** ppSat2, sat_solver ** ppSat3 ) { int i, k, iObj, status, nVars = 2; // int i, k, iObj, status, nVars = 1; Vec_Int_t * vLits = Vec_IntAlloc( 16 ); sat_solver * pSat = sat_solver_new(); if ( ppSat1 ) *ppSat1 = sat_solver_new(); if ( ppSat2 ) *ppSat2 = sat_solver_new(); if ( ppSat3 ) *ppSat3 = sat_solver_new(); // assign SAT variable numbers Vec_IntWriteEntry( vMap, iCoObjId, nVars++ ); Vec_IntForEachEntry( vSupp, iObj, k ) Vec_IntWriteEntry( vMap, iObj, nVars++ ); Vec_IntForEachEntry( vAnds, iObj, k ) if ( pCnf->pObj2Clause[iObj] != -1 ) Vec_IntWriteEntry( vMap, iObj, nVars++ ); // Vec_IntForEachEntry( vSupp, iObj, k ) // Vec_IntWriteEntry( vMap, iObj, nVars++ ); // create clauses for the internal nodes and for the output sat_solver_setnvars( pSat, nVars ); if ( ppSat1 ) sat_solver_setnvars( *ppSat1, nVars ); if ( ppSat2 ) sat_solver_setnvars( *ppSat2, nVars ); if ( ppSat3 ) sat_solver_setnvars( *ppSat3, nVars ); Vec_IntPush( vAnds, iCoObjId ); Vec_IntForEachEntry( vAnds, iObj, k ) { int iClaBeg, iClaEnd, * pLit; if ( pCnf->pObj2Clause[iObj] == -1 ) continue; iClaBeg = pCnf->pObj2Clause[iObj]; iClaEnd = iClaBeg + pCnf->pObj2Count[iObj]; assert( iClaBeg < iClaEnd ); for ( i = iClaBeg; i < iClaEnd; i++ ) { Vec_IntClear( vLits ); for ( pLit = pCnf->pClauses[i]; pLit < pCnf->pClauses[i+1]; pLit++ ) Vec_IntPush( vLits, Abc_Lit2LitV(Vec_IntArray(vMap), *pLit) ); status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) ); assert( status ); (void) status; if ( ppSat1 ) sat_solver_addclause( *ppSat1, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) ); if ( ppSat2 ) sat_solver_addclause( *ppSat2, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) ); if ( ppSat3 ) sat_solver_addclause( *ppSat3, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) ); } } Vec_IntPop( vAnds ); Vec_IntFree( vLits ); assert( nVars == sat_solver_nvars(pSat) ); return pSat; } /**Function************************************************************* Synopsis [Computes SOPs for each output.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Vec_Str_t * Abc_NtkClpGiaOne( Gia_Man_t * p, int iCo, int nCubeLim, int nBTLimit, int fCanon, int fReverse, Vec_Int_t * vSupp, int fVerbose, Vec_Int_t * vClass, Vec_Wec_t * vSupps ) { Vec_Str_t * vSop; abctime clk = Abc_Clock(); extern Vec_Str_t * Bmc_CollapseOneOld( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ); Gia_Man_t * pGia = Gia_ManDupCones( p, &iCo, 1, 1 ); if ( fVerbose ) printf( "Output %4d: Supp = %4d. Cone =%6d.\n", iCo, Vec_IntSize(vSupp), Gia_ManAndNum(pGia) ); vSop = Bmc_CollapseOneOld( pGia, nCubeLim, nBTLimit, fCanon, fReverse, fVerbose ); Gia_ManStop( pGia ); if ( vSop == NULL ) return NULL; Abc_NtkCollapseReduce( vSop, vSupp, vClass, vSupps ); if ( fVerbose ) printf( "Supp new = %4d. Sop = %4d. ", Vec_IntSize(vSupp), Vec_StrSize(vSop)/(Vec_IntSize(vSupp) +3) ); if ( fVerbose ) Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); return vSop; } Vec_Str_t * Abc_NtkClpGiaOne2( Cnf_Dat_t * pCnf, Gia_Man_t * p, int iCo, int nCubeLim, int nBTLimit, int fCanon, int fReverse, Vec_Int_t * vSupp, Vec_Int_t * vMap, int fVerbose, Vec_Int_t * vClass, Vec_Wec_t * vSupps ) { Vec_Str_t * vSop; sat_solver * pSat, * pSat1 = NULL, * pSat2 = NULL, * pSat3 = NULL; Gia_Obj_t * pObj; abctime clk = Abc_Clock(); extern Vec_Str_t * Bmc_CollapseOne_int( sat_solver * pSat, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ); extern Vec_Str_t * Bmc_CollapseOne_int2( sat_solver * pSat, sat_solver * pSat2, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ); extern Vec_Str_t * Bmc_CollapseOne_int3( sat_solver * pSat, sat_solver * pSat1, sat_solver * pSat2, sat_solver * pSat3, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ); int i, iCoObjId = Gia_ObjId( p, Gia_ManCo(p, iCo) ); Vec_Int_t * vAnds = Vec_IntAlloc( 100 ); Vec_Int_t * vSuppObjs = Vec_IntAlloc( 100 ); Gia_ManForEachCiVec( vSupp, p, pObj, i ) Vec_IntPush( vSuppObjs, Gia_ObjId(p, pObj) ); Gia_ManIncrementTravId( p ); Gia_ManCollectAnds( p, &iCoObjId, 1, vAnds, NULL ); assert( Vec_IntSize(vAnds) > 0 ); // pSat = Abc_NtkClpDeriveSatSolver( pCnf, iCoObjId, vSuppObjs, vAnds, vMap, &pSat1, &pSat2, &pSat3 ); pSat = Abc_NtkClpDeriveSatSolver( pCnf, iCoObjId, vSuppObjs, vAnds, vMap, NULL, NULL, NULL ); Vec_IntFree( vSuppObjs ); if ( fVerbose ) printf( "Output %4d: Supp = %4d. Cone =%6d.\n", iCo, Vec_IntSize(vSupp), Vec_IntSize(vAnds) ); // vSop = Bmc_CollapseOne_int3( pSat, pSat1, pSat2, pSat3, Vec_IntSize(vSupp), nCubeLim, nBTLimit, fCanon, fReverse, fVerbose ); // vSop = Bmc_CollapseOne_int2( pSat, pSat1, Vec_IntSize(vSupp), nCubeLim, nBTLimit, fCanon, fReverse, fVerbose ); vSop = Bmc_CollapseOne_int( pSat, Vec_IntSize(vSupp), nCubeLim, nBTLimit, fCanon, fReverse, fVerbose ); sat_solver_delete( pSat ); if ( pSat1 ) sat_solver_delete( pSat1 ); if ( pSat2 ) sat_solver_delete( pSat2 ); if ( pSat3 ) sat_solver_delete( pSat3 ); Vec_IntFree( vAnds ); if ( vSop == NULL ) return NULL; Abc_NtkCollapseReduce( vSop, vSupp, vClass, vSupps ); if ( fVerbose ) printf( "Supp new = %4d. Sop = %4d. ", Vec_IntSize(vSupp), Vec_StrSize(vSop)/(Vec_IntSize(vSupp) +3) ); if ( fVerbose ) Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); return vSop; } Vec_Ptr_t * Abc_GiaDeriveSops( Abc_Ntk_t * pNtkNew, Gia_Man_t * p, Vec_Wec_t * vSupps, int nCubeLim, int nBTLimit, int nCostMax, int fCanon, int fReverse, int fCnfShared, int fVerbose ) { ProgressBar * pProgress; abctime clk = Abc_Clock(); Vec_Ptr_t * vSops = NULL, * vSopsRepr; Vec_Int_t * vReprs, * vClass, * vReprSuppSizes; int i, k, Entry, iCo, * pOrder; Vec_Wec_t * vClasses; Cnf_Dat_t * pCnf = NULL; Vec_Int_t * vMap = NULL; // derive classes of outputs vClasses = Gia_ManIsoStrashReduceInt( p, vSupps, 0 ); if ( fVerbose ) { printf( "Considering %d (out of %d) outputs. ", Vec_WecSize(vClasses), Gia_ManCoNum(p) ); Abc_PrintTime( 1, "Reduction time", Abc_Clock() - clk ); } // derive representatives vReprs = Vec_WecCollectFirsts( vClasses ); vReprSuppSizes = Vec_IntAlloc( Vec_IntSize(vReprs) ); Vec_IntForEachEntry( vReprs, Entry, i ) Vec_IntPush( vReprSuppSizes, Vec_IntSize(Vec_WecEntry(vSupps, Entry)) ); pOrder = Abc_MergeSortCost( Vec_IntArray(vReprSuppSizes), Vec_IntSize(vReprSuppSizes) ); Vec_IntFree( vReprSuppSizes ); // consider SOPs for representatives if ( fCnfShared ) { vMap = Vec_IntStartFull( Gia_ManObjNum(p) ); pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 1, 0, 0, 0 ); } vSopsRepr = Vec_PtrStart( Vec_IntSize(vReprs) ); pProgress = Extra_ProgressBarStart( stdout, Vec_IntSize(vReprs) ); Extra_ProgressBarUpdate( pProgress, 0, NULL ); for ( i = 0; i < Vec_IntSize(vReprs); i++ ) { int iEntry = pOrder[Vec_IntSize(vReprs) - 1 - i]; int iCoThis = Vec_IntEntry( vReprs, iEntry ); Vec_Int_t * vSupp = Vec_WecEntry( vSupps, iCoThis ); Vec_Str_t * vSop; if ( Vec_IntSize(vSupp) < 2 ) { Vec_PtrWriteEntry( vSopsRepr, iEntry, (void *)(ABC_PTRINT_T)1 ); continue; } if ( fCnfShared && !fCanon ) vSop = Abc_NtkClpGiaOne2( pCnf, p, iCoThis, nCubeLim, nBTLimit, fCanon, fReverse, vSupp, vMap, i ? 0 : fVerbose, Vec_WecEntry(vClasses, iEntry), vSupps ); else vSop = Abc_NtkClpGiaOne( p, iCoThis, nCubeLim, nBTLimit, fCanon, fReverse, vSupp, i ? 0 : fVerbose, Vec_WecEntry(vClasses, iEntry), vSupps ); if ( vSop == NULL ) goto finish; assert( Vec_IntSize( Vec_WecEntry(vSupps, iCoThis) ) == Abc_SopGetVarNum(Vec_StrArray(vSop)) ); Extra_ProgressBarUpdate( pProgress, i, NULL ); Vec_PtrWriteEntry( vSopsRepr, iEntry, Abc_SopRegister( (Mem_Flex_t *)pNtkNew->pManFunc, Vec_StrArray(vSop) ) ); Vec_StrFree( vSop ); } Extra_ProgressBarStop( pProgress ); if ( fCnfShared ) { Cnf_DataFree( pCnf ); Vec_IntFree( vMap ); } // derive SOPs for each output vSops = Vec_PtrStart( Gia_ManCoNum(p) ); Vec_WecForEachLevel ( vClasses, vClass, i ) Vec_IntForEachEntry( vClass, iCo, k ) Vec_PtrWriteEntry( vSops, iCo, Vec_PtrEntry(vSopsRepr, i) ); assert( Vec_PtrCountZero(vSops) == 0 ); /* // verify for ( i = 0; i < Gia_ManCoNum(p); i++ ) { Vec_Int_t * vSupp = Vec_WecEntry( vSupps, i ); char * pSop = (char *)Vec_PtrEntry( vSops, i ); assert( Vec_IntSize(vSupp) == Abc_SopGetVarNum(pSop) ); } */ // cleanup finish: ABC_FREE( pOrder ); Vec_IntFree( vReprs ); Vec_WecFree( vClasses ); Vec_PtrFree( vSopsRepr ); return vSops; } Abc_Ntk_t * Abc_NtkFromSopsInt( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int nCostMax, int fCanon, int fReverse, int fCnfShared, int fVerbose ) { Abc_Ntk_t * pNtkNew; Gia_Man_t * pGia; Vec_Wec_t * vSupps; Vec_Int_t * vSupp; Vec_Ptr_t * vSops; Abc_Obj_t * pNode, * pNodeNew, * pDriver; int i, k, iCi; pGia = Abc_NtkClpGia( pNtk ); vSupps = Gia_ManCreateCoSupps( pGia, fVerbose ); // check the largest output if ( nCubeLim > 0 && nCostMax > 0 ) { int iCoMax = Gia_ManCoLargestSupp( pGia, vSupps ); int iObjMax = Gia_ObjId( pGia, Gia_ManCo(pGia, iCoMax) ); int nSuppMax = Vec_IntSize( Vec_WecEntry(vSupps, iCoMax) ); int nNodeMax = Gia_ManConeSize( pGia, &iObjMax, 1 ); word Cost = (word)nNodeMax * (word)nSuppMax * (word)nCubeLim; if ( Cost > (word)nCostMax ) { printf( "Cost of the largest output cone exceeded the limit (%d * %d * %d > %d).\n", nNodeMax, nSuppMax, nCubeLim, nCostMax ); Gia_ManStop( pGia ); Vec_WecFree( vSupps ); return NULL; } } pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP ); vSops = Abc_GiaDeriveSops( pNtkNew, pGia, vSupps, nCubeLim, nBTLimit, nCostMax, fCanon, fReverse, fCnfShared, fVerbose ); Gia_ManStop( pGia ); if ( vSops == NULL ) { Vec_WecFree( vSupps ); Abc_NtkDelete( pNtkNew ); return NULL; } Abc_NtkForEachCo( pNtk, pNode, i ) { 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 ); pNodeNew->pData = Abc_SopRegister( (Mem_Flex_t *)pNtkNew->pManFunc, Abc_ObjFaninC0(pNode) ? "0 1\n" : "1 1\n" ); Abc_ObjAddFanin( pNode->pCopy, pNodeNew ); 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_NtkCreateNode( pNtkNew ); vSupp = Vec_WecEntry( vSupps, i ); Vec_IntForEachEntry( vSupp, iCi, k ) Abc_ObjAddFanin( pNodeNew, Abc_NtkCi(pNtkNew, iCi) ); pNodeNew->pData = Abc_SopRegister( (Mem_Flex_t *)pNtkNew->pManFunc, (const char*)Vec_PtrEntry( vSops, i ) ); assert( pNodeNew->pData != (void *)(ABC_PTRINT_T)1 ); Abc_ObjAddFanin( pNode->pCopy, pNodeNew ); } Vec_WecFree( vSupps ); Vec_PtrFree( vSops ); Abc_NtkSortSops( pNtkNew ); return pNtkNew; } Abc_Ntk_t * Abc_NtkCollapseSat( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int nCostMax, int fCanon, int fReverse, int fCnfShared, int fVerbose ) { Abc_Ntk_t * pNtkNew; assert( Abc_NtkIsStrash(pNtk) ); pNtkNew = Abc_NtkFromSopsInt( pNtk, nCubeLim, nBTLimit, nCostMax, fCanon, fReverse, fCnfShared, fVerbose ); if ( pNtkNew == NULL ) return NULL; if ( pNtk->pExdc ) pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc ); if ( !Abc_NtkCheck( pNtkNew ) ) { printf( "Abc_NtkCollapseSat: The network check has failed.\n" ); Abc_NtkDelete( pNtkNew ); return NULL; } return pNtkNew; } //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END