diff options
Diffstat (limited to 'src/temp/ivy')
| -rw-r--r-- | src/temp/ivy/ivy.h | 105 | ||||
| -rw-r--r-- | src/temp/ivy/ivyBalance.c | 11 | ||||
| -rw-r--r-- | src/temp/ivy/ivyCut.c | 1 | ||||
| -rw-r--r-- | src/temp/ivy/ivyCutTrav.c | 473 | ||||
| -rw-r--r-- | src/temp/ivy/ivyDfs.c | 2 | ||||
| -rw-r--r-- | src/temp/ivy/ivyHaig.c | 348 | ||||
| -rw-r--r-- | src/temp/ivy/ivyMan.c | 58 | ||||
| -rw-r--r-- | src/temp/ivy/ivyMem.c | 2 | ||||
| -rw-r--r-- | src/temp/ivy/ivyMulti.c | 39 | ||||
| -rw-r--r-- | src/temp/ivy/ivyObj.c | 15 | ||||
| -rw-r--r-- | src/temp/ivy/ivyOper.c | 39 | ||||
| -rw-r--r-- | src/temp/ivy/ivySeq.c | 4 |
12 files changed, 1002 insertions, 95 deletions
diff --git a/src/temp/ivy/ivy.h b/src/temp/ivy/ivy.h index a36c795b..2409284e 100644 --- a/src/temp/ivy/ivy.h +++ b/src/temp/ivy/ivy.h @@ -110,14 +110,17 @@ struct Ivy_Man_t_ int nTravIds; // the traversal ID int nLevelMax; // the maximum level Vec_Int_t * vRequired; // required times -// Vec_Ptr_t * vFanouts; // representation of the fanouts int fFanout; // fanout is allocated void * pData; // the temporary data void * pCopy; // the temporary data + Ivy_Man_t * pHaig; // history AIG if present // 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; }; @@ -197,51 +200,54 @@ static inline int Ivy_ManNodeNum( Ivy_Man_t * p ) { return p->nO 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 ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type; } -static inline Ivy_Init_t Ivy_ObjInit( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Init; } -static inline int Ivy_ObjIsConst1( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Id == 0; } -static inline int Ivy_ObjIsGhost( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Id < 0; } -static inline int Ivy_ObjIsNone( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_NONE; } -static inline int Ivy_ObjIsPi( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_PI; } -static inline int Ivy_ObjIsPo( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_PO; } -static inline int Ivy_ObjIsCi( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_PI || pObj->Type == IVY_LATCH; } -static inline int Ivy_ObjIsCo( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_PO || pObj->Type == IVY_LATCH; } -static inline int Ivy_ObjIsAssert( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_ASSERT; } -static inline int Ivy_ObjIsLatch( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_LATCH; } -static inline int Ivy_ObjIsAnd( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_AND; } -static inline int Ivy_ObjIsExor( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_EXOR; } -static inline int Ivy_ObjIsBuf( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_BUF; } -static inline int Ivy_ObjIsNode( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_AND || pObj->Type == IVY_EXOR; } -static inline int Ivy_ObjIsTerm( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_PI || pObj->Type == IVY_PO || pObj->Type == IVY_ASSERT; } -static inline int Ivy_ObjIsHash( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_AND || pObj->Type == IVY_EXOR || pObj->Type == IVY_LATCH; } -static inline int Ivy_ObjIsOneFanin( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(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 ) { assert( !Ivy_IsComplement(pObj) ); return pObj->fMarkA; } -static inline void Ivy_ObjSetMarkA( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); pObj->fMarkA = 1; } -static inline void Ivy_ObjClearMarkA( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); pObj->fMarkA = 0; } +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 ) { assert( !Ivy_IsComplement(pObj) ); pObj->TravId = TravId; } -static inline void Ivy_ObjSetTravIdCurrent( Ivy_Man_t * p, Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); pObj->TravId = p->nTravIds; } -static inline void Ivy_ObjSetTravIdPrevious( Ivy_Man_t * p, Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); pObj->TravId = p->nTravIds - 1; } -static inline int Ivy_ObjIsTravIdCurrent( Ivy_Man_t * p, Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return (int )((int)pObj->TravId == p->nTravIds); } -static inline int Ivy_ObjIsTravIdPrevious( Ivy_Man_t * p, Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return (int )((int)pObj->TravId == p->nTravIds - 1); } - -static inline int Ivy_ObjId( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Id; } -static inline int Ivy_ObjPhase( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->fPhase; } -static inline int Ivy_ObjExorFanout( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->fExFan; } -static inline int Ivy_ObjRefs( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->nRefs; } -static inline void Ivy_ObjRefsInc( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); pObj->nRefs++; } -static inline void Ivy_ObjRefsDec( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); assert( pObj->nRefs > 0 ); pObj->nRefs--; } -static inline int Ivy_ObjFaninId0( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->pFanin0? Ivy_ObjId(Ivy_Regular(pObj->pFanin0)) : 0; } -static inline int Ivy_ObjFaninId1( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->pFanin1? Ivy_ObjId(Ivy_Regular(pObj->pFanin1)) : 0; } -static inline int Ivy_ObjFaninC0( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return Ivy_IsComplement(pObj->pFanin0); } -static inline int Ivy_ObjFaninC1( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return Ivy_IsComplement(pObj->pFanin1); } -static inline Ivy_Obj_t * Ivy_ObjFanin0( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return Ivy_Regular(pObj->pFanin0); } -static inline Ivy_Obj_t * Ivy_ObjFanin1( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return Ivy_Regular(pObj->pFanin1); } -static inline Ivy_Obj_t * Ivy_ObjChild0( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->pFanin0; } -static inline Ivy_Obj_t * Ivy_ObjChild1( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->pFanin1; } -static inline int Ivy_ObjLevel( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Level; } -static inline int Ivy_ObjLevelNew( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return 1 + Ivy_ObjIsExor(pObj) + IVY_MAX(Ivy_ObjFanin0(pObj)->Level, Ivy_ObjFanin1(pObj)->Level); } +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 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 void Ivy_ObjClean( Ivy_Obj_t * pObj ) { int IdSaved = pObj->Id; @@ -415,10 +421,19 @@ extern void Ivy_ObjPatchFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_ 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 ); +/*=== ivyHaig.c ==========================================================*/ +extern void Ivy_ManHaigStart( Ivy_Man_t * p ); +extern void Ivy_ManHaigTrasfer( Ivy_Man_t * p, Ivy_Man_t * pNew ); +extern void Ivy_ManHaigStop( Ivy_Man_t * p ); +extern void Ivy_ManHaigPrintStats( Ivy_Man_t * p ); +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 ); /*=== ivyIsop.c ==========================================================*/ extern int Ivy_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vCover, int fTryBoth ); /*=== ivyMan.c ==========================================================*/ extern Ivy_Man_t * Ivy_ManStart(); +extern Ivy_Man_t * Ivy_ManDup( Ivy_Man_t * p ); 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 ); diff --git a/src/temp/ivy/ivyBalance.c b/src/temp/ivy/ivyBalance.c index 0303485a..3e8bd6d2 100644 --- a/src/temp/ivy/ivyBalance.c +++ b/src/temp/ivy/ivyBalance.c @@ -59,6 +59,9 @@ Ivy_Man_t * Ivy_ManBalance( Ivy_Man_t * p, int fUpdateLevel ) Ivy_ManConst1(p)->TravId = Ivy_EdgeFromNode( Ivy_ManConst1(pNew) ); Ivy_ManForEachPi( p, pObj, i ) pObj->TravId = Ivy_EdgeFromNode( Ivy_ObjCreatePi(pNew) ); + // if HAIG is defined, trasfer the pointers to the PIs/latches +// if ( p->pHaig ) +// Ivy_ManHaigTrasfer( p, pNew ); // balance the AIG vStore = Vec_VecAlloc( 50 ); Ivy_ManForEachPo( p, pObj, i ) @@ -327,10 +330,18 @@ void Ivy_NodeBalancePermute( Ivy_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, i // get the two last nodes pObj1 = Vec_PtrEntry( vSuper, RightBound + 1 ); pObj2 = Vec_PtrEntry( vSuper, RightBound ); + if ( Ivy_Regular(pObj1) == p->pConst1 || Ivy_Regular(pObj2) == p->pConst1 ) + return; // find the first node that can be shared for ( i = RightBound; i >= LeftBound; i-- ) { pObj3 = Vec_PtrEntry( vSuper, i ); + if ( Ivy_Regular(pObj3) == p->pConst1 ) + { + Vec_PtrWriteEntry( vSuper, i, pObj2 ); + Vec_PtrWriteEntry( vSuper, RightBound, pObj3 ); + return; + } pGhost = Ivy_ObjCreateGhost( p, pObj1, pObj3, fExor? IVY_EXOR : IVY_AND, IVY_INIT_NONE ); if ( Ivy_TableLookup( p, pGhost ) ) { diff --git a/src/temp/ivy/ivyCut.c b/src/temp/ivy/ivyCut.c index 65ba4aac..d918c96c 100644 --- a/src/temp/ivy/ivyCut.c +++ b/src/temp/ivy/ivyCut.c @@ -889,7 +889,6 @@ Ivy_Store_t * Ivy_NodeFindCutsAll( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeaves { static Ivy_Store_t CutStore, * pCutStore = &CutStore; Ivy_Cut_t CutNew, * pCutNew = &CutNew, * pCut; - Ivy_Man_t * pMan = p; Ivy_Obj_t * pLeaf; int i, k, iLeaf0, iLeaf1; diff --git a/src/temp/ivy/ivyCutTrav.c b/src/temp/ivy/ivyCutTrav.c new file mode 100644 index 00000000..ea57c9f5 --- /dev/null +++ b/src/temp/ivy/ivyCutTrav.c @@ -0,0 +1,473 @@ +/**CFile**************************************************************** + + FileName [ivyCutTrav.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: ivyCutTrav.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ivy.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static unsigned * Ivy_NodeCutElementary( Vec_Int_t * vStore, int nWords, int NodeId ); +static void Ivy_NodeComputeVolume( Ivy_Obj_t * pObj, int nNodeLimit, Vec_Ptr_t * vNodes, Vec_Ptr_t * vFront ); +static void Ivy_NodeFindCutsMerge( Vec_Ptr_t * vCuts0, Vec_Ptr_t * vCuts1, Vec_Ptr_t * vCuts, int nLeaves, int nWords, Vec_Int_t * vStore ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Computes cuts for one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Store_t * Ivy_NodeFindCutsTravAll( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeaves, int nNodeLimit, + Vec_Ptr_t * vNodes, Vec_Ptr_t * vFront, Vec_Int_t * vStore, Vec_Vec_t * vBitCuts ) +{ + static Ivy_Store_t CutStore, * pCutStore = &CutStore; + Vec_Ptr_t * vCuts, * vCuts0, * vCuts1; + unsigned * pBitCut; + Ivy_Obj_t * pLeaf; + Ivy_Cut_t * pCut; + int i, k, nWords, nNodes; + + assert( nLeaves <= IVY_CUT_INPUT ); + + // find the given number of nodes in the TFI + Ivy_NodeComputeVolume( pObj, nNodeLimit - 1, vNodes, vFront ); + nNodes = Vec_PtrSize(vNodes); +// assert( nNodes <= nNodeLimit ); + + // make sure vBitCuts has enough room + Vec_VecExpand( vBitCuts, nNodes-1 ); + Vec_VecClear( vBitCuts ); + + // prepare the memory manager + Vec_IntClear( vStore ); + Vec_IntGrow( vStore, 64000 ); + + // set elementary cuts for the leaves + nWords = Extra_BitWordNum( nNodes ); + Vec_PtrForEachEntry( vFront, pLeaf, i ) + { + assert( Ivy_ObjTravId(pLeaf) < nNodes ); + // get the new bitcut + pBitCut = Ivy_NodeCutElementary( vStore, nWords, Ivy_ObjTravId(pLeaf) ); + // set it as the cut of this leaf + Vec_VecPush( vBitCuts, Ivy_ObjTravId(pLeaf), pBitCut ); + } + + // compute the cuts for each node + Vec_PtrForEachEntry( vNodes, pLeaf, i ) + { + // skip the leaves + vCuts = Vec_VecEntry( vBitCuts, Ivy_ObjTravId(pLeaf) ); + if ( Vec_PtrSize(vCuts) > 0 ) + continue; + // add elementary cut + pBitCut = Ivy_NodeCutElementary( vStore, nWords, Ivy_ObjTravId(pLeaf) ); + // set it as the cut of this leaf + Vec_VecPush( vBitCuts, Ivy_ObjTravId(pLeaf), pBitCut ); + // get the fanin cuts + vCuts0 = Vec_VecEntry( vBitCuts, Ivy_ObjTravId( Ivy_ObjFanin0(pLeaf) ) ); + vCuts1 = Vec_VecEntry( vBitCuts, Ivy_ObjTravId( Ivy_ObjFanin1(pLeaf) ) ); + assert( Vec_PtrSize(vCuts0) > 0 ); + assert( Vec_PtrSize(vCuts1) > 0 ); + // merge the cuts + Ivy_NodeFindCutsMerge( vCuts0, vCuts1, vCuts, nLeaves, nWords, vStore ); + } + + // start the structure + pCutStore->nCuts = 0; + pCutStore->nCutsMax = IVY_CUT_LIMIT; + // collect the cuts of the root node + vCuts = Vec_VecEntry( vBitCuts, Ivy_ObjTravId(pObj) ); + Vec_PtrForEachEntry( vCuts, pBitCut, i ) + { + pCut = pCutStore->pCuts + pCutStore->nCuts++; + pCut->nSize = 0; + pCut->nSizeMax = nLeaves; + pCut->uHash = 0; + for ( k = 0; k < nNodes; k++ ) + if ( Extra_TruthHasBit(pBitCut, k) ) + pCut->pArray[ pCut->nSize++ ] = Ivy_ObjId( Vec_PtrEntry(vNodes, k) ); + assert( pCut->nSize <= nLeaves ); + if ( pCutStore->nCuts == pCutStore->nCutsMax ) + break; + } + + // clean the travIds + Vec_PtrForEachEntry( vNodes, pLeaf, i ) + pLeaf->TravId = 0; + return pCutStore; +} + +/**Function************************************************************* + + Synopsis [Creates elementary bit-cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned * Ivy_NodeCutElementary( Vec_Int_t * vStore, int nWords, int NodeId ) +{ + unsigned * pBitCut; + pBitCut = Vec_IntFetch( vStore, nWords ); + memset( pBitCut, 0, 4 * nWords ); + Extra_TruthSetBit( pBitCut, NodeId ); + return pBitCut; +} + +/**Function************************************************************* + + Synopsis [Compares the node by level.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_CompareNodesByLevel( Ivy_Obj_t ** ppObj1, Ivy_Obj_t ** ppObj2 ) +{ + Ivy_Obj_t * pObj1 = *ppObj1; + Ivy_Obj_t * pObj2 = *ppObj2; + if ( pObj1->Level < pObj2->Level ) + return -1; + if ( pObj1->Level > pObj2->Level ) + return 1; + return 0; +} + +/**Function************************************************************* + + Synopsis [Mark all nodes up to the given depth.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_NodeComputeVolumeTrav1_rec( Ivy_Obj_t * pObj, int Depth ) +{ + if ( Ivy_ObjIsCi(pObj) || Depth == 0 ) + return; + Ivy_NodeComputeVolumeTrav1_rec( Ivy_ObjFanin0(pObj), Depth - 1 ); + Ivy_NodeComputeVolumeTrav1_rec( Ivy_ObjFanin1(pObj), Depth - 1 ); + pObj->fMarkA = 1; +} + +/**Function************************************************************* + + Synopsis [Collect the marked nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_NodeComputeVolumeTrav2_rec( Ivy_Obj_t * pObj, Vec_Ptr_t * vNodes ) +{ + if ( !pObj->fMarkA ) + return; + Ivy_NodeComputeVolumeTrav2_rec( Ivy_ObjFanin0(pObj), vNodes ); + Ivy_NodeComputeVolumeTrav2_rec( Ivy_ObjFanin1(pObj), vNodes ); + Vec_PtrPush( vNodes, pObj ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_NodeComputeVolume( Ivy_Obj_t * pObj, int nNodeLimit, Vec_Ptr_t * vNodes, Vec_Ptr_t * vFront ) +{ + Ivy_Obj_t * pTemp, * pFanin; + int i, nNodes; + // mark nodes up to the given depth + Ivy_NodeComputeVolumeTrav1_rec( pObj, 6 ); + // collect the marked nodes + Vec_PtrClear( vFront ); + Ivy_NodeComputeVolumeTrav2_rec( pObj, vFront ); + // find the fanins that are not marked + Vec_PtrClear( vNodes ); + Vec_PtrForEachEntry( vFront, pTemp, i ) + { + pFanin = Ivy_ObjFanin0(pTemp); + if ( !pFanin->fMarkA ) + { + pFanin->fMarkA = 1; + Vec_PtrPush( vNodes, pFanin ); + } + pFanin = Ivy_ObjFanin1(pTemp); + if ( !pFanin->fMarkA ) + { + pFanin->fMarkA = 1; + Vec_PtrPush( vNodes, pFanin ); + } + } + // remember the number of nodes in the frontier + nNodes = Vec_PtrSize( vNodes ); + // add the remaining nodes + Vec_PtrForEachEntry( vFront, pTemp, i ) + Vec_PtrPush( vNodes, pTemp ); + // unmark the nodes + Vec_PtrForEachEntry( vNodes, pTemp, i ) + { + pTemp->fMarkA = 0; + pTemp->TravId = i; + } + // collect the frontier nodes + Vec_PtrClear( vFront ); + Vec_PtrForEachEntryStop( vNodes, pTemp, i, nNodes ) + Vec_PtrPush( vFront, pTemp ); +// printf( "%d ", Vec_PtrSize(vNodes) ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_NodeComputeVolume2( Ivy_Obj_t * pObj, int nNodeLimit, Vec_Ptr_t * vNodes, Vec_Ptr_t * vFront ) +{ + Ivy_Obj_t * pLeaf, * pPivot, * pFanin; + int LevelMax, i; + assert( Ivy_ObjIsNode(pObj) ); + // clear arrays + Vec_PtrClear( vNodes ); + Vec_PtrClear( vFront ); + // add the root + pObj->fMarkA = 1; + Vec_PtrPush( vNodes, pObj ); + Vec_PtrPush( vFront, pObj ); + // expand node with maximum level + LevelMax = pObj->Level; + do { + // get the node to expand + pPivot = NULL; + Vec_PtrForEachEntryReverse( vFront, pLeaf, i ) + { + if ( (int)pLeaf->Level == LevelMax ) + { + pPivot = pLeaf; + break; + } + } + // decrease level if we did not find the node + if ( pPivot == NULL ) + { + if ( --LevelMax == 0 ) + break; + continue; + } + // the node to expand is found + // remove it from frontier + Vec_PtrRemove( vFront, pPivot ); + // add fanins + pFanin = Ivy_ObjFanin0(pPivot); + if ( !pFanin->fMarkA ) + { + pFanin->fMarkA = 1; + Vec_PtrPush( vNodes, pFanin ); + Vec_PtrPush( vFront, pFanin ); + } + pFanin = Ivy_ObjFanin1(pPivot); + if ( pFanin && !pFanin->fMarkA ) + { + pFanin->fMarkA = 1; + Vec_PtrPush( vNodes, pFanin ); + Vec_PtrPush( vFront, pFanin ); + } + // quit if we collected enough nodes + } while ( Vec_PtrSize(vNodes) < nNodeLimit ); + + // sort nodes by level + Vec_PtrSort( vNodes, Ivy_CompareNodesByLevel ); + // make sure the nodes are ordered in the increasing number of levels + pFanin = Vec_PtrEntry( vNodes, 0 ); + pPivot = Vec_PtrEntryLast( vNodes ); + assert( pFanin->Level <= pPivot->Level ); + + // clean the marks and remember node numbers in the TravId + Vec_PtrForEachEntry( vNodes, pFanin, i ) + { + pFanin->fMarkA = 0; + pFanin->TravId = i; + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Extra_TruthOrWords( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nWords ) +{ + int w; + for ( w = nWords-1; w >= 0; w-- ) + pOut[w] = pIn0[w] | pIn1[w]; +} +static inline int Extra_TruthIsImplyWords( unsigned * pIn1, unsigned * pIn2, int nWords ) +{ + int w; + for ( w = nWords-1; w >= 0; w-- ) + if ( pIn1[w] & ~pIn2[w] ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Merges two sets of bit-cuts at a node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_NodeFindCutsMerge( Vec_Ptr_t * vCuts0, Vec_Ptr_t * vCuts1, Vec_Ptr_t * vCuts, + int nLeaves, int nWords, Vec_Int_t * vStore ) +{ + unsigned * pBitCut, * pBitCut0, * pBitCut1, * pBitCutTest; + int i, k, c, w, Counter; + // iterate through the cut pairs + Vec_PtrForEachEntry( vCuts0, pBitCut0, i ) + Vec_PtrForEachEntry( vCuts1, pBitCut1, k ) + { + // skip infeasible cuts + Counter = 0; + for ( w = 0; w < nWords; w++ ) + { + Counter += Extra_WordCountOnes( pBitCut0[w] | pBitCut1[w] ); + if ( Counter > nLeaves ) + break; + } + if ( Counter > nLeaves ) + continue; + // the new cut is feasible - create it + pBitCutTest = Vec_IntFetch( vStore, nWords ); + Extra_TruthOrWords( pBitCutTest, pBitCut0, pBitCut1, nWords ); + // filter contained cuts; try to find containing cut + w = 0; + Vec_PtrForEachEntry( vCuts, pBitCut, c ) + { + if ( Extra_TruthIsImplyWords( pBitCut, pBitCutTest, nWords ) ) + break; + if ( Extra_TruthIsImplyWords( pBitCutTest, pBitCut, nWords ) ) + continue; + Vec_PtrWriteEntry( vCuts, w++, pBitCut ); + } + if ( c != Vec_PtrSize(vCuts) ) + continue; + Vec_PtrShrink( vCuts, w ); + // add the cut + Vec_PtrPush( vCuts, pBitCutTest ); + } +} + +/**Function************************************************************* + + Synopsis [Compute the set of all cuts.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManTestCutsTravAll( Ivy_Man_t * p ) +{ + Ivy_Store_t * pStore; + Ivy_Obj_t * pObj; + Vec_Ptr_t * vNodes, * vFront; + Vec_Int_t * vStore; + Vec_Vec_t * vBitCuts; + int i, nCutsCut, nCutsTotal, nNodeTotal, nNodeOver; + int clk = clock(); + + vNodes = Vec_PtrAlloc( 100 ); + vFront = Vec_PtrAlloc( 100 ); + vStore = Vec_IntAlloc( 100 ); + vBitCuts = Vec_VecAlloc( 100 ); + + nNodeTotal = nNodeOver = 0; + nCutsTotal = -Ivy_ManNodeNum(p); + Ivy_ManForEachObj( p, pObj, i ) + { + if ( !Ivy_ObjIsNode(pObj) ) + continue; + pStore = Ivy_NodeFindCutsTravAll( p, pObj, 4, 60, vNodes, vFront, vStore, vBitCuts ); + nCutsCut = pStore->nCuts; + nCutsTotal += nCutsCut; + nNodeOver += (nCutsCut == IVY_CUT_LIMIT); + nNodeTotal++; + } + printf( "Total cuts = %6d. Trivial = %6d. Nodes = %6d. Satur = %6d. ", + nCutsTotal, Ivy_ManPiNum(p) + Ivy_ManNodeNum(p), nNodeTotal, nNodeOver ); + PRT( "Time", clock() - clk ); + + Vec_PtrFree( vNodes ); + Vec_PtrFree( vFront ); + Vec_IntFree( vStore ); + Vec_VecFree( vBitCuts ); + +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ivy/ivyDfs.c b/src/temp/ivy/ivyDfs.c index 7246ec25..314bed8d 100644 --- a/src/temp/ivy/ivyDfs.c +++ b/src/temp/ivy/ivyDfs.c @@ -119,7 +119,7 @@ Vec_Int_t * Ivy_ManDfsSeq( Ivy_Man_t * p, Vec_Int_t ** pvLatches ) Ivy_ManForEachNodeVec( p, vNodes, pObj, i ) Ivy_ObjClearMarkA(pObj); // make sure network does not have dangling nodes - assert( Vec_IntSize(vNodes) == Ivy_ManNodeNum(p) + Ivy_ManBufNum(p) ); +// assert( Vec_IntSize(vNodes) == Ivy_ManNodeNum(p) + Ivy_ManBufNum(p) ); *pvLatches = vLatches; return vNodes; } diff --git a/src/temp/ivy/ivyHaig.c b/src/temp/ivy/ivyHaig.c new file mode 100644 index 00000000..7ce71a60 --- /dev/null +++ b/src/temp/ivy/ivyHaig.c @@ -0,0 +1,348 @@ +/**CFile**************************************************************** + + FileName [ivyHaig.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [HAIG management procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: ivyHaig.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ivy.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/* + HAIGing rules in working AIG: + - The node points to the representative of its class + - The pointer can be complemented if they have different polarity + + Choice node rules in HAIG: + - Equivalent nodes are linked into a ring + - Exactly one node in the ring has fanouts (this node is called representative) + - Pointer going from a node to the next node in the ring is complemented + if the first node is complemented, compared to the representative node + - The representative node always has non-complemented pointer to the next node + - New nodes are inserted into the ring before the representative node +*/ + +// returns the representative node of the given HAIG node +static inline Ivy_Obj_t * Ivy_HaigObjRepr( Ivy_Obj_t * pObj ) +{ + Ivy_Obj_t * pTemp; + assert( !Ivy_IsComplement(pObj) ); + // if the node has no equivalent or has fanout, it is representative + if ( pObj->pEquiv == NULL || Ivy_ObjRefs(pObj) > 0 ) + return pObj; + // the node belongs to a class and is not a representative + // complemented edge (pObj->pEquiv) tells if it is complemented w.r.t. the repr + for ( pTemp = Ivy_Regular(pObj->pEquiv); pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) ) + if ( Ivy_ObjRefs(pTemp) > 0 ) + break; + // return the representative node + assert( pTemp != pObj ); + return Ivy_NotCond( pTemp, Ivy_IsComplement(pObj->pEquiv) ); +} + +// counts the number of nodes in the equivalence class +static inline int Ivy_HaigObjCountClass( Ivy_Obj_t * pObj ) +{ + Ivy_Obj_t * pTemp; + int Counter; + assert( !Ivy_IsComplement(pObj) ); + assert( Ivy_ObjRefs(pObj) > 0 ); + if ( pObj->pEquiv == NULL ) + return 1; + Counter = 1; + assert( !Ivy_IsComplement(pObj->pEquiv) ); + for ( pTemp = pObj->pEquiv; pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) ) + Counter++; + return Counter; +} + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Starts HAIG for the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManHaigStart( Ivy_Man_t * p ) +{ + assert( p->pHaig == NULL ); + p->pHaig = Ivy_ManDup( p ); +} + +/**Function************************************************************* + + Synopsis [Transfers the HAIG to the newly created manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManHaigTrasfer( Ivy_Man_t * p, Ivy_Man_t * pNew ) +{ + Ivy_Obj_t * pObj; + int i; + assert( p->pHaig != NULL ); + Ivy_ManConst1(pNew)->pEquiv = Ivy_ManConst1(p)->pEquiv; + Ivy_ManForEachPi( pNew, pObj, i ) + pObj->pEquiv = Ivy_ManPi( p, i )->pEquiv; + pNew->pHaig = p->pHaig; +} + +/**Function************************************************************* + + Synopsis [Stops HAIG for the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManHaigStop( Ivy_Man_t * p ) +{ + Ivy_Obj_t * pObj; + int i; + assert( p->pHaig != NULL ); + Ivy_ManStop( p->pHaig ); + p->pHaig = NULL; + // remove dangling pointers to the HAIG objects + Ivy_ManForEachObj( p, pObj, i ) + pObj->pEquiv = NULL; +} + +/**Function************************************************************* + + Synopsis [Creates a new node in HAIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManHaigCreateObj( Ivy_Man_t * p, Ivy_Obj_t * pObj ) +{ + assert( p->pHaig != NULL ); + assert( !Ivy_IsComplement(pObj) ); + if ( Ivy_ObjType(pObj) == IVY_BUF ) + pObj->pEquiv = Ivy_ObjChild0Equiv(pObj); + else if ( Ivy_ObjType(pObj) == IVY_LATCH ) + pObj->pEquiv = Ivy_Latch( p->pHaig, Ivy_ObjChild0Equiv(pObj), pObj->Init ); + else if ( Ivy_ObjType(pObj) == IVY_AND ) + pObj->pEquiv = Ivy_And( p->pHaig, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) ); + else assert( 0 ); + // make sure the node points to the representative + pObj->pEquiv = Ivy_NotCond( Ivy_HaigObjRepr(Ivy_Regular(pObj->pEquiv)), Ivy_IsComplement(pObj->pEquiv) ); +} + +/**Function************************************************************* + + Synopsis [Sets the pair of equivalent nodes in HAIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManHaigCreateChoice( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew ) +{ + Ivy_Obj_t * pObjOldHaig, * pObjNewHaig; + Ivy_Obj_t * pObjOldHaigR, * pObjNewHaigR; + int fCompl; + assert( p->pHaig != NULL ); + // get pointers to the classes + pObjOldHaig = pObjOld->pEquiv; + pObjNewHaig = Ivy_NotCond( Ivy_Regular(pObjNew)->pEquiv, Ivy_IsComplement(pObjNew) ); + // get regular pointers + pObjOldHaigR = Ivy_Regular(pObjOldHaig); + pObjNewHaigR = Ivy_Regular(pObjNewHaig); + // check if there is phase difference between them + fCompl = (Ivy_IsComplement(pObjOldHaig) != Ivy_IsComplement(pObjNewHaig)); + // if the class is the same, nothing to do + if ( pObjOldHaigR == pObjNewHaigR ) + return; + // combine classes + // assume the second node does not belong to a class + assert( pObjNewHaigR->pEquiv == NULL ); + // add this node to the class of pObjOldHaig + if ( pObjOldHaigR->pEquiv == NULL ) + pObjNewHaigR->pEquiv = Ivy_NotCond( pObjOldHaigR, fCompl ); + else + pObjNewHaigR->pEquiv = Ivy_NotCond( pObjOldHaigR->pEquiv, fCompl ); + pObjOldHaigR->pEquiv = pObjNewHaigR; + // update the class of the new node + Ivy_Regular(pObjNew)->pEquiv = Ivy_NotCond( pObjOldHaigR, fCompl ^ Ivy_IsComplement(pObjNew) ); +} + +/**Function************************************************************* + + Synopsis [Count the number of choices and choice nodes in HAIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_ManHaigCountChoices( Ivy_Man_t * p, int * pnChoices ) +{ + Ivy_Obj_t * pObj; + int nChoices, nChoiceNodes, Counter, i; + assert( p->pHaig != NULL ); + nChoices = nChoiceNodes = 0; + Ivy_ManForEachObj( p->pHaig, pObj, i ) + { + if ( Ivy_ObjIsTerm(pObj) || i == 0 ) + continue; + if ( Ivy_ObjRefs(pObj) == 0 ) + { + assert( pObj->pEquiv == Ivy_HaigObjRepr(pObj) ); + continue; + } + Counter = Ivy_HaigObjCountClass( pObj ); + nChoiceNodes += (int)(Counter > 1); + nChoices += Counter - 1; + } + *pnChoices = nChoices; + return nChoiceNodes; +} + +/**Function************************************************************* + + Synopsis [Prints statistics of the HAIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManHaigPrintStats( Ivy_Man_t * p ) +{ + int nChoices, nChoiceNodes; + assert( p->pHaig != NULL ); + printf( "Original : " ); + Ivy_ManPrintStats( p ); + printf( "HAIG : " ); + Ivy_ManPrintStats( p->pHaig ); + + // print choice node stats + nChoiceNodes = Ivy_ManHaigCountChoices( p, &nChoices ); + printf( "Total choice nodes = %d. Total choices = %d.\n", nChoiceNodes, nChoices ); + Ivy_ManHaigSimulate( p ); +} + + +/**Function************************************************************* + + Synopsis [Applies the simulation rules.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Ivy_Init_t Ivy_ManHaigSimulateAnd( Ivy_Init_t In0, Ivy_Init_t In1 ) +{ + assert( In0 != IVY_INIT_NONE && In1 != IVY_INIT_NONE ); + if ( In0 == IVY_INIT_DC || In1 == IVY_INIT_DC ) + return IVY_INIT_DC; + if ( In0 == IVY_INIT_1 && In1 == IVY_INIT_1 ) + return IVY_INIT_1; + return IVY_INIT_0; +} + +/**Function************************************************************* + + Synopsis [Simulate HAIG using modified 3-valued simulation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManHaigSimulate( Ivy_Man_t * p ) +{ + Vec_Int_t * vNodes, * vLatches; + Ivy_Obj_t * pObj; + Ivy_Init_t In0, In1; + int i, k, Counter; + assert( p->pHaig != NULL ); + p = p->pHaig; + // collect latches and nodes in the DFS order + vNodes = Ivy_ManDfsSeq( p, &vLatches ); + // set the PI values + Ivy_ManConst1(p)->Init = IVY_INIT_0; + Ivy_ManForEachPi( p, pObj, i ) + pObj->Init = IVY_INIT_0; + // set the latch values + Ivy_ManForEachNodeVec( p, vLatches, pObj, i ) + pObj->Init = IVY_INIT_DC; + // perform several rounds of simulation + for ( k = 0; k < 5; k++ ) + { + // count the number of non-determinate values + Counter = 0; + Ivy_ManForEachNodeVec( p, vLatches, pObj, i ) + Counter += ( pObj->Init == IVY_INIT_DC ); + printf( "Iter %d : Non-determinate = %d\n", k, Counter ); + // simulate the internal nodes + Ivy_ManForEachNodeVec( p, vNodes, pObj, i ) + { + In0 = Ivy_InitNotCond( Ivy_ObjFanin0(pObj)->Init, Ivy_ObjFaninC0(pObj) ); + In1 = Ivy_InitNotCond( Ivy_ObjFanin1(pObj)->Init, Ivy_ObjFaninC1(pObj) ); + pObj->Init = Ivy_ManHaigSimulateAnd( In0, In1 ); + } + // simulate the latches + Ivy_ManForEachNodeVec( p, vLatches, pObj, i ) + pObj->Level = Ivy_ObjFanin0(pObj)->Init; + Ivy_ManForEachNodeVec( p, vLatches, pObj, i ) + pObj->Init = pObj->Level, pObj->Level = 0; + } + // free arrays + Vec_IntFree( vNodes ); + Vec_IntFree( vLatches ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ivy/ivyMan.c b/src/temp/ivy/ivyMan.c index 9839567f..e3b8a5b8 100644 --- a/src/temp/ivy/ivyMan.c +++ b/src/temp/ivy/ivyMan.c @@ -70,6 +70,62 @@ Ivy_Man_t * Ivy_ManStart() /**Function************************************************************* + Synopsis [Duplicates the AIG manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Man_t * Ivy_ManDup( Ivy_Man_t * p ) +{ + Vec_Int_t * vNodes, * vLatches; + Ivy_Man_t * pNew; + Ivy_Obj_t * pObj; + int i; + // collect latches and nodes in the DFS order + vNodes = Ivy_ManDfsSeq( p, &vLatches ); + // create the new manager + pNew = Ivy_ManStart(); + // create the PIs + Ivy_ManConst1(p)->pEquiv = Ivy_ManConst1(pNew); + Ivy_ManForEachPi( p, pObj, i ) + pObj->pEquiv = Ivy_ObjCreatePi(pNew); + // create the fake PIs for latches + Ivy_ManForEachNodeVec( p, vLatches, pObj, i ) + pObj->pEquiv = Ivy_ObjCreatePi(pNew); + // duplicate internal nodes + Ivy_ManForEachNodeVec( p, vNodes, pObj, i ) + pObj->pEquiv = Ivy_And( pNew, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) ); + // add the POs + Ivy_ManForEachPo( p, pObj, i ) + Ivy_ObjCreatePo( pNew, Ivy_ObjChild0Equiv(pObj) ); + // transform additional PI nodes into latches and connect them + Ivy_ManForEachNodeVec( p, vLatches, pObj, i ) + { + assert( !Ivy_ObjFaninC0(pObj) ); + pObj->pEquiv->Type = IVY_LATCH; + pObj->pEquiv->Init = pObj->Init; + Ivy_ObjConnect( pNew, pObj->pEquiv, Ivy_ObjChild0Equiv(pObj), NULL ); + } + // shrink the arrays + Vec_PtrShrink( pNew->vPis, Ivy_ManPiNum(p) ); + // update the counters of different objects + pNew->nObjs[IVY_PI] -= Ivy_ManLatchNum(p); + pNew->nObjs[IVY_LATCH] += Ivy_ManLatchNum(p); + // free arrays + Vec_IntFree( vNodes ); + Vec_IntFree( vLatches ); + // check the resulting network + if ( !Ivy_ManCheck(pNew) ) + printf( "Ivy_ManMakeSeq(): The check has failed.\n" ); + return pNew; +} + +/**Function************************************************************* + Synopsis [Stops the AIG manager.] Description [] @@ -81,6 +137,8 @@ Ivy_Man_t * Ivy_ManStart() ***********************************************************************/ void Ivy_ManStop( Ivy_Man_t * p ) { + if ( p->time1 ) { PRT( "Update lev ", p->time1 ); } + if ( p->time2 ) { PRT( "Update levR ", p->time2 ); } // Ivy_TableProfile( p ); // if ( p->vFanouts ) Ivy_ManStopFanout( p ); if ( p->vChunks ) Ivy_ManStopMemory( p ); diff --git a/src/temp/ivy/ivyMem.c b/src/temp/ivy/ivyMem.c index 6ca33541..09c73c49 100644 --- a/src/temp/ivy/ivyMem.c +++ b/src/temp/ivy/ivyMem.c @@ -89,7 +89,7 @@ void Ivy_ManAddMemory( Ivy_Man_t * p ) int i, nBytes; assert( sizeof(Ivy_Obj_t) <= 64 ); assert( p->pListFree == NULL ); - assert( (Ivy_ManObjNum(p) & IVY_PAGE_MASK) == 0 ); +// assert( (Ivy_ManObjNum(p) & IVY_PAGE_MASK) == 0 ); // allocate new memory page nBytes = sizeof(Ivy_Obj_t) * (1<<IVY_PAGE_SIZE) + 64; pMemory = ALLOC( char, nBytes ); diff --git a/src/temp/ivy/ivyMulti.c b/src/temp/ivy/ivyMulti.c index f098332d..a7970156 100644 --- a/src/temp/ivy/ivyMulti.c +++ b/src/temp/ivy/ivyMulti.c @@ -294,45 +294,6 @@ int Ivy_MultiCover( Ivy_Man_t * p, Ivy_Eva_t * pEvals, int nLeaves, int nEvals, } } -/**Function************************************************************* - - Synopsis [Constructs the well-balanced tree of gates.] - - Description [Disregards levels and possible logic sharing.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Ivy_Obj_t * Ivy_Multi_rec( Ivy_Man_t * p, Ivy_Obj_t ** ppObjs, int nObjs, Ivy_Type_t Type ) -{ - Ivy_Obj_t * pObj1, * pObj2; - if ( nObjs == 1 ) - return ppObjs[0]; - pObj1 = Ivy_Multi_rec( p, ppObjs, nObjs/2, Type ); - pObj2 = Ivy_Multi_rec( p, ppObjs + nObjs/2, nObjs - nObjs/2, Type ); - return Ivy_Oper( p, pObj1, pObj2, Type ); -} - -/**Function************************************************************* - - Synopsis [Old code.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Ivy_Obj_t * Ivy_Multi( Ivy_Man_t * p, Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ) -{ - assert( Type == IVY_AND || Type == IVY_EXOR ); - assert( nArgs > 0 ); - return Ivy_Multi_rec( p, pArgs, nArgs, Type ); -} - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/temp/ivy/ivyObj.c b/src/temp/ivy/ivyObj.c index 3122c8c8..e8924b5b 100644 --- a/src/temp/ivy/ivyObj.c +++ b/src/temp/ivy/ivyObj.c @@ -79,7 +79,6 @@ Ivy_Obj_t * Ivy_ObjCreate( Ivy_Man_t * p, Ivy_Obj_t * pGhost ) assert( Ivy_TableLookup(p, pGhost) == NULL ); // get memory for the new object pObj = Ivy_ManFetchMemory( p ); -//printf( "Reusing %p.\n", pObj ); assert( Ivy_ObjIsNone(pObj) ); pObj->Id = Vec_PtrSize(p->vObjs); Vec_PtrPush( p->vObjs, pObj ); @@ -115,6 +114,9 @@ Ivy_Obj_t * Ivy_ObjCreate( Ivy_Man_t * p, Ivy_Obj_t * pGhost ) // update node counters of the manager p->nObjs[Ivy_ObjType(pObj)]++; p->nCreated++; + // if HAIG is defined, create a corresponding node + if ( p->pHaig ) + Ivy_ManHaigCreateObj( p, pObj ); return pObj; } @@ -258,7 +260,6 @@ void Ivy_ObjDelete( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fFreeTop ) // free the node Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL ); Ivy_ManRecycleMemory( p, pObj ); -//printf( "Recycling after delete %p.\n", pObj ); } else { @@ -312,7 +313,7 @@ void Ivy_ObjDelete_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fFreeTop ) ***********************************************************************/ void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, int fDeleteOld, int fFreeTop, int fUpdateLevel ) { - int nRefsOld; + int nRefsOld;//, clk; // the object to be replaced cannot be complemented assert( !Ivy_IsComplement(pObjOld) ); // the object to be replaced cannot be a terminal @@ -321,12 +322,16 @@ void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, in assert( !Ivy_ObjIsBuf(Ivy_Regular(pObjNew)) ); // the object cannot be the same assert( pObjOld != Ivy_Regular(pObjNew) ); + // if HAIG is defined, create the choice node + if ( p->pHaig ) + Ivy_ManHaigCreateChoice( p, pObjOld, pObjNew ); // if the new object is complemented or already used, add the buffer if ( Ivy_IsComplement(pObjNew) || Ivy_ObjIsLatch(pObjNew) || Ivy_ObjRefs(pObjNew) > 0 || Ivy_ObjIsPi(pObjNew) || Ivy_ObjIsConst1(pObjNew) ) pObjNew = Ivy_ObjCreate( p, Ivy_ObjCreateGhost(p, pObjNew, NULL, IVY_BUF, IVY_INIT_NONE) ); assert( !Ivy_IsComplement(pObjNew) ); if ( fUpdateLevel ) { +//clk = clock(); // if the new node's arrival time is different, recursively update arrival time of the fanouts if ( p->fFanout && !Ivy_ObjIsBuf(pObjNew) && pObjOld->Level != pObjNew->Level ) { @@ -334,7 +339,9 @@ void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, in pObjOld->Level = pObjNew->Level; Ivy_ObjUpdateLevel_rec( p, pObjOld ); } +//p->time1 += clock() - clk; // if the new node's required time has changed, recursively update required time of the fanins +//clk = clock(); if ( p->vRequired ) { int ReqNew = Vec_IntEntry(p->vRequired, pObjOld->Id); @@ -344,6 +351,7 @@ void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, in Ivy_ObjUpdateLevelR_rec( p, pObjNew, ReqNew ); } } +//p->time2 += clock() - clk; } // delete the old object if ( fDeleteOld ) @@ -375,7 +383,6 @@ void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, in // recycle the object that was taken over by pObjOld Vec_PtrWriteEntry( p->vObjs, pObjNew->Id, NULL ); Ivy_ManRecycleMemory( p, pObjNew ); -//printf( "Recycling after patch %p.\n", pObjNew ); // if the new node is the buffer propagate it if ( p->fFanout && Ivy_ObjIsBuf(pObjOld) ) Vec_PtrPush( p->vBufs, pObjOld ); diff --git a/src/temp/ivy/ivyOper.c b/src/temp/ivy/ivyOper.c index af216e45..8115ce4f 100644 --- a/src/temp/ivy/ivyOper.c +++ b/src/temp/ivy/ivyOper.c @@ -210,6 +210,45 @@ Ivy_Obj_t * Ivy_Maj( Ivy_Man_t * p, Ivy_Obj_t * pA, Ivy_Obj_t * pB, Ivy_Obj_t * /**Function************************************************************* + Synopsis [Constructs the well-balanced tree of gates.] + + Description [Disregards levels and possible logic sharing.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_Multi_rec( Ivy_Man_t * p, Ivy_Obj_t ** ppObjs, int nObjs, Ivy_Type_t Type ) +{ + Ivy_Obj_t * pObj1, * pObj2; + if ( nObjs == 1 ) + return ppObjs[0]; + pObj1 = Ivy_Multi_rec( p, ppObjs, nObjs/2, Type ); + pObj2 = Ivy_Multi_rec( p, ppObjs + nObjs/2, nObjs - nObjs/2, Type ); + return Ivy_Oper( p, pObj1, pObj2, Type ); +} + +/**Function************************************************************* + + Synopsis [Old code.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_Multi( Ivy_Man_t * p, Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ) +{ + assert( Type == IVY_AND || Type == IVY_EXOR ); + assert( nArgs > 0 ); + return Ivy_Multi_rec( p, pArgs, nArgs, Type ); +} + +/**Function************************************************************* + Synopsis [Implements the miter.] Description [] diff --git a/src/temp/ivy/ivySeq.c b/src/temp/ivy/ivySeq.c index 7cf55b69..11660e42 100644 --- a/src/temp/ivy/ivySeq.c +++ b/src/temp/ivy/ivySeq.c @@ -80,10 +80,6 @@ int Ivy_ManRewriteSeq( Ivy_Man_t * p, int fUseZeroCost, int fVerbose ) // stop if all nodes have been tried once if ( i > nNodes ) break; - if ( i == 8648 ) - { - int x = 0; - } // for each cut, try to resynthesize it nGain = Ivy_NodeRewriteSeq( p, pManRwt, pNode, fUseZeroCost ); if ( nGain > 0 || nGain == 0 && fUseZeroCost ) |