diff options
Diffstat (limited to 'src/base/abci/abcIvy.c')
| -rw-r--r-- | src/base/abci/abcIvy.c | 1105 |
1 files changed, 0 insertions, 1105 deletions
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c deleted file mode 100644 index a470448e..00000000 --- a/src/base/abci/abcIvy.c +++ /dev/null @@ -1,1105 +0,0 @@ -/**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 "abc.h" -#include "dec.h" -#include "ivy.h" -#include "fraig.h" - -//////////////////////////////////////////////////////////////////////// -/// 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 ); -extern char * Mio_GateReadSop( void * pGate ); - -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; - int fCleanup = 1; -//timeRetime = 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 = 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(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; - int 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 = clock(); - -clk = 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) ); -//PRT( " ", clock() - clk ); -//printf( "\n" ); -/* - printf( "Moves = %d. ", nMoves ); - printf( "MovesS = %d. ", nMovesS ); - printf( "Clauses = %d. ", nClauses ); - PRT( "Time", timeInv ); -*/ -// Ivy_ManRewriteSeq( pMan, 1, 0 ); -//printf( "Haig size = %d.\n", Ivy_ManNodeNum(pMan->pHaig) ); -// Ivy_ManHaigPostprocess( pMan, fVerbose ); -//timeRetime = 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 ) -{ - extern void Ivy_CutComputeAll( Ivy_Man_t * p, 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 = clock(); - Ivy_ManRewritePre( pMan, fUpdateLevel, fUseZeroCost, fVerbose ); -//timeRetime = 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 = clock(); - Ivy_ManRewriteSeq( pMan, fUseZeroCost, fVerbose ); -//timeRetime = 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 = pPars; - Abc_Ntk_t * pNtk = *ppNtk, * pNtkTemp; - Abc_Obj_t * pObj, * pFanin; - Ivy_Man_t * pMan; - 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 = ALLOC( int, Abc_NtkPiNum(pNtk) ); - memset( pNtk->pModel, 0, sizeof(int) * Abc_NtkPiNum(pNtk) ); - return 0; - } - - // if SAT only, solve without iteration - RetValue = Abc_NtkMiterSat( pNtk, 2*(sint64)pParams->nMiteringLimitStart, (sint64)0, 0, NULL, NULL ); - if ( RetValue >= 0 ) - return RetValue; - - // apply AIG rewriting - if ( pParams->fUseRewriting && Abc_NtkNodeNum(pNtk) > 500 ) - { -// int clk = 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) ); -//PRT( "Time", clock() - clk ); - } - - // convert ABC network into IVY network - pMan = Abc_NtkIvyBefore( pNtk, 0, 0 ); - - // solve the CEC problem - RetValue = Ivy_FraigProve( &pMan, pParams ); - // convert IVY network into ABC network - pNtk = Abc_NtkIvyAfter( pNtkTemp = pNtk, pMan, 0, 0 ); - Abc_NtkDelete( pNtkTemp ); - // transfer model if given - pNtk->pModel = pMan->pData; pMan->pData = NULL; - Ivy_ManStop( pMan ); - - // try to prove it using brute force SAT - 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(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 ) ) - { - FREE( pInit ); - printf( "Abc_NtkStrash: The network check has failed.\n" ); - Abc_NtkDelete( pNtkAig ); - return NULL; - } - - 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( pNtk->pManFunc, pFaninNew0, pFaninNew1 ); - else - pObjNew = Abc_AigAnd( 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( pNtk->pManFunc, pFaninNew0, pFaninNew1 ); - else - pObjNew = Abc_AigAnd( 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( 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(pNode->pData); - else - pSop = pNode->pData; - - // consider the constant node - if ( Abc_NodeIsConst(pNode) ) - return Ivy_NotCond( Ivy_ManConst1(pMan), Abc_SopIsConst0(pSop) ); - - // consider the special case of EXOR function - if ( Abc_SopIsExorType(pSop) ) - return Abc_NodeStrashAigExorAig( pMan, pNode, pSop ); - - // decide when to use factoring - if ( fUseFactor && Abc_ObjFaninNum(pNode) > 2 && Abc_SopGetCubeNum(pSop) > 1 ) - 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; - - // 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 - 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 ); - extern Ivy_Obj_t * Dec_GraphToNetworkIvy( 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 /// -//////////////////////////////////////////////////////////////////////// - - |