/**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" #include "misc/extra/extraBdd.h" 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, 0) ) { 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 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; } // 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, 0) ) { 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