diff options
Diffstat (limited to 'src/temp/ivy')
-rw-r--r-- | src/temp/ivy/ivy.h | 450 | ||||
-rw-r--r-- | src/temp/ivy/ivyBalance.c | 421 | ||||
-rw-r--r-- | src/temp/ivy/ivyCanon.c | 147 | ||||
-rw-r--r-- | src/temp/ivy/ivyCheck.c | 121 | ||||
-rw-r--r-- | src/temp/ivy/ivyCut.c | 205 | ||||
-rw-r--r-- | src/temp/ivy/ivyDfs.c | 152 | ||||
-rw-r--r-- | src/temp/ivy/ivyDsd.c | 819 | ||||
-rw-r--r-- | src/temp/ivy/ivyMan.c | 207 | ||||
-rw-r--r-- | src/temp/ivy/ivyMulti.c | 427 | ||||
-rw-r--r-- | src/temp/ivy/ivyObj.c | 325 | ||||
-rw-r--r-- | src/temp/ivy/ivyOper.c | 254 | ||||
-rw-r--r-- | src/temp/ivy/ivyRewrite.c | 365 | ||||
-rw-r--r-- | src/temp/ivy/ivySeq.c | 101 | ||||
-rw-r--r-- | src/temp/ivy/ivyTable.c | 237 | ||||
-rw-r--r-- | src/temp/ivy/ivyUndo.c | 165 | ||||
-rw-r--r-- | src/temp/ivy/ivyUtil.c | 369 | ||||
-rw-r--r-- | src/temp/ivy/ivy_.c | 48 | ||||
-rw-r--r-- | src/temp/ivy/module.make | 14 |
18 files changed, 4827 insertions, 0 deletions
diff --git a/src/temp/ivy/ivy.h b/src/temp/ivy/ivy.h new file mode 100644 index 00000000..55ada384 --- /dev/null +++ b/src/temp/ivy/ivy.h @@ -0,0 +1,450 @@ +/**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 "vec.h" + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Ivy_Man_t_ Ivy_Man_t; +typedef struct Ivy_Obj_t_ Ivy_Obj_t; + +// object types +typedef enum { + IVY_NONE, // 0: unused node + 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: internal AND node + IVY_EXOR, // 6: internal EXOR node + IVY_BUF, // 7: internal buffer (temporary) + IVY_ANDM, // 8: multi-input AND (logic network only) + IVY_EXORM, // 9: multi-input EXOR (logic network only) + IVY_LUT // 10: multi-input LUT (logic network only) +} 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_ // 6 words +{ + int Id; // integer ID + int TravId; // traversal ID + int Fanin0; // fanin ID + int Fanin1; // fanin ID + int nRefs; // reference counter + unsigned Type : 4; // object type + unsigned fPhase : 1; // value under 000...0 pattern + unsigned fMarkA : 1; // multipurpose mask + unsigned fMarkB : 1; // multipurpose mask + unsigned fExFan : 1; // set to 1 if last fanout added is EXOR + unsigned fComp0 : 1; // complemented attribute + unsigned fComp1 : 1; // complemented attribute + unsigned Init : 2; // latch initial value + unsigned LevelR : 8; // reverse logic level + unsigned Level : 12; // logic level +}; + +// the AIG manager +struct Ivy_Man_t_ +{ + // AIG nodes + int nObjs[12]; // the number of objects by type + int nCreated; // the number of created objects + int nDeleted; // the number of deleted objects + int ObjIdNext; // the next free obj ID to assign + int nObjsAlloc; // the allocated number of nodes + Ivy_Obj_t * pObjs; // the array of all nodes + Vec_Int_t * vPis; // the array of PIs + Vec_Int_t * vPos; // the array of POs + // stuctural hash table + int * pTable; // structural hash table + int nTableSize; // structural hash table size + // various data members + int fExtended; // set to 1 in extended mode + int nTravIds; // the traversal ID + int nLevelMax; // the maximum level + void * pData; // the temporary data + // truth table of the 8-LUTs + unsigned * pMemory; // memory for truth tables + Vec_Int_t * vTruths; // offset for truth table of each node + // storage for the undo operation + Vec_Int_t * vFree; // storage for all deleted entries + Ivy_Obj_t * pUndos; // description of recently deleted nodes + int nUndos; // the number of recently deleted nodes + int nUndosAlloc; // the number of allocated cells + int fRecording; // shows that recording goes on +}; + + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +#define IVY_SANDBOX_SIZE 1 + +#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 int Ivy_FanCreate( int Id, int fCompl ) { return (Id << 1) | fCompl; } +static inline int Ivy_FanId( int Fan ) { return Fan >> 1; } +static inline int Ivy_FanCompl( int Fan ) { return Fan & 1; } + +static inline int Ivy_LeafCreate( int Id, int Lat ) { return (Id << 4) | Lat; } +static inline int Ivy_LeafId( int Leaf ) { return Leaf >> 4; } +static inline int Ivy_LeafLat( int Leaf ) { return Leaf & 15; } + +static inline Ivy_Obj_t * Ivy_Regular( Ivy_Obj_t * p ) { return (Ivy_Obj_t *)((unsigned)(p) & ~01); } +static inline Ivy_Obj_t * Ivy_Not( Ivy_Obj_t * p ) { return (Ivy_Obj_t *)((unsigned)(p) ^ 01); } +static inline Ivy_Obj_t * Ivy_NotCond( Ivy_Obj_t * p, int c ) { return (Ivy_Obj_t *)((unsigned)(p) ^ (c)); } +static inline int Ivy_IsComplement( Ivy_Obj_t * p ) { return (int )(((unsigned)p) & 01); } + +static inline Ivy_Obj_t * Ivy_ManConst0( Ivy_Man_t * p ) { return Ivy_Not(p->pObjs); } +static inline Ivy_Obj_t * Ivy_ManConst1( Ivy_Man_t * p ) { return p->pObjs; } +static inline Ivy_Obj_t * Ivy_ManGhost( Ivy_Man_t * p ) { return p->pObjs - IVY_SANDBOX_SIZE; } +static inline Ivy_Obj_t * Ivy_ManPi( Ivy_Man_t * p, int i ) { return p->pObjs + Vec_IntEntry(p->vPis,i); } +static inline Ivy_Obj_t * Ivy_ManPo( Ivy_Man_t * p, int i ) { return p->pObjs + Vec_IntEntry(p->vPos,i); } +static inline Ivy_Obj_t * Ivy_ManObj( Ivy_Man_t * p, int i ) { return p->pObjs + i; } + +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_ManAndMultiNum( Ivy_Man_t * p ) { return p->nObjs[IVY_ANDM]; } +static inline int Ivy_ManExorMultiNum( Ivy_Man_t * p ) { return p->nObjs[IVY_EXORM]; } +static inline int Ivy_ManLutNum( Ivy_Man_t * p ) { return p->nObjs[IVY_LUT]; } +static inline int Ivy_ManObjNum( Ivy_Man_t * p ) { return p->nCreated - p->nDeleted; } +static inline int Ivy_ManObjIdNext( Ivy_Man_t * p ) { return p->ObjIdNext; } +static inline int Ivy_ManObjAllocNum( Ivy_Man_t * p ) { return p->nObjsAlloc; } +static inline int Ivy_ManNodeNum( Ivy_Man_t * p ) { return p->fExtended? p->nObjs[IVY_ANDM]+p->nObjs[IVY_EXORM]+p->nObjs[IVY_LUT] : 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 ) { 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_ObjIsAndMulti( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_ANDM; } +static inline int Ivy_ObjIsExorMulti( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_EXORM; } +static inline int Ivy_ObjIsLut( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_LUT; } +static inline int Ivy_ObjIsNodeExt( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type >= IVY_ANDM; } + +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_Man_t * Ivy_ObjMan( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return *((Ivy_Man_t **)(pObj - pObj->Id - IVY_SANDBOX_SIZE - 1)); } +static inline Ivy_Obj_t * Ivy_ObjConst0( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return Ivy_Not(pObj - pObj->Id); } +static inline Ivy_Obj_t * Ivy_ObjConst1( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj - pObj->Id; } +static inline Ivy_Obj_t * Ivy_ObjGhost( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj - pObj->Id - IVY_SANDBOX_SIZE; } +static inline Ivy_Obj_t * Ivy_ObjObj( Ivy_Obj_t * pObj, int n ) { assert( !Ivy_IsComplement(pObj) ); return pObj - pObj->Id + n; } +static inline Ivy_Obj_t * Ivy_ObjNext( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj - pObj->Id + pObj->TravId; } + +static inline void Ivy_ObjSetTravId( Ivy_Obj_t * pObj, int TravId ) { assert( !Ivy_IsComplement(pObj) ); pObj->TravId = TravId; } +static inline void Ivy_ObjSetTravIdCurrent( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); pObj->TravId = Ivy_ObjMan(pObj)->nTravIds; } +static inline void Ivy_ObjSetTravIdPrevious( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); pObj->TravId = Ivy_ObjMan(pObj)->nTravIds - 1; } +static inline int Ivy_ObjIsTravIdCurrent( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return (int )((int)pObj->TravId == Ivy_ObjMan(pObj)->nTravIds); } +static inline int Ivy_ObjIsTravIdPrevious( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return (int )((int)pObj->TravId == Ivy_ObjMan(pObj)->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->Fanin0; } +static inline int Ivy_ObjFaninId1( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Fanin1; } +static inline int Ivy_ObjFaninC0( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->fComp0; } +static inline int Ivy_ObjFaninC1( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->fComp1; } +static inline Ivy_Obj_t * Ivy_ObjFanin0( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return Ivy_ObjObj(pObj, pObj->Fanin0); } +static inline Ivy_Obj_t * Ivy_ObjFanin1( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return Ivy_ObjObj(pObj, pObj->Fanin1); } +static inline Ivy_Obj_t * Ivy_ObjChild0( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return Ivy_NotCond( Ivy_ObjFanin0(pObj), Ivy_ObjFaninC0(pObj) ); } +static inline Ivy_Obj_t * Ivy_ObjChild1( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return Ivy_NotCond( Ivy_ObjFanin1(pObj), Ivy_ObjFaninC1(pObj) ); } +static inline int Ivy_ObjLevelR( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->LevelR; } +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_MAX(Ivy_ObjFanin0(pObj)->Level, Ivy_ObjFanin1(pObj)->Level); } +static inline void Ivy_ObjClean( Ivy_Obj_t * pObj ) { + int IdSaved = pObj->Id; + if ( IdSaved == 54 ) + { + int x = 0; + } + 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_ObjFaninId0(pObj) == Ivy_ObjId(pFanin) ) return 0; + if ( Ivy_ObjFaninId1(pObj) == Ivy_ObjId(pFanin) ) return 1; + assert(0); return -1; +} +static inline int Ivy_ObjFanoutC( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout ) +{ + if ( Ivy_ObjFaninId0(pFanout) == Ivy_ObjId(pObj) ) return Ivy_ObjFaninC0(pObj); + if ( Ivy_ObjFaninId1(pFanout) == Ivy_ObjId(pObj) ) return Ivy_ObjFaninC1(pObj); + assert(0); return -1; +} + +// create the ghost of the new node +static inline Ivy_Obj_t * Ivy_ObjCreateGhost( Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Type_t Type, Ivy_Init_t Init ) +{ + Ivy_Obj_t * pGhost; + int Temp; + pGhost = Ivy_ObjGhost(Ivy_Regular(p0)); + pGhost->Type = Type; + pGhost->Init = Init; + pGhost->fComp0 = Ivy_IsComplement(p0); + pGhost->fComp1 = Ivy_IsComplement(p1); + pGhost->Fanin0 = Ivy_ObjId(Ivy_Regular(p0)); + pGhost->Fanin1 = Ivy_ObjId(Ivy_Regular(p1)); + if ( pGhost->Fanin0 < pGhost->Fanin1 ) + { + Temp = pGhost->Fanin0, pGhost->Fanin0 = pGhost->Fanin1, pGhost->Fanin1 = Temp; + Temp = pGhost->fComp0, pGhost->fComp0 = pGhost->fComp1, pGhost->fComp1 = Temp; + } + assert( Ivy_ObjIsOneFanin(pGhost) || pGhost->Fanin0 > pGhost->Fanin1 ); + return pGhost; +} + +// create the ghost of the new node +static inline Ivy_Obj_t * Ivy_ObjCreateGhost2( Ivy_Man_t * p, Ivy_Obj_t * pObjDead ) +{ + Ivy_Obj_t * pGhost; + pGhost = Ivy_ManGhost(p); + pGhost->Type = pObjDead->Type; + pGhost->Init = pObjDead->Init; + pGhost->fComp0 = pObjDead->fComp0; + pGhost->fComp1 = pObjDead->fComp1; + pGhost->Fanin0 = pObjDead->Fanin0; + pGhost->Fanin1 = pObjDead->Fanin1; + assert( Ivy_ObjIsOneFanin(pGhost) || pGhost->Fanin0 > pGhost->Fanin1 ); + 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; +} + +// extended fanins +static inline Vec_Int_t * Ivy_ObjGetFanins( Ivy_Obj_t * pObj ) { assert(Ivy_ObjMan(pObj)->fExtended); return (Vec_Int_t *)*(((int*)pObj)+2); } +static inline void Ivy_ObjSetFanins( Ivy_Obj_t * pObj, Vec_Int_t * vFanins ) { assert(Ivy_ObjMan(pObj)->fExtended); assert(Ivy_ObjGetFanins(pObj)==NULL); *(Vec_Int_t **)(((int*)pObj)+2) = vFanins; } +static inline void Ivy_ObjStartFanins( Ivy_Obj_t * pObj, int nFanins ) { assert(Ivy_ObjMan(pObj)->fExtended); Ivy_ObjSetFanins( pObj, Vec_IntAlloc(nFanins) ); } +static inline void Ivy_ObjAddFanin( Ivy_Obj_t * pObj, int Fanin ) { assert(Ivy_ObjMan(pObj)->fExtended); Vec_IntPush( Ivy_ObjGetFanins(pObj), Fanin ); } +static inline int Ivy_ObjReadFanin( Ivy_Obj_t * pObj, int i ) { assert(Ivy_ObjMan(pObj)->fExtended); return Vec_IntEntry( Ivy_ObjGetFanins(pObj), i ); } +static inline int Ivy_ObjFaninNum( Ivy_Obj_t * pObj ) { assert(Ivy_ObjMan(pObj)->fExtended); return Vec_IntSize( Ivy_ObjGetFanins(pObj) ); } + +//////////////////////////////////////////////////////////////////////// +/// ITERATORS /// +//////////////////////////////////////////////////////////////////////// + +// iterator over all objects, including those currently not used +#define Ivy_ManForEachObj( p, pObj, i ) \ + for ( i = 0, pObj = p->pObjs; i < p->ObjIdNext; i++, pObj++ ) +// iterator over the primary inputs +#define Ivy_ManForEachPi( p, pObj, i ) \ + for ( i = 0; i < Vec_IntSize(p->vPis) && ((pObj) = Ivy_ManPi(p, i)); i++ ) +// iterator over the primary outputs +#define Ivy_ManForEachPo( p, pObj, i ) \ + for ( i = 0; i < Vec_IntSize(p->vPos) && ((pObj) = Ivy_ManPo(p, i)); i++ ) +// iterator over the combinational inputs +#define Ivy_ManForEachCi( p, pObj, i ) \ + for ( i = 0, pObj = p->pObjs; i < p->ObjIdNext; i++, pObj++ ) \ + if ( !Ivy_ObjIsCi(pObj) ) {} else +// iterator over the combinational outputs +#define Ivy_ManForEachCo( p, pObj, i ) \ + for ( i = 0, pObj = p->pObjs; i < p->ObjIdNext; i++, pObj++ ) \ + if ( !Ivy_ObjIsCo(pObj) ) {} else +// iterator over logic nodes (AND and EXOR gates) +#define Ivy_ManForEachNode( p, pObj, i ) \ + for ( i = 1, pObj = p->pObjs+i; i < p->ObjIdNext; i++, pObj++ ) \ + if ( !Ivy_ObjIsNode(pObj) ) {} else +// iterator over logic latches +#define Ivy_ManForEachLatch( p, pObj, i ) \ + for ( i = 1, pObj = p->pObjs+i; i < p->ObjIdNext; i++, pObj++ ) \ + 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++ ) + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== ivyCanon.c ========================================================*/ +extern Ivy_Obj_t * Ivy_CanonAnd( Ivy_Obj_t * p0, Ivy_Obj_t * p1 ); +extern Ivy_Obj_t * Ivy_CanonExor( Ivy_Obj_t * p0, Ivy_Obj_t * p1 ); +extern Ivy_Obj_t * Ivy_CanonLatch( Ivy_Obj_t * pObj, Ivy_Init_t Init ); +/*=== ivyCheck.c ========================================================*/ +extern int Ivy_ManCheck( Ivy_Man_t * p ); +/*=== ivyCut.c ==========================================================*/ +extern void Ivy_ManSeqFindCut( Ivy_Obj_t * pNode, Vec_Int_t * vFront, Vec_Int_t * vInside, int nSize ); +/*=== ivyBalance.c ======================================================*/ +extern int Ivy_ManBalance( Ivy_Man_t * p, int fUpdateLevel ); +/*=== ivyDfs.c ==========================================================*/ +extern Vec_Int_t * Ivy_ManDfs( Ivy_Man_t * p ); +extern Vec_Int_t * Ivy_ManDfsExt( Ivy_Man_t * p ); +/*=== 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 ); +/*=== ivyMan.c ==========================================================*/ +extern Ivy_Man_t * Ivy_ManStart( int nPis, int nPos, int nNodesMax ); +extern void Ivy_ManStop( Ivy_Man_t * p ); +extern void Ivy_ManGrow( Ivy_Man_t * p ); +extern int Ivy_ManCleanup( Ivy_Man_t * p ); +extern void Ivy_ManPrintStats( Ivy_Man_t * p ); +/*=== ivyMulti.c ==========================================================*/ +extern Ivy_Obj_t * Ivy_Multi( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ); +extern Ivy_Obj_t * Ivy_Multi1( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ); +extern Ivy_Obj_t * Ivy_Multi_rec( Ivy_Obj_t ** ppObjs, int nObjs, Ivy_Type_t Type ); +extern Ivy_Obj_t * Ivy_MultiBalance_rec( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ); +/*=== ivyObj.c ==========================================================*/ +extern Ivy_Obj_t * Ivy_ObjCreate( Ivy_Obj_t * pGhost ); +extern Ivy_Obj_t * Ivy_ObjCreateExt( Ivy_Man_t * p, Ivy_Type_t Type ); +extern void Ivy_ObjConnect( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanin ); +extern void Ivy_ObjDelete( Ivy_Obj_t * pObj, int fFreeTop ); +extern void Ivy_ObjDelete_rec( Ivy_Obj_t * pObj, int fFreeTop ); +extern void Ivy_ObjReplace( Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, int fDeleteOld, int fFreeTop ); +extern void Ivy_NodeFixBufferFanins( Ivy_Obj_t * pNode ); +/*=== ivyOper.c =========================================================*/ +extern Ivy_Obj_t * Ivy_Oper( Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Type_t Type ); +extern Ivy_Obj_t * Ivy_And( Ivy_Obj_t * p0, Ivy_Obj_t * p1 ); +extern Ivy_Obj_t * Ivy_Or( Ivy_Obj_t * p0, Ivy_Obj_t * p1 ); +extern Ivy_Obj_t * Ivy_Exor( Ivy_Obj_t * p0, Ivy_Obj_t * p1 ); +extern Ivy_Obj_t * Ivy_Mux( Ivy_Obj_t * pC, Ivy_Obj_t * p1, Ivy_Obj_t * p0 ); +extern Ivy_Obj_t * Ivy_Maj( Ivy_Obj_t * pA, Ivy_Obj_t * pB, Ivy_Obj_t * pC ); +extern Ivy_Obj_t * Ivy_Miter( Vec_Ptr_t * vPairs ); +/*=== ivyRewrite.c =========================================================*/ +extern int Ivy_ManSeqRewrite( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost ); +/*=== ivyTable.c ========================================================*/ +extern Ivy_Obj_t * Ivy_TableLookup( Ivy_Obj_t * pObj ); +extern void Ivy_TableInsert( Ivy_Obj_t * pObj ); +extern void Ivy_TableDelete( Ivy_Obj_t * pObj ); +extern void Ivy_TableUpdate( Ivy_Obj_t * pObj, int ObjIdNew ); +extern int Ivy_TableCountEntries( Ivy_Man_t * p ); +extern void Ivy_TableResize( Ivy_Man_t * p ); +/*=== ivyUndo.c =========================================================*/ +extern void Ivy_ManUndoStart( Ivy_Man_t * p ); +extern void Ivy_ManUndoStop( Ivy_Man_t * p ); +extern void Ivy_ManUndoRecord( Ivy_Man_t * p, Ivy_Obj_t * pObj ); +extern void Ivy_ManUndoPerform( Ivy_Man_t * p, Ivy_Obj_t * pRoot ); +/*=== ivyUtil.c =========================================================*/ +extern void Ivy_ManIncrementTravId( Ivy_Man_t * p ); +extern void Ivy_ManCleanTravId( Ivy_Man_t * p ); +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 unsigned * Ivy_ManCutTruth( Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes, Vec_Int_t * vTruth ); +extern Ivy_Obj_t * Ivy_NodeRealFanin_rec( Ivy_Obj_t * pNode, int iFanin ); +extern Vec_Int_t * Ivy_ManLatches( Ivy_Man_t * p ); + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/temp/ivy/ivyBalance.c b/src/temp/ivy/ivyBalance.c new file mode 100644 index 00000000..bbe69dd9 --- /dev/null +++ b/src/temp/ivy/ivyBalance.c @@ -0,0 +1,421 @@ +/**CFile**************************************************************** + + FileName [ivyBalance.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [Algebraic AIG balancing.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: ivyBalance.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ivy.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static void Ivy_NodeBalance( Ivy_Obj_t * pNode, int fUpdateLevel, Vec_Ptr_t * vFront, Vec_Ptr_t * vSpots ); + +// this procedure returns 1 if the node cannot be expanded +static inline int Ivy_NodeStopFanin( Ivy_Obj_t * pNode, int iFanin ) +{ + if ( iFanin == 0 ) + return Ivy_ObjFanin0(pNode)->Type != pNode->Type || Ivy_ObjRefs(Ivy_ObjFanin0(pNode)) > 1 || Ivy_ObjFaninC0(pNode); + else + return Ivy_ObjFanin1(pNode)->Type != pNode->Type || Ivy_ObjRefs(Ivy_ObjFanin1(pNode)) > 1 || Ivy_ObjFaninC1(pNode); +} + +// this procedure returns 1 if the node cannot be recursively dereferenced +static inline int Ivy_NodeBalanceDerefFanin( Ivy_Obj_t * pNode, int iFanin ) +{ + if ( iFanin == 0 ) + return Ivy_ObjFanin0(pNode)->Type == pNode->Type && Ivy_ObjRefs(Ivy_ObjFanin0(pNode)) == 0 && !Ivy_ObjFaninC0(pNode); + else + return Ivy_ObjFanin1(pNode)->Type == pNode->Type && Ivy_ObjRefs(Ivy_ObjFanin1(pNode)) == 0 && !Ivy_ObjFaninC1(pNode); +} + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Performs algebraic balancing of the AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_ManBalance( Ivy_Man_t * p, int fUpdateLevel ) +{ + Vec_Int_t * vNodes; + Vec_Ptr_t * vFront, * vSpots; + Ivy_Obj_t * pNode; + int i; + vSpots = Vec_PtrAlloc( 50 ); + vFront = Vec_PtrAlloc( 50 ); + vNodes = Ivy_ManDfs( p ); + Ivy_ManForEachNodeVec( p, vNodes, pNode, i ) + { + if ( Ivy_ObjIsBuf(pNode) ) + continue; + // fix the fanin buffer problem + Ivy_NodeFixBufferFanins( pNode ); + // skip node if it became a buffer + if ( Ivy_ObjIsBuf(pNode) ) + continue; + // skip nodes with one fanout if type of the node is the same as type of the fanout + // such nodes will be processed when the fanouts are processed + if ( Ivy_ObjRefs(pNode) == 1 && Ivy_ObjIsExor(pNode) == Ivy_ObjExorFanout(pNode) ) + continue; + assert( Ivy_ObjRefs(pNode) > 0 ); + // do not balance the node if both if its fanins have more than one fanout + if ( Ivy_NodeStopFanin(pNode, 0) && Ivy_NodeStopFanin(pNode, 1) ) + continue; + // try balancing this node + Ivy_NodeBalance( pNode, fUpdateLevel, vFront, vSpots ); + } + Vec_IntFree( vNodes ); + Vec_PtrFree( vSpots ); + Vec_PtrFree( vFront ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Dereferences MFFC of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_NodeBalanceDeref_rec( Ivy_Obj_t * pNode ) +{ + Ivy_Obj_t * pFan; + // deref the first fanin + pFan = Ivy_ObjFanin0(pNode); + Ivy_ObjRefsDec( pFan ); + if ( Ivy_NodeBalanceDerefFanin(pNode, 0) ) + Ivy_NodeBalanceDeref_rec( pFan ); + // deref the second fanin + pFan = Ivy_ObjFanin1(pNode); + Ivy_ObjRefsDec( pFan ); + if ( Ivy_NodeBalanceDerefFanin(pNode, 1) ) + Ivy_NodeBalanceDeref_rec( pFan ); +} + +/**Function************************************************************* + + Synopsis [Removes nodes inside supergate and determines frontier.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_NodeBalanceCollect_rec( Ivy_Obj_t * pNode, Vec_Ptr_t * vSpots, Vec_Ptr_t * vFront ) +{ + Ivy_Obj_t * pFanin; + // skip visited nodes + if ( Vec_PtrFind(vSpots, pNode) >= 0 ) + return; + // collect node + Vec_PtrPush( vSpots, pNode ); + // first fanin + pFanin = Ivy_ObjFanin0(pNode); + if ( Ivy_ObjRefs(pFanin) == 0 ) + Ivy_NodeBalanceCollect_rec( pFanin, vSpots, vFront ); + else if ( Ivy_ObjIsExor(pNode) && Vec_PtrFind(vFront, Ivy_ObjChild0(pNode)) >= 0 ) + Vec_PtrRemove( vFront, Ivy_ObjChild0(pNode) ); + else + Vec_PtrPushUnique( vFront, Ivy_ObjChild0(pNode) ); + // second fanin + pFanin = Ivy_ObjFanin1(pNode); + if ( Ivy_ObjRefs(pFanin) == 0 ) + Ivy_NodeBalanceCollect_rec( pFanin, vSpots, vFront ); + else if ( Ivy_ObjIsExor(pNode) && Vec_PtrFind(vFront, Ivy_ObjChild1(pNode)) >= 0 ) + Vec_PtrRemove( vFront, Ivy_ObjChild1(pNode) ); + else + Vec_PtrPushUnique( vFront, Ivy_ObjChild1(pNode) ); +} + +/**Function************************************************************* + + Synopsis [Comparison procedure for two nodes by level.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_BalanceCompareByLevel( Ivy_Obj_t ** pp1, Ivy_Obj_t ** pp2 ) +{ + int Level1 = Ivy_ObjLevel( *pp1 ); + int Level2 = Ivy_ObjLevel( *pp2 ); + if ( Level1 > Level2 ) + return -1; + if ( Level1 < Level2 ) + return 1; + return 0; +} + +/**Function************************************************************* + + Synopsis [Removes nodes inside supergate and determines frontier.] + + Description [Return 1 if the output needs to be complemented.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_NodeBalancePrepare( Ivy_Obj_t * pNode, Vec_Ptr_t * vFront, Vec_Ptr_t * vSpots ) +{ + Ivy_Man_t * pMan = Ivy_ObjMan( pNode ); + Ivy_Obj_t * pObj, * pNext; + int i, k, Counter = 0; + // dereference the cone + Ivy_NodeBalanceDeref_rec( pNode ); + // collect the frontier and the internal nodes + Vec_PtrClear( vFront ); + Vec_PtrClear( vSpots ); + Ivy_NodeBalanceCollect_rec( pNode, vSpots, vFront ); + // remove all the nodes + Vec_PtrForEachEntry( vSpots, pObj, i ) + { + // skip the first entry (the node itself) + if ( i == 0 ) continue; + // collect the free entries + Vec_IntPush( pMan->vFree, pObj->Id ); + Ivy_ObjDelete( pObj, 1 ); + } + // sort nodes by level in decreasing order + qsort( (void *)Vec_PtrArray(vFront), Vec_PtrSize(vFront), sizeof(Ivy_Obj_t *), + (int (*)(const void *, const void *))Ivy_BalanceCompareByLevel ); + // check if there are nodes and their complements + Counter = 0; + Vec_PtrForEachEntry( vFront, pObj, i ) + { + if ( i == Vec_PtrSize(vFront) - 1 ) + break; + pNext = Vec_PtrEntry( vFront, i+1 ); + if ( Ivy_Regular(pObj) == Ivy_Regular(pNext) ) + { + assert( pObj == Ivy_Not(pNext) ); + Vec_PtrWriteEntry( vFront, i, NULL ); + Vec_PtrWriteEntry( vFront, i+1, NULL ); + i++; + Counter++; + } + } + // if there are no complemented pairs, go ahead and balance + if ( Counter == 0 ) + return 0; + // if there are complemented pairs and this is AND, create const 0 + if ( Counter > 0 && Ivy_ObjIsAnd(pNode) ) + { + Vec_PtrClear( vFront ); + Vec_PtrPush( vFront, Ivy_ManConst0(pMan) ); + return 0; + } + assert( Counter > 0 && Ivy_ObjIsExor(pNode) ); + // remove the pairs + k = 0; + Vec_PtrForEachEntry( vFront, pObj, i ) + if ( pObj ) + Vec_PtrWriteEntry( vFront, k++, pObj ); + Vec_PtrShrink( vFront, k ); + // add constant zero node if nothing is left + if ( Vec_PtrSize(vFront) == 0 ) + Vec_PtrPush( vFront, Ivy_ManConst0(pMan) ); + // return 1 if the number of pairs is odd (need to complement the output) + return Counter & 1; +} + +/**Function************************************************************* + + Synopsis [Finds the left bound on the next candidate to be paired.] + + Description [The nodes in the array are in the decreasing order of levels. + The last node in the array has the smallest level. By default it would be paired + with the next node on the left. However, it may be possible to pair it with some + other node on the left, in such a way that the new node is shared. This procedure + finds the index of the left-most node, which can be paired with the last node.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_NodeBalanceFindLeft( Vec_Ptr_t * vSuper ) +{ + Ivy_Obj_t * pNodeRight, * pNodeLeft; + int Current; + // if two or less nodes, pair with the first + if ( Vec_PtrSize(vSuper) < 3 ) + return 0; + // set the pointer to the one before the last + Current = Vec_PtrSize(vSuper) - 2; + pNodeRight = Vec_PtrEntry( vSuper, Current ); + // go through the nodes to the left of this one + for ( Current--; Current >= 0; Current-- ) + { + // get the next node on the left + pNodeLeft = Vec_PtrEntry( vSuper, Current ); + // if the level of this node is different, quit the loop + if ( Ivy_Regular(pNodeLeft)->Level != Ivy_Regular(pNodeRight)->Level ) + break; + } + Current++; + // get the node, for which the equality holds + pNodeLeft = Vec_PtrEntry( vSuper, Current ); + assert( Ivy_Regular(pNodeLeft)->Level == Ivy_Regular(pNodeRight)->Level ); + return Current; +} + +/**Function************************************************************* + + Synopsis [Moves closer to the end the node that is best for sharing.] + + Description [If there is no node with sharing, randomly chooses one of + the legal nodes.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_NodeBalancePermute( Ivy_Man_t * pMan, Vec_Ptr_t * vSuper, int LeftBound, int fExor ) +{ + Ivy_Obj_t * pNode1, * pNode2, * pNode3, * pGhost; + int RightBound, i; + // get the right bound + RightBound = Vec_PtrSize(vSuper) - 2; + assert( LeftBound <= RightBound ); + if ( LeftBound == RightBound ) + return; + // get the two last nodes + pNode1 = Vec_PtrEntry( vSuper, RightBound + 1 ); + pNode2 = Vec_PtrEntry( vSuper, RightBound ); + // find the first node that can be shared + for ( i = RightBound; i >= LeftBound; i-- ) + { + pNode3 = Vec_PtrEntry( vSuper, i ); + pGhost = Ivy_ObjCreateGhost( pNode1, pNode3, fExor? IVY_EXOR : IVY_AND, IVY_INIT_NONE ); + if ( Ivy_TableLookup( pGhost ) ) + { + if ( pNode3 == pNode2 ) + return; + Vec_PtrWriteEntry( vSuper, i, pNode2 ); + Vec_PtrWriteEntry( vSuper, RightBound, pNode3 ); + return; + } + } +/* + // we did not find the node to share, randomize choice + { + int Choice = rand() % (RightBound - LeftBound + 1); + pNode3 = Vec_PtrEntry( vSuper, LeftBound + Choice ); + if ( pNode3 == pNode2 ) + return; + Vec_PtrWriteEntry( vSuper, LeftBound + Choice, pNode2 ); + Vec_PtrWriteEntry( vSuper, RightBound, pNode3 ); + } +*/ +} + +/**Function************************************************************* + + Synopsis [Inserts a new node in the order by levels.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_NodeBalancePushUniqueOrderByLevel( Vec_Ptr_t * vFront, Ivy_Obj_t * pNode ) +{ + Ivy_Obj_t * pNode1, * pNode2; + int i; + if ( Vec_PtrPushUnique(vFront, pNode) ) + return; + // find the p of the node + for ( i = vFront->nSize-1; i > 0; i-- ) + { + pNode1 = vFront->pArray[i ]; + pNode2 = vFront->pArray[i-1]; + if ( Ivy_Regular(pNode1)->Level <= Ivy_Regular(pNode2)->Level ) + break; + vFront->pArray[i ] = pNode2; + vFront->pArray[i-1] = pNode1; + } +} + +/**Function************************************************************* + + Synopsis [Balances one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_NodeBalance( Ivy_Obj_t * pNode, int fUpdateLevel, Vec_Ptr_t * vFront, Vec_Ptr_t * vSpots ) +{ + Ivy_Man_t * pMan = Ivy_ObjMan( pNode ); + Ivy_Obj_t * pFan0, * pFan1, * pNodeNew; + int fCompl, LeftBound; + // remove internal nodes and derive the frontier + fCompl = Ivy_NodeBalancePrepare( pNode, vFront, vSpots ); + assert( Vec_PtrSize(vFront) > 0 ); + // balance the nodes + while ( Vec_PtrSize(vFront) > 1 ) + { + // find the left bound on the node to be paired + LeftBound = (!fUpdateLevel)? 0 : Ivy_NodeBalanceFindLeft( vFront ); + // find the node that can be shared (if no such node, randomize choice) + Ivy_NodeBalancePermute( pMan, vFront, LeftBound, Ivy_ObjIsExor(pNode) ); + // pull out the last two nodes + pFan0 = Vec_PtrPop(vFront); assert( !Ivy_ObjIsConst1(Ivy_Regular(pFan0)) ); + pFan1 = Vec_PtrPop(vFront); assert( !Ivy_ObjIsConst1(Ivy_Regular(pFan1)) ); + // create the new node + pNodeNew = Ivy_ObjCreate( Ivy_ObjCreateGhost(pFan0, pFan1, Ivy_ObjType(pNode), IVY_INIT_NONE) ); + // add the new node to the frontier + Ivy_NodeBalancePushUniqueOrderByLevel( vFront, pNodeNew ); + } + assert( Vec_PtrSize(vFront) == 1 ); + // perform the replacement + Ivy_ObjReplace( pNode, Ivy_NotCond(Vec_PtrPop(vFront), fCompl), 1, 1 ); +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ivy/ivyCanon.c b/src/temp/ivy/ivyCanon.c new file mode 100644 index 00000000..c6f43d15 --- /dev/null +++ b/src/temp/ivy/ivyCanon.c @@ -0,0 +1,147 @@ +/**CFile**************************************************************** + + FileName [ivyCanon.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [Finding canonical form of objects.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: ivyCanon.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ivy.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static Ivy_Obj_t * Ivy_TableLookupPair_rec( Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1, int fCompl0, int fCompl1, Ivy_Type_t Type ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Creates the canonical form of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_CanonPair_rec( Ivy_Obj_t * pGhost ) +{ + Ivy_Obj_t * pResult, * pLat0, * pLat1; + Ivy_Init_t Init, Init0, Init1; + int fCompl0, fCompl1; + Ivy_Type_t Type; + assert( Ivy_ObjIsNode(pGhost) ); + assert( Ivy_ObjIsAnd(pGhost) || (!Ivy_ObjFaninC0(pGhost) && !Ivy_ObjFaninC1(pGhost)) ); + assert( Ivy_ObjFaninId0(pGhost) != 0 && Ivy_ObjFaninId1(pGhost) != 0 ); + // consider the case when the pair is canonical + if ( !Ivy_ObjIsLatch(Ivy_ObjFanin0(pGhost)) || !Ivy_ObjIsLatch(Ivy_ObjFanin1(pGhost)) ) + { + if ( pResult = Ivy_TableLookup( pGhost ) ) + return pResult; + return Ivy_ObjCreate( pGhost ); + } + /// remember the latches + pLat0 = Ivy_ObjFanin0(pGhost); + pLat1 = Ivy_ObjFanin1(pGhost); + // remember type and compls + Type = Ivy_ObjType(pGhost); + fCompl0 = Ivy_ObjFaninC0(pGhost); + fCompl1 = Ivy_ObjFaninC1(pGhost); + // modify the fanins to be latch fanins + pGhost->Fanin0 = Ivy_ObjFaninId0(pLat0); + pGhost->Fanin1 = Ivy_ObjFaninId0(pLat1); + // call recursively + pResult = Ivy_CanonPair_rec( pGhost ); + // build latch on top of this + Init0 = Ivy_InitNotCond( Ivy_ObjInit(pLat0), fCompl0 ); + Init1 = Ivy_InitNotCond( Ivy_ObjInit(pLat1), fCompl1 ); + Init = (Type == IVY_AND)? Ivy_InitAnd(Init0, Init1) : Ivy_InitExor(Init0, Init1); + return Ivy_CanonLatch( pResult, Init ); +} + +/**Function************************************************************* + + Synopsis [Creates the canonical form of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_CanonAnd( Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 ) +{ + Ivy_Obj_t * pGhost, * pResult; + pGhost = Ivy_ObjCreateGhost( pObj0, pObj1, IVY_AND, IVY_INIT_NONE ); + pResult = Ivy_CanonPair_rec( pGhost ); + return pResult; +} + +/**Function************************************************************* + + Synopsis [Creates the canonical form of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_CanonExor( Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 ) +{ + Ivy_Obj_t * pGhost, * pResult; + int fCompl = Ivy_IsComplement(pObj0) ^ Ivy_IsComplement(pObj1); + pObj0 = Ivy_Regular(pObj0); + pObj1 = Ivy_Regular(pObj1); + pGhost = Ivy_ObjCreateGhost( pObj0, pObj1, IVY_EXOR, IVY_INIT_NONE ); + pResult = Ivy_CanonPair_rec( pGhost ); + return Ivy_NotCond( pResult, fCompl ); +} + +/**Function************************************************************* + + Synopsis [Creates the canonical form of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_CanonLatch( Ivy_Obj_t * pObj, Ivy_Init_t Init ) +{ + Ivy_Obj_t * pGhost, * pResult; + int fCompl = Ivy_IsComplement(pObj); + pObj = Ivy_Regular(pObj); + pGhost = Ivy_ObjCreateGhost( pObj, Ivy_ObjConst1(pObj), IVY_LATCH, Ivy_InitNotCond(Init, fCompl) ); + pResult = Ivy_TableLookup( pGhost ); + if ( pResult == NULL ) + pResult = Ivy_ObjCreate( pGhost ); + return Ivy_NotCond( pResult, fCompl ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ivy/ivyCheck.c b/src/temp/ivy/ivyCheck.c new file mode 100644 index 00000000..c39eac12 --- /dev/null +++ b/src/temp/ivy/ivyCheck.c @@ -0,0 +1,121 @@ +/**CFile**************************************************************** + + FileName [ivyCheck.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [AIG checking procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: ivyCheck.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ivy.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Checks the consistency of the AIG manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_ManCheck( Ivy_Man_t * pMan ) +{ + Ivy_Obj_t * pObj, * pObj2; + int i; + Ivy_ManForEachObj( pMan, pObj, i ) + { + // skip deleted nodes + if ( Ivy_ObjIsNone(pObj) ) + continue; + // consider the constant node and PIs + if ( i == 0 || Ivy_ObjIsPi(pObj) ) + { + if ( Ivy_ObjFaninId0(pObj) || Ivy_ObjFaninId1(pObj) || Ivy_ObjLevel(pObj) ) + { + printf( "Ivy_ManCheck: The AIG has non-standard constant or PI node with ID \"%d\".\n", pObj->Id ); + return 0; + } + continue; + } + if ( Ivy_ObjIsPo(pObj) ) + { + if ( Ivy_ObjFaninId1(pObj) ) + { + printf( "Ivy_ManCheck: The AIG has non-standard PO node with ID \"%d\".\n", pObj->Id ); + return 0; + } + continue; + } + if ( Ivy_ObjIsBuf(pObj) ) + { + continue; + } + if ( Ivy_ObjIsLatch(pObj) ) + { + if ( Ivy_ObjFaninId1(pObj) != 0 ) + { + printf( "Ivy_ManCheck: The latch with ID \"%d\" contains second fanin.\n", pObj->Id ); + return 0; + } + if ( Ivy_ObjInit(pObj) == 0 ) + { + printf( "Ivy_ManCheck: The latch with ID \"%d\" does not have initial state.\n", pObj->Id ); + return 0; + } + pObj2 = Ivy_TableLookup( pObj ); + if ( pObj2 != pObj ) + printf( "Ivy_ManCheck: Latch with ID \"%d\" is not in the structural hashing table.\n", pObj->Id ); + continue; + } + // consider the AND node + if ( !Ivy_ObjFaninId0(pObj) || !Ivy_ObjFaninId1(pObj) ) + { + printf( "Ivy_ManCheck: The AIG has internal node \"%d\" with a constant fanin.\n", pObj->Id ); + return 0; + } + if ( Ivy_ObjFaninId0(pObj) <= Ivy_ObjFaninId1(pObj) ) + { + printf( "Ivy_ManCheck: The AIG has node \"%d\" with a wrong ordering of fanins.\n", pObj->Id ); + return 0; + } +// if ( Ivy_ObjLevel(pObj) != Ivy_ObjLevelNew(pObj) ) +// printf( "Ivy_ManCheck: Node with ID \"%d\" has level that does not agree with the fanin levels.\n", pObj->Id ); + pObj2 = Ivy_TableLookup( pObj ); + if ( pObj2 != pObj ) + printf( "Ivy_ManCheck: Node with ID \"%d\" is not in the structural hashing table.\n", pObj->Id ); + } + // count the number of nodes in the table + if ( Ivy_TableCountEntries(pMan) != Ivy_ManAndNum(pMan) + Ivy_ManExorNum(pMan) + Ivy_ManLatchNum(pMan) ) + { + printf( "Ivy_ManCheck: The number of nodes in the structural hashing table is wrong.\n" ); + return 0; + } + return 1; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ivy/ivyCut.c b/src/temp/ivy/ivyCut.c new file mode 100644 index 00000000..a8fd148b --- /dev/null +++ b/src/temp/ivy/ivyCut.c @@ -0,0 +1,205 @@ +/**CFile**************************************************************** + + FileName [ivyCut.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [Computes reconvergence driven sequential cut.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: ivyCut.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ivy.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Evaluate the cost of removing the node from the set of leaves.] + + Description [Returns the number of new leaves that will be brought in. + Returns large number if the node cannot be removed from the set of leaves.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Ivy_NodeGetLeafCostOne( Ivy_Man_t * p, int Leaf, Vec_Int_t * vInside ) +{ + Ivy_Obj_t * pNode; + int nLatches, FaninLeaf, Cost; + // make sure leaf is not a contant node + assert( Leaf > 0 ); + // get the node + pNode = Ivy_ManObj( p, Ivy_LeafId(Leaf) ); + // cannot expand over the PI node + if ( Ivy_ObjIsPi(pNode) || Ivy_ObjIsConst1(pNode) ) + return 999; + // get the number of latches + nLatches = Ivy_LeafLat(Leaf) + Ivy_ObjIsLatch(pNode); + if ( nLatches > 15 ) + return 999; + // get the first fanin + FaninLeaf = Ivy_LeafCreate( Ivy_ObjFaninId0(pNode), nLatches ); + Cost = FaninLeaf && (Vec_IntFind(vInside, FaninLeaf) == -1); + // quit if this is the one fanin node + if ( Ivy_ObjIsLatch(pNode) || Ivy_ObjIsBuf(pNode) ) + return Cost; + assert( Ivy_ObjIsNode(pNode) ); + // get the second fanin + FaninLeaf = Ivy_LeafCreate( Ivy_ObjFaninId1(pNode), nLatches ); + Cost += FaninLeaf && (Vec_IntFind(vInside, FaninLeaf) == -1); + return Cost; +} + +/**Function************************************************************* + + Synopsis [Builds reconvergence-driven cut by changing one leaf at a time.] + + Description [This procedure looks at the current leaves and tries to change + one leaf at a time in such a way that the cut grows as little as possible. + In evaluating the fanins, this procedure looks only at their immediate + predecessors (this is why it is called a one-level construction procedure).] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_ManSeqFindCut_int( Ivy_Man_t * p, Vec_Int_t * vFront, Vec_Int_t * vInside, int nSizeLimit ) +{ + Ivy_Obj_t * pNode; + int CostBest, CostCur, Leaf, LeafBest, Next, nLatches, i; + int LeavesBest[10]; + int Counter; + + // add random selection of the best fanin!!! + + // find the best fanin + CostBest = 99; + LeafBest = -1; + Counter = -1; +//printf( "Evaluating fanins of the cut:\n" ); + Vec_IntForEachEntry( vFront, Leaf, i ) + { + CostCur = Ivy_NodeGetLeafCostOne( p, Leaf, vInside ); +//printf( " Fanin %s has cost %d.\n", Ivy_ObjName(pNode), CostCur ); + if ( CostBest > CostCur ) + { + CostBest = CostCur; + LeafBest = Leaf; + LeavesBest[0] = Leaf; + Counter = 1; + } + else if ( CostBest == CostCur ) + LeavesBest[Counter++] = Leaf; + + if ( CostBest <= 1 ) // can be if ( CostBest <= 1 ) + break; + } + if ( CostBest == 99 ) + return 0; +// return Ivy_NodeBuildCutLevelTwo_int( vInside, vFront, nFaninLimit ); + + assert( CostBest < 3 ); + if ( Vec_IntSize(vFront) - 1 + CostBest > nSizeLimit ) + return 0; +// return Ivy_NodeBuildCutLevelTwo_int( vInside, vFront, nFaninLimit ); + + assert( Counter > 0 ); +printf( "%d", Counter ); + + LeafBest = LeavesBest[rand() % Counter]; + + // remove the node from the array + assert( LeafBest >= 0 ); + Vec_IntRemove( vFront, LeafBest ); +//printf( "Removing fanin %s.\n", Ivy_ObjName(pNode) ); + + // get the node and its latches + pNode = Ivy_ManObj( p, Ivy_LeafId(LeafBest) ); + nLatches = Ivy_LeafLat(LeafBest) + Ivy_ObjIsLatch(pNode); + assert( Ivy_ObjIsNode(pNode) || Ivy_ObjIsLatch(pNode) || Ivy_ObjIsBuf(pNode) ); + + // add the left child to the fanins + Next = Ivy_LeafCreate( Ivy_ObjFaninId0(pNode), nLatches ); + if ( Next && Vec_IntFind(vInside, Next) == -1 ) + { +//printf( "Adding fanin %s.\n", Ivy_ObjName(pNext) ); + Vec_IntPush( vFront, Next ); + Vec_IntPush( vInside, Next ); + } + + // quit if this is the one fanin node + if ( Ivy_ObjIsLatch(pNode) || Ivy_ObjIsBuf(pNode) ) + return 1; + assert( Ivy_ObjIsNode(pNode) ); + + // add the right child to the fanins + Next = Ivy_LeafCreate( Ivy_ObjFaninId1(pNode), nLatches ); + if ( Next && Vec_IntFind(vInside, Next) == -1 ) + { +//printf( "Adding fanin %s.\n", Ivy_ObjName(pNext) ); + Vec_IntPush( vFront, Next ); + Vec_IntPush( vInside, Next ); + } + assert( Vec_IntSize(vFront) <= nSizeLimit ); + // keep doing this + return 1; +} + +/**Function************************************************************* + + Synopsis [Computes one sequential cut of the given size.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManSeqFindCut( Ivy_Obj_t * pRoot, Vec_Int_t * vFront, Vec_Int_t * vInside, int nSize ) +{ + assert( !Ivy_IsComplement(pRoot) ); + assert( Ivy_ObjIsNode(pRoot) ); + assert( Ivy_ObjFaninId0(pRoot) ); + assert( Ivy_ObjFaninId1(pRoot) ); + + // start the cut + Vec_IntClear( vFront ); + Vec_IntPush( vFront, Ivy_LeafCreate(Ivy_ObjFaninId0(pRoot), 0) ); + Vec_IntPush( vFront, Ivy_LeafCreate(Ivy_ObjFaninId1(pRoot), 0) ); + + // start the visited nodes + Vec_IntClear( vInside ); + Vec_IntPush( vInside, Ivy_LeafCreate(pRoot->Id, 0) ); + Vec_IntPush( vInside, Ivy_LeafCreate(Ivy_ObjFaninId0(pRoot), 0) ); + Vec_IntPush( vInside, Ivy_LeafCreate(Ivy_ObjFaninId1(pRoot), 0) ); + + // compute the cut + while ( Ivy_ManSeqFindCut_int( Ivy_ObjMan(pRoot), vFront, vInside, nSize ) ); + assert( Vec_IntSize(vFront) <= nSize ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ivy/ivyDfs.c b/src/temp/ivy/ivyDfs.c new file mode 100644 index 00000000..2db80b00 --- /dev/null +++ b/src/temp/ivy/ivyDfs.c @@ -0,0 +1,152 @@ +/**CFile**************************************************************** + + FileName [ivyDfs.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [DFS collection procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: ivyDfs.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ivy.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Collects nodes in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManDfs_rec( Ivy_Obj_t * pObj, Vec_Int_t * vNodes ) +{ + if ( Ivy_ObjIsConst1(pObj) || Ivy_ObjIsCi(pObj) ) + return; + if ( Ivy_ObjIsMarkA(pObj) ) + return; + Ivy_ObjSetMarkA(pObj); + assert( Ivy_ObjIsBuf(pObj) || Ivy_ObjIsAnd(pObj) || Ivy_ObjIsExor(pObj) ); + Ivy_ManDfs_rec( Ivy_ObjFanin0(pObj), vNodes ); + if ( !Ivy_ObjIsBuf(pObj) ) + Ivy_ManDfs_rec( Ivy_ObjFanin1(pObj), vNodes ); + Vec_IntPush( vNodes, pObj->Id ); +} + +/**Function************************************************************* + + Synopsis [Collects AND/EXOR nodes in the DFS order from CIs to COs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Ivy_ManDfs( Ivy_Man_t * p ) +{ + Vec_Int_t * vNodes; + Ivy_Obj_t * pObj; + int i; + // collect the nodes + vNodes = Vec_IntAlloc( Ivy_ManNodeNum(p) ); + if ( Ivy_ManLatchNum(p) > 0 ) + Ivy_ManForEachCo( p, pObj, i ) + Ivy_ManDfs_rec( Ivy_ObjFanin0(pObj), vNodes ); + else + Ivy_ManForEachPo( p, pObj, i ) + Ivy_ManDfs_rec( Ivy_ObjFanin0(pObj), vNodes ); + // unmark the collected nodes + 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) ); + return vNodes; +} + +/**Function************************************************************* + + Synopsis [Collects nodes in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManDfsExt_rec( Ivy_Obj_t * pObj, Vec_Int_t * vNodes ) +{ + Vec_Int_t * vFanins; + int i, Fanin; + if ( !Ivy_ObjIsNodeExt(pObj) || Ivy_ObjIsMarkA(pObj) ) + return; + // mark the node as visited + Ivy_ObjSetMarkA(pObj); + // traverse the fanins + vFanins = Ivy_ObjGetFanins( pObj ); + Vec_IntForEachEntry( vFanins, Fanin, i ) + Ivy_ManDfsExt_rec( Ivy_ObjObj(pObj, Ivy_FanId(Fanin)), vNodes ); + // add the node + Vec_IntPush( vNodes, pObj->Id ); +} + +/**Function************************************************************* + + Synopsis [Collects nodes in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Ivy_ManDfsExt( Ivy_Man_t * p ) +{ + Vec_Int_t * vNodes; + Ivy_Obj_t * pObj, * pFanin; + int i; + assert( p->fExtended ); + assert( Ivy_ManLatchNum(p) == 0 ); + // make sure network does not have buffers + vNodes = Vec_IntAlloc( 10 ); + Ivy_ManForEachPo( p, pObj, i ) + { + pFanin = Ivy_ManObj( p, Ivy_FanId( Ivy_ObjReadFanin(pObj,0) ) ); + Ivy_ManDfsExt_rec( pFanin, vNodes ); + } + Ivy_ManForEachNodeVec( p, vNodes, pObj, i ) + Ivy_ObjClearMarkA(pObj); + // make sure network does not have dangling nodes + // the network may have dangling nodes if some fanins of ESOPs do not appear in cubes +// assert( p->nNodes == Vec_PtrSize(vNodes) ); + return vNodes; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ivy/ivyDsd.c b/src/temp/ivy/ivyDsd.c new file mode 100644 index 00000000..5dfdd30f --- /dev/null +++ b/src/temp/ivy/ivyDsd.c @@ -0,0 +1,819 @@ +/**CFile**************************************************************** + + FileName [ivyDsd.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [Disjoint-support decomposition.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: ivyDsd.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ivy.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +// decomposition types +typedef enum { + IVY_DEC_PI, // 0: var + IVY_DEC_CONST1, // 1: CONST1 + IVY_DEC_BUF, // 2: BUF + IVY_DEC_AND, // 3: AND + IVY_DEC_EXOR, // 4: EXOR + IVY_DEC_MUX, // 5: MUX + IVY_DEC_MAJ, // 6: MAJ + IVY_DEC_PRIME // 7: undecomposable +} Ivy_DecType_t; + +typedef struct Ivy_Dec_t_ Ivy_Dec_t; +struct Ivy_Dec_t_ +{ + unsigned Type : 4; // the node type (PI, CONST1, AND, EXOR, MUX, PRIME) + unsigned fCompl : 1; // shows if node is complemented (root node only) + unsigned nFans : 3; // the number of fanins + unsigned Fan0 : 4; // fanin 0 + unsigned Fan1 : 4; // fanin 1 + unsigned Fan2 : 4; // fanin 2 + unsigned Fan3 : 4; // fanin 3 + unsigned Fan4 : 4; // fanin 4 + unsigned Fan5 : 4; // fanin 5 +}; + +static inline int Ivy_DecToInt( Ivy_Dec_t Node ) { return *((int *)&Node); } +static inline Ivy_Dec_t Ivy_IntToDec( int Node ) { return *((Ivy_Dec_t *)&Node); } +static inline void Ivy_DecClear( Ivy_Dec_t * pNode ) { *((int *)pNode) = 0; } + + +static unsigned s_Masks[6][2] = { + { 0x55555555, 0xAAAAAAAA }, + { 0x33333333, 0xCCCCCCCC }, + { 0x0F0F0F0F, 0xF0F0F0F0 }, + { 0x00FF00FF, 0xFF00FF00 }, + { 0x0000FFFF, 0xFFFF0000 }, + { 0x00000000, 0xFFFFFFFF } +}; + +static inline int Ivy_TruthWordCountOnes( unsigned uWord ) +{ + uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555); + uWord = (uWord & 0x33333333) + ((uWord>>2) & 0x33333333); + uWord = (uWord & 0x0F0F0F0F) + ((uWord>>4) & 0x0F0F0F0F); + uWord = (uWord & 0x00FF00FF) + ((uWord>>8) & 0x00FF00FF); + return (uWord & 0x0000FFFF) + (uWord>>16); +} + +static inline int Ivy_TruthCofactorIsConst( unsigned uTruth, int Var, int Cof, int Const ) +{ + if ( Const == 0 ) + return (uTruth & s_Masks[Var][Cof]) == 0; + else + return (uTruth & s_Masks[Var][Cof]) == s_Masks[Var][Cof]; +} + +static inline int Ivy_TruthCofactorIsOne( unsigned uTruth, int Var ) +{ + return (uTruth & s_Masks[Var][0]) == 0; +} + +static inline unsigned Ivy_TruthCofactor( unsigned uTruth, int Var ) +{ + unsigned uCofactor = uTruth & s_Masks[Var >> 1][(Var & 1) == 0]; + int Shift = (1 << (Var >> 1)); + if ( Var & 1 ) + return uCofactor | (uCofactor << Shift); + return uCofactor | (uCofactor >> Shift); +} + +static inline unsigned Ivy_TruthCofactor2( unsigned uTruth, int Var0, int Var1 ) +{ + return Ivy_TruthCofactor( Ivy_TruthCofactor(uTruth, Var0), Var1 ); +} + +// returns 1 if the truth table depends on this var (var is regular interger var) +static inline int Ivy_TruthDepends( unsigned uTruth, int Var ) +{ + return Ivy_TruthCofactor(uTruth, Var << 1) != Ivy_TruthCofactor(uTruth, (Var << 1) | 1); +} + +static inline void Ivy_DecSetVar( Ivy_Dec_t * pNode, int iNum, unsigned Var ) +{ + assert( iNum >= 0 && iNum <= 5 ); + switch( iNum ) + { + case 0: pNode->Fan0 = Var; break; + case 1: pNode->Fan1 = Var; break; + case 2: pNode->Fan2 = Var; break; + case 3: pNode->Fan3 = Var; break; + case 4: pNode->Fan4 = Var; break; + case 5: pNode->Fan5 = Var; break; + } +} + +static inline unsigned Ivy_DecGetVar( Ivy_Dec_t * pNode, int iNum ) +{ + assert( iNum >= 0 && iNum <= 5 ); + switch( iNum ) + { + case 0: return pNode->Fan0; + case 1: return pNode->Fan1; + case 2: return pNode->Fan2; + case 3: return pNode->Fan3; + case 4: return pNode->Fan4; + case 5: return pNode->Fan5; + } + return ~0; +} + +static int Ivy_TruthDecompose_rec( unsigned uTruth, Vec_Int_t * vTree ); +static int Ivy_TruthRecognizeMuxMaj( unsigned uTruth, int * pSupp, int nSupp, Vec_Int_t * vTree ); + +//int nTruthDsd; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Computes DSD of truth table of 5 variables or less.] + + Description [Returns 1 if the function is a constant or is fully + DSD decomposable using AND/EXOR/MUX gates.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_TruthDsd( unsigned uTruth, Vec_Int_t * vTree ) +{ + Ivy_Dec_t Node; + int i, RetValue; + // set the PI variables + Vec_IntClear( vTree ); + for ( i = 0; i < 5; i++ ) + Vec_IntPush( vTree, 0 ); + // check if it is a constant + if ( uTruth == 0 || ~uTruth == 0 ) + { + Ivy_DecClear( &Node ); + Node.Type = IVY_DEC_CONST1; + Node.fCompl = (uTruth == 0); + Vec_IntPush( vTree, Ivy_DecToInt(Node) ); + return 1; + } + // perform the decomposition + RetValue = Ivy_TruthDecompose_rec( uTruth, vTree ); + if ( RetValue == -1 ) + return 0; + // get the topmost node + if ( (RetValue >> 1) < 5 ) + { // add buffer + Ivy_DecClear( &Node ); + Node.Type = IVY_DEC_BUF; + Node.fCompl = (RetValue & 1); + Node.Fan0 = ((RetValue >> 1) << 1); + Vec_IntPush( vTree, Ivy_DecToInt(Node) ); + } + else if ( RetValue & 1 ) + { // check if the topmost node has to be complemented + Node = Ivy_IntToDec( Vec_IntPop(vTree) ); + assert( Node.fCompl == 0 ); + Node.fCompl = (RetValue & 1); + Vec_IntPush( vTree, Ivy_DecToInt(Node) ); + } + if ( uTruth != Ivy_TruthDsdCompute(vTree) ) + printf( "Verification failed.\n" ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Computes DSD of truth table.] + + Description [Returns the number of topmost decomposition node.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_TruthDecompose_rec( unsigned uTruth, Vec_Int_t * vTree ) +{ + Ivy_Dec_t Node; + int Supp[5], Vars0[5], Vars1[5], Vars2[5], * pVars; + int nSupp, Count0, Count1, Count2, nVars, RetValue, fCompl, i; + unsigned uTruthCof, uCof0, uCof1; + + // get constant confactors + Count0 = Count1 = Count2 = nSupp = 0; + for ( i = 0; i < 5; i++ ) + { + if ( Ivy_TruthCofactorIsConst(uTruth, i, 0, 0) ) + Vars0[Count0++] = (i << 1) | 0; + else if ( Ivy_TruthCofactorIsConst(uTruth, i, 1, 0) ) + Vars0[Count0++] = (i << 1) | 1; + else if ( Ivy_TruthCofactorIsConst(uTruth, i, 0, 1) ) + Vars1[Count1++] = (i << 1) | 0; + else if ( Ivy_TruthCofactorIsConst(uTruth, i, 1, 1) ) + Vars1[Count1++] = (i << 1) | 1; + else + { + uCof0 = Ivy_TruthCofactor( uTruth, (i << 1) | 1 ); + uCof1 = Ivy_TruthCofactor( uTruth, (i << 1) | 0 ); + if ( uCof0 == ~uCof1 ) + Vars2[Count2++] = (i << 1) | 0; + else if ( uCof0 != uCof1 ) + Supp[nSupp++] = i; + } + } + assert( Count0 == 0 || Count1 == 0 ); + assert( Count0 == 0 || Count2 == 0 ); + assert( Count1 == 0 || Count2 == 0 ); + + // consider the case of a single variable + if ( Count0 == 1 && nSupp == 0 ) + return Vars0[0]; + + // consider more complex decompositions + if ( Count0 == 0 && Count1 == 0 && Count2 == 0 ) + return Ivy_TruthRecognizeMuxMaj( uTruth, Supp, nSupp, vTree ); + + // extract the nodes + Ivy_DecClear( &Node ); + if ( Count0 > 0 ) + nVars = Count0, pVars = Vars0, Node.Type = IVY_DEC_AND, fCompl = 0; + else if ( Count1 > 0 ) + nVars = Count1, pVars = Vars1, Node.Type = IVY_DEC_AND, fCompl = 1, uTruth = ~uTruth; + else if ( Count2 > 0 ) + nVars = Count2, pVars = Vars2, Node.Type = IVY_DEC_EXOR, fCompl = 0; + else + assert( 0 ); + Node.nFans = nVars+(nSupp>0); + + // compute cofactor + uTruthCof = uTruth; + for ( i = 0; i < nVars; i++ ) + { + uTruthCof = Ivy_TruthCofactor( uTruthCof, pVars[i] ); + Ivy_DecSetVar( &Node, i, pVars[i] ); + } + + if ( Node.Type == IVY_DEC_EXOR ) + fCompl ^= ((Node.nFans & 1) == 0); + + if ( nSupp > 0 ) + { + assert( uTruthCof != 0 && ~uTruthCof != 0 ); + // call recursively + RetValue = Ivy_TruthDecompose_rec( uTruthCof, vTree ); + // quit if non-decomposable + if ( RetValue == -1 ) + return -1; + // remove the complement from the child if the node is EXOR + if ( Node.Type == IVY_DEC_EXOR && (RetValue & 1) ) + { + fCompl ^= 1; + RetValue ^= 1; + } + // set the new decomposition + Ivy_DecSetVar( &Node, nVars, RetValue ); + } + else if ( Node.Type == IVY_DEC_EXOR ) + fCompl ^= (uTruthCof == 0); + + Vec_IntPush( vTree, Ivy_DecToInt(Node) ); + return ((Vec_IntSize(vTree)-1) << 1) | fCompl; +} + +/**Function************************************************************* + + Synopsis [Returns a non-negative number if the truth table is a MUX.] + + Description [If the truth table is a MUX, returns the variable as follows: + first, control variable; second, positive cofactor; third, negative cofactor.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_TruthRecognizeMuxMaj( unsigned uTruth, int * pSupp, int nSupp, Vec_Int_t * vTree ) +{ + Ivy_Dec_t Node; + int i, k, RetValue0, RetValue1; + unsigned uCof0, uCof1, Num; + char Count[3]; + assert( nSupp >= 3 ); + // start the node + Ivy_DecClear( &Node ); + Node.Type = IVY_DEC_MUX; + Node.nFans = 3; + // try each of the variables + for ( i = 0; i < nSupp; i++ ) + { + // get the cofactors with respect to these variables + uCof0 = Ivy_TruthCofactor( uTruth, (pSupp[i] << 1) | 1 ); + uCof1 = Ivy_TruthCofactor( uTruth, pSupp[i] << 1 ); + // go through all other variables and make sure + // each of them belongs to the support of one cofactor + for ( k = 0; k < nSupp; k++ ) + { + if ( k == i ) + continue; + if ( Ivy_TruthDepends(uCof0, pSupp[k]) && Ivy_TruthDepends(uCof1, pSupp[k]) ) + break; + } + if ( k < nSupp ) + continue; + // MUX decomposition exists + RetValue0 = Ivy_TruthDecompose_rec( uCof0, vTree ); + if ( RetValue0 == -1 ) + break; + RetValue1 = Ivy_TruthDecompose_rec( uCof1, vTree ); + if ( RetValue1 == -1 ) + break; + // both of them exist; create the node + Ivy_DecSetVar( &Node, 0, pSupp[i] << 1 ); + Ivy_DecSetVar( &Node, 1, RetValue1 ); + Ivy_DecSetVar( &Node, 2, RetValue0 ); + Vec_IntPush( vTree, Ivy_DecToInt(Node) ); + return ((Vec_IntSize(vTree)-1) << 1) | 0; + } + // check majority gate + if ( nSupp > 3 ) + return -1; + if ( Ivy_TruthWordCountOnes(uTruth) != 16 ) + return -1; + // this is a majority gate; determine polarity + Node.Type = IVY_DEC_MAJ; + Count[0] = Count[1] = Count[2] = 0; + for ( i = 0; i < 8; i++ ) + { + Num = 0; + for ( k = 0; k < 3; k++ ) + if ( i & (1 << k) ) + Num |= (1 << pSupp[k]); + assert( Num < 32 ); + if ( (uTruth & (1 << Num)) == 0 ) + continue; + for ( k = 0; k < 3; k++ ) + if ( i & (1 << k) ) + Count[k]++; + } + assert( Count[0] == 1 || Count[0] == 3 ); + assert( Count[1] == 1 || Count[1] == 3 ); + assert( Count[2] == 1 || Count[2] == 3 ); + Ivy_DecSetVar( &Node, 0, (pSupp[0] << 1)|(Count[0] == 1) ); + Ivy_DecSetVar( &Node, 1, (pSupp[1] << 1)|(Count[1] == 1) ); + Ivy_DecSetVar( &Node, 2, (pSupp[2] << 1)|(Count[2] == 1) ); + Vec_IntPush( vTree, Ivy_DecToInt(Node) ); + return ((Vec_IntSize(vTree)-1) << 1) | 0; +} + + +/**Function************************************************************* + + Synopsis [Computes truth table of decomposition tree for verification.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned Ivy_TruthDsdCompute_rec( int iNode, Vec_Int_t * vTree ) +{ + unsigned uTruthChild, uTruthTotal; + int Var, i; + // get the node + Ivy_Dec_t Node = Ivy_IntToDec( Vec_IntEntry(vTree, iNode) ); + // compute the node function + if ( Node.Type == IVY_DEC_CONST1 ) + return s_Masks[5][ !Node.fCompl ]; + if ( Node.Type == IVY_DEC_PI ) + return s_Masks[iNode][ !Node.fCompl ]; + if ( Node.Type == IVY_DEC_BUF ) + { + uTruthTotal = Ivy_TruthDsdCompute_rec( Node.Fan0 >> 1, vTree ); + return Node.fCompl? ~uTruthTotal : uTruthTotal; + } + if ( Node.Type == IVY_DEC_AND ) + { + uTruthTotal = s_Masks[5][1]; + for ( i = 0; i < (int)Node.nFans; i++ ) + { + Var = Ivy_DecGetVar( &Node, i ); + uTruthChild = Ivy_TruthDsdCompute_rec( Var >> 1, vTree ); + uTruthTotal = (Var & 1)? uTruthTotal & ~uTruthChild : uTruthTotal & uTruthChild; + } + return Node.fCompl? ~uTruthTotal : uTruthTotal; + } + if ( Node.Type == IVY_DEC_EXOR ) + { + uTruthTotal = 0; + for ( i = 0; i < (int)Node.nFans; i++ ) + { + Var = Ivy_DecGetVar( &Node, i ); + uTruthTotal ^= Ivy_TruthDsdCompute_rec( Var >> 1, vTree ); + assert( (Var & 1) == 0 ); + } + return Node.fCompl? ~uTruthTotal : uTruthTotal; + } + assert( Node.fCompl == 0 ); + if ( Node.Type == IVY_DEC_MUX || Node.Type == IVY_DEC_MAJ ) + { + unsigned uTruthChildC, uTruthChild1, uTruthChild0; + int VarC, Var1, Var0; + VarC = Ivy_DecGetVar( &Node, 0 ); + Var1 = Ivy_DecGetVar( &Node, 1 ); + Var0 = Ivy_DecGetVar( &Node, 2 ); + uTruthChildC = Ivy_TruthDsdCompute_rec( VarC >> 1, vTree ); + uTruthChild1 = Ivy_TruthDsdCompute_rec( Var1 >> 1, vTree ); + uTruthChild0 = Ivy_TruthDsdCompute_rec( Var0 >> 1, vTree ); + assert( Node.Type == IVY_DEC_MAJ || (VarC & 1) == 0 ); + uTruthChildC = (VarC & 1)? ~uTruthChildC : uTruthChildC; + uTruthChild1 = (Var1 & 1)? ~uTruthChild1 : uTruthChild1; + uTruthChild0 = (Var0 & 1)? ~uTruthChild0 : uTruthChild0; + if ( Node.Type == IVY_DEC_MUX ) + return (uTruthChildC & uTruthChild1) | (~uTruthChildC & uTruthChild0); + else + return (uTruthChildC & uTruthChild1) | (uTruthChildC & uTruthChild0) | (uTruthChild1 & uTruthChild0); + } + assert( 0 ); + return 0; +} + + +/**Function************************************************************* + + Synopsis [Computes truth table of decomposition tree for verification.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned Ivy_TruthDsdCompute( Vec_Int_t * vTree ) +{ + return Ivy_TruthDsdCompute_rec( Vec_IntSize(vTree)-1, vTree ); +} + +/**Function************************************************************* + + Synopsis [Prints the decomposition tree.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_TruthDsdPrint_rec( FILE * pFile, int iNode, Vec_Int_t * vTree ) +{ + int Var, i; + // get the node + Ivy_Dec_t Node = Ivy_IntToDec( Vec_IntEntry(vTree, iNode) ); + // compute the node function + if ( Node.Type == IVY_DEC_CONST1 ) + fprintf( pFile, "Const1%s", (Node.fCompl? "\'" : "") ); + else if ( Node.Type == IVY_DEC_PI ) + fprintf( pFile, "%c%s", 'a' + iNode, (Node.fCompl? "\'" : "") ); + else if ( Node.Type == IVY_DEC_BUF ) + { + Ivy_TruthDsdPrint_rec( pFile, Node.Fan0 >> 1, vTree ); + fprintf( pFile, "%s", (Node.fCompl? "\'" : "") ); + } + else if ( Node.Type == IVY_DEC_AND ) + { + fprintf( pFile, "AND(" ); + for ( i = 0; i < (int)Node.nFans; i++ ) + { + Var = Ivy_DecGetVar( &Node, i ); + Ivy_TruthDsdPrint_rec( pFile, Var >> 1, vTree ); + fprintf( pFile, "%s", (Var & 1)? "\'" : "" ); + if ( i != (int)Node.nFans-1 ) + fprintf( pFile, "," ); + } + fprintf( pFile, ")%s", (Node.fCompl? "\'" : "") ); + } + else if ( Node.Type == IVY_DEC_EXOR ) + { + fprintf( pFile, "EXOR(" ); + for ( i = 0; i < (int)Node.nFans; i++ ) + { + Var = Ivy_DecGetVar( &Node, i ); + Ivy_TruthDsdPrint_rec( pFile, Var >> 1, vTree ); + if ( i != (int)Node.nFans-1 ) + fprintf( pFile, "," ); + assert( (Var & 1) == 0 ); + } + fprintf( pFile, ")%s", (Node.fCompl? "\'" : "") ); + } + else if ( Node.Type == IVY_DEC_MUX || Node.Type == IVY_DEC_MAJ ) + { + int VarC, Var1, Var0; + assert( Node.fCompl == 0 ); + VarC = Ivy_DecGetVar( &Node, 0 ); + Var1 = Ivy_DecGetVar( &Node, 1 ); + Var0 = Ivy_DecGetVar( &Node, 2 ); + fprintf( pFile, "%s", (Node.Type == IVY_DEC_MUX)? "MUX(" : "MAJ(" ); + Ivy_TruthDsdPrint_rec( pFile, VarC >> 1, vTree ); + fprintf( pFile, "%s", (VarC & 1)? "\'" : "" ); + fprintf( pFile, "," ); + Ivy_TruthDsdPrint_rec( pFile, Var1 >> 1, vTree ); + fprintf( pFile, "%s", (Var1 & 1)? "\'" : "" ); + fprintf( pFile, "," ); + Ivy_TruthDsdPrint_rec( pFile, Var0 >> 1, vTree ); + fprintf( pFile, "%s", (Var0 & 1)? "\'" : "" ); + fprintf( pFile, ")" ); + } + else assert( 0 ); +} + + +/**Function************************************************************* + + Synopsis [Prints the decomposition tree.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_TruthDsdPrint( FILE * pFile, Vec_Int_t * vTree ) +{ + fprintf( pFile, "F = " ); + Ivy_TruthDsdPrint_rec( pFile, Vec_IntSize(vTree)-1, vTree ); + fprintf( pFile, "\n" ); +} + +/**Function************************************************************* + + Synopsis [Implement DSD in the AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_ManDsdConstruct_rec( Ivy_Man_t * p, Vec_Int_t * vFront, int iNode, Vec_Int_t * vTree ) +{ + Ivy_Obj_t * pResult, * pChild, * pNodes[16]; + int Var, i; + // get the node + Ivy_Dec_t Node = Ivy_IntToDec( Vec_IntEntry(vTree, iNode) ); + // compute the node function + if ( Node.Type == IVY_DEC_CONST1 ) + return Ivy_NotCond( Ivy_ManConst1(p), Node.fCompl ); + if ( Node.Type == IVY_DEC_PI ) + { + pResult = Ivy_ManObj( p, Vec_IntEntry(vFront, iNode) ); + return Ivy_NotCond( pResult, Node.fCompl ); + } + if ( Node.Type == IVY_DEC_BUF ) + { + pResult = Ivy_ManDsdConstruct_rec( p, vFront, Node.Fan0 >> 1, vTree ); + return Ivy_NotCond( pResult, Node.fCompl ); + } + if ( Node.Type == IVY_DEC_AND || Node.Type == IVY_DEC_EXOR ) + { + for ( i = 0; i < (int)Node.nFans; i++ ) + { + Var = Ivy_DecGetVar( &Node, i ); + assert( Node.Type == IVY_DEC_AND || (Var & 1) == 0 ); + pChild = Ivy_ManDsdConstruct_rec( p, vFront, Var >> 1, vTree ); + pChild = Ivy_NotCond( pChild, (Var & 1) ); + pNodes[i] = pChild; + } + +// Ivy_MultiEval( pNodes, Node.nFans, Node.Type == IVY_DEC_AND ? IVY_AND : IVY_EXOR ); + + pResult = Ivy_Multi( pNodes, Node.nFans, Node.Type == IVY_DEC_AND ? IVY_AND : IVY_EXOR ); + return Ivy_NotCond( pResult, Node.fCompl ); + } + assert( Node.fCompl == 0 ); + if ( Node.Type == IVY_DEC_MUX || Node.Type == IVY_DEC_MAJ ) + { + int VarC, Var1, Var0; + VarC = Ivy_DecGetVar( &Node, 0 ); + Var1 = Ivy_DecGetVar( &Node, 1 ); + Var0 = Ivy_DecGetVar( &Node, 2 ); + pNodes[0] = Ivy_ManDsdConstruct_rec( p, vFront, VarC >> 1, vTree ); + pNodes[1] = Ivy_ManDsdConstruct_rec( p, vFront, Var1 >> 1, vTree ); + pNodes[2] = Ivy_ManDsdConstruct_rec( p, vFront, Var0 >> 1, vTree ); + assert( Node.Type == IVY_DEC_MAJ || (VarC & 1) == 0 ); + pNodes[0] = Ivy_NotCond( pNodes[0], (VarC & 1) ); + pNodes[1] = Ivy_NotCond( pNodes[1], (Var1 & 1) ); + pNodes[2] = Ivy_NotCond( pNodes[2], (Var0 & 1) ); + if ( Node.Type == IVY_DEC_MUX ) + return Ivy_Mux( pNodes[0], pNodes[1], pNodes[2] ); + else + return Ivy_Maj( pNodes[0], pNodes[1], pNodes[2] ); + } + assert( 0 ); + return 0; +} + +/**Function************************************************************* + + Synopsis [Implement DSD in the AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_ManDsdConstruct( Ivy_Man_t * p, Vec_Int_t * vFront, Vec_Int_t * vTree ) +{ + int Entry, i; + // implement latches on the frontier (TEMPORARY!!!) + Vec_IntForEachEntry( vFront, Entry, i ) + Vec_IntWriteEntry( vFront, i, Ivy_LeafId(Entry) ); + // recursively construct the tree + return Ivy_ManDsdConstruct_rec( p, vFront, Vec_IntSize(vTree)-1, vTree ); +} + + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_TruthDsdComputePrint( unsigned uTruth ) +{ + static Vec_Int_t * vTree = NULL; + if ( vTree == NULL ) + vTree = Vec_IntAlloc( 12 ); + if ( Ivy_TruthDsd( uTruth, vTree ) ) + Ivy_TruthDsdPrint( stdout, vTree ); + else + printf( "Undecomposable\n" ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_TruthTestOne( unsigned uTruth ) +{ + static int Counter = 0; + static Vec_Int_t * vTree = NULL; + // decompose + if ( vTree == NULL ) + vTree = Vec_IntAlloc( 12 ); + + if ( !Ivy_TruthDsd( uTruth, vTree ) ) + { +// printf( "Undecomposable\n" ); + } + else + { +// nTruthDsd++; + printf( "%5d : ", Counter++ ); + Extra_PrintBinary( stdout, &uTruth, 32 ); + printf( " " ); + Ivy_TruthDsdPrint( stdout, vTree ); + if ( uTruth != Ivy_TruthDsdCompute(vTree) ) + printf( "Verification failed.\n" ); + } +// Vec_IntFree( vTree ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_TruthTest() +{ + FILE * pFile; + char Buffer[100]; + unsigned uTruth; + int i; + + pFile = fopen( "npn4.txt", "r" ); + for ( i = 0; i < 222; i++ ) +// pFile = fopen( "npn5.txt", "r" ); +// for ( i = 0; i < 616126; i++ ) + { + fscanf( pFile, "%s", Buffer ); + Extra_ReadHexadecimal( &uTruth, Buffer+2, 4 ); +// Extra_ReadHexadecimal( &uTruth, Buffer+2, 5 ); + uTruth |= (uTruth << 16); +// uTruth = ~uTruth; + Ivy_TruthTestOne( uTruth ); + } + fclose( pFile ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_TruthTest3() +{ + FILE * pFile; + char Buffer[100]; + unsigned uTruth; + int i; + + pFile = fopen( "npn3.txt", "r" ); + for ( i = 0; i < 14; i++ ) + { + fscanf( pFile, "%s", Buffer ); + Extra_ReadHexadecimal( &uTruth, Buffer+2, 3 ); + uTruth = uTruth | (uTruth << 8) | (uTruth << 16) | (uTruth << 24); + Ivy_TruthTestOne( uTruth ); + } + fclose( pFile ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_TruthTest5() +{ + FILE * pFile; + char Buffer[100]; + unsigned uTruth; + int i; + +// pFile = fopen( "npn4.txt", "r" ); +// for ( i = 0; i < 222; i++ ) + pFile = fopen( "npn5.txt", "r" ); + for ( i = 0; i < 616126; i++ ) + { + fscanf( pFile, "%s", Buffer ); +// Extra_ReadHexadecimal( &uTruth, Buffer+2, 4 ); + Extra_ReadHexadecimal( &uTruth, Buffer+2, 5 ); +// uTruth |= (uTruth << 16); +// uTruth = ~uTruth; + Ivy_TruthTestOne( uTruth ); + } + fclose( pFile ); +} + + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ivy/ivyMan.c b/src/temp/ivy/ivyMan.c new file mode 100644 index 00000000..04c31f3d --- /dev/null +++ b/src/temp/ivy/ivyMan.c @@ -0,0 +1,207 @@ +/**CFile**************************************************************** + + FileName [ivyMan.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [AIG manager.] + + 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 $] + +***********************************************************************/ + +#include "ivy.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Starts the AIG manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Man_t * Ivy_ManStart( int nPis, int nPos, int nNodesMax ) +{ + Ivy_Man_t * p; + Ivy_Obj_t * pObj; + int i, nTotalSize; + // start the manager + p = ALLOC( Ivy_Man_t, 1 ); + memset( p, 0, sizeof(Ivy_Man_t) ); + p->nTravIds = 1; + // AIG nodes + p->nObjsAlloc = 1 + nPis + nPos + nNodesMax; +// p->nObjsAlloc += (p->nObjsAlloc & 1); // make it even + nTotalSize = p->nObjsAlloc + IVY_SANDBOX_SIZE + 1; + p->pObjs = ALLOC( Ivy_Obj_t, nTotalSize ); + memset( p->pObjs, 0, sizeof(Ivy_Obj_t) * nTotalSize ); + // temporary storage for deleted entries + p->vFree = Vec_IntAlloc( 100 ); + // set the node IDs + for ( i = 0, pObj = p->pObjs; i < nTotalSize; i++, pObj++ ) + pObj->Id = i - IVY_SANDBOX_SIZE - 1; + // remember the manager in the first entry + *((Ivy_Man_t **)p->pObjs) = p; + p->pObjs += IVY_SANDBOX_SIZE + 1; + // create the constant node + p->nCreated = 1; + p->ObjIdNext = 1; + Ivy_ManConst1(p)->fPhase = 1; + // create PIs + pObj = Ivy_ManGhost(p); + pObj->Type = IVY_PI; + p->vPis = Vec_IntAlloc( 100 ); + for ( i = 0; i < nPis; i++ ) + Ivy_ObjCreate( pObj ); + // create POs + pObj->Type = IVY_PO; + p->vPos = Vec_IntAlloc( 100 ); + for ( i = 0; i < nPos; i++ ) + Ivy_ObjCreate( pObj ); + // start the table + p->nTableSize = p->nObjsAlloc*5/2+13; + p->pTable = ALLOC( int, p->nTableSize ); + memset( p->pTable, 0, sizeof(int) * p->nTableSize ); + // allocate undo storage + p->nUndosAlloc = 100; + p->pUndos = ALLOC( Ivy_Obj_t, p->nUndosAlloc ); + memset( p->pUndos, 0, sizeof(Ivy_Obj_t) * p->nUndosAlloc ); + return p; +} + +/**Function************************************************************* + + Synopsis [Stops the AIG manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManStop( Ivy_Man_t * p ) +{ + if ( p->fExtended ) + { + Ivy_Obj_t * pObj; + int i; + Ivy_ManForEachObj( p, pObj, i ) + if ( Ivy_ObjGetFanins(pObj) ) + Vec_IntFree( Ivy_ObjGetFanins(pObj) ); + } + if ( p->vFree ) Vec_IntFree( p->vFree ); + if ( p->vTruths ) Vec_IntFree( p->vTruths ); + if ( p->vPis ) Vec_IntFree( p->vPis ); + if ( p->vPos ) Vec_IntFree( p->vPos ); + FREE( p->pMemory ); + free( p->pObjs - IVY_SANDBOX_SIZE - 1 ); + free( p->pTable ); + free( p->pUndos ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [Returns the number of dangling nodes removed.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManGrow( Ivy_Man_t * p ) +{ + int i; + assert( p->ObjIdNext == p->nObjsAlloc ); + if ( p->ObjIdNext != p->nObjsAlloc ) + return; +// printf( "Ivy_ObjCreate(): Reallocing the node array.\n" ); + p->nObjsAlloc = 2 * p->nObjsAlloc; + p->pObjs = REALLOC( Ivy_Obj_t, p->pObjs - IVY_SANDBOX_SIZE - 1, p->nObjsAlloc + IVY_SANDBOX_SIZE + 1 ) + IVY_SANDBOX_SIZE + 1; + memset( p->pObjs + p->ObjIdNext, 0, sizeof(Ivy_Obj_t) * p->nObjsAlloc / 2 ); + for ( i = p->nObjsAlloc / 2; i < p->nObjsAlloc; i++ ) + Ivy_ManObj( p, i )->Id = i; +} + +/**Function************************************************************* + + Synopsis [Returns the number of dangling nodes removed.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_ManCleanup( Ivy_Man_t * p ) +{ + Ivy_Obj_t * pNode; + int i, nNodesOld; + nNodesOld = Ivy_ManNodeNum(p); + Ivy_ManForEachNode( p, pNode, i ) + if ( Ivy_ObjRefs(pNode) == 0 ) + Ivy_ObjDelete_rec( pNode, 1 ); + return nNodesOld - Ivy_ManNodeNum(p); +} + +/**Function************************************************************* + + Synopsis [Stops the AIG manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManPrintStats( Ivy_Man_t * p ) +{ + printf( "PI/PO = %d/%d ", Ivy_ManPiNum(p), Ivy_ManPoNum(p) ); + if ( p->fExtended ) + { + printf( "Am = %d. ", Ivy_ManAndMultiNum(p) ); + printf( "Xm = %d. ", Ivy_ManExorMultiNum(p) ); + printf( "Lut = %d. ", Ivy_ManLutNum(p) ); + } + else + { + printf( "A = %d. ", Ivy_ManAndNum(p) ); + printf( "X = %d. ", Ivy_ManExorNum(p) ); + printf( "B = %d. ", Ivy_ManBufNum(p) ); + } + printf( "MaxID = %d. ", p->ObjIdNext-1 ); + printf( "All = %d. ", p->nObjsAlloc ); + printf( "Cre = %d. ", p->nCreated ); + printf( "Del = %d. ", p->nDeleted ); + printf( "\n" ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ivy/ivyMulti.c b/src/temp/ivy/ivyMulti.c new file mode 100644 index 00000000..059d1500 --- /dev/null +++ b/src/temp/ivy/ivyMulti.c @@ -0,0 +1,427 @@ +/**CFile**************************************************************** + + FileName [ivyMulti.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [Constructing multi-input AND/EXOR gates.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: ivyMulti.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ivy.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Ivy_Eval_t_ Ivy_Eval_t; +struct Ivy_Eval_t_ +{ + unsigned Mask : 5; // the mask of covered nodes + unsigned Weight : 3; // the number of covered nodes + unsigned Cost : 4; // the number of overlapping nodes + unsigned Level : 12; // the level of this node + unsigned Fan0 : 4; // the first fanin + unsigned Fan1 : 4; // the second fanin +}; + +static Ivy_Obj_t * Ivy_MultiBuild_rec( Ivy_Eval_t * pEvals, int iNum, Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ); +static void Ivy_MultiSort( Ivy_Obj_t ** pArgs, int nArgs ); +static int Ivy_MultiPushUniqueOrderByLevel( Ivy_Obj_t ** pArray, int nArgs, Ivy_Obj_t * pNode ); +static Ivy_Obj_t * Ivy_MultiEval( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ); + + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**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_Obj_t ** ppObjs, int nObjs, Ivy_Type_t Type ) +{ + Ivy_Obj_t * pObj1, * pObj2; + if ( nObjs == 1 ) + return ppObjs[0]; + pObj1 = Ivy_Multi_rec( ppObjs, nObjs/2, Type ); + pObj2 = Ivy_Multi_rec( ppObjs + nObjs/2, nObjs - nObjs/2, Type ); + return Ivy_Oper( pObj1, pObj2, Type ); +} + +/**Function************************************************************* + + Synopsis [Constructs a balanced tree while taking sharing into account.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_Multi( Ivy_Obj_t ** pArgsInit, int nArgs, Ivy_Type_t Type ) +{ + static char NumBits[32] = {0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5}; + static Ivy_Eval_t pEvals[15+15*14/2]; + static Ivy_Obj_t * pArgs[16]; + Ivy_Eval_t * pEva, * pEvaBest; + int nArgsNew, nEvals, i, k; + Ivy_Obj_t * pTemp; + + // consider the case of one argument + assert( nArgs > 0 ); + if ( nArgs == 1 ) + return pArgsInit[0]; + // consider the case of two arguments + if ( nArgs == 2 ) + return Ivy_Oper( pArgsInit[0], pArgsInit[1], Type ); + +//Ivy_MultiEval( pArgsInit, nArgs, Type ); printf( "\n" ); + + // set the initial ones + for ( i = 0; i < nArgs; i++ ) + { + pArgs[i] = pArgsInit[i]; + pEva = pEvals + i; + pEva->Mask = (1 << i); + pEva->Weight = 1; + pEva->Cost = 0; + pEva->Level = Ivy_Regular(pArgs[i])->Level; + pEva->Fan0 = 0; + pEva->Fan1 = 0; + } + + // find the available nodes + pEvaBest = pEvals; + nArgsNew = nArgs; + for ( i = 1; i < nArgsNew; i++ ) + for ( k = 0; k < i; k++ ) + if ( pTemp = Ivy_TableLookup(Ivy_ObjCreateGhost(pArgs[k], pArgs[i], Type, IVY_INIT_NONE)) ) + { + pEva = pEvals + nArgsNew; + pEva->Mask = pEvals[k].Mask | pEvals[i].Mask; + pEva->Weight = NumBits[pEva->Mask]; + pEva->Cost = pEvals[k].Cost + pEvals[i].Cost + NumBits[pEvals[k].Mask & pEvals[i].Mask]; + pEva->Level = 1 + IVY_MAX(pEvals[k].Level, pEvals[i].Level); + pEva->Fan0 = k; + pEva->Fan1 = i; +// assert( pEva->Level == (unsigned)Ivy_ObjLevel(pTemp) ); + // compare + if ( pEvaBest->Weight < pEva->Weight || + pEvaBest->Weight == pEva->Weight && pEvaBest->Cost > pEva->Cost || + pEvaBest->Weight == pEva->Weight && pEvaBest->Cost == pEva->Cost && pEvaBest->Level > pEva->Level ) + pEvaBest = pEva; + // save the argument + pArgs[nArgsNew++] = pTemp; + if ( nArgsNew == 15 ) + goto Outside; + } +Outside: + +// printf( "Best = %d.\n", pEvaBest - pEvals ); + + // the case of no common nodes + if ( nArgsNew == nArgs ) + { + Ivy_MultiSort( pArgs, nArgs ); + return Ivy_MultiBalance_rec( pArgs, nArgs, Type ); + } + // the case of one common node + if ( nArgsNew == nArgs + 1 ) + { + assert( pEvaBest - pEvals == nArgs ); + k = 0; + for ( i = 0; i < nArgs; i++ ) + if ( i != (int)pEvaBest->Fan0 && i != (int)pEvaBest->Fan1 ) + pArgs[k++] = pArgs[i]; + pArgs[k++] = pArgs[nArgs]; + assert( k == nArgs - 1 ); + nArgs = k; + Ivy_MultiSort( pArgs, nArgs ); + return Ivy_MultiBalance_rec( pArgs, nArgs, Type ); + } + // the case when there is a node that covers everything + if ( (int)pEvaBest->Mask == ((1 << nArgs) - 1) ) + return Ivy_MultiBuild_rec( pEvals, pEvaBest - pEvals, pArgs, nArgsNew, Type ); + + // evaluate node pairs + nEvals = nArgsNew; + for ( i = 1; i < nArgsNew; i++ ) + for ( k = 0; k < i; k++ ) + { + pEva = pEvals + nEvals; + pEva->Mask = pEvals[k].Mask | pEvals[i].Mask; + pEva->Weight = NumBits[pEva->Mask]; + pEva->Cost = pEvals[k].Cost + pEvals[i].Cost + NumBits[pEvals[k].Mask & pEvals[i].Mask]; + pEva->Level = 1 + IVY_MAX(pEvals[k].Level, pEvals[i].Level); + pEva->Fan0 = k; + pEva->Fan1 = i; + // compare + if ( pEvaBest->Weight < pEva->Weight || + pEvaBest->Weight == pEva->Weight && pEvaBest->Cost > pEva->Cost || + pEvaBest->Weight == pEva->Weight && pEvaBest->Cost == pEva->Cost && pEvaBest->Level > pEva->Level ) + pEvaBest = pEva; + // save the argument + nEvals++; + } + assert( pEvaBest - pEvals >= nArgsNew ); + +// printf( "Used (%d, %d).\n", pEvaBest->Fan0, pEvaBest->Fan1 ); + + // get the best implementation + pTemp = Ivy_MultiBuild_rec( pEvals, pEvaBest - pEvals, pArgs, nArgsNew, Type ); + + // collect those not covered by EvaBest + k = 0; + for ( i = 0; i < nArgs; i++ ) + if ( (pEvaBest->Mask & (1 << i)) == 0 ) + pArgs[k++] = pArgs[i]; + pArgs[k++] = pTemp; + assert( k == nArgs - (int)pEvaBest->Weight + 1 ); + nArgs = k; + Ivy_MultiSort( pArgs, nArgs ); + return Ivy_MultiBalance_rec( pArgs, nArgs, Type ); +} + +/**Function************************************************************* + + Synopsis [Implements multi-input AND/EXOR operation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_MultiBuild_rec( Ivy_Eval_t * pEvals, int iNum, Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ) +{ + Ivy_Obj_t * pNode0, * pNode1; + if ( iNum < nArgs ) + return pArgs[iNum]; + pNode0 = Ivy_MultiBuild_rec( pEvals, pEvals[iNum].Fan0, pArgs, nArgs, Type ); + pNode1 = Ivy_MultiBuild_rec( pEvals, pEvals[iNum].Fan1, pArgs, nArgs, Type ); + return Ivy_Oper( pNode0, pNode1, Type ); +} + +/**Function************************************************************* + + Synopsis [Selection-sorts the nodes in the decreasing over of level.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_MultiSort( Ivy_Obj_t ** pArgs, int nArgs ) +{ + Ivy_Obj_t * pTemp; + int i, j, iBest; + + for ( i = 0; i < nArgs-1; i++ ) + { + iBest = i; + for ( j = i+1; j < nArgs; j++ ) + if ( Ivy_Regular(pArgs[j])->Level > Ivy_Regular(pArgs[iBest])->Level ) + iBest = j; + pTemp = pArgs[i]; + pArgs[i] = pArgs[iBest]; + pArgs[iBest] = pTemp; + } +} + +/**Function************************************************************* + + Synopsis [Inserts a new node in the order by levels.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_MultiPushUniqueOrderByLevel( Ivy_Obj_t ** pArray, int nArgs, Ivy_Obj_t * pNode ) +{ + Ivy_Obj_t * pNode1, * pNode2; + int i; + // try to find the node in the array + for ( i = 0; i < nArgs; i++ ) + if ( pArray[i] == pNode ) + return nArgs; + // put the node last + pArray[nArgs++] = pNode; + // find the place to put the new node + for ( i = nArgs-1; i > 0; i-- ) + { + pNode1 = pArray[i ]; + pNode2 = pArray[i-1]; + if ( Ivy_Regular(pNode1)->Level <= Ivy_Regular(pNode2)->Level ) + break; + pArray[i ] = pNode2; + pArray[i-1] = pNode1; + } + return nArgs; +} + +/**Function************************************************************* + + Synopsis [Balances the array recursively.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_MultiBalance_rec( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ) +{ + Ivy_Obj_t * pNodeNew; + // consider the case of one argument + assert( nArgs > 0 ); + if ( nArgs == 1 ) + return pArgs[0]; + // consider the case of two arguments + if ( nArgs == 2 ) + return Ivy_Oper( pArgs[0], pArgs[1], Type ); + // get the last two nodes + pNodeNew = Ivy_Oper( pArgs[nArgs-1], pArgs[nArgs-2], Type ); + // add the new node + nArgs = Ivy_MultiPushUniqueOrderByLevel( pArgs, nArgs - 2, pNodeNew ); + return Ivy_MultiBalance_rec( pArgs, nArgs, Type ); +} + +/**Function************************************************************* + + Synopsis [Implements multi-input AND/EXOR operation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_MultiEval( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ) +{ + Ivy_Obj_t * pTemp; + int i, k; + int nArgsOld = nArgs; + for ( i = 0; i < nArgs; i++ ) + printf( "%d[%d] ", i, Ivy_Regular(pArgs[i])->Level ); + for ( i = 1; i < nArgs; i++ ) + for ( k = 0; k < i; k++ ) + { + pTemp = Ivy_TableLookup(Ivy_ObjCreateGhost(pArgs[k], pArgs[i], Type, IVY_INIT_NONE)); + if ( pTemp != NULL ) + { + printf( "%d[%d]=(%d,%d) ", nArgs, Ivy_Regular(pTemp)->Level, k, i ); + pArgs[nArgs++] = pTemp; + } + } + printf( " ((%d/%d)) ", nArgsOld, nArgs-nArgsOld ); + return NULL; +} + + + +/**Function************************************************************* + + Synopsis [Old code.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_Multi1( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ) +{ + Ivy_Obj_t * pArgsRef[5], * pTemp; + int i, k, m, nArgsNew, Counter = 0; + + +//Ivy_MultiEval( pArgs, nArgs, Type ); printf( "\n" ); + + + assert( Type == IVY_AND || Type == IVY_EXOR ); + assert( nArgs > 0 ); + if ( nArgs == 1 ) + return pArgs[0]; + + // find the nodes with more than one fanout + nArgsNew = 0; + for ( i = 0; i < nArgs; i++ ) + if ( Ivy_ObjRefs( Ivy_Regular(pArgs[i]) ) > 0 ) + pArgsRef[nArgsNew++] = pArgs[i]; + + // go through pairs + if ( nArgsNew >= 2 ) + for ( i = 0; i < nArgsNew; i++ ) + for ( k = i + 1; k < nArgsNew; k++ ) + if ( pTemp = Ivy_TableLookup(Ivy_ObjCreateGhost(pArgsRef[i], pArgsRef[k], Type, IVY_INIT_NONE)) ) + Counter++; +// printf( "%d", Counter ); + + // go through pairs + if ( nArgsNew >= 2 ) + for ( i = 0; i < nArgsNew; i++ ) + for ( k = i + 1; k < nArgsNew; k++ ) + if ( pTemp = Ivy_TableLookup(Ivy_ObjCreateGhost(pArgsRef[i], pArgsRef[k], Type, IVY_INIT_NONE)) ) + { + nArgsNew = 0; + for ( m = 0; m < nArgs; m++ ) + if ( pArgs[m] != pArgsRef[i] && pArgs[m] != pArgsRef[k] ) + pArgs[nArgsNew++] = pArgs[m]; + pArgs[nArgsNew++] = pTemp; + assert( nArgsNew == nArgs - 1 ); + return Ivy_Multi1( pArgs, nArgsNew, Type ); + } + return Ivy_Multi_rec( pArgs, nArgs, Type ); +} + +/**Function************************************************************* + + Synopsis [Old code.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_Multi2( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ) +{ + assert( Type == IVY_AND || Type == IVY_EXOR ); + assert( nArgs > 0 ); + return Ivy_Multi_rec( pArgs, nArgs, Type ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ivy/ivyObj.c b/src/temp/ivy/ivyObj.c new file mode 100644 index 00000000..5d063525 --- /dev/null +++ b/src/temp/ivy/ivyObj.c @@ -0,0 +1,325 @@ +/**CFile**************************************************************** + + FileName [ivyObj.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [Adding/removing objects.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: ivyObj.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ivy.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Create the new node assuming it does not exist.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_ObjCreate( Ivy_Obj_t * pGhost ) +{ + Ivy_Man_t * p = Ivy_ObjMan(pGhost); + Ivy_Obj_t * pObj; + assert( !Ivy_IsComplement(pGhost) ); + assert( Ivy_ObjIsGhost(pGhost) ); + + assert( Ivy_TableLookup(pGhost) == NULL ); + + // realloc the node array + if ( p->ObjIdNext == p->nObjsAlloc ) + { + Ivy_ManGrow( p ); + pGhost = Ivy_ManGhost( p ); + } + // get memory for the new object + if ( Vec_IntSize(p->vFree) > 0 ) + pObj = p->pObjs + Vec_IntPop(p->vFree); + else + pObj = p->pObjs + p->ObjIdNext++; + assert( pObj->Id == pObj - p->pObjs ); + assert( Ivy_ObjIsNone(pObj) ); + // add basic info (fanins, compls, type, init) + Ivy_ObjOverwrite( pObj, pGhost ); + // increment references of the fanins + Ivy_ObjRefsInc( Ivy_ObjFanin0(pObj) ); + Ivy_ObjRefsInc( Ivy_ObjFanin1(pObj) ); + // add the node to the structural hash table + Ivy_TableInsert( pObj ); + // compute level + if ( Ivy_ObjIsNode(pObj) ) + pObj->Level = Ivy_ObjLevelNew(pObj); + else if ( Ivy_ObjIsLatch(pObj) ) + pObj->Level = 0; + else if ( Ivy_ObjIsOneFanin(pObj) ) + pObj->Level = Ivy_ObjFanin0(pObj)->Level; + else if ( !Ivy_ObjIsPi(pObj) ) + assert( 0 ); + // mark the fanins in a special way if the node is EXOR + if ( Ivy_ObjIsExor(pObj) ) + { + Ivy_ObjFanin0(pObj)->fExFan = 1; + Ivy_ObjFanin1(pObj)->fExFan = 1; + } + // add PIs/POs to the arrays + if ( Ivy_ObjIsPi(pObj) ) + Vec_IntPush( p->vPis, pObj->Id ); + else if ( Ivy_ObjIsPo(pObj) ) + Vec_IntPush( p->vPos, pObj->Id ); + // update node counters of the manager + p->nObjs[Ivy_ObjType(pObj)]++; + p->nCreated++; + return pObj; +} + +/**Function************************************************************* + + Synopsis [Create the new node assuming it does not exist.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_ObjCreateExt( Ivy_Man_t * p, Ivy_Type_t Type ) +{ + Ivy_Obj_t * pObj; + assert( Type == IVY_ANDM || Type == IVY_EXORM || Type == IVY_LUT ); + // realloc the node array + if ( p->ObjIdNext == p->nObjsAlloc ) + Ivy_ManGrow( p ); + // create the new node + pObj = p->pObjs + p->ObjIdNext; + assert( pObj->Id == p->ObjIdNext ); + p->ObjIdNext++; + pObj->Type = Type; + // update node counters of the manager + p->nObjs[Type]++; + p->nCreated++; + return pObj; +} + +/**Function************************************************************* + + Synopsis [Connect the object to the fanin.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ObjConnect( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanin ) +{ + assert( !Ivy_IsComplement(pObj) ); + assert( Ivy_ObjIsOneFanin(pObj) ); + assert( Ivy_ObjFaninId0(pObj) == 0 ); + // add the first fanin + pObj->fComp0 = Ivy_IsComplement(pFanin); + pObj->Fanin0 = Ivy_Regular(pFanin)->Id; + // increment references of the fanins + Ivy_ObjRefsInc( Ivy_ObjFanin0(pObj) ); + // add the node to the structural hash table + Ivy_TableInsert( pObj ); +} + +/**Function************************************************************* + + Synopsis [Deletes the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ObjDelete( Ivy_Obj_t * pObj, int fFreeTop ) +{ + Ivy_Man_t * p; + assert( !Ivy_IsComplement(pObj) ); + assert( Ivy_ObjRefs(pObj) == 0 ); + // remove connections + Ivy_ObjRefsDec(Ivy_ObjFanin0(pObj)); + Ivy_ObjRefsDec(Ivy_ObjFanin1(pObj)); + // remove the node from the structural hash table + Ivy_TableDelete( pObj ); + // update node counters of the manager + p = Ivy_ObjMan(pObj); + p->nObjs[pObj->Type]--; + p->nDeleted++; + // remove PIs/POs from the arrays + if ( Ivy_ObjIsPi(pObj) ) + Vec_IntRemove( p->vPis, pObj->Id ); + else if ( Ivy_ObjIsPo(pObj) ) + Vec_IntRemove( p->vPos, pObj->Id ); + // recorde the deleted node + if ( p->fRecording ) + Ivy_ManUndoRecord( p, pObj ); + // clean the node's memory + Ivy_ObjClean( pObj ); + // remember the entry + if ( fFreeTop ) + Vec_IntPush( p->vFree, pObj->Id ); +} + +/**Function************************************************************* + + Synopsis [Deletes the MFFC of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ObjDelete_rec( Ivy_Obj_t * pObj, int fFreeTop ) +{ + Ivy_Obj_t * pFanin0, * pFanin1; + assert( !Ivy_IsComplement(pObj) ); + assert( !Ivy_ObjIsPo(pObj) && !Ivy_ObjIsNone(pObj) ); + if ( Ivy_ObjIsConst1(pObj) || Ivy_ObjIsPi(pObj) ) + return; + pFanin0 = Ivy_ObjFanin0(pObj); + pFanin1 = Ivy_ObjFanin1(pObj); + Ivy_ObjDelete( pObj, fFreeTop ); + if ( !Ivy_ObjIsNone(pFanin0) && Ivy_ObjRefs(pFanin0) == 0 ) + Ivy_ObjDelete_rec( pFanin0, 1 ); + if ( !Ivy_ObjIsNone(pFanin1) && Ivy_ObjRefs(pFanin1) == 0 ) + Ivy_ObjDelete_rec( pFanin1, 1 ); +} + +/**Function************************************************************* + + Synopsis [Replaces one object by another.] + + Description [Both objects are currently in the manager. The new object + (pObjNew) should be used instead of the old object (pObjOld). If the + new object is complemented or used, the buffer is added.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ObjReplace( Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, int fDeleteOld, int fFreeTop ) +{ + int nRefsOld; + // the object to be replaced cannot be complemented + assert( !Ivy_IsComplement(pObjOld) ); + // the object to be replaced cannot be a terminal + assert( Ivy_ObjIsNone(pObjOld) || !Ivy_ObjIsTerm(pObjOld) ); + // the object to be used cannot be a PO or assert + assert( !Ivy_ObjIsPo(Ivy_Regular(pObjNew)) ); + // the object cannot be the same + assert( pObjOld != Ivy_Regular(pObjNew) ); + // if the new object is complemented or already used, add the buffer + if ( Ivy_IsComplement(pObjNew) || Ivy_ObjRefs(pObjNew) > 0 || Ivy_ObjIsPi(pObjNew) || Ivy_ObjIsConst1(pObjNew) ) + pObjNew = Ivy_ObjCreate( Ivy_ObjCreateGhost(pObjNew, Ivy_ObjConst1(pObjOld), IVY_BUF, IVY_INIT_NONE) ); + assert( !Ivy_IsComplement(pObjNew) ); + // remember the reference counter + nRefsOld = pObjOld->nRefs; + pObjOld->nRefs = 0; + // delete the old object + if ( fDeleteOld ) + Ivy_ObjDelete_rec( pObjOld, fFreeTop ); + // transfer the old object + assert( Ivy_ObjRefs(pObjNew) == 0 ); + Ivy_ObjOverwrite( pObjOld, pObjNew ); + pObjOld->nRefs = nRefsOld; + // update the hash table + Ivy_TableUpdate( pObjNew, pObjOld->Id ); + // create the object that was taken over by pObjOld + Ivy_ObjClean( pObjNew ); + // remember the entry + Vec_IntPush( Ivy_ObjMan(pObjOld)->vFree, pObjNew->Id ); +} + +/**Function************************************************************* + + Synopsis [Returns the first real fanins (not a buffer/inverter).] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_NodeRealFanin_rec( Ivy_Obj_t * pNode, int iFanin ) +{ + if ( iFanin == 0 ) + { + if ( Ivy_ObjIsBuf(Ivy_ObjFanin0(pNode)) ) + return Ivy_NotCond( Ivy_NodeRealFanin_rec(Ivy_ObjFanin0(pNode), 0), Ivy_ObjFaninC0(pNode) ); + else + return Ivy_ObjChild0(pNode); + } + else + { + if ( Ivy_ObjIsBuf(Ivy_ObjFanin1(pNode)) ) + return Ivy_NotCond( Ivy_NodeRealFanin_rec(Ivy_ObjFanin1(pNode), 0), Ivy_ObjFaninC1(pNode) ); + else + return Ivy_ObjChild1(pNode); + } +} + +/**Function************************************************************* + + Synopsis [Fixes buffer fanins.] + + Description [This situation happens because NodeReplace is a lazy + procedure, which does not propagate the change to the fanouts but + instead records the change in the form of a buf/inv node.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_NodeFixBufferFanins( Ivy_Obj_t * pNode ) +{ + Ivy_Obj_t * pFanReal0, * pFanReal1, * pResult; + assert( Ivy_ObjIsNode(pNode) ); + if ( !Ivy_ObjIsBuf(Ivy_ObjFanin0(pNode)) && !Ivy_ObjIsBuf(Ivy_ObjFanin1(pNode)) ) + return; + // get the real fanins + pFanReal0 = Ivy_NodeRealFanin_rec( pNode, 0 ); + pFanReal1 = Ivy_NodeRealFanin_rec( pNode, 1 ); + // get the new node + pResult = Ivy_Oper( pFanReal0, pFanReal1, Ivy_ObjType(pNode) ); + // perform the replacement + Ivy_ObjReplace( pNode, pResult, 1, 0 ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ivy/ivyOper.c b/src/temp/ivy/ivyOper.c new file mode 100644 index 00000000..a10ba343 --- /dev/null +++ b/src/temp/ivy/ivyOper.c @@ -0,0 +1,254 @@ +/**CFile**************************************************************** + + FileName [ivyOper.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [AIG operations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: ivyOper.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ivy.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +// procedure to detect an EXOR gate +static inline int Ivy_ObjIsExorType( Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Obj_t ** ppFan0, Ivy_Obj_t ** ppFan1 ) +{ + if ( !Ivy_IsComplement(p0) || !Ivy_IsComplement(p1) ) + return 0; + p0 = Ivy_Regular(p0); + p1 = Ivy_Regular(p1); + if ( !Ivy_ObjIsAnd(p0) || !Ivy_ObjIsAnd(p1) ) + return 0; + if ( Ivy_ObjFanin0(p0) != Ivy_ObjFanin0(p1) || Ivy_ObjFanin1(p0) != Ivy_ObjFanin1(p1) ) + return 0; + if ( Ivy_ObjFaninC0(p0) == Ivy_ObjFaninC0(p1) || Ivy_ObjFaninC1(p0) == Ivy_ObjFaninC1(p1) ) + return 0; + *ppFan0 = Ivy_ObjChild0(p0); + *ppFan1 = Ivy_ObjChild1(p0); + return 1; +} + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Perform one operation.] + + Description [The argument nodes can be complemented.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_Oper( Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Type_t Type ) +{ + if ( Type == IVY_AND ) + return Ivy_And( p0, p1 ); + if ( Type == IVY_EXOR ) + return Ivy_Exor( p0, p1 ); + assert( 0 ); + return NULL; +} + +/**Function************************************************************* + + Synopsis [Performs canonicization step.] + + Description [The argument nodes can be complemented.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_And( Ivy_Obj_t * p0, Ivy_Obj_t * p1 ) +{ + Ivy_Obj_t * pConst1 = Ivy_ObjConst1(Ivy_Regular(p0)); + Ivy_Obj_t * pFan0, * pFan1; + // check trivial cases + if ( p0 == p1 ) + return p0; + if ( p0 == Ivy_Not(p1) ) + return Ivy_Not(pConst1); + if ( Ivy_Regular(p0) == pConst1 ) + return p0 == pConst1 ? p1 : Ivy_Not(pConst1); + if ( Ivy_Regular(p1) == pConst1 ) + return p1 == pConst1 ? p0 : Ivy_Not(pConst1); + // check if it can be an EXOR gate + if ( Ivy_ObjIsExorType( p0, p1, &pFan0, &pFan1 ) ) + return Ivy_CanonExor( pFan0, pFan1 ); + return Ivy_CanonAnd( p0, p1 ); +} + +/**Function************************************************************* + + Synopsis [Performs canonicization step.] + + Description [The argument nodes can be complemented.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_Exor( Ivy_Obj_t * p0, Ivy_Obj_t * p1 ) +{ + Ivy_Obj_t * pConst1 = Ivy_ObjConst1(Ivy_Regular(p0)); + // check trivial cases + if ( p0 == p1 ) + return Ivy_Not(pConst1); + if ( p0 == Ivy_Not(p1) ) + return pConst1; + if ( Ivy_Regular(p0) == pConst1 ) + return Ivy_NotCond( p1, p0 == pConst1 ); + if ( Ivy_Regular(p1) == pConst1 ) + return Ivy_NotCond( p0, p1 == pConst1 ); + // check the table + return Ivy_CanonExor( p0, p1 ); +} + +/**Function************************************************************* + + Synopsis [Performs canonicization step.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_Latch( Ivy_Obj_t * pObj, Ivy_Init_t Init ) +{ + return Ivy_CanonLatch( pObj, Init ); +} + +/**Function************************************************************* + + Synopsis [Implements Boolean OR.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_Or( Ivy_Obj_t * p0, Ivy_Obj_t * p1 ) +{ + return Ivy_Not( Ivy_And( Ivy_Not(p0), Ivy_Not(p1) ) ); +} + +/**Function************************************************************* + + Synopsis [Implements ITE operation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_Mux( Ivy_Obj_t * pC, Ivy_Obj_t * p1, Ivy_Obj_t * p0 ) +{ + Ivy_Obj_t * pConst1 = Ivy_ObjConst1(Ivy_Regular(p0)); + Ivy_Obj_t * pTempA1, * pTempA2, * pTempB1, * pTempB2, * pTemp; + int Count0, Count1; + // consider trivial cases + if ( p0 == Ivy_Not(p1) ) + return Ivy_Exor( pC, p0 ); + // other cases can be added + // implement the first MUX (F = C * x1 + C' * x0) + pTempA1 = Ivy_TableLookup( Ivy_ObjCreateGhost(pC, p1, IVY_AND, IVY_INIT_NONE) ); + pTempA2 = Ivy_TableLookup( Ivy_ObjCreateGhost(Ivy_Not(pC), p0, IVY_AND, IVY_INIT_NONE) ); + if ( pTempA1 && pTempA2 ) + { + pTemp = Ivy_TableLookup( Ivy_ObjCreateGhost(Ivy_Not(pTempA1), Ivy_Not(pTempA2), IVY_AND, IVY_INIT_NONE) ); + if ( pTemp ) return Ivy_Not(pTemp); + } + Count0 = (pTempA1 != NULL) + (pTempA2 != NULL); + // implement the second MUX (F' = C * x1' + C' * x0') + pTempB1 = Ivy_TableLookup( Ivy_ObjCreateGhost(pC, Ivy_Not(p1), IVY_AND, IVY_INIT_NONE) ); + pTempB2 = Ivy_TableLookup( Ivy_ObjCreateGhost(Ivy_Not(pC), Ivy_Not(p0), IVY_AND, IVY_INIT_NONE) ); + if ( pTempB1 && pTempB2 ) + { + pTemp = Ivy_TableLookup( Ivy_ObjCreateGhost(Ivy_Not(pTempB1), Ivy_Not(pTempB2), IVY_AND, IVY_INIT_NONE) ); + if ( pTemp ) return pTemp; + } + Count1 = (pTempB1 != NULL) + (pTempB2 != NULL); + // compare and decide which one to implement + if ( Count0 >= Count1 ) + { + pTempA1 = pTempA1? pTempA1 : Ivy_And(pC, p1); + pTempA2 = pTempA2? pTempA2 : Ivy_And(Ivy_Not(pC), p0); + return Ivy_Or( pTempA1, pTempA2 ); + } + pTempB1 = pTempB1? pTempB1 : Ivy_And(pC, Ivy_Not(p1)); + pTempB2 = pTempB2? pTempB2 : Ivy_And(Ivy_Not(pC), Ivy_Not(p0)); + return Ivy_Not( Ivy_Or( pTempB1, pTempB2 ) ); + +// return Ivy_Or( Ivy_And(pC, p1), Ivy_And(Ivy_Not(pC), p0) ); +} + +/**Function************************************************************* + + Synopsis [Implements ITE operation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_Maj( Ivy_Obj_t * pA, Ivy_Obj_t * pB, Ivy_Obj_t * pC ) +{ + return Ivy_Or( Ivy_Or(Ivy_And(pA, pB), Ivy_And(pA, pC)), Ivy_And(pB, pC) ); +} + +/**Function************************************************************* + + Synopsis [Implements the miter.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_Miter( Vec_Ptr_t * vPairs ) +{ + int i; + assert( vPairs->nSize > 0 ); + assert( vPairs->nSize % 2 == 0 ); + // go through the cubes of the node's SOP + for ( i = 0; i < vPairs->nSize; i += 2 ) + vPairs->pArray[i/2] = Ivy_Not( Ivy_Exor( vPairs->pArray[i], vPairs->pArray[i+1] ) ); + vPairs->nSize = vPairs->nSize/2; + return Ivy_Not( Ivy_Multi_rec( (Ivy_Obj_t **)vPairs->pArray, vPairs->nSize, IVY_AND ) ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ivy/ivyRewrite.c b/src/temp/ivy/ivyRewrite.c new file mode 100644 index 00000000..031db9bc --- /dev/null +++ b/src/temp/ivy/ivyRewrite.c @@ -0,0 +1,365 @@ +/**CFile**************************************************************** + + FileName [ivyRewrite.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [AIG rewriting.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: ivyRewrite.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ivy.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static unsigned Ivy_ManSeqFindTruth( Ivy_Obj_t * pNode, Vec_Int_t * vFront ); +static void Ivy_ManSeqCollectCone( Ivy_Obj_t * pNode, Vec_Int_t * vCone ); +static int Ivy_ManSeqGetCost( Ivy_Man_t * p, Vec_Int_t * vCone ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Performs Boolean rewriting of sequential AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_ManSeqRewrite( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost ) +{ + Vec_Int_t * vNodes, * vFront, * vInside, * vTree; + Ivy_Obj_t * pNode, * pNodeNew, * pTemp; + int i, k, nCostOld, nCostInt, nCostInt2, nCostNew, RetValue, Entry, nRefsSaved, nInputs; + int clk, clkCut = 0, clkTru = 0, clkDsd = 0, clkUpd = 0, clkStart = clock(); + unsigned uTruth; + + nInputs = 4; + vTree = Vec_IntAlloc( 8 ); + vFront = Vec_IntAlloc( 8 ); + vInside = Vec_IntAlloc( 50 ); + vNodes = Ivy_ManDfs( p ); + Ivy_ManForEachNodeVec( p, vNodes, pNode, i ) + { + if ( Ivy_ObjIsBuf(pNode) ) + continue; + // fix the fanin buffer problem + Ivy_NodeFixBufferFanins( pNode ); + if ( Ivy_ObjIsBuf(pNode) ) + continue; + + // find one sequential cut rooted at this node +clk = clock(); + Ivy_ManSeqFindCut( pNode, vFront, vInside, nInputs ); +clkCut += clock() - clk; + // compute the truth table of the cut +clk = clock(); + uTruth = Ivy_ManSeqFindTruth( pNode, vFront ); +clkTru += clock() - clk; + // decompose the truth table +clk = clock(); + RetValue = Ivy_TruthDsd( uTruth, vTree ); +clkDsd += clock() - clk; + if ( !RetValue ) + continue; // DSD does not exist +// Ivy_TruthDsdPrint( stdout, vTree ); + +clk = clock(); + // remember the cost of the current network + nCostOld = Ivy_ManGetCost(p); + // increment references of the cut variables + Vec_IntForEachEntry( vFront, Entry, k ) + { + pTemp = Ivy_ManObj(p, Ivy_LeafId(Entry)); + Ivy_ObjRefsInc( pTemp ); + } + // dereference and record undo + nRefsSaved = pNode->nRefs; pNode->nRefs = 0; + Ivy_ManUndoStart( p ); + Ivy_ObjDelete_rec( pNode, 0 ); + Ivy_ManUndoStop( p ); + pNode->nRefs = nRefsSaved; + + // get the intermediate cost + nCostInt = Ivy_ManGetCost(p); + +// printf( "Removed by dereferencing = %d.\n", nCostOld - nCostInt ); + + // construct the new logic cone + pNodeNew = Ivy_ManDsdConstruct( p, vFront, vTree ); + // remember the cost + nCostNew = Ivy_ManGetCost(p); + +// printf( "Added by dereferencing = %d.\n", nCostInt - nCostNew ); +// nCostNew = nCostNew; + +/* + if ( Ivy_Regular(pNodeNew)->nRefs == 0 ) + Ivy_ObjDelete_rec( Ivy_Regular(pNodeNew), 1 ); + // get the intermediate cost + nCostInt2 = Ivy_ManGetCost(p); + assert( nCostInt == nCostInt2 ); + + Ivy_ManUndoPerform( p, pNode ); + pNode->nRefs = nRefsSaved; + + Vec_IntForEachEntry( vFront, Entry, k ) + { +// pTemp = Ivy_ManObj(p, Ivy_LeafId(Entry)); + pTemp = Ivy_ManObj(p, Entry); + Ivy_ObjRefsDec( pTemp ); + } +clkUpd += clock() - clk; + continue; +*/ + + // detect the case when they are exactly the same +// if ( pNodeNew == pNode ) +// continue; + + // compare the costs + if ( nCostOld > nCostNew || nCostOld == nCostNew && fUseZeroCost ) + { // accept the change +// printf( "NODES GAINED = %d\n", nCostOld - nCostNew ); + + Ivy_ObjReplace( pNode, pNodeNew, 0, 1 ); + pNode->nRefs = nRefsSaved; + } + else + { // reject change +// printf( "Rejected\n" ); + + if ( Ivy_Regular(pNodeNew)->nRefs == 0 ) + Ivy_ObjDelete_rec( Ivy_Regular(pNodeNew), 1 ); + + // get the intermediate cost + nCostInt2 = Ivy_ManGetCost(p); + assert( nCostInt == nCostInt2 ); + + // reconstruct the old node + Ivy_ManUndoPerform( p, pNode ); + pNode->nRefs = nRefsSaved; + } + // decrement references of the cut variables + Vec_IntForEachEntry( vFront, Entry, k ) + { +// pTemp = Ivy_ManObj(p, Ivy_LeafId(Entry)); + pTemp = Ivy_ManObj(p, Entry); + if ( Ivy_ObjIsNone(pTemp) ) + continue; + Ivy_ObjRefsDec( pTemp ); + if ( Ivy_ObjRefs(pTemp) == 0 ) + Ivy_ObjDelete_rec( pTemp, 1 ); + } + +clkUpd += clock() - clk; + } + +PRT( "Cut ", clkCut ); +PRT( "Truth ", clkTru ); +PRT( "DSD ", clkDsd ); +PRT( "Update ", clkUpd ); +PRT( "TOTAL ", clock() - clkStart ); + + Vec_IntFree( vTree ); + Vec_IntFree( vFront ); + Vec_IntFree( vInside ); + Vec_IntFree( vNodes ); + + if ( !Ivy_ManCheck(p) ) + { + printf( "Ivy_ManSeqRewrite(): The check has failed.\n" ); + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Computes the truth table of the sequential cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned Ivy_ManSeqFindTruth_rec( Ivy_Man_t * p, unsigned Node, Vec_Int_t * vFront ) +{ + static unsigned uMasks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 }; + unsigned uTruth0, uTruth1; + Ivy_Obj_t * pNode; + int nLatches, Number; + // consider the case of a constant + if ( Node == 0 ) + return ~((unsigned)0); + // try to find this node in the frontier + Number = Vec_IntFind( vFront, Node ); + if ( Number >= 0 ) + return uMasks[Number]; + // get the node + pNode = Ivy_ManObj( p, Ivy_LeafId(Node) ); + assert( !Ivy_ObjIsPi(pNode) && !Ivy_ObjIsConst1(pNode) ); + // get the number of latches + nLatches = Ivy_LeafLat(Node) + Ivy_ObjIsLatch(pNode); + // expand the first fanin + uTruth0 = Ivy_ManSeqFindTruth_rec( p, Ivy_LeafCreate(Ivy_ObjFaninId0(pNode), nLatches), vFront ); + if ( Ivy_ObjFaninC0(pNode) ) + uTruth0 = ~uTruth0; + // quit if this is the one fanin node + if ( Ivy_ObjIsLatch(pNode) || Ivy_ObjIsBuf(pNode) ) + return uTruth0; + assert( Ivy_ObjIsNode(pNode) ); + // expand the second fanin + uTruth1 = Ivy_ManSeqFindTruth_rec( p, Ivy_LeafCreate(Ivy_ObjFaninId1(pNode), nLatches), vFront ); + if ( Ivy_ObjFaninC1(pNode) ) + uTruth1 = ~uTruth1; + // return the truth table + return Ivy_ObjIsAnd(pNode)? uTruth0 & uTruth1 : uTruth0 ^ uTruth1; +} + +/**Function************************************************************* + + Synopsis [Computes the truth table of the sequential cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned Ivy_ManSeqFindTruth( Ivy_Obj_t * pNode, Vec_Int_t * vFront ) +{ + assert( Ivy_ObjIsNode(pNode) ); + return Ivy_ManSeqFindTruth_rec( Ivy_ObjMan(pNode), Ivy_LeafCreate(pNode->Id, 0), vFront ); +} + + +/**Function************************************************************* + + Synopsis [Recursively dereferences the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManSeqDeref_rec( Ivy_Obj_t * pNode, Vec_Int_t * vCone ) +{ + Ivy_Obj_t * pFan; + assert( !Ivy_IsComplement(pNode) ); + assert( !Ivy_ObjIsNone(pNode) ); + if ( Ivy_ObjIsPi(pNode) ) + return; + // deref the first fanin + pFan = Ivy_ObjFanin0(pNode); + Ivy_ObjRefsDec( pFan ); + if ( Ivy_ObjRefs( pFan ) == 0 ) + Ivy_ManSeqDeref_rec( pFan, vCone ); + // deref the second fanin + pFan = Ivy_ObjFanin1(pNode); + Ivy_ObjRefsDec( pFan ); + if ( Ivy_ObjRefs( pFan ) == 0 ) + Ivy_ManSeqDeref_rec( pFan, vCone ); + // save the node + Vec_IntPush( vCone, pNode->Id ); +} + +/**Function************************************************************* + + Synopsis [Recursively references the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManSeqRef_rec( Ivy_Obj_t * pNode ) +{ + Ivy_Obj_t * pFan; + assert( !Ivy_IsComplement(pNode) ); + assert( !Ivy_ObjIsNone(pNode) ); + if ( Ivy_ObjIsPi(pNode) ) + return; + // ref the first fanin + pFan = Ivy_ObjFanin0(pNode); + if ( Ivy_ObjRefs( pFan ) == 0 ) + Ivy_ManSeqRef_rec( pFan ); + Ivy_ObjRefsInc( pFan ); + // ref the second fanin + pFan = Ivy_ObjFanin1(pNode); + if ( Ivy_ObjRefs( pFan ) == 0 ) + Ivy_ManSeqRef_rec( pFan ); + Ivy_ObjRefsInc( pFan ); +} + +/**Function************************************************************* + + Synopsis [Collect MFFC of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManSeqCollectCone( Ivy_Obj_t * pNode, Vec_Int_t * vCone ) +{ + Vec_IntClear( vCone ); + Ivy_ManSeqDeref_rec( pNode, vCone ); + Ivy_ManSeqRef_rec( pNode ); +} + +/**Function************************************************************* + + Synopsis [Computes the cost of the logic cone.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_ManSeqGetCost( Ivy_Man_t * p, Vec_Int_t * vCone ) +{ + Ivy_Obj_t * pObj; + int i, Cost = 0; + Ivy_ManForEachNodeVec( p, vCone, pObj, i ) + { + if ( Ivy_ObjIsAnd(pObj) ) + Cost += 1; + else if ( Ivy_ObjIsExor(pObj) ) + Cost += 2; + } + return 0; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ivy/ivySeq.c b/src/temp/ivy/ivySeq.c new file mode 100644 index 00000000..d8fbdd9b --- /dev/null +++ b/src/temp/ivy/ivySeq.c @@ -0,0 +1,101 @@ +/**CFile**************************************************************** + + FileName [ivySeq.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: ivySeq.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ivy.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Converts a combinational AIG manager into a sequential one.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManMakeSeq( Ivy_Man_t * p, int nLatches ) +{ + Vec_Int_t * vNodes; + Ivy_Obj_t * pObj, * pObjNew, * pFan0, * pFan1; + int i, fChanges; + assert( nLatches < Ivy_ManPiNum(p) && nLatches < Ivy_ManPoNum(p) ); + // change POs into buffers + assert( Ivy_ManPoNum(p) == Vec_IntSize(p->vPos) ); + for ( i = Ivy_ManPoNum(p) - nLatches; i < Vec_IntSize(p->vPos); i++ ) + { + pObj = Ivy_ManPo(p, i); + pObj->Type = IVY_BUF; + } + // change PIs into latches and connect them to the corresponding POs + assert( Ivy_ManPiNum(p) == Vec_IntSize(p->vPis) ); + for ( i = Ivy_ManPiNum(p) - nLatches; i < Vec_IntSize(p->vPis); i++ ) + { + pObj = Ivy_ManPi(p, i); + pObj->Type = IVY_LATCH; + Ivy_ObjConnect( pObj, Ivy_ManPo(p, Ivy_ManPoNum(p) - Ivy_ManPiNum(p)) ); + } + // shrink the array + Vec_IntShrink( p->vPis, Ivy_ManPiNum(p) - nLatches ); + Vec_IntShrink( p->vPos, Ivy_ManPoNum(p) - nLatches ); + // update the counters of different objects + p->nObjs[IVY_PI] -= nLatches; + p->nObjs[IVY_PO] -= nLatches; + p->nObjs[IVY_BUF] += nLatches; + p->nObjs[IVY_LATCH] += nLatches; + // perform structural hashing while there are changes + fChanges = 1; + while ( fChanges ) + { + fChanges = 0; + vNodes = Ivy_ManDfs( p ); + Ivy_ManForEachNodeVec( p, vNodes, pObj, i ) + { + if ( Ivy_ObjIsBuf(pObj) ) + continue; + pFan0 = Ivy_NodeRealFanin_rec( pObj, 0 ); + pFan1 = Ivy_NodeRealFanin_rec( pObj, 1 ); + if ( Ivy_ObjIsAnd(pObj) ) + pObjNew = Ivy_And(pFan0, pFan1); + else if ( Ivy_ObjIsExor(pObj) ) + pObjNew = Ivy_Exor(pFan0, pFan1); + else assert( 0 ); + if ( pObjNew == pObj ) + continue; + Ivy_ObjReplace( pObj, pObjNew, 1, 1 ); + fChanges = 1; + } + Vec_IntFree( vNodes ); + } +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ivy/ivyTable.c b/src/temp/ivy/ivyTable.c new file mode 100644 index 00000000..815caa29 --- /dev/null +++ b/src/temp/ivy/ivyTable.c @@ -0,0 +1,237 @@ +/**CFile**************************************************************** + + FileName [ivyTable.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [Structural hashing table.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: ivyTable.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ivy.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +// hashing the node +static unsigned Ivy_Hash( Ivy_Obj_t * pObj, int TableSize ) +{ + unsigned Key = Ivy_ObjIsExor(pObj) * 1699; + Key ^= Ivy_ObjFaninId0(pObj) * 7937; + Key ^= Ivy_ObjFaninId1(pObj) * 2971; + Key ^= Ivy_ObjFaninC0(pObj) * 911; + Key ^= Ivy_ObjFaninC1(pObj) * 353; + Key ^= Ivy_ObjInit(pObj) * 911; + return Key % TableSize; +} + +// returns the place where this node is stored (or should be stored) +static int * Ivy_TableFind( Ivy_Obj_t * pObj ) +{ + Ivy_Man_t * p; + int i; + assert( Ivy_ObjIsHash(pObj) ); + p = Ivy_ObjMan(pObj); + for ( i = Ivy_Hash(pObj, p->nTableSize); p->pTable[i]; i = (i+1) % p->nTableSize ) + if ( p->pTable[i] == pObj->Id ) + break; + return p->pTable + i; +} + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Checks if node with the given attributes is in the hash table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_TableLookup( Ivy_Obj_t * pObj ) +{ + Ivy_Man_t * p; + Ivy_Obj_t * pEntry; + int i; + assert( !Ivy_IsComplement(pObj) ); + if ( !Ivy_ObjIsHash(pObj) ) + return NULL; + assert( Ivy_ObjIsLatch(pObj) || Ivy_ObjFaninId0(pObj) > 0 ); + assert( Ivy_ObjFaninId0(pObj) == 0 || Ivy_ObjFaninId0(pObj) > Ivy_ObjFaninId1(pObj) ); + p = Ivy_ObjMan(pObj); + for ( i = Ivy_Hash(pObj, p->nTableSize); p->pTable[i]; i = (i+1) % p->nTableSize ) + { + pEntry = Ivy_ObjObj( pObj, p->pTable[i] ); + if ( Ivy_ObjFaninId0(pEntry) == Ivy_ObjFaninId0(pObj) && + Ivy_ObjFaninId1(pEntry) == Ivy_ObjFaninId1(pObj) && + Ivy_ObjFaninC0(pEntry) == Ivy_ObjFaninC0(pObj) && + Ivy_ObjFaninC1(pEntry) == Ivy_ObjFaninC1(pObj) && + Ivy_ObjInit(pEntry) == Ivy_ObjInit(pObj) && + Ivy_ObjType(pEntry) == Ivy_ObjType(pObj) ) + return Ivy_ObjObj( pObj, p->pTable[i] ); + } + return NULL; +} + +/**Function************************************************************* + + Synopsis [Adds the node to the hash table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_TableInsert( Ivy_Obj_t * pObj ) +{ + int * pPlace; + assert( !Ivy_IsComplement(pObj) ); + if ( !Ivy_ObjIsHash(pObj) ) + return; + pPlace = Ivy_TableFind( pObj ); + assert( *pPlace == 0 ); + *pPlace = pObj->Id; +} + +/**Function************************************************************* + + Synopsis [Deletes the node from the hash table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_TableDelete( Ivy_Obj_t * pObj ) +{ + Ivy_Man_t * p; + Ivy_Obj_t * pEntry; + int i, * pPlace; + assert( !Ivy_IsComplement(pObj) ); + if ( !Ivy_ObjIsHash(pObj) ) + return; + pPlace = Ivy_TableFind( pObj ); + assert( *pPlace == pObj->Id ); // node should be in the table + *pPlace = 0; + // rehash the adjacent entries + p = Ivy_ObjMan(pObj); + i = pPlace - p->pTable; + for ( i = (i+1) % p->nTableSize; p->pTable[i]; i = (i+1) % p->nTableSize ) + { + pEntry = Ivy_ObjObj( pObj, p->pTable[i] ); + p->pTable[i] = 0; + Ivy_TableInsert( pEntry ); + } +} + +/**Function************************************************************* + + Synopsis [Updates the table to point to the new node.] + + Description [If the old node (pObj) is in the table, updates the table + to point to an object with different ID (ObjIdNew). The table should + not contain an object with ObjIdNew (this is currently not checked).] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_TableUpdate( Ivy_Obj_t * pObj, int ObjIdNew ) +{ + int * pPlace; + assert( !Ivy_IsComplement(pObj) ); + if ( !Ivy_ObjIsHash(pObj) ) + return; + pPlace = Ivy_TableFind( pObj ); + assert( *pPlace == pObj->Id ); // node should be in the table + *pPlace = ObjIdNew; +} + +/**Function************************************************************* + + Synopsis [Count the number of nodes in the table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_TableCountEntries( Ivy_Man_t * p ) +{ + int i, Counter = 0; + for ( i = 0; i < p->nTableSize; i++ ) + Counter += (p->pTable[i] != 0); + return Counter; +} + +/**Function************************************************************* + + Synopsis [Resizes the table.] + + Description [Typically this procedure should not be called.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_TableResize( Ivy_Man_t * p ) +{ + int * pTableOld, * pPlace; + int nTableSizeOld, Counter, e, clk; + assert( 0 ); +clk = clock(); + // save the old table + pTableOld = p->pTable; + nTableSizeOld = p->nTableSize; + // get the new table + p->nTableSize = p->nObjsAlloc*5/2+13; + p->pTable = ALLOC( int, p->nTableSize ); + memset( p->pTable, 0, sizeof(int) * p->nTableSize ); + // rehash the entries from the old table + Counter = 0; + for ( e = 0; e < nTableSizeOld; e++ ) + { + if ( pTableOld[e] == 0 ) + continue; + Counter++; + // get the place where this entry goes in the table table + pPlace = Ivy_TableFind( Ivy_ManObj(p, pTableOld[e]) ); + assert( *pPlace == 0 ); // should not be in the table + *pPlace = pTableOld[e]; + } + assert( Counter == Ivy_ManHashObjNum(p) ); +// printf( "Increasing the structural table size from %6d to %6d. ", p->nTableSize, nTableSizeNew ); +// PRT( "Time", clock() - clk ); + // replace the table and the parameters + free( p->pTable ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ivy/ivyUndo.c b/src/temp/ivy/ivyUndo.c new file mode 100644 index 00000000..6612bf42 --- /dev/null +++ b/src/temp/ivy/ivyUndo.c @@ -0,0 +1,165 @@ +/**CFile**************************************************************** + + FileName [ivyUndo.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [Recording the results of recent deletion of logic cone.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: ivyUndo.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ivy.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManUndoStart( Ivy_Man_t * p ) +{ + p->fRecording = 1; + p->nUndos = 0; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManUndoStop( Ivy_Man_t * p ) +{ + p->fRecording = 0; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManUndoRecord( Ivy_Man_t * p, Ivy_Obj_t * pObj ) +{ + Ivy_Obj_t * pObjUndo; + if ( p->nUndos >= p->nUndosAlloc ) + { + printf( "Ivy_ManUndoRecord(): Not enough memory for undo.\n" ); + return; + } + pObjUndo = p->pUndos + p->nUndos++; + // required data for Ivy_ObjCreateGhost() + pObjUndo->Type = pObj->Type; + pObjUndo->Init = pObj->Init; + pObjUndo->Fanin0 = pObj->Fanin0; + pObjUndo->Fanin1 = pObj->Fanin1; + pObjUndo->fComp0 = pObj->fComp0; + pObjUndo->fComp1 = pObj->fComp1; + // additional data + pObjUndo->Id = pObj->Id; + pObjUndo->nRefs = pObj->nRefs; + pObjUndo->Level = pObj->Level; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Vec_IntPutLast( Vec_Int_t * vFree, int Last ) +{ + int Place, i; + // find the entry + Place = Vec_IntFind( vFree, Last ); + if ( Place == -1 ) + return 0; + // shift entries by one + assert( vFree->pArray[Place] == Last ); + for ( i = Place; i < Vec_IntSize(vFree) - 1; i++ ) + vFree->pArray[i] = vFree->pArray[i+1]; + // put the entry in the end + vFree->pArray[i] = Last; + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManUndoPerform( Ivy_Man_t * p, Ivy_Obj_t * pRoot ) +{ + Ivy_Obj_t * pObjUndo, * pObjNew; + int i; + assert( p->nUndos > 0 ); + assert( p->fRecording == 0 ); + for ( i = p->nUndos - 1; i >= 0; i-- ) + { + // get the undo object + pObjUndo = p->pUndos + i; + // if this is the last object + if ( i == 0 ) + Vec_IntPush( p->vFree, pRoot->Id ); + else + Vec_IntPutLast( p->vFree, pObjUndo->Id ); + // create the new object + pObjNew = Ivy_ObjCreate( Ivy_ObjCreateGhost2( p, pObjUndo) ); + pObjNew->nRefs = pObjUndo->nRefs; + pObjNew->Level = pObjUndo->Level; + // make sure the object is created in the same place as before + assert( pObjNew->Id == pObjUndo->Id ); + } + p->nUndos = 0; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ivy/ivyUtil.c b/src/temp/ivy/ivyUtil.c new file mode 100644 index 00000000..590affd7 --- /dev/null +++ b/src/temp/ivy/ivyUtil.c @@ -0,0 +1,369 @@ +/**CFile**************************************************************** + + FileName [ivyUtil.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [Various procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: ivyUtil.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ivy.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Increments the current traversal ID of the network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManIncrementTravId( Ivy_Man_t * p ) +{ + if ( p->nTravIds >= (1<<30)-1 - 1000 ) + Ivy_ManCleanTravId( p ); + p->nTravIds++; +} + +/**Function************************************************************* + + Synopsis [Sets the DFS ordering of the nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManCleanTravId( Ivy_Man_t * p ) +{ + Ivy_Obj_t * pObj; + int i; + p->nTravIds = 1; + Ivy_ManForEachObj( p, pObj, i ) + pObj->TravId = 0; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the node is the root of MUX or EXOR/NEXOR.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_ObjIsMuxType( Ivy_Obj_t * pNode ) +{ + Ivy_Obj_t * pNode0, * pNode1; + // check that the node is regular + assert( !Ivy_IsComplement(pNode) ); + // if the node is not AND, this is not MUX + if ( !Ivy_ObjIsAnd(pNode) ) + return 0; + // if the children are not complemented, this is not MUX + if ( !Ivy_ObjFaninC0(pNode) || !Ivy_ObjFaninC1(pNode) ) + return 0; + // get children + pNode0 = Ivy_ObjFanin0(pNode); + pNode1 = Ivy_ObjFanin1(pNode); + // if the children are not ANDs, this is not MUX + if ( !Ivy_ObjIsAnd(pNode0) || !Ivy_ObjIsAnd(pNode1) ) + return 0; + // otherwise the node is MUX iff it has a pair of equal grandchildren + return (Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC0(pNode1))) || + (Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC1(pNode1))) || + (Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC0(pNode1))) || + (Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC1(pNode1))); +} + +/**Function************************************************************* + + Synopsis [Recognizes what nodes are control and data inputs of a MUX.] + + Description [If the node is a MUX, returns the control variable C. + Assigns nodes T and E to be the then and else variables of the MUX. + Node C is never complemented. Nodes T and E can be complemented. + This function also recognizes EXOR/NEXOR gates as MUXes.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_ObjRecognizeMux( Ivy_Obj_t * pNode, Ivy_Obj_t ** ppNodeT, Ivy_Obj_t ** ppNodeE ) +{ + Ivy_Obj_t * pNode0, * pNode1; + assert( !Ivy_IsComplement(pNode) ); + assert( Ivy_ObjIsMuxType(pNode) ); + // get children + pNode0 = Ivy_ObjFanin0(pNode); + pNode1 = Ivy_ObjFanin1(pNode); + // find the control variable +// if ( pNode1->p1 == Fraig_Not(pNode2->p1) ) + if ( Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC0(pNode1)) ) + { +// if ( Fraig_IsComplement(pNode1->p1) ) + if ( Ivy_ObjFaninC0(pNode0) ) + { // pNode2->p1 is positive phase of C + *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2); + *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2); + return Ivy_ObjChild0(pNode1);//pNode2->p1; + } + else + { // pNode1->p1 is positive phase of C + *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2); + *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2); + return Ivy_ObjChild0(pNode0);//pNode1->p1; + } + } +// else if ( pNode1->p1 == Fraig_Not(pNode2->p2) ) + else if ( Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC1(pNode1)) ) + { +// if ( Fraig_IsComplement(pNode1->p1) ) + if ( Ivy_ObjFaninC0(pNode0) ) + { // pNode2->p2 is positive phase of C + *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1); + *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2); + return Ivy_ObjChild1(pNode1);//pNode2->p2; + } + else + { // pNode1->p1 is positive phase of C + *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2); + *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1); + return Ivy_ObjChild0(pNode0);//pNode1->p1; + } + } +// else if ( pNode1->p2 == Fraig_Not(pNode2->p1) ) + else if ( Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC0(pNode1)) ) + { +// if ( Fraig_IsComplement(pNode1->p2) ) + if ( Ivy_ObjFaninC1(pNode0) ) + { // pNode2->p1 is positive phase of C + *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2); + *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1); + return Ivy_ObjChild0(pNode1);//pNode2->p1; + } + else + { // pNode1->p2 is positive phase of C + *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1); + *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2); + return Ivy_ObjChild1(pNode0);//pNode1->p2; + } + } +// else if ( pNode1->p2 == Fraig_Not(pNode2->p2) ) + else if ( Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC1(pNode1)) ) + { +// if ( Fraig_IsComplement(pNode1->p2) ) + if ( Ivy_ObjFaninC1(pNode0) ) + { // pNode2->p2 is positive phase of C + *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1); + *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1); + return Ivy_ObjChild1(pNode1);//pNode2->p2; + } + else + { // pNode1->p2 is positive phase of C + *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1); + *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1); + return Ivy_ObjChild1(pNode0);//pNode1->p2; + } + } + assert( 0 ); // this is not MUX + return NULL; +} + +/**Function************************************************************* + + Synopsis [Computes truth table of the cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManCollectCut_rec( Ivy_Obj_t * pNode, Vec_Int_t * vNodes ) +{ + if ( pNode->fMarkA ) + return; + pNode->fMarkA = 1; + assert( Ivy_ObjIsAnd(pNode) || Ivy_ObjIsExor(pNode) ); + Ivy_ManCollectCut_rec( Ivy_ObjFanin0(pNode), vNodes ); + Ivy_ManCollectCut_rec( Ivy_ObjFanin1(pNode), vNodes ); + Vec_IntPush( vNodes, pNode->Id ); +} + +/**Function************************************************************* + + Synopsis [Computes truth table of the cut.] + + Description [Does not modify the array of leaves. Uses array vTruth to store + temporary truth tables. The returned pointer should be used immediately.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManCollectCut( Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes ) +{ + int i, Leaf; + // collect and mark the leaves + Vec_IntClear( vNodes ); + Vec_IntForEachEntry( vLeaves, Leaf, i ) + { + Vec_IntPush( vNodes, Leaf ); + Ivy_ObjObj(pRoot, Leaf)->fMarkA = 1; + } + // collect and mark the nodes + Ivy_ManCollectCut_rec( pRoot, vNodes ); + // clean the nodes + Vec_IntForEachEntry( vNodes, Leaf, i ) + Ivy_ObjObj(pRoot, Leaf)->fMarkA = 0; +} + +/**Function************************************************************* + + Synopsis [Returns the pointer to the truth table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned * Ivy_ObjGetTruthStore( int ObjNum, Vec_Int_t * vTruth ) +{ + return ((unsigned *)Vec_IntArray(vTruth)) + 8 * ObjNum; +} + +/**Function************************************************************* + + Synopsis [Computes truth table of the cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManCutTruthOne( Ivy_Obj_t * pNode, Vec_Int_t * vTruth, int nWords ) +{ + unsigned * pTruth, * pTruth0, * pTruth1; + int i; + pTruth = Ivy_ObjGetTruthStore( pNode->TravId, vTruth ); + pTruth0 = Ivy_ObjGetTruthStore( Ivy_ObjFanin0(pNode)->TravId, vTruth ); + pTruth1 = Ivy_ObjGetTruthStore( Ivy_ObjFanin1(pNode)->TravId, vTruth ); + if ( Ivy_ObjIsExor(pNode) ) + for ( i = 0; i < nWords; i++ ) + pTruth[i] = pTruth0[i] ^ pTruth1[i]; + else if ( !Ivy_ObjFaninC0(pNode) && !Ivy_ObjFaninC1(pNode) ) + for ( i = 0; i < nWords; i++ ) + pTruth[i] = pTruth0[i] & pTruth1[i]; + else if ( !Ivy_ObjFaninC0(pNode) && Ivy_ObjFaninC1(pNode) ) + for ( i = 0; i < nWords; i++ ) + pTruth[i] = pTruth0[i] & ~pTruth1[i]; + else if ( Ivy_ObjFaninC0(pNode) && !Ivy_ObjFaninC1(pNode) ) + for ( i = 0; i < nWords; i++ ) + pTruth[i] = ~pTruth0[i] & pTruth1[i]; + else // if ( Ivy_ObjFaninC0(pNode) && Ivy_ObjFaninC1(pNode) ) + for ( i = 0; i < nWords; i++ ) + pTruth[i] = ~pTruth0[i] & ~pTruth1[i]; +} + +/**Function************************************************************* + + Synopsis [Computes truth table of the cut.] + + Description [Does not modify the array of leaves. Uses array vTruth to store + temporary truth tables. The returned pointer should be used immediately.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned * Ivy_ManCutTruth( Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes, Vec_Int_t * vTruth ) +{ + static unsigned uTruths[8][8] = { // elementary truth tables + { 0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA }, + { 0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC }, + { 0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0 }, + { 0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00 }, + { 0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000 }, + { 0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF }, + { 0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF }, + { 0x00000000,0x00000000,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF } + }; + int i, Leaf; + // collect the cut + Ivy_ManCollectCut( pRoot, vLeaves, vNodes ); + // set the node numbers + Vec_IntForEachEntry( vNodes, Leaf, i ) + Ivy_ObjObj(pRoot, Leaf)->TravId = i; + // alloc enough memory + Vec_IntClear( vTruth ); + Vec_IntGrow( vTruth, 8 * Vec_IntSize(vNodes) ); + // set the elementary truth tables + Vec_IntForEachEntry( vLeaves, Leaf, i ) + memcpy( Ivy_ObjGetTruthStore(i, vTruth), uTruths[i], 8 * sizeof(unsigned) ); + // compute truths for other nodes + Vec_IntForEachEntryStart( vNodes, Leaf, i, Vec_IntSize(vLeaves) ) + Ivy_ManCutTruthOne( Ivy_ObjObj(pRoot, Leaf), vTruth, 8 ); + return Ivy_ObjGetTruthStore( pRoot->TravId, vTruth ); +} + +/**Function************************************************************* + + Synopsis [Collect the latches.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Ivy_ManLatches( Ivy_Man_t * p ) +{ + Vec_Int_t * vLatches; + Ivy_Obj_t * pObj; + int i; + vLatches = Vec_IntAlloc( Ivy_ManLatchNum(p) ); + Ivy_ManForEachLatch( p, pObj, i ) + Vec_IntPush( vLatches, pObj->Id ); + return vLatches; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ivy/ivy_.c b/src/temp/ivy/ivy_.c new file mode 100644 index 00000000..65689689 --- /dev/null +++ b/src/temp/ivy/ivy_.c @@ -0,0 +1,48 @@ +/**CFile**************************************************************** + + FileName [ivy_.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: ivy_.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ivy.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ivy/module.make b/src/temp/ivy/module.make new file mode 100644 index 00000000..d59a3fa3 --- /dev/null +++ b/src/temp/ivy/module.make @@ -0,0 +1,14 @@ +SRC += src/temp/ivy/ivyBalance.c \ + src/temp/ivy/ivyCanon.c \ + src/temp/ivy/ivyCheck.c \ + src/temp/ivy/ivyCut.c \ + src/temp/ivy/ivyDfs.c \ + src/temp/ivy/ivyDsd.c \ + src/temp/ivy/ivyMan.c \ + src/temp/ivy/ivyObj.c \ + src/temp/ivy/ivyOper.c \ + src/temp/ivy/ivyRewrite.c \ + src/temp/ivy/ivySeq.c \ + src/temp/ivy/ivyTable.c \ + src/temp/ivy/ivyUndo.c \ + src/temp/ivy/ivyUtil.c |