| /**CFile**************************************************************** |
| |
| FileName [abcIvy.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [Network and node package.] |
| |
| Synopsis [Strashing of the current network.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - June 20, 2005.] |
| |
| Revision [$Id: abcIvy.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "base/abc/abc.h" |
| #include "bool/dec/dec.h" |
| #include "proof/fra/fra.h" |
| #include "aig/ivy/ivy.h" |
| #include "proof/fraig/fraig.h" |
| #include "map/mio/mio.h" |
| #include "aig/aig/aig.h" |
| |
| #ifdef ABC_USE_CUDD |
| #include "bdd/extrab/extraBdd.h" |
| #endif |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); |
| extern void Aig_ManStop( Aig_Man_t * pMan ); |
| //extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose ); |
| extern Ivy_Obj_t * Dec_GraphToNetworkIvy( Ivy_Man_t * pMan, Dec_Graph_t * pGraph ); |
| extern void Ivy_CutComputeAll( Ivy_Man_t * p, int nInputs ); |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| static Abc_Ntk_t * Abc_NtkFromIvy( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan ); |
| static Abc_Ntk_t * Abc_NtkFromIvySeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan, int fHaig ); |
| static Ivy_Man_t * Abc_NtkToIvy( Abc_Ntk_t * pNtkOld ); |
| |
| static void Abc_NtkStrashPerformAig( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan ); |
| static Ivy_Obj_t * Abc_NodeStrashAig( Ivy_Man_t * pMan, Abc_Obj_t * pNode ); |
| static Ivy_Obj_t * Abc_NodeStrashAigSopAig( Ivy_Man_t * pMan, Abc_Obj_t * pNode, char * pSop ); |
| static Ivy_Obj_t * Abc_NodeStrashAigExorAig( Ivy_Man_t * pMan, Abc_Obj_t * pNode, char * pSop ); |
| static Ivy_Obj_t * Abc_NodeStrashAigFactorAig( Ivy_Man_t * pMan, Abc_Obj_t * pNode, char * pSop ); |
| |
| typedef int Abc_Edge_t; |
| static inline Abc_Edge_t Abc_EdgeCreate( int Id, int fCompl ) { return (Id << 1) | fCompl; } |
| static inline int Abc_EdgeId( Abc_Edge_t Edge ) { return Edge >> 1; } |
| static inline int Abc_EdgeIsComplement( Abc_Edge_t Edge ) { return Edge & 1; } |
| static inline Abc_Edge_t Abc_EdgeRegular( Abc_Edge_t Edge ) { return (Edge >> 1) << 1; } |
| static inline Abc_Edge_t Abc_EdgeNot( Abc_Edge_t Edge ) { return Edge ^ 1; } |
| static inline Abc_Edge_t Abc_EdgeNotCond( Abc_Edge_t Edge, int fCond ) { return Edge ^ fCond; } |
| static inline Abc_Edge_t Abc_EdgeFromNode( Abc_Obj_t * pNode ) { return Abc_EdgeCreate( Abc_ObjRegular(pNode)->Id, Abc_ObjIsComplement(pNode) ); } |
| static inline Abc_Obj_t * Abc_EdgeToNode( Abc_Ntk_t * p, Abc_Edge_t Edge ) { return Abc_ObjNotCond( Abc_NtkObj(p, Abc_EdgeId(Edge)), Abc_EdgeIsComplement(Edge) ); } |
| |
| static inline Abc_Obj_t * Abc_ObjFanin0Ivy( Abc_Ntk_t * p, Ivy_Obj_t * pObj ) { return Abc_ObjNotCond( Abc_EdgeToNode(p, Ivy_ObjFanin0(pObj)->TravId), Ivy_ObjFaninC0(pObj) ); } |
| static inline Abc_Obj_t * Abc_ObjFanin1Ivy( Abc_Ntk_t * p, Ivy_Obj_t * pObj ) { return Abc_ObjNotCond( Abc_EdgeToNode(p, Ivy_ObjFanin1(pObj)->TravId), Ivy_ObjFaninC1(pObj) ); } |
| |
| static Vec_Int_t * Abc_NtkCollectLatchValuesIvy( Abc_Ntk_t * pNtk, int fUseDcs ); |
| |
| extern int timeRetime; |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [Prepares the IVY package.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq, int fUseDc ) |
| { |
| Ivy_Man_t * pMan; |
| //timeRetime = Abc_Clock(); |
| assert( !Abc_NtkIsNetlist(pNtk) ); |
| if ( Abc_NtkIsBddLogic(pNtk) ) |
| { |
| if ( !Abc_NtkBddToSop(pNtk, -1, ABC_INFINITY) ) |
| { |
| printf( "Abc_NtkIvyBefore(): Converting to SOPs has failed.\n" ); |
| return NULL; |
| } |
| } |
| if ( fSeq && Abc_NtkCountSelfFeedLatches(pNtk) ) |
| { |
| printf( "Warning: The network has %d self-feeding latches.\n", Abc_NtkCountSelfFeedLatches(pNtk) ); |
| // return NULL; |
| } |
| // print warning about choice nodes |
| if ( Abc_NtkGetChoiceNum( pNtk ) ) |
| printf( "Warning: The choice nodes in the initial AIG are removed by strashing.\n" ); |
| // convert to the AIG manager |
| pMan = Abc_NtkToIvy( pNtk ); |
| if ( !Ivy_ManCheck( pMan ) ) |
| { |
| printf( "AIG check has failed.\n" ); |
| Ivy_ManStop( pMan ); |
| return NULL; |
| } |
| // Ivy_ManPrintStats( pMan ); |
| if ( fSeq ) |
| { |
| int nLatches = Abc_NtkLatchNum(pNtk); |
| Vec_Int_t * vInit = Abc_NtkCollectLatchValuesIvy( pNtk, fUseDc ); |
| Ivy_ManMakeSeq( pMan, nLatches, vInit->pArray ); |
| Vec_IntFree( vInit ); |
| // Ivy_ManPrintStats( pMan ); |
| } |
| //timeRetime = Abc_Clock() - timeRetime; |
| return pMan; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Prepares the IVY package.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Abc_Ntk_t * Abc_NtkIvyAfter( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan, int fSeq, int fHaig ) |
| { |
| Abc_Ntk_t * pNtkAig; |
| int nNodes, fCleanup = 1; |
| // convert from the AIG manager |
| if ( fSeq ) |
| pNtkAig = Abc_NtkFromIvySeq( pNtk, pMan, fHaig ); |
| else |
| pNtkAig = Abc_NtkFromIvy( pNtk, pMan ); |
| // report the cleanup results |
| if ( !fHaig && fCleanup && (nNodes = Abc_AigCleanup((Abc_Aig_t *)pNtkAig->pManFunc)) ) |
| printf( "Warning: AIG cleanup removed %d nodes (this is not a bug).\n", nNodes ); |
| // duplicate EXDC |
| if ( pNtk->pExdc ) |
| pNtkAig->pExdc = Abc_NtkDup( pNtk->pExdc ); |
| // make sure everything is okay |
| if ( !Abc_NtkCheck( pNtkAig ) ) |
| { |
| printf( "Abc_NtkStrash: The network check has failed.\n" ); |
| Abc_NtkDelete( pNtkAig ); |
| return NULL; |
| } |
| return pNtkAig; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Gives the current ABC network to AIG manager for processing.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Abc_Ntk_t * Abc_NtkIvyStrash( Abc_Ntk_t * pNtk ) |
| { |
| Abc_Ntk_t * pNtkAig; |
| Ivy_Man_t * pMan; |
| pMan = Abc_NtkIvyBefore( pNtk, 1, 0 ); |
| if ( pMan == NULL ) |
| return NULL; |
| pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1, 0 ); |
| Ivy_ManStop( pMan ); |
| return pNtkAig; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Gives the current ABC network to AIG manager for processing.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Abc_Ntk_t * Abc_NtkIvyHaig( Abc_Ntk_t * pNtk, int nIters, int fUseZeroCost, int fVerbose ) |
| { |
| Abc_Ntk_t * pNtkAig; |
| Ivy_Man_t * pMan; |
| abctime clk; |
| // int i; |
| /* |
| extern int nMoves; |
| extern int nMovesS; |
| extern int nClauses; |
| extern int timeInv; |
| |
| nMoves = 0; |
| nMovesS = 0; |
| nClauses = 0; |
| timeInv = 0; |
| */ |
| pMan = Abc_NtkIvyBefore( pNtk, 1, 1 ); |
| if ( pMan == NULL ) |
| return NULL; |
| //timeRetime = Abc_Clock(); |
| |
| clk = Abc_Clock(); |
| Ivy_ManHaigStart( pMan, fVerbose ); |
| // Ivy_ManRewriteSeq( pMan, 0, 0 ); |
| // for ( i = 0; i < nIters; i++ ) |
| // Ivy_ManRewriteSeq( pMan, fUseZeroCost, 0 ); |
| |
| //printf( "%d ", Ivy_ManNodeNum(pMan) ); |
| Ivy_ManRewriteSeq( pMan, 0, 0 ); |
| Ivy_ManRewriteSeq( pMan, 0, 0 ); |
| Ivy_ManRewriteSeq( pMan, 1, 0 ); |
| //printf( "%d ", Ivy_ManNodeNum(pMan) ); |
| //printf( "%d ", Ivy_ManNodeNum(pMan->pHaig) ); |
| //ABC_PRT( " ", Abc_Clock() - clk ); |
| //printf( "\n" ); |
| /* |
| printf( "Moves = %d. ", nMoves ); |
| printf( "MovesS = %d. ", nMovesS ); |
| printf( "Clauses = %d. ", nClauses ); |
| ABC_PRT( "Time", timeInv ); |
| */ |
| // Ivy_ManRewriteSeq( pMan, 1, 0 ); |
| //printf( "Haig size = %d.\n", Ivy_ManNodeNum(pMan->pHaig) ); |
| // Ivy_ManHaigPostprocess( pMan, fVerbose ); |
| //timeRetime = Abc_Clock() - timeRetime; |
| |
| // write working AIG into the current network |
| // pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1, 0 ); |
| // write HAIG into the current network |
| pNtkAig = Abc_NtkIvyAfter( pNtk, pMan->pHaig, 1, 1 ); |
| |
| Ivy_ManHaigStop( pMan ); |
| Ivy_ManStop( pMan ); |
| return pNtkAig; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Gives the current ABC network to AIG manager for processing.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Abc_NtkIvyCuts( Abc_Ntk_t * pNtk, int nInputs ) |
| { |
| Ivy_Man_t * pMan; |
| pMan = Abc_NtkIvyBefore( pNtk, 1, 0 ); |
| if ( pMan == NULL ) |
| return; |
| Ivy_CutComputeAll( pMan, nInputs ); |
| Ivy_ManStop( pMan ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Gives the current ABC network to AIG manager for processing.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Abc_Ntk_t * Abc_NtkIvyRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeroCost, int fVerbose ) |
| { |
| Abc_Ntk_t * pNtkAig; |
| Ivy_Man_t * pMan; |
| pMan = Abc_NtkIvyBefore( pNtk, 0, 0 ); |
| if ( pMan == NULL ) |
| return NULL; |
| //timeRetime = Abc_Clock(); |
| Ivy_ManRewritePre( pMan, fUpdateLevel, fUseZeroCost, fVerbose ); |
| //timeRetime = Abc_Clock() - timeRetime; |
| pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 ); |
| Ivy_ManStop( pMan ); |
| return pNtkAig; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Gives the current ABC network to AIG manager for processing.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Abc_Ntk_t * Abc_NtkIvyRewriteSeq( Abc_Ntk_t * pNtk, int fUseZeroCost, int fVerbose ) |
| { |
| Abc_Ntk_t * pNtkAig; |
| Ivy_Man_t * pMan; |
| pMan = Abc_NtkIvyBefore( pNtk, 1, 1 ); |
| if ( pMan == NULL ) |
| return NULL; |
| //timeRetime = Abc_Clock(); |
| Ivy_ManRewriteSeq( pMan, fUseZeroCost, fVerbose ); |
| //timeRetime = Abc_Clock() - timeRetime; |
| // Ivy_ManRewriteSeq( pMan, 1, 0 ); |
| // Ivy_ManRewriteSeq( pMan, 1, 0 ); |
| pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1, 0 ); |
| Ivy_ManStop( pMan ); |
| return pNtkAig; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Gives the current ABC network to AIG manager for processing.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Abc_Ntk_t * Abc_NtkIvyResyn0( Abc_Ntk_t * pNtk, int fUpdateLevel, int fVerbose ) |
| { |
| Abc_Ntk_t * pNtkAig; |
| Ivy_Man_t * pMan, * pTemp; |
| pMan = Abc_NtkIvyBefore( pNtk, 0, 0 ); |
| if ( pMan == NULL ) |
| return NULL; |
| pMan = Ivy_ManResyn0( pTemp = pMan, fUpdateLevel, fVerbose ); |
| Ivy_ManStop( pTemp ); |
| pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 ); |
| Ivy_ManStop( pMan ); |
| return pNtkAig; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Gives the current ABC network to AIG manager for processing.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Abc_Ntk_t * Abc_NtkIvyResyn( Abc_Ntk_t * pNtk, int fUpdateLevel, int fVerbose ) |
| { |
| Abc_Ntk_t * pNtkAig; |
| Ivy_Man_t * pMan, * pTemp; |
| pMan = Abc_NtkIvyBefore( pNtk, 0, 0 ); |
| if ( pMan == NULL ) |
| return NULL; |
| pMan = Ivy_ManResyn( pTemp = pMan, fUpdateLevel, fVerbose ); |
| Ivy_ManStop( pTemp ); |
| pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 ); |
| Ivy_ManStop( pMan ); |
| return pNtkAig; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Gives the current ABC network to AIG manager for processing.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Abc_Ntk_t * Abc_NtkIvySat( Abc_Ntk_t * pNtk, int nConfLimit, int fVerbose ) |
| { |
| Ivy_FraigParams_t Params, * pParams = &Params; |
| Abc_Ntk_t * pNtkAig; |
| Ivy_Man_t * pMan, * pTemp; |
| pMan = Abc_NtkIvyBefore( pNtk, 0, 0 ); |
| if ( pMan == NULL ) |
| return NULL; |
| Ivy_FraigParamsDefault( pParams ); |
| pParams->nBTLimitMiter = nConfLimit; |
| pParams->fVerbose = fVerbose; |
| // pMan = Ivy_FraigPerform( pTemp = pMan, pParams ); |
| pMan = Ivy_FraigMiter( pTemp = pMan, pParams ); |
| Ivy_ManStop( pTemp ); |
| pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 ); |
| Ivy_ManStop( pMan ); |
| return pNtkAig; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Sets the final nodes to point to the original nodes.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Abc_NtkTransferPointers( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig ) |
| { |
| Abc_Obj_t * pObj; |
| Ivy_Obj_t * pObjIvy, * pObjFraig; |
| int i; |
| pObj = Abc_AigConst1(pNtk); |
| pObj->pCopy = Abc_AigConst1(pNtkAig); |
| Abc_NtkForEachCi( pNtk, pObj, i ) |
| pObj->pCopy = Abc_NtkCi(pNtkAig, i); |
| Abc_NtkForEachCo( pNtk, pObj, i ) |
| pObj->pCopy = Abc_NtkCo(pNtkAig, i); |
| Abc_NtkForEachLatch( pNtk, pObj, i ) |
| pObj->pCopy = Abc_NtkBox(pNtkAig, i); |
| Abc_NtkForEachNode( pNtk, pObj, i ) |
| { |
| pObjIvy = (Ivy_Obj_t *)pObj->pCopy; |
| if ( pObjIvy == NULL ) |
| continue; |
| pObjFraig = Ivy_ObjEquiv( pObjIvy ); |
| if ( pObjFraig == NULL ) |
| continue; |
| pObj->pCopy = Abc_EdgeToNode( pNtkAig, Ivy_Regular(pObjFraig)->TravId ); |
| pObj->pCopy = Abc_ObjNotCond( pObj->pCopy, Ivy_IsComplement(pObjFraig) ); |
| } |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Gives the current ABC network to AIG manager for processing.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fVerbose ) |
| { |
| Ivy_FraigParams_t Params, * pParams = &Params; |
| Abc_Ntk_t * pNtkAig; |
| Ivy_Man_t * pMan, * pTemp; |
| pMan = Abc_NtkIvyBefore( pNtk, 0, 0 ); |
| if ( pMan == NULL ) |
| return NULL; |
| Ivy_FraigParamsDefault( pParams ); |
| pParams->nBTLimitNode = nConfLimit; |
| pParams->fVerbose = fVerbose; |
| pParams->fProve = fProve; |
| pParams->fDoSparse = fDoSparse; |
| pMan = Ivy_FraigPerform( pTemp = pMan, pParams ); |
| // transfer the pointers |
| if ( fTransfer == 1 ) |
| { |
| Vec_Ptr_t * vCopies; |
| vCopies = Abc_NtkSaveCopy( pNtk ); |
| pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 ); |
| Abc_NtkLoadCopy( pNtk, vCopies ); |
| Vec_PtrFree( vCopies ); |
| Abc_NtkTransferPointers( pNtk, pNtkAig ); |
| } |
| else |
| pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 ); |
| Ivy_ManStop( pTemp ); |
| Ivy_ManStop( pMan ); |
| return pNtkAig; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Gives the current ABC network to AIG manager for processing.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars ) |
| { |
| Prove_Params_t * pParams = (Prove_Params_t *)pPars; |
| Abc_Ntk_t * pNtk = *ppNtk, * pNtkTemp; |
| Abc_Obj_t * pObj, * pFanin; |
| Ivy_Man_t * pMan; |
| Aig_Man_t * pMan2; |
| int RetValue; |
| assert( Abc_NtkIsStrash(pNtk) || Abc_NtkIsLogic(pNtk) ); |
| // experiment with various parameters settings |
| // pParams->fUseBdds = 1; |
| // pParams->fBddReorder = 1; |
| // pParams->nTotalBacktrackLimit = 10000; |
| |
| // strash the network if it is not strashed already |
| if ( !Abc_NtkIsStrash(pNtk) ) |
| { |
| pNtk = Abc_NtkStrash( pNtkTemp = pNtk, 0, 1, 0 ); |
| Abc_NtkDelete( pNtkTemp ); |
| } |
| |
| // check the case when the 0000 simulation pattern detect the bug |
| pObj = Abc_NtkPo(pNtk,0); |
| pFanin = Abc_ObjFanin0(pObj); |
| if ( Abc_ObjFanin0(pObj)->fPhase != (unsigned)Abc_ObjFaninC0(pObj) ) |
| { |
| pNtk->pModel = ABC_CALLOC( int, Abc_NtkCiNum(pNtk) ); |
| return 0; |
| } |
| |
| // changed in "src\sat\fraig\fraigMan.c" |
| // pParams->nMiteringLimitStart = 300; // starting mitering limit |
| // to be |
| // pParams->nMiteringLimitStart = 5000; // starting mitering limit |
| |
| // if SAT only, solve without iteration |
| // RetValue = Abc_NtkMiterSat( pNtk, 2*(ABC_INT64_T)pParams->nMiteringLimitStart, (ABC_INT64_T)0, 0, NULL, NULL ); |
| pMan2 = Abc_NtkToDar( pNtk, 0, 0 ); |
| RetValue = Fra_FraigSat( pMan2, (ABC_INT64_T)pParams->nMiteringLimitStart, (ABC_INT64_T)0, 0, 0, 0, 1, 0, 0, 0 ); |
| pNtk->pModel = (int *)pMan2->pData, pMan2->pData = NULL; |
| Aig_ManStop( pMan2 ); |
| // pNtk->pModel = Aig_ManReleaseData( pMan2 ); |
| if ( RetValue >= 0 ) |
| return RetValue; |
| |
| // apply AIG rewriting |
| if ( pParams->fUseRewriting && Abc_NtkNodeNum(pNtk) > 500 ) |
| { |
| // abctime clk = Abc_Clock(); |
| //printf( "Before rwsat = %d. ", Abc_NtkNodeNum(pNtk) ); |
| pParams->fUseRewriting = 0; |
| pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 ); |
| Abc_NtkDelete( pNtkTemp ); |
| Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 ); |
| pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 ); |
| Abc_NtkDelete( pNtkTemp ); |
| Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 ); |
| Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 ); |
| //printf( "After rwsat = %d. ", Abc_NtkNodeNum(pNtk) ); |
| //ABC_PRT( "Time", Abc_Clock() - clk ); |
| } |
| |
| // convert ABC network into IVY network |
| pMan = Abc_NtkIvyBefore( pNtk, 0, 0 ); |
| |
| // solve the CEC problem |
| RetValue = Ivy_FraigProve( &pMan, pParams ); |
| // RetValue = -1; |
| |
| // convert IVY network into ABC network |
| pNtk = Abc_NtkIvyAfter( pNtkTemp = pNtk, pMan, 0, 0 ); |
| Abc_NtkDelete( pNtkTemp ); |
| // transfer model if given |
| pNtk->pModel = (int *)pMan->pData; pMan->pData = NULL; |
| Ivy_ManStop( pMan ); |
| |
| // try to prove it using brute force SAT with good CNF encoding |
| if ( RetValue < 0 ) |
| { |
| pMan2 = Abc_NtkToDar( pNtk, 0, 0 ); |
| // dump the miter before entering high-effort solving |
| if ( pParams->fVerbose ) |
| { |
| char pFileName[100]; |
| sprintf( pFileName, "cecmiter.aig" ); |
| Ioa_WriteAiger( pMan2, pFileName, 0, 0 ); |
| printf( "Intermediate reduced miter is written into file \"%s\".\n", pFileName ); |
| } |
| RetValue = Fra_FraigSat( pMan2, pParams->nMiteringLimitLast, 0, 0, 0, 0, 0, 0, 0, pParams->fVerbose ); |
| pNtk->pModel = (int *)pMan2->pData, pMan2->pData = NULL; |
| Aig_ManStop( pMan2 ); |
| } |
| |
| // try to prove it using brute force BDDs |
| #ifdef ABC_USE_CUDD |
| if ( RetValue < 0 && pParams->fUseBdds ) |
| { |
| if ( pParams->fVerbose ) |
| { |
| printf( "Attempting BDDs with node limit %d ...\n", pParams->nBddSizeLimit ); |
| fflush( stdout ); |
| } |
| pNtk = Abc_NtkCollapse( pNtkTemp = pNtk, pParams->nBddSizeLimit, 0, pParams->fBddReorder, 0 ); |
| if ( pNtk ) |
| { |
| Abc_NtkDelete( pNtkTemp ); |
| RetValue = ( (Abc_NtkNodeNum(pNtk) == 1) && (Abc_ObjFanin0(Abc_NtkPo(pNtk,0))->pData == Cudd_ReadLogicZero((DdManager *)pNtk->pManFunc)) ); |
| } |
| else |
| pNtk = pNtkTemp; |
| } |
| #endif |
| |
| // return the result |
| *ppNtk = pNtk; |
| return RetValue; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Gives the current ABC network to AIG manager for processing.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk ) |
| { |
| // Abc_Ntk_t * pNtkAig; |
| Ivy_Man_t * pMan;//, * pTemp; |
| // int fCleanup = 1; |
| // int nNodes; |
| // int nLatches = Abc_NtkLatchNum(pNtk); |
| Vec_Int_t * vInit = Abc_NtkCollectLatchValuesIvy( pNtk, 0 ); |
| |
| assert( !Abc_NtkIsNetlist(pNtk) ); |
| if ( Abc_NtkIsBddLogic(pNtk) ) |
| { |
| if ( !Abc_NtkBddToSop(pNtk, -1, ABC_INFINITY) ) |
| { |
| Vec_IntFree( vInit ); |
| printf( "Abc_NtkIvy(): Converting to SOPs has failed.\n" ); |
| return NULL; |
| } |
| } |
| if ( Abc_NtkCountSelfFeedLatches(pNtk) ) |
| { |
| printf( "Warning: The network has %d self-feeding latches. Quitting.\n", Abc_NtkCountSelfFeedLatches(pNtk) ); |
| return NULL; |
| } |
| |
| // print warning about choice nodes |
| if ( Abc_NtkGetChoiceNum( pNtk ) ) |
| printf( "Warning: The choice nodes in the initial AIG are removed by strashing.\n" ); |
| |
| // convert to the AIG manager |
| pMan = Abc_NtkToIvy( pNtk ); |
| if ( !Ivy_ManCheck( pMan ) ) |
| { |
| Vec_IntFree( vInit ); |
| printf( "AIG check has failed.\n" ); |
| Ivy_ManStop( pMan ); |
| return NULL; |
| } |
| |
| // Ivy_MffcTest( pMan ); |
| // Ivy_ManPrintStats( pMan ); |
| |
| // pMan = Ivy_ManBalance( pTemp = pMan, 1 ); |
| // Ivy_ManStop( pTemp ); |
| |
| // Ivy_ManSeqRewrite( pMan, 0, 0 ); |
| // Ivy_ManTestCutsAlg( pMan ); |
| // Ivy_ManTestCutsBool( pMan ); |
| // Ivy_ManRewriteAlg( pMan, 1, 1 ); |
| |
| // pMan = Ivy_ManResyn( pTemp = pMan, 1, 0 ); |
| // Ivy_ManStop( pTemp ); |
| |
| // Ivy_ManTestCutsAll( pMan ); |
| // Ivy_ManTestCutsTravAll( pMan ); |
| |
| // Ivy_ManPrintStats( pMan ); |
| |
| // Ivy_ManPrintStats( pMan ); |
| // Ivy_ManRewritePre( pMan, 1, 0, 0 ); |
| // Ivy_ManPrintStats( pMan ); |
| // printf( "\n" ); |
| |
| // Ivy_ManPrintStats( pMan ); |
| // Ivy_ManMakeSeq( pMan, nLatches, pInit ); |
| // Ivy_ManPrintStats( pMan ); |
| |
| // Ivy_ManRequiredLevels( pMan ); |
| |
| // Ivy_FastMapPerform( pMan, 8 ); |
| Ivy_ManStop( pMan ); |
| return NULL; |
| |
| |
| /* |
| // convert from the AIG manager |
| pNtkAig = Abc_NtkFromIvy( pNtk, pMan ); |
| // pNtkAig = Abc_NtkFromIvySeq( pNtk, pMan ); |
| Ivy_ManStop( pMan ); |
| |
| // report the cleanup results |
| if ( fCleanup && (nNodes = Abc_AigCleanup(pNtkAig->pManFunc)) ) |
| printf( "Warning: AIG cleanup removed %d nodes (this is not a bug).\n", nNodes ); |
| // duplicate EXDC |
| if ( pNtk->pExdc ) |
| pNtkAig->pExdc = Abc_NtkDup( pNtk->pExdc ); |
| // make sure everything is okay |
| if ( !Abc_NtkCheck( pNtkAig ) ) |
| { |
| ABC_FREE( pInit ); |
| printf( "Abc_NtkStrash: The network check has failed.\n" ); |
| Abc_NtkDelete( pNtkAig ); |
| return NULL; |
| } |
| |
| ABC_FREE( pInit ); |
| return pNtkAig; |
| */ |
| } |
| |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Converts the network from the AIG manager into ABC.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Abc_Ntk_t * Abc_NtkFromIvy( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan ) |
| { |
| Vec_Int_t * vNodes; |
| Abc_Ntk_t * pNtk; |
| Abc_Obj_t * pObj, * pObjNew, * pFaninNew, * pFaninNew0, * pFaninNew1; |
| Ivy_Obj_t * pNode; |
| int i; |
| // perform strashing |
| pNtk = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG ); |
| // transfer the pointers to the basic nodes |
| Ivy_ManConst1(pMan)->TravId = Abc_EdgeFromNode( Abc_AigConst1(pNtk) ); |
| Abc_NtkForEachCi( pNtkOld, pObj, i ) |
| Ivy_ManPi(pMan, i)->TravId = Abc_EdgeFromNode( pObj->pCopy ); |
| // rebuild the AIG |
| vNodes = Ivy_ManDfs( pMan ); |
| Ivy_ManForEachNodeVec( pMan, vNodes, pNode, i ) |
| { |
| // add the first fanin |
| pFaninNew0 = Abc_ObjFanin0Ivy( pNtk, pNode ); |
| if ( Ivy_ObjIsBuf(pNode) ) |
| { |
| pNode->TravId = Abc_EdgeFromNode( pFaninNew0 ); |
| continue; |
| } |
| // add the second fanin |
| pFaninNew1 = Abc_ObjFanin1Ivy( pNtk, pNode ); |
| // create the new node |
| if ( Ivy_ObjIsExor(pNode) ) |
| pObjNew = Abc_AigXor( (Abc_Aig_t *)pNtk->pManFunc, pFaninNew0, pFaninNew1 ); |
| else |
| pObjNew = Abc_AigAnd( (Abc_Aig_t *)pNtk->pManFunc, pFaninNew0, pFaninNew1 ); |
| pNode->TravId = Abc_EdgeFromNode( pObjNew ); |
| } |
| // connect the PO nodes |
| Abc_NtkForEachCo( pNtkOld, pObj, i ) |
| { |
| pFaninNew = Abc_ObjFanin0Ivy( pNtk, Ivy_ManPo(pMan, i) ); |
| Abc_ObjAddFanin( pObj->pCopy, pFaninNew ); |
| } |
| Vec_IntFree( vNodes ); |
| if ( !Abc_NtkCheck( pNtk ) ) |
| fprintf( stdout, "Abc_NtkFromIvy(): Network check has failed.\n" ); |
| return pNtk; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Converts the network from the AIG manager into ABC.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Abc_Ntk_t * Abc_NtkFromIvySeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan, int fHaig ) |
| { |
| Vec_Int_t * vNodes, * vLatches; |
| Abc_Ntk_t * pNtk; |
| Abc_Obj_t * pObj, * pObjNew, * pFaninNew, * pFaninNew0, * pFaninNew1; |
| Ivy_Obj_t * pNode, * pTemp; |
| int i; |
| // assert( Ivy_ManLatchNum(pMan) > 0 ); |
| // perform strashing |
| pNtk = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG ); |
| // transfer the pointers to the basic nodes |
| Ivy_ManConst1(pMan)->TravId = Abc_EdgeFromNode( Abc_AigConst1(pNtk) ); |
| Abc_NtkForEachPi( pNtkOld, pObj, i ) |
| Ivy_ManPi(pMan, i)->TravId = Abc_EdgeFromNode( pObj->pCopy ); |
| // create latches of the new network |
| vNodes = Ivy_ManDfsSeq( pMan, &vLatches ); |
| Ivy_ManForEachNodeVec( pMan, vLatches, pNode, i ) |
| { |
| pObjNew = Abc_NtkCreateLatch( pNtk ); |
| pFaninNew0 = Abc_NtkCreateBi( pNtk ); |
| pFaninNew1 = Abc_NtkCreateBo( pNtk ); |
| Abc_ObjAddFanin( pObjNew, pFaninNew0 ); |
| Abc_ObjAddFanin( pFaninNew1, pObjNew ); |
| if ( fHaig || Ivy_ObjInit(pNode) == IVY_INIT_DC ) |
| Abc_LatchSetInitDc( pObjNew ); |
| else if ( Ivy_ObjInit(pNode) == IVY_INIT_1 ) |
| Abc_LatchSetInit1( pObjNew ); |
| else if ( Ivy_ObjInit(pNode) == IVY_INIT_0 ) |
| Abc_LatchSetInit0( pObjNew ); |
| else assert( 0 ); |
| pNode->TravId = Abc_EdgeFromNode( pFaninNew1 ); |
| } |
| Abc_NtkAddDummyBoxNames( pNtk ); |
| // rebuild the AIG |
| Ivy_ManForEachNodeVec( pMan, vNodes, pNode, i ) |
| { |
| // add the first fanin |
| pFaninNew0 = Abc_ObjFanin0Ivy( pNtk, pNode ); |
| if ( Ivy_ObjIsBuf(pNode) ) |
| { |
| pNode->TravId = Abc_EdgeFromNode( pFaninNew0 ); |
| continue; |
| } |
| // add the second fanin |
| pFaninNew1 = Abc_ObjFanin1Ivy( pNtk, pNode ); |
| // create the new node |
| if ( Ivy_ObjIsExor(pNode) ) |
| pObjNew = Abc_AigXor( (Abc_Aig_t *)pNtk->pManFunc, pFaninNew0, pFaninNew1 ); |
| else |
| pObjNew = Abc_AigAnd( (Abc_Aig_t *)pNtk->pManFunc, pFaninNew0, pFaninNew1 ); |
| pNode->TravId = Abc_EdgeFromNode( pObjNew ); |
| // process the choice nodes |
| if ( fHaig && pNode->pEquiv && Ivy_ObjRefs(pNode) > 0 ) |
| { |
| pFaninNew = Abc_EdgeToNode( pNtk, pNode->TravId ); |
| // pFaninNew->fPhase = 0; |
| assert( !Ivy_IsComplement(pNode->pEquiv) ); |
| for ( pTemp = pNode->pEquiv; pTemp != pNode; pTemp = Ivy_Regular(pTemp->pEquiv) ) |
| { |
| pFaninNew1 = Abc_EdgeToNode( pNtk, pTemp->TravId ); |
| // pFaninNew1->fPhase = Ivy_IsComplement( pTemp->pEquiv ); |
| pFaninNew->pData = pFaninNew1; |
| pFaninNew = pFaninNew1; |
| } |
| pFaninNew->pData = NULL; |
| // printf( "Writing choice node %d.\n", pNode->Id ); |
| } |
| } |
| // connect the PO nodes |
| Abc_NtkForEachPo( pNtkOld, pObj, i ) |
| { |
| pFaninNew = Abc_ObjFanin0Ivy( pNtk, Ivy_ManPo(pMan, i) ); |
| Abc_ObjAddFanin( pObj->pCopy, pFaninNew ); |
| } |
| // connect the latches |
| Ivy_ManForEachNodeVec( pMan, vLatches, pNode, i ) |
| { |
| pFaninNew = Abc_ObjFanin0Ivy( pNtk, pNode ); |
| Abc_ObjAddFanin( Abc_ObjFanin0(Abc_NtkBox(pNtk, i)), pFaninNew ); |
| } |
| Vec_IntFree( vLatches ); |
| Vec_IntFree( vNodes ); |
| if ( !Abc_NtkCheck( pNtk ) ) |
| fprintf( stdout, "Abc_NtkFromIvySeq(): Network check has failed.\n" ); |
| return pNtk; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Converts the network from the AIG manager into ABC.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Ivy_Man_t * Abc_NtkToIvy( Abc_Ntk_t * pNtkOld ) |
| { |
| Ivy_Man_t * pMan; |
| Abc_Obj_t * pObj; |
| Ivy_Obj_t * pFanin; |
| int i; |
| // create the manager |
| assert( Abc_NtkHasSop(pNtkOld) || Abc_NtkIsStrash(pNtkOld) ); |
| pMan = Ivy_ManStart(); |
| // create the PIs |
| if ( Abc_NtkIsStrash(pNtkOld) ) |
| Abc_AigConst1(pNtkOld)->pCopy = (Abc_Obj_t *)Ivy_ManConst1(pMan); |
| Abc_NtkForEachCi( pNtkOld, pObj, i ) |
| pObj->pCopy = (Abc_Obj_t *)Ivy_ObjCreatePi(pMan); |
| // perform the conversion of the internal nodes |
| Abc_NtkStrashPerformAig( pNtkOld, pMan ); |
| // create the POs |
| Abc_NtkForEachCo( pNtkOld, pObj, i ) |
| { |
| pFanin = (Ivy_Obj_t *)Abc_ObjFanin0(pObj)->pCopy; |
| pFanin = Ivy_NotCond( pFanin, Abc_ObjFaninC0(pObj) ); |
| Ivy_ObjCreatePo( pMan, pFanin ); |
| } |
| Ivy_ManCleanup( pMan ); |
| return pMan; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Prepares the network for strashing.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Abc_NtkStrashPerformAig( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan ) |
| { |
| // ProgressBar * pProgress; |
| Vec_Ptr_t * vNodes; |
| Abc_Obj_t * pNode; |
| int i; |
| vNodes = Abc_NtkDfs( pNtk, 0 ); |
| // pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize ); |
| Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i ) |
| { |
| // Extra_ProgressBarUpdate( pProgress, i, NULL ); |
| pNode->pCopy = (Abc_Obj_t *)Abc_NodeStrashAig( pMan, pNode ); |
| } |
| // Extra_ProgressBarStop( pProgress ); |
| Vec_PtrFree( vNodes ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Strashes one logic node.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Ivy_Obj_t * Abc_NodeStrashAig( Ivy_Man_t * pMan, Abc_Obj_t * pNode ) |
| { |
| int fUseFactor = 1; |
| char * pSop; |
| Ivy_Obj_t * pFanin0, * pFanin1; |
| |
| assert( Abc_ObjIsNode(pNode) ); |
| |
| // consider the case when the graph is an AIG |
| if ( Abc_NtkIsStrash(pNode->pNtk) ) |
| { |
| if ( Abc_AigNodeIsConst(pNode) ) |
| return Ivy_ManConst1(pMan); |
| pFanin0 = (Ivy_Obj_t *)Abc_ObjFanin0(pNode)->pCopy; |
| pFanin0 = Ivy_NotCond( pFanin0, Abc_ObjFaninC0(pNode) ); |
| pFanin1 = (Ivy_Obj_t *)Abc_ObjFanin1(pNode)->pCopy; |
| pFanin1 = Ivy_NotCond( pFanin1, Abc_ObjFaninC1(pNode) ); |
| return Ivy_And( pMan, pFanin0, pFanin1 ); |
| } |
| |
| // get the SOP of the node |
| if ( Abc_NtkHasMapping(pNode->pNtk) ) |
| pSop = Mio_GateReadSop((Mio_Gate_t *)pNode->pData); |
| else |
| pSop = (char *)pNode->pData; |
| |
| // consider the constant node |
| if ( Abc_NodeIsConst(pNode) ) |
| return Ivy_NotCond( Ivy_ManConst1(pMan), Abc_SopIsConst0(pSop) ); |
| |
| // decide when to use factoring |
| if ( fUseFactor && Abc_ObjFaninNum(pNode) > 2 && Abc_SopGetCubeNum(pSop) > 1 && !Abc_SopIsExorType(pSop) ) |
| return Abc_NodeStrashAigFactorAig( pMan, pNode, pSop ); |
| return Abc_NodeStrashAigSopAig( pMan, pNode, pSop ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Strashes one logic node using its SOP.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Ivy_Obj_t * Abc_NodeStrashAigSopAig( Ivy_Man_t * pMan, Abc_Obj_t * pNode, char * pSop ) |
| { |
| Abc_Obj_t * pFanin; |
| Ivy_Obj_t * pAnd, * pSum; |
| char * pCube; |
| int i, nFanins; |
| int fExor = Abc_SopIsExorType(pSop); |
| |
| // get the number of node's fanins |
| nFanins = Abc_ObjFaninNum( pNode ); |
| assert( nFanins == Abc_SopGetVarNum(pSop) ); |
| // go through the cubes of the node's SOP |
| pSum = Ivy_Not( Ivy_ManConst1(pMan) ); |
| Abc_SopForEachCube( pSop, nFanins, pCube ) |
| { |
| // create the AND of literals |
| pAnd = Ivy_ManConst1(pMan); |
| Abc_ObjForEachFanin( pNode, pFanin, i ) // pFanin can be a net |
| { |
| if ( pCube[i] == '1' ) |
| pAnd = Ivy_And( pMan, pAnd, (Ivy_Obj_t *)pFanin->pCopy ); |
| else if ( pCube[i] == '0' ) |
| pAnd = Ivy_And( pMan, pAnd, Ivy_Not((Ivy_Obj_t *)pFanin->pCopy) ); |
| } |
| // add to the sum of cubes |
| if ( fExor ) |
| pSum = Ivy_Exor( pMan, pSum, pAnd ); |
| else |
| pSum = Ivy_Or( pMan, pSum, pAnd ); |
| } |
| // decide whether to complement the result |
| if ( Abc_SopIsComplement(pSop) ) |
| pSum = Ivy_Not(pSum); |
| return pSum; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Strashed n-input XOR function.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Ivy_Obj_t * Abc_NodeStrashAigExorAig( Ivy_Man_t * pMan, Abc_Obj_t * pNode, char * pSop ) |
| { |
| Abc_Obj_t * pFanin; |
| Ivy_Obj_t * pSum; |
| int i, nFanins; |
| // get the number of node's fanins |
| nFanins = Abc_ObjFaninNum( pNode ); |
| assert( nFanins == Abc_SopGetVarNum(pSop) ); |
| // go through the cubes of the node's SOP |
| pSum = Ivy_Not( Ivy_ManConst1(pMan) ); |
| for ( i = 0; i < nFanins; i++ ) |
| { |
| pFanin = Abc_ObjFanin( pNode, i ); |
| pSum = Ivy_Exor( pMan, pSum, (Ivy_Obj_t *)pFanin->pCopy ); |
| } |
| if ( Abc_SopIsComplement(pSop) ) |
| pSum = Ivy_Not(pSum); |
| return pSum; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Strashes one logic node using its SOP.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Ivy_Obj_t * Abc_NodeStrashAigFactorAig( Ivy_Man_t * pMan, Abc_Obj_t * pRoot, char * pSop ) |
| { |
| Dec_Graph_t * pFForm; |
| Dec_Node_t * pNode; |
| Ivy_Obj_t * pAnd; |
| int i; |
| |
| // extern Ivy_Obj_t * Dec_GraphToNetworkAig( Ivy_Man_t * pMan, Dec_Graph_t * pGraph ); |
| |
| // assert( 0 ); |
| |
| // perform factoring |
| pFForm = Dec_Factor( pSop ); |
| // collect the fanins |
| Dec_GraphForEachLeaf( pFForm, pNode, i ) |
| pNode->pFunc = Abc_ObjFanin(pRoot,i)->pCopy; |
| // perform strashing |
| // pAnd = Dec_GraphToNetworkAig( pMan, pFForm ); |
| pAnd = Dec_GraphToNetworkIvy( pMan, pFForm ); |
| // pAnd = NULL; |
| |
| Dec_GraphFree( pFForm ); |
| return pAnd; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Strashes one logic node using its SOP.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Int_t * Abc_NtkCollectLatchValuesIvy( Abc_Ntk_t * pNtk, int fUseDcs ) |
| { |
| Abc_Obj_t * pLatch; |
| Vec_Int_t * vArray; |
| int i; |
| vArray = Vec_IntAlloc( Abc_NtkLatchNum(pNtk) ); |
| Abc_NtkForEachLatch( pNtk, pLatch, i ) |
| { |
| if ( fUseDcs || Abc_LatchIsInitDc(pLatch) ) |
| Vec_IntPush( vArray, IVY_INIT_DC ); |
| else if ( Abc_LatchIsInit1(pLatch) ) |
| Vec_IntPush( vArray, IVY_INIT_1 ); |
| else if ( Abc_LatchIsInit0(pLatch) ) |
| Vec_IntPush( vArray, IVY_INIT_0 ); |
| else assert( 0 ); |
| } |
| return vArray; |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
