diff options
Diffstat (limited to 'src/aig/ivy/ivy.h')
| -rw-r--r-- | src/aig/ivy/ivy.h | 557 |
1 files changed, 0 insertions, 557 deletions
diff --git a/src/aig/ivy/ivy.h b/src/aig/ivy/ivy.h deleted file mode 100644 index ed19d67c..00000000 --- a/src/aig/ivy/ivy.h +++ /dev/null @@ -1,557 +0,0 @@ -/**CFile**************************************************************** - - FileName [ivy.h] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [And-Inverter Graph package.] - - Synopsis [External declarations.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - May 11, 2006.] - - Revision [$Id: ivy.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#ifndef __IVY_H__ -#define __IVY_H__ - -#ifdef __cplusplus -extern "C" { -#endif - -//////////////////////////////////////////////////////////////////////// -/// INCLUDES /// -//////////////////////////////////////////////////////////////////////// - -#include <stdio.h> -#include "extra.h" -#include "vec.h" - -//////////////////////////////////////////////////////////////////////// -/// PARAMETERS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// BASIC TYPES /// -//////////////////////////////////////////////////////////////////////// - -typedef struct Ivy_Man_t_ Ivy_Man_t; -typedef struct Ivy_Obj_t_ Ivy_Obj_t; -typedef int Ivy_Edge_t; -typedef struct Ivy_FraigParams_t_ Ivy_FraigParams_t; - -// object types -typedef enum { - IVY_NONE, // 0: non-existent object - IVY_PI, // 1: primary input (and constant 1 node) - IVY_PO, // 2: primary output - IVY_ASSERT, // 3: assertion - IVY_LATCH, // 4: sequential element - IVY_AND, // 5: AND node - IVY_EXOR, // 6: EXOR node - IVY_BUF, // 7: buffer (temporary) - IVY_VOID // 8: unused object -} Ivy_Type_t; - -// latch initial values -typedef enum { - IVY_INIT_NONE, // 0: not a latch - IVY_INIT_0, // 1: zero - IVY_INIT_1, // 2: one - IVY_INIT_DC // 3: don't-care -} Ivy_Init_t; - -// the AIG node -struct Ivy_Obj_t_ // 24 bytes (32-bit) or 32 bytes (64-bit) // 10 words - 16 words -{ - int Id; // integer ID - int TravId; // traversal ID - unsigned Type : 4; // object type - unsigned fMarkA : 1; // multipurpose mask - unsigned fMarkB : 1; // multipurpose mask - unsigned fExFan : 1; // set to 1 if last fanout added is EXOR - unsigned fPhase : 1; // value under 000...0 pattern - unsigned fFailTfo : 1; // the TFO of the failed node - unsigned Init : 2; // latch initial value - unsigned Level : 21; // logic level - int nRefs; // reference counter - Ivy_Obj_t * pFanin0; // fanin - Ivy_Obj_t * pFanin1; // fanin - Ivy_Obj_t * pFanout; // fanout - Ivy_Obj_t * pNextFan0; // next fanout of the first fanin - Ivy_Obj_t * pNextFan1; // next fanout of the second fanin - Ivy_Obj_t * pPrevFan0; // prev fanout of the first fanin - Ivy_Obj_t * pPrevFan1; // prev fanout of the second fanin - Ivy_Obj_t * pEquiv; // equivalent node -}; - -// the AIG manager -struct Ivy_Man_t_ -{ - // AIG nodes - Vec_Ptr_t * vPis; // the array of PIs - Vec_Ptr_t * vPos; // the array of POs - Vec_Ptr_t * vBufs; // the array of buffers - Vec_Ptr_t * vObjs; // the array of objects - Ivy_Obj_t * pConst1; // the constant 1 node - Ivy_Obj_t Ghost; // the ghost node - // AIG node counters - int nObjs[IVY_VOID];// the number of objects by type - int nCreated; // the number of created objects - int nDeleted; // the number of deleted objects - // stuctural hash table - int * pTable; // structural hash table - int nTableSize; // structural hash table size - // various data members - int fCatchExor; // set to 1 to detect EXORs - int nTravIds; // the traversal ID - int nLevelMax; // the maximum level - Vec_Int_t * vRequired; // required times - int fFanout; // fanout is allocated - void * pData; // the temporary data - void * pCopy; // the temporary data - Ivy_Man_t * pHaig; // history AIG if present - int nClassesSkip; // the number of skipped classes - // memory management - Vec_Ptr_t * vChunks; // allocated memory pieces - Vec_Ptr_t * vPages; // memory pages used by nodes - Ivy_Obj_t * pListFree; // the list of free nodes - // timing statistics - int time1; - int time2; -}; - -struct Ivy_FraigParams_t_ -{ - int nSimWords; // the number of words in the simulation info - double dSimSatur; // the ratio of refined classes when saturation is reached - int fPatScores; // enables simulation pattern scoring - int MaxScore; // max score after which resimulation is used - double dActConeRatio; // the ratio of cone to be bumped - double dActConeBumpMax; // the largest bump in activity - int fProve; // prove the miter outputs - int fVerbose; // verbose output - int fDoSparse; // skip sparse functions - int nBTLimitNode; // conflict limit at a node - int nBTLimitMiter; // conflict limit at an output -// int nBTLimitGlobal; // conflict limit global -// int nInsLimitNode; // inspection limit at a node -// int nInsLimitMiter; // inspection limit at an output -// int nInsLimitGlobal; // inspection limit global -}; - - -#define IVY_CUT_LIMIT 256 -#define IVY_CUT_INPUT 6 - -typedef struct Ivy_Cut_t_ Ivy_Cut_t; -struct Ivy_Cut_t_ -{ - int nLatches; - short nSize; - short nSizeMax; - int pArray[IVY_CUT_INPUT]; - unsigned uHash; -}; - -typedef struct Ivy_Store_t_ Ivy_Store_t; -struct Ivy_Store_t_ -{ - int nCuts; - int nCutsM; - int nCutsMax; - int fSatur; - Ivy_Cut_t pCuts[IVY_CUT_LIMIT]; // storage for cuts -}; - -#define IVY_LEAF_MASK 255 -#define IVY_LEAF_BITS 8 - -//////////////////////////////////////////////////////////////////////// -/// MACRO DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -#define IVY_MIN(a,b) (((a) < (b))? (a) : (b)) -#define IVY_MAX(a,b) (((a) > (b))? (a) : (b)) - -static inline int Ivy_BitWordNum( int nBits ) { return (nBits>>5) + ((nBits&31) > 0); } -static inline int Ivy_TruthWordNum( int nVars ) { return nVars <= 5 ? 1 : (1 << (nVars - 5)); } -static inline int Ivy_InfoHasBit( unsigned * p, int i ) { return (p[(i)>>5] & (1<<((i) & 31))) > 0; } -static inline void Ivy_InfoSetBit( unsigned * p, int i ) { p[(i)>>5] |= (1<<((i) & 31)); } -static inline void Ivy_InfoXorBit( unsigned * p, int i ) { p[(i)>>5] ^= (1<<((i) & 31)); } - -static inline Ivy_Obj_t * Ivy_Regular( Ivy_Obj_t * p ) { return (Ivy_Obj_t *)((unsigned long)(p) & ~01); } -static inline Ivy_Obj_t * Ivy_Not( Ivy_Obj_t * p ) { return (Ivy_Obj_t *)((unsigned long)(p) ^ 01); } -static inline Ivy_Obj_t * Ivy_NotCond( Ivy_Obj_t * p, int c ) { return (Ivy_Obj_t *)((unsigned long)(p) ^ (c)); } -static inline int Ivy_IsComplement( Ivy_Obj_t * p ) { return (int )(((unsigned long)p) & 01); } - -static inline Ivy_Obj_t * Ivy_ManConst0( Ivy_Man_t * p ) { return Ivy_Not(p->pConst1); } -static inline Ivy_Obj_t * Ivy_ManConst1( Ivy_Man_t * p ) { return p->pConst1; } -static inline Ivy_Obj_t * Ivy_ManGhost( Ivy_Man_t * p ) { return &p->Ghost; } -static inline Ivy_Obj_t * Ivy_ManPi( Ivy_Man_t * p, int i ) { return (Ivy_Obj_t *)Vec_PtrEntry(p->vPis, i); } -static inline Ivy_Obj_t * Ivy_ManPo( Ivy_Man_t * p, int i ) { return (Ivy_Obj_t *)Vec_PtrEntry(p->vPos, i); } -static inline Ivy_Obj_t * Ivy_ManObj( Ivy_Man_t * p, int i ) { return (Ivy_Obj_t *)Vec_PtrEntry(p->vObjs, i); } - -static inline Ivy_Edge_t Ivy_EdgeCreate( int Id, int fCompl ) { return (Id << 1) | fCompl; } -static inline int Ivy_EdgeId( Ivy_Edge_t Edge ) { return Edge >> 1; } -static inline int Ivy_EdgeIsComplement( Ivy_Edge_t Edge ) { return Edge & 1; } -static inline Ivy_Edge_t Ivy_EdgeRegular( Ivy_Edge_t Edge ) { return (Edge >> 1) << 1; } -static inline Ivy_Edge_t Ivy_EdgeNot( Ivy_Edge_t Edge ) { return Edge ^ 1; } -static inline Ivy_Edge_t Ivy_EdgeNotCond( Ivy_Edge_t Edge, int fCond ) { return Edge ^ fCond; } -static inline Ivy_Edge_t Ivy_EdgeFromNode( Ivy_Obj_t * pNode ) { return Ivy_EdgeCreate( Ivy_Regular(pNode)->Id, Ivy_IsComplement(pNode) ); } -static inline Ivy_Obj_t * Ivy_EdgeToNode( Ivy_Man_t * p, Ivy_Edge_t Edge ){ return Ivy_NotCond( Ivy_ManObj(p, Ivy_EdgeId(Edge)), Ivy_EdgeIsComplement(Edge) ); } - -static inline int Ivy_LeafCreate( int Id, int Lat ) { return (Id << IVY_LEAF_BITS) | Lat; } -static inline int Ivy_LeafId( int Leaf ) { return Leaf >> IVY_LEAF_BITS; } -static inline int Ivy_LeafLat( int Leaf ) { return Leaf & IVY_LEAF_MASK; } - -static inline int Ivy_ManPiNum( Ivy_Man_t * p ) { return p->nObjs[IVY_PI]; } -static inline int Ivy_ManPoNum( Ivy_Man_t * p ) { return p->nObjs[IVY_PO]; } -static inline int Ivy_ManAssertNum( Ivy_Man_t * p ) { return p->nObjs[IVY_ASSERT]; } -static inline int Ivy_ManLatchNum( Ivy_Man_t * p ) { return p->nObjs[IVY_LATCH]; } -static inline int Ivy_ManAndNum( Ivy_Man_t * p ) { return p->nObjs[IVY_AND]; } -static inline int Ivy_ManExorNum( Ivy_Man_t * p ) { return p->nObjs[IVY_EXOR]; } -static inline int Ivy_ManBufNum( Ivy_Man_t * p ) { return p->nObjs[IVY_BUF]; } -static inline int Ivy_ManObjNum( Ivy_Man_t * p ) { return p->nCreated - p->nDeleted; } -static inline int Ivy_ManObjIdMax( Ivy_Man_t * p ) { return Vec_PtrSize(p->vObjs)-1; } -static inline int Ivy_ManNodeNum( Ivy_Man_t * p ) { return p->nObjs[IVY_AND]+p->nObjs[IVY_EXOR];} -static inline int Ivy_ManHashObjNum( Ivy_Man_t * p ) { return p->nObjs[IVY_AND]+p->nObjs[IVY_EXOR]+p->nObjs[IVY_LATCH]; } -static inline int Ivy_ManGetCost( Ivy_Man_t * p ) { return p->nObjs[IVY_AND]+3*p->nObjs[IVY_EXOR]+8*p->nObjs[IVY_LATCH]; } - -static inline Ivy_Type_t Ivy_ObjType( Ivy_Obj_t * pObj ) { return pObj->Type; } -static inline Ivy_Init_t Ivy_ObjInit( Ivy_Obj_t * pObj ) { return pObj->Init; } -static inline int Ivy_ObjIsConst1( Ivy_Obj_t * pObj ) { return pObj->Id == 0; } -static inline int Ivy_ObjIsGhost( Ivy_Obj_t * pObj ) { return pObj->Id < 0; } -static inline int Ivy_ObjIsNone( Ivy_Obj_t * pObj ) { return pObj->Type == IVY_NONE; } -static inline int Ivy_ObjIsPi( Ivy_Obj_t * pObj ) { return pObj->Type == IVY_PI; } -static inline int Ivy_ObjIsPo( Ivy_Obj_t * pObj ) { return pObj->Type == IVY_PO; } -static inline int Ivy_ObjIsCi( Ivy_Obj_t * pObj ) { return pObj->Type == IVY_PI || pObj->Type == IVY_LATCH; } -static inline int Ivy_ObjIsCo( Ivy_Obj_t * pObj ) { return pObj->Type == IVY_PO || pObj->Type == IVY_LATCH; } -static inline int Ivy_ObjIsAssert( Ivy_Obj_t * pObj ) { return pObj->Type == IVY_ASSERT; } -static inline int Ivy_ObjIsLatch( Ivy_Obj_t * pObj ) { return pObj->Type == IVY_LATCH; } -static inline int Ivy_ObjIsAnd( Ivy_Obj_t * pObj ) { return pObj->Type == IVY_AND; } -static inline int Ivy_ObjIsExor( Ivy_Obj_t * pObj ) { return pObj->Type == IVY_EXOR; } -static inline int Ivy_ObjIsBuf( Ivy_Obj_t * pObj ) { return pObj->Type == IVY_BUF; } -static inline int Ivy_ObjIsNode( Ivy_Obj_t * pObj ) { return pObj->Type == IVY_AND || pObj->Type == IVY_EXOR; } -static inline int Ivy_ObjIsTerm( Ivy_Obj_t * pObj ) { return pObj->Type == IVY_PI || pObj->Type == IVY_PO || pObj->Type == IVY_ASSERT; } -static inline int Ivy_ObjIsHash( Ivy_Obj_t * pObj ) { return pObj->Type == IVY_AND || pObj->Type == IVY_EXOR || pObj->Type == IVY_LATCH; } -static inline int Ivy_ObjIsOneFanin( Ivy_Obj_t * pObj ) { return pObj->Type == IVY_PO || pObj->Type == IVY_ASSERT || pObj->Type == IVY_BUF || pObj->Type == IVY_LATCH; } - -static inline int Ivy_ObjIsMarkA( Ivy_Obj_t * pObj ) { return pObj->fMarkA; } -static inline void Ivy_ObjSetMarkA( Ivy_Obj_t * pObj ) { pObj->fMarkA = 1; } -static inline void Ivy_ObjClearMarkA( Ivy_Obj_t * pObj ) { pObj->fMarkA = 0; } - -static inline void Ivy_ObjSetTravId( Ivy_Obj_t * pObj, int TravId ) { pObj->TravId = TravId; } -static inline void Ivy_ObjSetTravIdCurrent( Ivy_Man_t * p, Ivy_Obj_t * pObj ) { pObj->TravId = p->nTravIds; } -static inline void Ivy_ObjSetTravIdPrevious( Ivy_Man_t * p, Ivy_Obj_t * pObj ) { pObj->TravId = p->nTravIds - 1; } -static inline int Ivy_ObjIsTravIdCurrent( Ivy_Man_t * p, Ivy_Obj_t * pObj ) { return (int )((int)pObj->TravId == p->nTravIds); } -static inline int Ivy_ObjIsTravIdPrevious( Ivy_Man_t * p, Ivy_Obj_t * pObj ) { return (int )((int)pObj->TravId == p->nTravIds - 1); } - -static inline int Ivy_ObjId( Ivy_Obj_t * pObj ) { return pObj->Id; } -static inline int Ivy_ObjTravId( Ivy_Obj_t * pObj ) { return pObj->TravId; } -static inline int Ivy_ObjPhase( Ivy_Obj_t * pObj ) { return pObj->fPhase; } -static inline int Ivy_ObjExorFanout( Ivy_Obj_t * pObj ) { return pObj->fExFan; } -static inline int Ivy_ObjRefs( Ivy_Obj_t * pObj ) { return pObj->nRefs; } -static inline void Ivy_ObjRefsInc( Ivy_Obj_t * pObj ) { pObj->nRefs++; } -static inline void Ivy_ObjRefsDec( Ivy_Obj_t * pObj ) { assert( pObj->nRefs > 0 ); pObj->nRefs--; } -static inline int Ivy_ObjFaninId0( Ivy_Obj_t * pObj ) { return pObj->pFanin0? Ivy_ObjId(Ivy_Regular(pObj->pFanin0)) : 0; } -static inline int Ivy_ObjFaninId1( Ivy_Obj_t * pObj ) { return pObj->pFanin1? Ivy_ObjId(Ivy_Regular(pObj->pFanin1)) : 0; } -static inline int Ivy_ObjFaninC0( Ivy_Obj_t * pObj ) { return Ivy_IsComplement(pObj->pFanin0); } -static inline int Ivy_ObjFaninC1( Ivy_Obj_t * pObj ) { return Ivy_IsComplement(pObj->pFanin1); } -static inline Ivy_Obj_t * Ivy_ObjFanin0( Ivy_Obj_t * pObj ) { return Ivy_Regular(pObj->pFanin0); } -static inline Ivy_Obj_t * Ivy_ObjFanin1( Ivy_Obj_t * pObj ) { return Ivy_Regular(pObj->pFanin1); } -static inline Ivy_Obj_t * Ivy_ObjChild0( Ivy_Obj_t * pObj ) { return pObj->pFanin0; } -static inline Ivy_Obj_t * Ivy_ObjChild1( Ivy_Obj_t * pObj ) { return pObj->pFanin1; } -static inline Ivy_Obj_t * Ivy_ObjChild0Equiv( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return Ivy_ObjFanin0(pObj)? Ivy_NotCond(Ivy_ObjFanin0(pObj)->pEquiv, Ivy_ObjFaninC0(pObj)) : NULL; } -static inline Ivy_Obj_t * Ivy_ObjChild1Equiv( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return Ivy_ObjFanin1(pObj)? Ivy_NotCond(Ivy_ObjFanin1(pObj)->pEquiv, Ivy_ObjFaninC1(pObj)) : NULL; } -static inline Ivy_Obj_t * Ivy_ObjEquiv( Ivy_Obj_t * pObj ) { return Ivy_Regular(pObj)->pEquiv? Ivy_NotCond(Ivy_Regular(pObj)->pEquiv, Ivy_IsComplement(pObj)) : NULL; } -static inline int Ivy_ObjLevel( Ivy_Obj_t * pObj ) { return pObj->Level; } -static inline int Ivy_ObjLevelNew( Ivy_Obj_t * pObj ) { return 1 + Ivy_ObjIsExor(pObj) + IVY_MAX(Ivy_ObjFanin0(pObj)->Level, Ivy_ObjFanin1(pObj)->Level); } -static inline int Ivy_ObjFaninPhase( Ivy_Obj_t * pObj ) { return Ivy_IsComplement(pObj)? !Ivy_Regular(pObj)->fPhase : pObj->fPhase; } - -static inline void Ivy_ObjClean( Ivy_Obj_t * pObj ) -{ - int IdSaved = pObj->Id; - memset( pObj, 0, sizeof(Ivy_Obj_t) ); - pObj->Id = IdSaved; -} -static inline void Ivy_ObjOverwrite( Ivy_Obj_t * pBase, Ivy_Obj_t * pData ) -{ - int IdSaved = pBase->Id; - memcpy( pBase, pData, sizeof(Ivy_Obj_t) ); - pBase->Id = IdSaved; -} -static inline int Ivy_ObjWhatFanin( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanin ) -{ - if ( Ivy_ObjFanin0(pObj) == pFanin ) return 0; - if ( Ivy_ObjFanin1(pObj) == pFanin ) return 1; - assert(0); return -1; -} -static inline int Ivy_ObjFanoutC( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout ) -{ - if ( Ivy_ObjFanin0(pFanout) == pObj ) return Ivy_ObjFaninC0(pObj); - if ( Ivy_ObjFanin1(pFanout) == pObj ) return Ivy_ObjFaninC1(pObj); - assert(0); return -1; -} - -// create the ghost of the new node -static inline Ivy_Obj_t * Ivy_ObjCreateGhost( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Type_t Type, Ivy_Init_t Init ) -{ - Ivy_Obj_t * pGhost, * pTemp; - assert( Type != IVY_AND || !Ivy_ObjIsConst1(Ivy_Regular(p0)) ); - assert( p1 == NULL || !Ivy_ObjIsConst1(Ivy_Regular(p1)) ); - assert( Type == IVY_PI || Ivy_Regular(p0) != Ivy_Regular(p1) ); - assert( Type != IVY_LATCH || !Ivy_IsComplement(p0) ); -// assert( p1 == NULL || (!Ivy_ObjIsLatch(Ivy_Regular(p0)) || !Ivy_ObjIsLatch(Ivy_Regular(p1))) ); - pGhost = Ivy_ManGhost(p); - pGhost->Type = Type; - pGhost->Init = Init; - pGhost->pFanin0 = p0; - pGhost->pFanin1 = p1; - if ( p1 && Ivy_ObjFaninId0(pGhost) > Ivy_ObjFaninId1(pGhost) ) - pTemp = pGhost->pFanin0, pGhost->pFanin0 = pGhost->pFanin1, pGhost->pFanin1 = pTemp; - return pGhost; -} - -// get the complemented initial state -static Ivy_Init_t Ivy_InitNotCond( Ivy_Init_t Init, int fCompl ) -{ - assert( Init != IVY_INIT_NONE ); - if ( fCompl == 0 ) - return Init; - if ( Init == IVY_INIT_0 ) - return IVY_INIT_1; - if ( Init == IVY_INIT_1 ) - return IVY_INIT_0; - return IVY_INIT_DC; -} - -// get the initial state after forward retiming over AND gate -static Ivy_Init_t Ivy_InitAnd( Ivy_Init_t InitA, Ivy_Init_t InitB ) -{ - assert( InitA != IVY_INIT_NONE && InitB != IVY_INIT_NONE ); - if ( InitA == IVY_INIT_0 || InitB == IVY_INIT_0 ) - return IVY_INIT_0; - if ( InitA == IVY_INIT_DC || InitB == IVY_INIT_DC ) - return IVY_INIT_DC; - return IVY_INIT_1; -} - -// get the initial state after forward retiming over EXOR gate -static Ivy_Init_t Ivy_InitExor( Ivy_Init_t InitA, Ivy_Init_t InitB ) -{ - assert( InitA != IVY_INIT_NONE && InitB != IVY_INIT_NONE ); - if ( InitA == IVY_INIT_DC || InitB == IVY_INIT_DC ) - return IVY_INIT_DC; - if ( InitA == IVY_INIT_0 && InitB == IVY_INIT_1 ) - return IVY_INIT_1; - if ( InitA == IVY_INIT_1 && InitB == IVY_INIT_0 ) - return IVY_INIT_1; - return IVY_INIT_0; -} - -// internal memory manager -static inline Ivy_Obj_t * Ivy_ManFetchMemory( Ivy_Man_t * p ) -{ - extern void Ivy_ManAddMemory( Ivy_Man_t * p ); - Ivy_Obj_t * pTemp; - if ( p->pListFree == NULL ) - Ivy_ManAddMemory( p ); - pTemp = p->pListFree; - p->pListFree = *((Ivy_Obj_t **)pTemp); - memset( pTemp, 0, sizeof(Ivy_Obj_t) ); - return pTemp; -} -static inline void Ivy_ManRecycleMemory( Ivy_Man_t * p, Ivy_Obj_t * pEntry ) -{ - pEntry->Type = IVY_NONE; // distinquishes dead node from live node - *((Ivy_Obj_t **)pEntry) = p->pListFree; - p->pListFree = pEntry; -} - - -//////////////////////////////////////////////////////////////////////// -/// ITERATORS /// -//////////////////////////////////////////////////////////////////////// - -// iterator over the primary inputs -#define Ivy_ManForEachPi( p, pObj, i ) \ - Vec_PtrForEachEntry( p->vPis, pObj, i ) -// iterator over the primary outputs -#define Ivy_ManForEachPo( p, pObj, i ) \ - Vec_PtrForEachEntry( p->vPos, pObj, i ) -// iterator over all objects, including those currently not used -#define Ivy_ManForEachObj( p, pObj, i ) \ - Vec_PtrForEachEntry( p->vObjs, pObj, i ) if ( (pObj) == NULL ) {} else -// iterator over the combinational inputs -#define Ivy_ManForEachCi( p, pObj, i ) \ - Ivy_ManForEachObj( p, pObj, i ) if ( !Ivy_ObjIsCi(pObj) ) {} else -// iterator over the combinational outputs -#define Ivy_ManForEachCo( p, pObj, i ) \ - Ivy_ManForEachObj( p, pObj, i ) if ( !Ivy_ObjIsCo(pObj) ) {} else -// iterator over logic nodes (AND and EXOR gates) -#define Ivy_ManForEachNode( p, pObj, i ) \ - Ivy_ManForEachObj( p, pObj, i ) if ( !Ivy_ObjIsNode(pObj) ) {} else -// iterator over logic latches -#define Ivy_ManForEachLatch( p, pObj, i ) \ - Ivy_ManForEachObj( p, pObj, i ) if ( !Ivy_ObjIsLatch(pObj) ) {} else -// iterator over the nodes whose IDs are stored in the array -#define Ivy_ManForEachNodeVec( p, vIds, pObj, i ) \ - for ( i = 0; i < Vec_IntSize(vIds) && ((pObj) = Ivy_ManObj(p, Vec_IntEntry(vIds,i))); i++ ) -// iterator over the fanouts of an object -#define Ivy_ObjForEachFanout( p, pObj, vArray, pFanout, i ) \ - for ( i = 0, Ivy_ObjCollectFanouts(p, pObj, vArray); \ - i < Vec_PtrSize(vArray) && ((pFanout) = Vec_PtrEntry(vArray,i)); i++ ) - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -/*=== ivyBalance.c ========================================================*/ -extern Ivy_Man_t * Ivy_ManBalance( Ivy_Man_t * p, int fUpdateLevel ); -extern Ivy_Obj_t * Ivy_NodeBalanceBuildSuper( Ivy_Man_t * p, Vec_Ptr_t * vSuper, Ivy_Type_t Type, int fUpdateLevel ); -/*=== ivyCanon.c ========================================================*/ -extern Ivy_Obj_t * Ivy_CanonAnd( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1 ); -extern Ivy_Obj_t * Ivy_CanonExor( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1 ); -extern Ivy_Obj_t * Ivy_CanonLatch( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Init_t Init ); -/*=== ivyCheck.c ========================================================*/ -extern int Ivy_ManCheck( Ivy_Man_t * p ); -extern int Ivy_ManCheckFanoutNums( Ivy_Man_t * p ); -extern int Ivy_ManCheckFanouts( Ivy_Man_t * p ); -extern int Ivy_ManCheckChoices( Ivy_Man_t * p ); -/*=== ivyCut.c ==========================================================*/ -extern void Ivy_ManSeqFindCut( Ivy_Man_t * p, Ivy_Obj_t * pNode, Vec_Int_t * vFront, Vec_Int_t * vInside, int nSize ); -extern Ivy_Store_t * Ivy_NodeFindCutsAll( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeaves ); -/*=== ivyDfs.c ==========================================================*/ -extern Vec_Int_t * Ivy_ManDfs( Ivy_Man_t * p ); -extern Vec_Int_t * Ivy_ManDfsSeq( Ivy_Man_t * p, Vec_Int_t ** pvLatches ); -extern void Ivy_ManCollectCone( Ivy_Obj_t * pObj, Vec_Ptr_t * vFront, Vec_Ptr_t * vCone ); -extern Vec_Vec_t * Ivy_ManLevelize( Ivy_Man_t * p ); -extern Vec_Int_t * Ivy_ManRequiredLevels( Ivy_Man_t * p ); -extern int Ivy_ManIsAcyclic( Ivy_Man_t * p ); -extern int Ivy_ManSetLevels( Ivy_Man_t * p, int fHaig ); -/*=== ivyDsd.c ==========================================================*/ -extern int Ivy_TruthDsd( unsigned uTruth, Vec_Int_t * vTree ); -extern void Ivy_TruthDsdPrint( FILE * pFile, Vec_Int_t * vTree ); -extern unsigned Ivy_TruthDsdCompute( Vec_Int_t * vTree ); -extern void Ivy_TruthDsdComputePrint( unsigned uTruth ); -extern Ivy_Obj_t * Ivy_ManDsdConstruct( Ivy_Man_t * p, Vec_Int_t * vFront, Vec_Int_t * vTree ); -/*=== ivyFanout.c ==========================================================*/ -extern void Ivy_ManStartFanout( Ivy_Man_t * p ); -extern void Ivy_ManStopFanout( Ivy_Man_t * p ); -extern void Ivy_ObjAddFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout ); -extern void Ivy_ObjDeleteFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout ); -extern void Ivy_ObjPatchFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFanoutOld, Ivy_Obj_t * pFanoutNew ); -extern void Ivy_ObjCollectFanouts( Ivy_Man_t * p, Ivy_Obj_t * pObj, Vec_Ptr_t * vArray ); -extern Ivy_Obj_t * Ivy_ObjReadFirstFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj ); -extern int Ivy_ObjFanoutNum( Ivy_Man_t * p, Ivy_Obj_t * pObj ); -/*=== ivyFastMap.c =============================================================*/ -extern void Ivy_FastMapPerform( Ivy_Man_t * pAig, int nLimit, int fRecovery, int fVerbose ); -extern void Ivy_FastMapStop( Ivy_Man_t * pAig ); -extern void Ivy_FastMapReadSupp( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, Vec_Int_t * vLeaves ); -extern void Ivy_FastMapReverseLevel( Ivy_Man_t * pAig ); -/*=== ivyFraig.c ==========================================================*/ -extern int Ivy_FraigProve( Ivy_Man_t ** ppManAig, void * pPars ); -extern Ivy_Man_t * Ivy_FraigPerform( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams ); -extern Ivy_Man_t * Ivy_FraigMiter( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams ); -extern void Ivy_FraigParamsDefault( Ivy_FraigParams_t * pParams ); -/*=== ivyHaig.c ==========================================================*/ -extern void Ivy_ManHaigStart( Ivy_Man_t * p, int fVerbose ); -extern void Ivy_ManHaigTrasfer( Ivy_Man_t * p, Ivy_Man_t * pNew ); -extern void Ivy_ManHaigStop( Ivy_Man_t * p ); -extern void Ivy_ManHaigPostprocess( Ivy_Man_t * p, int fVerbose ); -extern void Ivy_ManHaigCreateObj( Ivy_Man_t * p, Ivy_Obj_t * pObj ); -extern void Ivy_ManHaigCreateChoice( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew ); -extern void Ivy_ManHaigSimulate( Ivy_Man_t * p ); -/*=== ivyMan.c ==========================================================*/ -extern Ivy_Man_t * Ivy_ManStart(); -extern Ivy_Man_t * Ivy_ManStartFrom( Ivy_Man_t * p ); -extern Ivy_Man_t * Ivy_ManDup( Ivy_Man_t * p ); -extern Ivy_Man_t * Ivy_ManFrames( Ivy_Man_t * pMan, int nLatches, int nFrames, int fInit, Vec_Ptr_t ** pvMapping ); -extern void Ivy_ManStop( Ivy_Man_t * p ); -extern int Ivy_ManCleanup( Ivy_Man_t * p ); -extern int Ivy_ManPropagateBuffers( Ivy_Man_t * p, int fUpdateLevel ); -extern void Ivy_ManPrintStats( Ivy_Man_t * p ); -extern void Ivy_ManMakeSeq( Ivy_Man_t * p, int nLatches, int * pInits ); -/*=== ivyMem.c ==========================================================*/ -extern void Ivy_ManStartMemory( Ivy_Man_t * p ); -extern void Ivy_ManStopMemory( Ivy_Man_t * p ); -/*=== ivyMulti.c ==========================================================*/ -extern Ivy_Obj_t * Ivy_Multi( Ivy_Man_t * p, Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ); -extern Ivy_Obj_t * Ivy_Multi1( Ivy_Man_t * p, Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ); -extern Ivy_Obj_t * Ivy_Multi_rec( Ivy_Man_t * p, Ivy_Obj_t ** ppObjs, int nObjs, Ivy_Type_t Type ); -extern Ivy_Obj_t * Ivy_MultiBalance_rec( Ivy_Man_t * p, Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ); -extern int Ivy_MultiPlus( Ivy_Man_t * p, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, Ivy_Type_t Type, int nLimit, Vec_Ptr_t * vSol ); -/*=== ivyObj.c ==========================================================*/ -extern Ivy_Obj_t * Ivy_ObjCreatePi( Ivy_Man_t * p ); -extern Ivy_Obj_t * Ivy_ObjCreatePo( Ivy_Man_t * p, Ivy_Obj_t * pDriver ); -extern Ivy_Obj_t * Ivy_ObjCreate( Ivy_Man_t * p, Ivy_Obj_t * pGhost ); -extern void Ivy_ObjConnect( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFan0, Ivy_Obj_t * pFan1 ); -extern void Ivy_ObjDisconnect( Ivy_Man_t * p, Ivy_Obj_t * pObj ); -extern void Ivy_ObjPatchFanin0( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFaninNew ); -extern void Ivy_ObjDelete( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fFreeTop ); -extern void Ivy_ObjDelete_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fFreeTop ); -extern void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, int fDeleteOld, int fFreeTop, int fUpdateLevel ); -extern void Ivy_NodeFixBufferFanins( Ivy_Man_t * p, Ivy_Obj_t * pNode, int fUpdateLevel ); -/*=== ivyOper.c =========================================================*/ -extern Ivy_Obj_t * Ivy_Oper( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Type_t Type ); -extern Ivy_Obj_t * Ivy_And( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1 ); -extern Ivy_Obj_t * Ivy_Or( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1 ); -extern Ivy_Obj_t * Ivy_Exor( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1 ); -extern Ivy_Obj_t * Ivy_Mux( Ivy_Man_t * p, Ivy_Obj_t * pC, Ivy_Obj_t * p1, Ivy_Obj_t * p0 ); -extern Ivy_Obj_t * Ivy_Maj( Ivy_Man_t * p, Ivy_Obj_t * pA, Ivy_Obj_t * pB, Ivy_Obj_t * pC ); -extern Ivy_Obj_t * Ivy_Miter( Ivy_Man_t * p, Vec_Ptr_t * vPairs ); -extern Ivy_Obj_t * Ivy_Latch( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Init_t Init ); -/*=== ivyResyn.c =========================================================*/ -extern Ivy_Man_t * Ivy_ManResyn0( Ivy_Man_t * p, int fUpdateLevel, int fVerbose ); -extern Ivy_Man_t * Ivy_ManResyn( Ivy_Man_t * p, int fUpdateLevel, int fVerbose ); -extern Ivy_Man_t * Ivy_ManRwsat( Ivy_Man_t * pMan, int fVerbose ); -/*=== ivyRewrite.c =========================================================*/ -extern int Ivy_ManSeqRewrite( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost ); -extern int Ivy_ManRewriteAlg( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost ); -extern int Ivy_ManRewritePre( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost, int fVerbose ); -/*=== ivySeq.c =========================================================*/ -extern int Ivy_ManRewriteSeq( Ivy_Man_t * p, int fUseZeroCost, int fVerbose ); -/*=== ivyShow.c =========================================================*/ -extern void Ivy_ManShow( Ivy_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold ); -/*=== ivyTable.c ========================================================*/ -extern Ivy_Obj_t * Ivy_TableLookup( Ivy_Man_t * p, Ivy_Obj_t * pObj ); -extern void Ivy_TableInsert( Ivy_Man_t * p, Ivy_Obj_t * pObj ); -extern void Ivy_TableDelete( Ivy_Man_t * p, Ivy_Obj_t * pObj ); -extern void Ivy_TableUpdate( Ivy_Man_t * p, Ivy_Obj_t * pObj, int ObjIdNew ); -extern int Ivy_TableCountEntries( Ivy_Man_t * p ); -extern void Ivy_TableProfile( Ivy_Man_t * p ); -/*=== ivyUtil.c =========================================================*/ -extern void Ivy_ManIncrementTravId( Ivy_Man_t * p ); -extern void Ivy_ManCleanTravId( Ivy_Man_t * p ); -extern unsigned * Ivy_ManCutTruth( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes, Vec_Int_t * vTruth ); -extern void Ivy_ManCollectCut( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes ); -extern Vec_Int_t * Ivy_ManLatches( Ivy_Man_t * p ); -extern int Ivy_ManLevels( Ivy_Man_t * p ); -extern void Ivy_ManResetLevels( Ivy_Man_t * p ); -extern int Ivy_ObjMffcLabel( Ivy_Man_t * p, Ivy_Obj_t * pObj ); -extern void Ivy_ObjUpdateLevel_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj ); -extern void Ivy_ObjUpdateLevelR_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj, int ReqNew ); -extern int Ivy_ObjIsMuxType( Ivy_Obj_t * pObj ); -extern Ivy_Obj_t * Ivy_ObjRecognizeMux( Ivy_Obj_t * pObj, Ivy_Obj_t ** ppObjT, Ivy_Obj_t ** ppObjE ); -extern Ivy_Obj_t * Ivy_ObjReal( Ivy_Obj_t * pObj ); -extern void Ivy_ObjPrintVerbose( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fHaig ); -extern void Ivy_ManPrintVerbose( Ivy_Man_t * p, int fHaig ); -extern int Ivy_CutTruthPrint( Ivy_Man_t * p, Ivy_Cut_t * pCut, unsigned uTruth ); - -#ifdef __cplusplus -} -#endif - -#endif - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - |