diff options
Diffstat (limited to 'src/aig/ivy/ivy.h')
| -rw-r--r-- | src/aig/ivy/ivy.h | 557 |
1 files changed, 557 insertions, 0 deletions
diff --git a/src/aig/ivy/ivy.h b/src/aig/ivy/ivy.h new file mode 100644 index 00000000..c7435a63 --- /dev/null +++ b/src/aig/ivy/ivy.h @@ -0,0 +1,557 @@ +/**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 /// +//////////////////////////////////////////////////////////////////////// + |