From 4812c90424dfc40d26725244723887a2d16ddfd9 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 1 Oct 2007 08:01:00 -0700 Subject: Version abc71001 --- src/aig/hop/cudd2.c | 355 +++++++++++++++++++++++++++++ src/aig/hop/cudd2.h | 82 +++++++ src/aig/hop/hop.h | 347 ++++++++++++++++++++++++++++ src/aig/hop/hopBalance.c | 391 ++++++++++++++++++++++++++++++++ src/aig/hop/hopCheck.c | 110 +++++++++ src/aig/hop/hopDfs.c | 399 +++++++++++++++++++++++++++++++++ src/aig/hop/hopMan.c | 164 ++++++++++++++ src/aig/hop/hopMem.c | 115 ++++++++++ src/aig/hop/hopObj.c | 271 ++++++++++++++++++++++ src/aig/hop/hopOper.c | 373 ++++++++++++++++++++++++++++++ src/aig/hop/hopTable.c | 262 ++++++++++++++++++++++ src/aig/hop/hopUtil.c | 572 +++++++++++++++++++++++++++++++++++++++++++++++ src/aig/hop/hop_.c | 48 ++++ src/aig/hop/module.make | 9 + 14 files changed, 3498 insertions(+) create mode 100644 src/aig/hop/cudd2.c create mode 100644 src/aig/hop/cudd2.h create mode 100644 src/aig/hop/hop.h create mode 100644 src/aig/hop/hopBalance.c create mode 100644 src/aig/hop/hopCheck.c create mode 100644 src/aig/hop/hopDfs.c create mode 100644 src/aig/hop/hopMan.c create mode 100644 src/aig/hop/hopMem.c create mode 100644 src/aig/hop/hopObj.c create mode 100644 src/aig/hop/hopOper.c create mode 100644 src/aig/hop/hopTable.c create mode 100644 src/aig/hop/hopUtil.c create mode 100644 src/aig/hop/hop_.c create mode 100644 src/aig/hop/module.make (limited to 'src/aig/hop') diff --git a/src/aig/hop/cudd2.c b/src/aig/hop/cudd2.c new file mode 100644 index 00000000..28d13ce0 --- /dev/null +++ b/src/aig/hop/cudd2.c @@ -0,0 +1,355 @@ +/**CFile**************************************************************** + + FileName [cudd2.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Minimalistic And-Inverter Graph package.] + + Synopsis [Recording AIGs for the BDD operations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - October 3, 2006.] + + Revision [$Id: cudd2.c,v 1.00 2006/10/03 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "hop.h" +#include "st.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Aig_CuddMan_t_ Aig_CuddMan_t; +struct Aig_CuddMan_t_ +{ + Aig_Man_t * pAig; // internal AIG package + st_table * pTable; // hash table mapping BDD nodes into AIG nodes +}; + +// static Cudd AIG manager used in this experiment +static Aig_CuddMan_t * s_pCuddMan = NULL; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Start AIG recording.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cudd2_Init( unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int cacheSize, unsigned long maxMemory, void * pCudd ) +{ + int v; + // start the BDD-to-AIG manager when the first BDD manager is allocated + if ( s_pCuddMan != NULL ) + return; + s_pCuddMan = ALLOC( Aig_CuddMan_t, 1 ); + s_pCuddMan->pAig = Aig_ManStart(); + s_pCuddMan->pTable = st_init_table( st_ptrcmp, st_ptrhash ); + for ( v = 0; v < (int)numVars; v++ ) + Aig_ObjCreatePi( s_pCuddMan->pAig ); +} + +/**Function************************************************************* + + Synopsis [Stops AIG recording.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cudd2_Quit( void * pCudd ) +{ + assert( s_pCuddMan != NULL ); + Aig_ManDumpBlif( s_pCuddMan->pAig, "aig_temp.blif" ); + Aig_ManStop( s_pCuddMan->pAig ); + st_free_table( s_pCuddMan->pTable ); + free( s_pCuddMan ); + s_pCuddMan = NULL; +} + +/**Function************************************************************* + + Synopsis [Fetches AIG node corresponding to the BDD node from the hash table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static Aig_Obj_t * Cudd2_GetArg( void * pArg ) +{ + Aig_Obj_t * pNode; + assert( s_pCuddMan != NULL ); + if ( !st_lookup( s_pCuddMan->pTable, (char *)Aig_Regular(pArg), (char **)&pNode ) ) + { + printf( "Cudd2_GetArg(): An argument BDD is not in the hash table.\n" ); + return NULL; + } + return Aig_NotCond( pNode, Aig_IsComplement(pArg) ); +} + +/**Function************************************************************* + + Synopsis [Inserts the AIG node corresponding to the BDD node into the hash table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static void Cudd2_SetArg( Aig_Obj_t * pNode, void * pResult ) +{ + assert( s_pCuddMan != NULL ); + if ( st_is_member( s_pCuddMan->pTable, (char *)Aig_Regular(pResult) ) ) + return; + pNode = Aig_NotCond( pNode, Aig_IsComplement(pResult) ); + st_insert( s_pCuddMan->pTable, (char *)Aig_Regular(pResult), (char *)pNode ); +} + +/**Function************************************************************* + + Synopsis [Registers constant 1 node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cudd2_bddOne( void * pCudd, void * pResult ) +{ + Cudd2_SetArg( Aig_ManConst1(s_pCuddMan->pAig), pResult ); +} + +/**Function************************************************************* + + Synopsis [Adds elementary variable.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cudd2_bddIthVar( void * pCudd, int iVar, void * pResult ) +{ + int v; + assert( s_pCuddMan != NULL ); + for ( v = Aig_ManPiNum(s_pCuddMan->pAig); v <= iVar; v++ ) + Aig_ObjCreatePi( s_pCuddMan->pAig ); + Cudd2_SetArg( Aig_ManPi(s_pCuddMan->pAig, iVar), pResult ); +} + +/**Function************************************************************* + + Synopsis [Performs BDD operation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cudd2_bddAnd( void * pCudd, void * pArg0, void * pArg1, void * pResult ) +{ + Aig_Obj_t * pNode0, * pNode1, * pNode; + pNode0 = Cudd2_GetArg( pArg0 ); + pNode1 = Cudd2_GetArg( pArg1 ); + pNode = Aig_And( s_pCuddMan->pAig, pNode0, pNode1 ); + Cudd2_SetArg( pNode, pResult ); +} + +/**Function************************************************************* + + Synopsis [Performs BDD operation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cudd2_bddOr( void * pCudd, void * pArg0, void * pArg1, void * pResult ) +{ + Cudd2_bddAnd( pCudd, Aig_Not(pArg0), Aig_Not(pArg1), Aig_Not(pResult) ); +} + +/**Function************************************************************* + + Synopsis [Performs BDD operation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cudd2_bddNand( void * pCudd, void * pArg0, void * pArg1, void * pResult ) +{ + Cudd2_bddAnd( pCudd, pArg0, pArg1, Aig_Not(pResult) ); +} + +/**Function************************************************************* + + Synopsis [Performs BDD operation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cudd2_bddNor( void * pCudd, void * pArg0, void * pArg1, void * pResult ) +{ + Cudd2_bddAnd( pCudd, Aig_Not(pArg0), Aig_Not(pArg1), pResult ); +} + +/**Function************************************************************* + + Synopsis [Performs BDD operation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cudd2_bddXor( void * pCudd, void * pArg0, void * pArg1, void * pResult ) +{ + Aig_Obj_t * pNode0, * pNode1, * pNode; + pNode0 = Cudd2_GetArg( pArg0 ); + pNode1 = Cudd2_GetArg( pArg1 ); + pNode = Aig_Exor( s_pCuddMan->pAig, pNode0, pNode1 ); + Cudd2_SetArg( pNode, pResult ); +} + +/**Function************************************************************* + + Synopsis [Performs BDD operation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cudd2_bddXnor( void * pCudd, void * pArg0, void * pArg1, void * pResult ) +{ + Cudd2_bddXor( pCudd, pArg0, pArg1, Aig_Not(pResult) ); +} + +/**Function************************************************************* + + Synopsis [Performs BDD operation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cudd2_bddIte( void * pCudd, void * pArg0, void * pArg1, void * pArg2, void * pResult ) +{ + Aig_Obj_t * pNode0, * pNode1, * pNode2, * pNode; + pNode0 = Cudd2_GetArg( pArg0 ); + pNode1 = Cudd2_GetArg( pArg1 ); + pNode2 = Cudd2_GetArg( pArg2 ); + pNode = Aig_Mux( s_pCuddMan->pAig, pNode0, pNode1, pNode2 ); + Cudd2_SetArg( pNode, pResult ); +} + +/**Function************************************************************* + + Synopsis [Performs BDD operation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cudd2_bddCompose( void * pCudd, void * pArg0, void * pArg1, int v, void * pResult ) +{ + Aig_Obj_t * pNode0, * pNode1, * pNode; + pNode0 = Cudd2_GetArg( pArg0 ); + pNode1 = Cudd2_GetArg( pArg1 ); + pNode = Aig_Compose( s_pCuddMan->pAig, pNode0, pNode1, v ); + Cudd2_SetArg( pNode, pResult ); +} + +/**Function************************************************************* + + Synopsis [Should be called after each containment check.] + + Description [Result should be 1 if Cudd2_bddLeq returned 1.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cudd2_bddLeq( void * pCudd, void * pArg0, void * pArg1, int Result ) +{ + Aig_Obj_t * pNode0, * pNode1, * pNode; + pNode0 = Cudd2_GetArg( pArg0 ); + pNode1 = Cudd2_GetArg( pArg1 ); + pNode = Aig_And( s_pCuddMan->pAig, pNode0, Aig_Not(pNode1) ); + Aig_ObjCreatePo( s_pCuddMan->pAig, pNode ); +} + +/**Function************************************************************* + + Synopsis [Should be called after each equality check.] + + Description [Result should be 1 if they are equal.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cudd2_bddEqual( void * pCudd, void * pArg0, void * pArg1, int Result ) +{ + Aig_Obj_t * pNode0, * pNode1, * pNode; + pNode0 = Cudd2_GetArg( pArg0 ); + pNode1 = Cudd2_GetArg( pArg1 ); + pNode = Aig_Exor( s_pCuddMan->pAig, pNode0, pNode1 ); + Aig_ObjCreatePo( s_pCuddMan->pAig, pNode ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/hop/cudd2.h b/src/aig/hop/cudd2.h new file mode 100644 index 00000000..69711c11 --- /dev/null +++ b/src/aig/hop/cudd2.h @@ -0,0 +1,82 @@ +/**CFile**************************************************************** + + FileName [cudd2.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Minimalistic And-Inverter Graph package.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - October 3, 2006.] + + Revision [$Id: cudd2.h,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __CUDD2_H__ +#define __CUDD2_H__ + +#ifdef __cplusplus +extern "C" { +#endif + +// HA: Added for printing messages +#ifndef MSG +#define MSG(msg) (printf("%s = \n",(msg))); +#endif + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + + +//////////////////////////////////////////////////////////////////////// +/// ITERATORS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +extern void Cudd2_Init ( unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int cacheSize, unsigned long maxMemory, void * pCudd ); +extern void Cudd2_Quit ( void * pCudd ); +extern void Cudd2_bddOne ( void * pCudd, void * pResult ); +extern void Cudd2_bddIthVar ( void * pCudd, int iVar, void * pResult ); +extern void Cudd2_bddAnd ( void * pCudd, void * pArg0, void * pArg1, void * pResult ); +extern void Cudd2_bddOr ( void * pCudd, void * pArg0, void * pArg1, void * pResult ); +extern void Cudd2_bddNand ( void * pCudd, void * pArg0, void * pArg1, void * pResult ); +extern void Cudd2_bddNor ( void * pCudd, void * pArg0, void * pArg1, void * pResult ); +extern void Cudd2_bddXor ( void * pCudd, void * pArg0, void * pArg1, void * pResult ); +extern void Cudd2_bddXnor ( void * pCudd, void * pArg0, void * pArg1, void * pResult ); +extern void Cudd2_bddIte ( void * pCudd, void * pArg0, void * pArg1, void * pArg2, void * pResult ); +extern void Cudd2_bddCompose( void * pCudd, void * pArg0, void * pArg1, int v, void * pResult ); +extern void Cudd2_bddLeq ( void * pCudd, void * pArg0, void * pArg1, int Result ); +extern void Cudd2_bddEqual ( void * pCudd, void * pArg0, void * pArg1, int Result ); + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/aig/hop/hop.h b/src/aig/hop/hop.h new file mode 100644 index 00000000..af1d9cd3 --- /dev/null +++ b/src/aig/hop/hop.h @@ -0,0 +1,347 @@ +/**CFile**************************************************************** + + FileName [hop.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Minimalistic And-Inverter Graph package.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: hop.h,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __HOP_H__ +#define __HOP_H__ + +#ifdef __cplusplus +extern "C" { +#endif + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include +#include +#include +#include +#include + +#include "vec.h" + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Hop_Man_t_ Hop_Man_t; +typedef struct Hop_Obj_t_ Hop_Obj_t; +typedef int Hop_Edge_t; + +// object types +typedef enum { + AIG_NONE, // 0: non-existent object + AIG_CONST1, // 1: constant 1 + AIG_PI, // 2: primary input + AIG_PO, // 3: primary output + AIG_AND, // 4: AND node + AIG_EXOR, // 5: EXOR node + AIG_VOID // 6: unused object +} Hop_Type_t; + +// the AIG node +struct Hop_Obj_t_ // 6 words +{ + void * pData; // misc + Hop_Obj_t * pNext; // strashing table + Hop_Obj_t * pFanin0; // fanin + Hop_Obj_t * pFanin1; // fanin + unsigned int Type : 3; // object type + unsigned int fPhase : 1; // value under 000...0 pattern + unsigned int fMarkA : 1; // multipurpose mask + unsigned int fMarkB : 1; // multipurpose mask + unsigned int nRefs : 26; // reference count (level) + int Id; // unique ID of the node +}; + +// the AIG manager +struct Hop_Man_t_ +{ + // AIG nodes + Vec_Ptr_t * vPis; // the array of PIs + Vec_Ptr_t * vPos; // the array of POs + Vec_Ptr_t * vObjs; // the array of all nodes (optional) + Hop_Obj_t * pConst1; // the constant 1 node + Hop_Obj_t Ghost; // the ghost node + // AIG node counters + int nObjs[AIG_VOID];// the number of objects by type + int nCreated; // the number of created objects + int nDeleted; // the number of deleted objects + // stuctural hash table + Hop_Obj_t ** pTable; // structural hash table + int nTableSize; // structural hash table size + // various data members + void * pData; // the temporary data + int nTravIds; // the current traversal ID + int fRefCount; // enables reference counting + int fCatchExor; // enables EXOR nodes + // memory management + Vec_Ptr_t * vChunks; // allocated memory pieces + Vec_Ptr_t * vPages; // memory pages used by nodes + Hop_Obj_t * pListFree; // the list of free nodes + // timing statistics + int time1; + int time2; +}; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +#define AIG_MIN(a,b) (((a) < (b))? (a) : (b)) +#define AIG_MAX(a,b) (((a) > (b))? (a) : (b)) + +#ifndef PRT +#define PRT(a,t) printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC)) +#endif + +static inline int Hop_BitWordNum( int nBits ) { return (nBits>>5) + ((nBits&31) > 0); } +static inline int Hop_TruthWordNum( int nVars ) { return nVars <= 5 ? 1 : (1 << (nVars - 5)); } +static inline int Hop_InfoHasBit( unsigned * p, int i ) { return (p[(i)>>5] & (1<<((i) & 31))) > 0; } +static inline void Hop_InfoSetBit( unsigned * p, int i ) { p[(i)>>5] |= (1<<((i) & 31)); } +static inline void Hop_InfoXorBit( unsigned * p, int i ) { p[(i)>>5] ^= (1<<((i) & 31)); } +static inline int Hop_Base2Log( unsigned n ) { int r; assert( n >= 0 ); if ( n < 2 ) return n; for ( r = 0, n--; n; n >>= 1, r++ ); return r; } +static inline int Hop_Base10Log( unsigned n ) { int r; assert( n >= 0 ); if ( n < 2 ) return n; for ( r = 0, n--; n; n /= 10, r++ ); return r; } + +static inline Hop_Obj_t * Hop_Regular( Hop_Obj_t * p ) { return (Hop_Obj_t *)((unsigned long)(p) & ~01); } +static inline Hop_Obj_t * Hop_Not( Hop_Obj_t * p ) { return (Hop_Obj_t *)((unsigned long)(p) ^ 01); } +static inline Hop_Obj_t * Hop_NotCond( Hop_Obj_t * p, int c ) { return (Hop_Obj_t *)((unsigned long)(p) ^ (c)); } +static inline int Hop_IsComplement( Hop_Obj_t * p ) { return (int)((unsigned long)(p) & 01); } + +static inline Hop_Obj_t * Hop_ManConst0( Hop_Man_t * p ) { return Hop_Not(p->pConst1); } +static inline Hop_Obj_t * Hop_ManConst1( Hop_Man_t * p ) { return p->pConst1; } +static inline Hop_Obj_t * Hop_ManGhost( Hop_Man_t * p ) { return &p->Ghost; } +static inline Hop_Obj_t * Hop_ManPi( Hop_Man_t * p, int i ) { return (Hop_Obj_t *)Vec_PtrEntry(p->vPis, i); } +static inline Hop_Obj_t * Hop_ManPo( Hop_Man_t * p, int i ) { return (Hop_Obj_t *)Vec_PtrEntry(p->vPos, i); } +static inline Hop_Obj_t * Hop_ManObj( Hop_Man_t * p, int i ) { return p->vObjs ? (Hop_Obj_t *)Vec_PtrEntry(p->vObjs, i) : NULL; } + +static inline Hop_Edge_t Hop_EdgeCreate( int Id, int fCompl ) { return (Id << 1) | fCompl; } +static inline int Hop_EdgeId( Hop_Edge_t Edge ) { return Edge >> 1; } +static inline int Hop_EdgeIsComplement( Hop_Edge_t Edge ) { return Edge & 1; } +static inline Hop_Edge_t Hop_EdgeRegular( Hop_Edge_t Edge ) { return (Edge >> 1) << 1; } +static inline Hop_Edge_t Hop_EdgeNot( Hop_Edge_t Edge ) { return Edge ^ 1; } +static inline Hop_Edge_t Hop_EdgeNotCond( Hop_Edge_t Edge, int fCond ) { return Edge ^ fCond; } + +static inline int Hop_ManPiNum( Hop_Man_t * p ) { return p->nObjs[AIG_PI]; } +static inline int Hop_ManPoNum( Hop_Man_t * p ) { return p->nObjs[AIG_PO]; } +static inline int Hop_ManAndNum( Hop_Man_t * p ) { return p->nObjs[AIG_AND]; } +static inline int Hop_ManExorNum( Hop_Man_t * p ) { return p->nObjs[AIG_EXOR]; } +static inline int Hop_ManNodeNum( Hop_Man_t * p ) { return p->nObjs[AIG_AND]+p->nObjs[AIG_EXOR];} +static inline int Hop_ManGetCost( Hop_Man_t * p ) { return p->nObjs[AIG_AND]+3*p->nObjs[AIG_EXOR]; } +static inline int Hop_ManObjNum( Hop_Man_t * p ) { return p->nCreated - p->nDeleted; } + +static inline Hop_Type_t Hop_ObjType( Hop_Obj_t * pObj ) { return (Hop_Type_t)pObj->Type; } +static inline int Hop_ObjIsNone( Hop_Obj_t * pObj ) { return pObj->Type == AIG_NONE; } +static inline int Hop_ObjIsConst1( Hop_Obj_t * pObj ) { assert(!Hop_IsComplement(pObj)); return pObj->Type == AIG_CONST1; } +static inline int Hop_ObjIsPi( Hop_Obj_t * pObj ) { return pObj->Type == AIG_PI; } +static inline int Hop_ObjIsPo( Hop_Obj_t * pObj ) { return pObj->Type == AIG_PO; } +static inline int Hop_ObjIsAnd( Hop_Obj_t * pObj ) { return pObj->Type == AIG_AND; } +static inline int Hop_ObjIsExor( Hop_Obj_t * pObj ) { return pObj->Type == AIG_EXOR; } +static inline int Hop_ObjIsNode( Hop_Obj_t * pObj ) { return pObj->Type == AIG_AND || pObj->Type == AIG_EXOR; } +static inline int Hop_ObjIsTerm( Hop_Obj_t * pObj ) { return pObj->Type == AIG_PI || pObj->Type == AIG_PO || pObj->Type == AIG_CONST1; } +static inline int Hop_ObjIsHash( Hop_Obj_t * pObj ) { return pObj->Type == AIG_AND || pObj->Type == AIG_EXOR; } + +static inline int Hop_ObjIsMarkA( Hop_Obj_t * pObj ) { return pObj->fMarkA; } +static inline void Hop_ObjSetMarkA( Hop_Obj_t * pObj ) { pObj->fMarkA = 1; } +static inline void Hop_ObjClearMarkA( Hop_Obj_t * pObj ) { pObj->fMarkA = 0; } + +static inline void Hop_ObjSetTravId( Hop_Obj_t * pObj, int TravId ) { pObj->pData = (void *)TravId; } +static inline void Hop_ObjSetTravIdCurrent( Hop_Man_t * p, Hop_Obj_t * pObj ) { pObj->pData = (void *)p->nTravIds; } +static inline void Hop_ObjSetTravIdPrevious( Hop_Man_t * p, Hop_Obj_t * pObj ) { pObj->pData = (void *)(p->nTravIds - 1); } +static inline int Hop_ObjIsTravIdCurrent( Hop_Man_t * p, Hop_Obj_t * pObj ) { return (int )((int)pObj->pData == p->nTravIds); } +static inline int Hop_ObjIsTravIdPrevious( Hop_Man_t * p, Hop_Obj_t * pObj ) { return (int )((int)pObj->pData == p->nTravIds - 1); } + +static inline int Hop_ObjTravId( Hop_Obj_t * pObj ) { return (int)pObj->pData; } +static inline int Hop_ObjPhase( Hop_Obj_t * pObj ) { return pObj->fPhase; } +static inline int Hop_ObjRefs( Hop_Obj_t * pObj ) { return pObj->nRefs; } +static inline void Hop_ObjRef( Hop_Obj_t * pObj ) { pObj->nRefs++; } +static inline void Hop_ObjDeref( Hop_Obj_t * pObj ) { assert( pObj->nRefs > 0 ); pObj->nRefs--; } +static inline void Hop_ObjClearRef( Hop_Obj_t * pObj ) { pObj->nRefs = 0; } +static inline int Hop_ObjFaninC0( Hop_Obj_t * pObj ) { return Hop_IsComplement(pObj->pFanin0); } +static inline int Hop_ObjFaninC1( Hop_Obj_t * pObj ) { return Hop_IsComplement(pObj->pFanin1); } +static inline Hop_Obj_t * Hop_ObjFanin0( Hop_Obj_t * pObj ) { return Hop_Regular(pObj->pFanin0); } +static inline Hop_Obj_t * Hop_ObjFanin1( Hop_Obj_t * pObj ) { return Hop_Regular(pObj->pFanin1); } +static inline Hop_Obj_t * Hop_ObjChild0( Hop_Obj_t * pObj ) { return pObj->pFanin0; } +static inline Hop_Obj_t * Hop_ObjChild1( Hop_Obj_t * pObj ) { return pObj->pFanin1; } +static inline Hop_Obj_t * Hop_ObjChild0Copy( Hop_Obj_t * pObj ) { assert( !Hop_IsComplement(pObj) ); return Hop_ObjFanin0(pObj)? Hop_NotCond((Hop_Obj_t *)Hop_ObjFanin0(pObj)->pData, Hop_ObjFaninC0(pObj)) : NULL; } +static inline Hop_Obj_t * Hop_ObjChild1Copy( Hop_Obj_t * pObj ) { assert( !Hop_IsComplement(pObj) ); return Hop_ObjFanin1(pObj)? Hop_NotCond((Hop_Obj_t *)Hop_ObjFanin1(pObj)->pData, Hop_ObjFaninC1(pObj)) : NULL; } +static inline int Hop_ObjLevel( Hop_Obj_t * pObj ) { return pObj->nRefs; } +static inline int Hop_ObjLevelNew( Hop_Obj_t * pObj ) { return 1 + Hop_ObjIsExor(pObj) + AIG_MAX(Hop_ObjFanin0(pObj)->nRefs, Hop_ObjFanin1(pObj)->nRefs); } +static inline int Hop_ObjFaninPhase( Hop_Obj_t * pObj ) { return Hop_IsComplement(pObj)? !Hop_Regular(pObj)->fPhase : pObj->fPhase; } +static inline void Hop_ObjClean( Hop_Obj_t * pObj ) { memset( pObj, 0, sizeof(Hop_Obj_t) ); } +static inline int Hop_ObjWhatFanin( Hop_Obj_t * pObj, Hop_Obj_t * pFanin ) +{ + if ( Hop_ObjFanin0(pObj) == pFanin ) return 0; + if ( Hop_ObjFanin1(pObj) == pFanin ) return 1; + assert(0); return -1; +} +static inline int Hop_ObjFanoutC( Hop_Obj_t * pObj, Hop_Obj_t * pFanout ) +{ + if ( Hop_ObjFanin0(pFanout) == pObj ) return Hop_ObjFaninC0(pObj); + if ( Hop_ObjFanin1(pFanout) == pObj ) return Hop_ObjFaninC1(pObj); + assert(0); return -1; +} + +// create the ghost of the new node +static inline Hop_Obj_t * Hop_ObjCreateGhost( Hop_Man_t * p, Hop_Obj_t * p0, Hop_Obj_t * p1, Hop_Type_t Type ) +{ + Hop_Obj_t * pGhost; + assert( Type != AIG_AND || !Hop_ObjIsConst1(Hop_Regular(p0)) ); + assert( p1 == NULL || !Hop_ObjIsConst1(Hop_Regular(p1)) ); + assert( Type == AIG_PI || Hop_Regular(p0) != Hop_Regular(p1) ); + pGhost = Hop_ManGhost(p); + pGhost->Type = Type; + if ( Hop_Regular(p0)->Id < Hop_Regular(p1)->Id ) + { + pGhost->pFanin0 = p0; + pGhost->pFanin1 = p1; + } + else + { + pGhost->pFanin0 = p1; + pGhost->pFanin1 = p0; + } + return pGhost; +} + +// internal memory manager +static inline Hop_Obj_t * Hop_ManFetchMemory( Hop_Man_t * p ) +{ + extern void Hop_ManAddMemory( Hop_Man_t * p ); + Hop_Obj_t * pTemp; + if ( p->pListFree == NULL ) + Hop_ManAddMemory( p ); + pTemp = p->pListFree; + p->pListFree = *((Hop_Obj_t **)pTemp); + memset( pTemp, 0, sizeof(Hop_Obj_t) ); + if ( p->vObjs ) + { + assert( p->nCreated == Vec_PtrSize(p->vObjs) ); + Vec_PtrPush( p->vObjs, pTemp ); + } + pTemp->Id = p->nCreated++; + return pTemp; +} +static inline void Hop_ManRecycleMemory( Hop_Man_t * p, Hop_Obj_t * pEntry ) +{ + pEntry->Type = AIG_NONE; // distinquishes dead node from live node + *((Hop_Obj_t **)pEntry) = p->pListFree; + p->pListFree = pEntry; +} + + +//////////////////////////////////////////////////////////////////////// +/// ITERATORS /// +//////////////////////////////////////////////////////////////////////// + +// iterator over the primary inputs +#define Hop_ManForEachPi( p, pObj, i ) \ + Vec_PtrForEachEntry( p->vPis, pObj, i ) +// iterator over the primary outputs +#define Hop_ManForEachPo( p, pObj, i ) \ + Vec_PtrForEachEntry( p->vPos, pObj, i ) +// iterator over all objects, including those currently not used +#define Hop_ManForEachNode( p, pObj, i ) \ + for ( i = 0; i < p->nTableSize; i++ ) \ + if ( ((pObj) = p->pTable[i]) == NULL ) {} else + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== hopBalance.c ========================================================*/ +extern Hop_Man_t * Hop_ManBalance( Hop_Man_t * p, int fUpdateLevel ); +extern Hop_Obj_t * Hop_NodeBalanceBuildSuper( Hop_Man_t * p, Vec_Ptr_t * vSuper, Hop_Type_t Type, int fUpdateLevel ); +/*=== hopCheck.c ========================================================*/ +extern int Hop_ManCheck( Hop_Man_t * p ); +/*=== hopDfs.c ==========================================================*/ +extern Vec_Ptr_t * Hop_ManDfs( Hop_Man_t * p ); +extern Vec_Ptr_t * Hop_ManDfsNode( Hop_Man_t * p, Hop_Obj_t * pNode ); +extern int Hop_ManCountLevels( Hop_Man_t * p ); +extern void Hop_ManCreateRefs( Hop_Man_t * p ); +extern int Hop_DagSize( Hop_Obj_t * pObj ); +extern void Hop_ConeUnmark_rec( Hop_Obj_t * pObj ); +extern Hop_Obj_t * Hop_Transfer( Hop_Man_t * pSour, Hop_Man_t * pDest, Hop_Obj_t * pObj, int nVars ); +extern Hop_Obj_t * Hop_Compose( Hop_Man_t * p, Hop_Obj_t * pRoot, Hop_Obj_t * pFunc, int iVar ); +/*=== hopMan.c ==========================================================*/ +extern Hop_Man_t * Hop_ManStart(); +extern Hop_Man_t * Hop_ManDup( Hop_Man_t * p ); +extern void Hop_ManStop( Hop_Man_t * p ); +extern int Hop_ManCleanup( Hop_Man_t * p ); +extern void Hop_ManPrintStats( Hop_Man_t * p ); +/*=== hopMem.c ==========================================================*/ +extern void Hop_ManStartMemory( Hop_Man_t * p ); +extern void Hop_ManStopMemory( Hop_Man_t * p ); +/*=== hopObj.c ==========================================================*/ +extern Hop_Obj_t * Hop_ObjCreatePi( Hop_Man_t * p ); +extern Hop_Obj_t * Hop_ObjCreatePo( Hop_Man_t * p, Hop_Obj_t * pDriver ); +extern Hop_Obj_t * Hop_ObjCreate( Hop_Man_t * p, Hop_Obj_t * pGhost ); +extern void Hop_ObjConnect( Hop_Man_t * p, Hop_Obj_t * pObj, Hop_Obj_t * pFan0, Hop_Obj_t * pFan1 ); +extern void Hop_ObjDisconnect( Hop_Man_t * p, Hop_Obj_t * pObj ); +extern void Hop_ObjDelete( Hop_Man_t * p, Hop_Obj_t * pObj ); +extern void Hop_ObjDelete_rec( Hop_Man_t * p, Hop_Obj_t * pObj ); +extern Hop_Obj_t * Hop_ObjRepr( Hop_Obj_t * pObj ); +extern void Hop_ObjCreateChoice( Hop_Obj_t * pOld, Hop_Obj_t * pNew ); +/*=== hopOper.c =========================================================*/ +extern Hop_Obj_t * Hop_IthVar( Hop_Man_t * p, int i ); +extern Hop_Obj_t * Hop_Oper( Hop_Man_t * p, Hop_Obj_t * p0, Hop_Obj_t * p1, Hop_Type_t Type ); +extern Hop_Obj_t * Hop_And( Hop_Man_t * p, Hop_Obj_t * p0, Hop_Obj_t * p1 ); +extern Hop_Obj_t * Hop_Or( Hop_Man_t * p, Hop_Obj_t * p0, Hop_Obj_t * p1 ); +extern Hop_Obj_t * Hop_Exor( Hop_Man_t * p, Hop_Obj_t * p0, Hop_Obj_t * p1 ); +extern Hop_Obj_t * Hop_Mux( Hop_Man_t * p, Hop_Obj_t * pC, Hop_Obj_t * p1, Hop_Obj_t * p0 ); +extern Hop_Obj_t * Hop_Maj( Hop_Man_t * p, Hop_Obj_t * pA, Hop_Obj_t * pB, Hop_Obj_t * pC ); +extern Hop_Obj_t * Hop_Miter( Hop_Man_t * p, Vec_Ptr_t * vPairs ); +extern Hop_Obj_t * Hop_CreateAnd( Hop_Man_t * p, int nVars ); +extern Hop_Obj_t * Hop_CreateOr( Hop_Man_t * p, int nVars ); +extern Hop_Obj_t * Hop_CreateExor( Hop_Man_t * p, int nVars ); +/*=== hopTable.c ========================================================*/ +extern Hop_Obj_t * Hop_TableLookup( Hop_Man_t * p, Hop_Obj_t * pGhost ); +extern void Hop_TableInsert( Hop_Man_t * p, Hop_Obj_t * pObj ); +extern void Hop_TableDelete( Hop_Man_t * p, Hop_Obj_t * pObj ); +extern int Hop_TableCountEntries( Hop_Man_t * p ); +extern void Hop_TableProfile( Hop_Man_t * p ); +/*=== hopUtil.c =========================================================*/ +extern void Hop_ManIncrementTravId( Hop_Man_t * p ); +extern void Hop_ManCleanData( Hop_Man_t * p ); +extern void Hop_ObjCleanData_rec( Hop_Obj_t * pObj ); +extern void Hop_ObjCollectMulti( Hop_Obj_t * pFunc, Vec_Ptr_t * vSuper ); +extern int Hop_ObjIsMuxType( Hop_Obj_t * pObj ); +extern int Hop_ObjRecognizeExor( Hop_Obj_t * pObj, Hop_Obj_t ** ppFan0, Hop_Obj_t ** ppFan1 ); +extern Hop_Obj_t * Hop_ObjRecognizeMux( Hop_Obj_t * pObj, Hop_Obj_t ** ppObjT, Hop_Obj_t ** ppObjE ); +extern void Hop_ObjPrintEqn( FILE * pFile, Hop_Obj_t * pObj, Vec_Vec_t * vLevels, int Level ); +extern void Hop_ObjPrintVerilog( FILE * pFile, Hop_Obj_t * pObj, Vec_Vec_t * vLevels, int Level ); +extern void Hop_ObjPrintVerbose( Hop_Obj_t * pObj, int fHaig ); +extern void Hop_ManPrintVerbose( Hop_Man_t * p, int fHaig ); +extern void Hop_ManDumpBlif( Hop_Man_t * p, char * pFileName ); + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/aig/hop/hopBalance.c b/src/aig/hop/hopBalance.c new file mode 100644 index 00000000..73c90685 --- /dev/null +++ b/src/aig/hop/hopBalance.c @@ -0,0 +1,391 @@ +/**CFile**************************************************************** + + FileName [hopBalance.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Minimalistic And-Inverter Graph package.] + + Synopsis [Algebraic AIG balancing.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: hopBalance.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "hop.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static Hop_Obj_t * Hop_NodeBalance_rec( Hop_Man_t * pNew, Hop_Obj_t * pObj, Vec_Vec_t * vStore, int Level, int fUpdateLevel ); +static Vec_Ptr_t * Hop_NodeBalanceCone( Hop_Obj_t * pObj, Vec_Vec_t * vStore, int Level ); +static int Hop_NodeBalanceFindLeft( Vec_Ptr_t * vSuper ); +static void Hop_NodeBalancePermute( Hop_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, int fExor ); +static void Hop_NodeBalancePushUniqueOrderByLevel( Vec_Ptr_t * vStore, Hop_Obj_t * pObj ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Performs algebraic balancing of the AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Hop_Man_t * Hop_ManBalance( Hop_Man_t * p, int fUpdateLevel ) +{ + Hop_Man_t * pNew; + Hop_Obj_t * pObj, * pObjNew; + Vec_Vec_t * vStore; + int i; + // create the new manager + pNew = Hop_ManStart(); + pNew->fRefCount = 0; + // map the PI nodes + Hop_ManCleanData( p ); + Hop_ManConst1(p)->pData = Hop_ManConst1(pNew); + Hop_ManForEachPi( p, pObj, i ) + pObj->pData = Hop_ObjCreatePi(pNew); + // balance the AIG + vStore = Vec_VecAlloc( 50 ); + Hop_ManForEachPo( p, pObj, i ) + { + pObjNew = Hop_NodeBalance_rec( pNew, Hop_ObjFanin0(pObj), vStore, 0, fUpdateLevel ); + Hop_ObjCreatePo( pNew, Hop_NotCond( pObjNew, Hop_ObjFaninC0(pObj) ) ); + } + Vec_VecFree( vStore ); + // remove dangling nodes +// Hop_ManCreateRefs( pNew ); +// if ( i = Hop_ManCleanup( pNew ) ) +// printf( "Cleanup after balancing removed %d dangling nodes.\n", i ); + // check the resulting AIG + if ( !Hop_ManCheck(pNew) ) + printf( "Hop_ManBalance(): The check has failed.\n" ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Returns the new node constructed.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Hop_Obj_t * Hop_NodeBalance_rec( Hop_Man_t * pNew, Hop_Obj_t * pObjOld, Vec_Vec_t * vStore, int Level, int fUpdateLevel ) +{ + Hop_Obj_t * pObjNew; + Vec_Ptr_t * vSuper; + int i; + assert( !Hop_IsComplement(pObjOld) ); + // return if the result is known + if ( pObjOld->pData ) + return pObjOld->pData; + assert( Hop_ObjIsNode(pObjOld) ); + // get the implication supergate + vSuper = Hop_NodeBalanceCone( pObjOld, vStore, Level ); + // check if supergate contains two nodes in the opposite polarity + if ( vSuper->nSize == 0 ) + return pObjOld->pData = Hop_ManConst0(pNew); + if ( Vec_PtrSize(vSuper) < 2 ) + printf( "BUG!\n" ); + // for each old node, derive the new well-balanced node + for ( i = 0; i < Vec_PtrSize(vSuper); i++ ) + { + pObjNew = Hop_NodeBalance_rec( pNew, Hop_Regular(vSuper->pArray[i]), vStore, Level + 1, fUpdateLevel ); + vSuper->pArray[i] = Hop_NotCond( pObjNew, Hop_IsComplement(vSuper->pArray[i]) ); + } + // build the supergate + pObjNew = Hop_NodeBalanceBuildSuper( pNew, vSuper, Hop_ObjType(pObjOld), fUpdateLevel ); + // make sure the balanced node is not assigned +// assert( pObjOld->Level >= Hop_Regular(pObjNew)->Level ); + assert( pObjOld->pData == NULL ); + return pObjOld->pData = pObjNew; +} + +/**Function************************************************************* + + Synopsis [Collects the nodes of the supergate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Hop_NodeBalanceCone_rec( Hop_Obj_t * pRoot, Hop_Obj_t * pObj, Vec_Ptr_t * vSuper ) +{ + int RetValue1, RetValue2, i; + // check if the node is visited + if ( Hop_Regular(pObj)->fMarkB ) + { + // check if the node occurs in the same polarity + for ( i = 0; i < vSuper->nSize; i++ ) + if ( vSuper->pArray[i] == pObj ) + return 1; + // check if the node is present in the opposite polarity + for ( i = 0; i < vSuper->nSize; i++ ) + if ( vSuper->pArray[i] == Hop_Not(pObj) ) + return -1; + assert( 0 ); + return 0; + } + // if the new node is complemented or a PI, another gate begins + if ( pObj != pRoot && (Hop_IsComplement(pObj) || Hop_ObjType(pObj) != Hop_ObjType(pRoot) || Hop_ObjRefs(pObj) > 1) ) + { + Vec_PtrPush( vSuper, pObj ); + Hop_Regular(pObj)->fMarkB = 1; + return 0; + } + assert( !Hop_IsComplement(pObj) ); + assert( Hop_ObjIsNode(pObj) ); + // go through the branches + RetValue1 = Hop_NodeBalanceCone_rec( pRoot, Hop_ObjChild0(pObj), vSuper ); + RetValue2 = Hop_NodeBalanceCone_rec( pRoot, Hop_ObjChild1(pObj), vSuper ); + if ( RetValue1 == -1 || RetValue2 == -1 ) + return -1; + // return 1 if at least one branch has a duplicate + return RetValue1 || RetValue2; +} + +/**Function************************************************************* + + Synopsis [Collects the nodes of the supergate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Hop_NodeBalanceCone( Hop_Obj_t * pObj, Vec_Vec_t * vStore, int Level ) +{ + Vec_Ptr_t * vNodes; + int RetValue, i; + assert( !Hop_IsComplement(pObj) ); + // extend the storage + if ( Vec_VecSize( vStore ) <= Level ) + Vec_VecPush( vStore, Level, 0 ); + // get the temporary array of nodes + vNodes = Vec_VecEntry( vStore, Level ); + Vec_PtrClear( vNodes ); + // collect the nodes in the implication supergate + RetValue = Hop_NodeBalanceCone_rec( pObj, pObj, vNodes ); + assert( vNodes->nSize > 1 ); + // unmark the visited nodes + Vec_PtrForEachEntry( vNodes, pObj, i ) + Hop_Regular(pObj)->fMarkB = 0; + // if we found the node and its complement in the same implication supergate, + // return empty set of nodes (meaning that we should use constant-0 node) + if ( RetValue == -1 ) + vNodes->nSize = 0; + return vNodes; +} + +/**Function************************************************************* + + Synopsis [Procedure used for sorting the nodes in decreasing order of levels.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Hop_NodeCompareLevelsDecrease( Hop_Obj_t ** pp1, Hop_Obj_t ** pp2 ) +{ + int Diff = Hop_ObjLevel(Hop_Regular(*pp1)) - Hop_ObjLevel(Hop_Regular(*pp2)); + if ( Diff > 0 ) + return -1; + if ( Diff < 0 ) + return 1; + return 0; +} + +/**Function************************************************************* + + Synopsis [Builds implication supergate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Hop_Obj_t * Hop_NodeBalanceBuildSuper( Hop_Man_t * p, Vec_Ptr_t * vSuper, Hop_Type_t Type, int fUpdateLevel ) +{ + Hop_Obj_t * pObj1, * pObj2; + int LeftBound; + assert( vSuper->nSize > 1 ); + // sort the new nodes by level in the decreasing order + Vec_PtrSort( vSuper, Hop_NodeCompareLevelsDecrease ); + // balance the nodes + while ( vSuper->nSize > 1 ) + { + // find the left bound on the node to be paired + LeftBound = (!fUpdateLevel)? 0 : Hop_NodeBalanceFindLeft( vSuper ); + // find the node that can be shared (if no such node, randomize choice) + Hop_NodeBalancePermute( p, vSuper, LeftBound, Type == AIG_EXOR ); + // pull out the last two nodes + pObj1 = Vec_PtrPop(vSuper); + pObj2 = Vec_PtrPop(vSuper); + Hop_NodeBalancePushUniqueOrderByLevel( vSuper, Hop_Oper(p, pObj1, pObj2, Type) ); + } + return Vec_PtrEntry(vSuper, 0); +} + +/**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 Hop_NodeBalanceFindLeft( Vec_Ptr_t * vSuper ) +{ + Hop_Obj_t * pObjRight, * pObjLeft; + 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; + pObjRight = 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 + pObjLeft = Vec_PtrEntry( vSuper, Current ); + // if the level of this node is different, quit the loop + if ( Hop_ObjLevel(Hop_Regular(pObjLeft)) != Hop_ObjLevel(Hop_Regular(pObjRight)) ) + break; + } + Current++; + // get the node, for which the equality holds + pObjLeft = Vec_PtrEntry( vSuper, Current ); + assert( Hop_ObjLevel(Hop_Regular(pObjLeft)) == Hop_ObjLevel(Hop_Regular(pObjRight)) ); + 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 Hop_NodeBalancePermute( Hop_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, int fExor ) +{ + Hop_Obj_t * pObj1, * pObj2, * pObj3, * 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 + pObj1 = Vec_PtrEntry( vSuper, RightBound + 1 ); + pObj2 = Vec_PtrEntry( vSuper, RightBound ); + if ( Hop_Regular(pObj1) == p->pConst1 || Hop_Regular(pObj2) == p->pConst1 ) + return; + // find the first node that can be shared + for ( i = RightBound; i >= LeftBound; i-- ) + { + pObj3 = Vec_PtrEntry( vSuper, i ); + if ( Hop_Regular(pObj3) == p->pConst1 ) + { + Vec_PtrWriteEntry( vSuper, i, pObj2 ); + Vec_PtrWriteEntry( vSuper, RightBound, pObj3 ); + return; + } + pGhost = Hop_ObjCreateGhost( p, pObj1, pObj3, fExor? AIG_EXOR : AIG_AND ); + if ( Hop_TableLookup( p, pGhost ) ) + { + if ( pObj3 == pObj2 ) + return; + Vec_PtrWriteEntry( vSuper, i, pObj2 ); + Vec_PtrWriteEntry( vSuper, RightBound, pObj3 ); + return; + } + } +/* + // we did not find the node to share, randomize choice + { + int Choice = rand() % (RightBound - LeftBound + 1); + pObj3 = Vec_PtrEntry( vSuper, LeftBound + Choice ); + if ( pObj3 == pObj2 ) + return; + Vec_PtrWriteEntry( vSuper, LeftBound + Choice, pObj2 ); + Vec_PtrWriteEntry( vSuper, RightBound, pObj3 ); + } +*/ +} + +/**Function************************************************************* + + Synopsis [Inserts a new node in the order by levels.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Hop_NodeBalancePushUniqueOrderByLevel( Vec_Ptr_t * vStore, Hop_Obj_t * pObj ) +{ + Hop_Obj_t * pObj1, * pObj2; + int i; + if ( Vec_PtrPushUnique(vStore, pObj) ) + return; + // find the p of the node + for ( i = vStore->nSize-1; i > 0; i-- ) + { + pObj1 = vStore->pArray[i ]; + pObj2 = vStore->pArray[i-1]; + if ( Hop_ObjLevel(Hop_Regular(pObj1)) <= Hop_ObjLevel(Hop_Regular(pObj2)) ) + break; + vStore->pArray[i ] = pObj2; + vStore->pArray[i-1] = pObj1; + } +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/hop/hopCheck.c b/src/aig/hop/hopCheck.c new file mode 100644 index 00000000..9120906f --- /dev/null +++ b/src/aig/hop/hopCheck.c @@ -0,0 +1,110 @@ +/**CFile**************************************************************** + + FileName [hopCheck.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Minimalistic And-Inverter Graph package.] + + Synopsis [AIG checking procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: hopCheck.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "hop.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Checks the consistency of the AIG manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Hop_ManCheck( Hop_Man_t * p ) +{ + Hop_Obj_t * pObj, * pObj2; + int i; + // check primary inputs + Hop_ManForEachPi( p, pObj, i ) + { + if ( Hop_ObjFanin0(pObj) || Hop_ObjFanin1(pObj) ) + { + printf( "Hop_ManCheck: The PI node \"%p\" has fanins.\n", pObj ); + return 0; + } + } + // check primary outputs + Hop_ManForEachPo( p, pObj, i ) + { + if ( !Hop_ObjFanin0(pObj) ) + { + printf( "Hop_ManCheck: The PO node \"%p\" has NULL fanin.\n", pObj ); + return 0; + } + if ( Hop_ObjFanin1(pObj) ) + { + printf( "Hop_ManCheck: The PO node \"%p\" has second fanin.\n", pObj ); + return 0; + } + } + // check internal nodes + Hop_ManForEachNode( p, pObj, i ) + { + if ( !Hop_ObjFanin0(pObj) || !Hop_ObjFanin1(pObj) ) + { + printf( "Hop_ManCheck: The AIG has internal node \"%p\" with a NULL fanin.\n", pObj ); + return 0; + } + if ( Hop_ObjFanin0(pObj)->Id >= Hop_ObjFanin1(pObj)->Id ) + { + printf( "Hop_ManCheck: The AIG has node \"%p\" with a wrong ordering of fanins.\n", pObj ); + return 0; + } + pObj2 = Hop_TableLookup( p, pObj ); + if ( pObj2 != pObj ) + { + printf( "Hop_ManCheck: Node \"%p\" is not in the structural hashing table.\n", pObj ); + return 0; + } + } + // count the total number of nodes + if ( Hop_ManObjNum(p) != 1 + Hop_ManPiNum(p) + Hop_ManPoNum(p) + Hop_ManAndNum(p) + Hop_ManExorNum(p) ) + { + printf( "Hop_ManCheck: The number of created nodes is wrong.\n" ); + return 0; + } + // count the number of nodes in the table + if ( Hop_TableCountEntries(p) != Hop_ManAndNum(p) + Hop_ManExorNum(p) ) + { + printf( "Hop_ManCheck: The number of nodes in the structural hashing table is wrong.\n" ); + return 0; + } +// if ( !Hop_ManIsAcyclic(p) ) +// return 0; + return 1; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/hop/hopDfs.c b/src/aig/hop/hopDfs.c new file mode 100644 index 00000000..49e5f221 --- /dev/null +++ b/src/aig/hop/hopDfs.c @@ -0,0 +1,399 @@ +/**CFile**************************************************************** + + FileName [hopDfs.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Minimalistic And-Inverter Graph package.] + + Synopsis [DFS traversal procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: hopDfs.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "hop.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Collects internal nodes in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Hop_ManDfs_rec( Hop_Obj_t * pObj, Vec_Ptr_t * vNodes ) +{ + assert( !Hop_IsComplement(pObj) ); + if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) ) + return; + Hop_ManDfs_rec( Hop_ObjFanin0(pObj), vNodes ); + Hop_ManDfs_rec( Hop_ObjFanin1(pObj), vNodes ); + assert( !Hop_ObjIsMarkA(pObj) ); // loop detection + Hop_ObjSetMarkA(pObj); + Vec_PtrPush( vNodes, pObj ); +} + +/**Function************************************************************* + + Synopsis [Collects internal nodes in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Hop_ManDfs( Hop_Man_t * p ) +{ + Vec_Ptr_t * vNodes; + Hop_Obj_t * pObj; + int i; + vNodes = Vec_PtrAlloc( Hop_ManNodeNum(p) ); + Hop_ManForEachNode( p, pObj, i ) + Hop_ManDfs_rec( pObj, vNodes ); + Hop_ManForEachNode( p, pObj, i ) + Hop_ObjClearMarkA(pObj); + return vNodes; +} + +/**Function************************************************************* + + Synopsis [Collects internal nodes in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Hop_ManDfsNode( Hop_Man_t * p, Hop_Obj_t * pNode ) +{ + Vec_Ptr_t * vNodes; + Hop_Obj_t * pObj; + int i; + assert( !Hop_IsComplement(pNode) ); + vNodes = Vec_PtrAlloc( 16 ); + Hop_ManDfs_rec( pNode, vNodes ); + Vec_PtrForEachEntry( vNodes, pObj, i ) + Hop_ObjClearMarkA(pObj); + return vNodes; +} + +/**Function************************************************************* + + Synopsis [Computes the max number of levels in the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Hop_ManCountLevels( Hop_Man_t * p ) +{ + Vec_Ptr_t * vNodes; + Hop_Obj_t * pObj; + int i, LevelsMax, Level0, Level1; + // initialize the levels + Hop_ManConst1(p)->pData = NULL; + Hop_ManForEachPi( p, pObj, i ) + pObj->pData = NULL; + // compute levels in a DFS order + vNodes = Hop_ManDfs( p ); + Vec_PtrForEachEntry( vNodes, pObj, i ) + { + Level0 = (int)Hop_ObjFanin0(pObj)->pData; + Level1 = (int)Hop_ObjFanin1(pObj)->pData; + pObj->pData = (void *)(1 + Hop_ObjIsExor(pObj) + AIG_MAX(Level0, Level1)); + } + Vec_PtrFree( vNodes ); + // get levels of the POs + LevelsMax = 0; + Hop_ManForEachPo( p, pObj, i ) + LevelsMax = AIG_MAX( LevelsMax, (int)Hop_ObjFanin0(pObj)->pData ); + return LevelsMax; +} + +/**Function************************************************************* + + Synopsis [Creates correct reference counters at each node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Hop_ManCreateRefs( Hop_Man_t * p ) +{ + Hop_Obj_t * pObj; + int i; + if ( p->fRefCount ) + return; + p->fRefCount = 1; + // clear refs + Hop_ObjClearRef( Hop_ManConst1(p) ); + Hop_ManForEachPi( p, pObj, i ) + Hop_ObjClearRef( pObj ); + Hop_ManForEachNode( p, pObj, i ) + Hop_ObjClearRef( pObj ); + Hop_ManForEachPo( p, pObj, i ) + Hop_ObjClearRef( pObj ); + // set refs + Hop_ManForEachNode( p, pObj, i ) + { + Hop_ObjRef( Hop_ObjFanin0(pObj) ); + Hop_ObjRef( Hop_ObjFanin1(pObj) ); + } + Hop_ManForEachPo( p, pObj, i ) + Hop_ObjRef( Hop_ObjFanin0(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Counts the number of AIG nodes rooted at this cone.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Hop_ConeMark_rec( Hop_Obj_t * pObj ) +{ + assert( !Hop_IsComplement(pObj) ); + if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) ) + return; + Hop_ConeMark_rec( Hop_ObjFanin0(pObj) ); + Hop_ConeMark_rec( Hop_ObjFanin1(pObj) ); + assert( !Hop_ObjIsMarkA(pObj) ); // loop detection + Hop_ObjSetMarkA( pObj ); +} + +/**Function************************************************************* + + Synopsis [Counts the number of AIG nodes rooted at this cone.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Hop_ConeCleanAndMark_rec( Hop_Obj_t * pObj ) +{ + assert( !Hop_IsComplement(pObj) ); + if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) ) + return; + Hop_ConeCleanAndMark_rec( Hop_ObjFanin0(pObj) ); + Hop_ConeCleanAndMark_rec( Hop_ObjFanin1(pObj) ); + assert( !Hop_ObjIsMarkA(pObj) ); // loop detection + Hop_ObjSetMarkA( pObj ); + pObj->pData = NULL; +} + +/**Function************************************************************* + + Synopsis [Counts the number of AIG nodes rooted at this cone.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Hop_ConeCountAndMark_rec( Hop_Obj_t * pObj ) +{ + int Counter; + assert( !Hop_IsComplement(pObj) ); + if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) ) + return 0; + Counter = 1 + Hop_ConeCountAndMark_rec( Hop_ObjFanin0(pObj) ) + + Hop_ConeCountAndMark_rec( Hop_ObjFanin1(pObj) ); + assert( !Hop_ObjIsMarkA(pObj) ); // loop detection + Hop_ObjSetMarkA( pObj ); + return Counter; +} + +/**Function************************************************************* + + Synopsis [Counts the number of AIG nodes rooted at this cone.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Hop_ConeUnmark_rec( Hop_Obj_t * pObj ) +{ + assert( !Hop_IsComplement(pObj) ); + if ( !Hop_ObjIsNode(pObj) || !Hop_ObjIsMarkA(pObj) ) + return; + Hop_ConeUnmark_rec( Hop_ObjFanin0(pObj) ); + Hop_ConeUnmark_rec( Hop_ObjFanin1(pObj) ); + assert( Hop_ObjIsMarkA(pObj) ); // loop detection + Hop_ObjClearMarkA( pObj ); +} + +/**Function************************************************************* + + Synopsis [Counts the number of AIG nodes rooted at this cone.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Hop_DagSize( Hop_Obj_t * pObj ) +{ + int Counter; + Counter = Hop_ConeCountAndMark_rec( Hop_Regular(pObj) ); + Hop_ConeUnmark_rec( Hop_Regular(pObj) ); + return Counter; +} + +/**Function************************************************************* + + Synopsis [Transfers the AIG from one manager into another.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Hop_Transfer_rec( Hop_Man_t * pDest, Hop_Obj_t * pObj ) +{ + assert( !Hop_IsComplement(pObj) ); + if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) ) + return; + Hop_Transfer_rec( pDest, Hop_ObjFanin0(pObj) ); + Hop_Transfer_rec( pDest, Hop_ObjFanin1(pObj) ); + pObj->pData = Hop_And( pDest, Hop_ObjChild0Copy(pObj), Hop_ObjChild1Copy(pObj) ); + assert( !Hop_ObjIsMarkA(pObj) ); // loop detection + Hop_ObjSetMarkA( pObj ); +} + +/**Function************************************************************* + + Synopsis [Transfers the AIG from one manager into another.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Hop_Obj_t * Hop_Transfer( Hop_Man_t * pSour, Hop_Man_t * pDest, Hop_Obj_t * pRoot, int nVars ) +{ + Hop_Obj_t * pObj; + int i; + // solve simple cases + if ( pSour == pDest ) + return pRoot; + if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) ) + return Hop_NotCond( Hop_ManConst1(pDest), Hop_IsComplement(pRoot) ); + // set the PI mapping + Hop_ManForEachPi( pSour, pObj, i ) + { + if ( i == nVars ) + break; + pObj->pData = Hop_IthVar(pDest, i); + } + // transfer and set markings + Hop_Transfer_rec( pDest, Hop_Regular(pRoot) ); + // clear the markings + Hop_ConeUnmark_rec( Hop_Regular(pRoot) ); + return Hop_NotCond( Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) ); +} + +/**Function************************************************************* + + Synopsis [Composes the AIG (pRoot) with the function (pFunc) using PI var (iVar).] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Hop_Compose_rec( Hop_Man_t * p, Hop_Obj_t * pObj, Hop_Obj_t * pFunc, Hop_Obj_t * pVar ) +{ + assert( !Hop_IsComplement(pObj) ); + if ( Hop_ObjIsMarkA(pObj) ) + return; + if ( Hop_ObjIsConst1(pObj) || Hop_ObjIsPi(pObj) ) + { + pObj->pData = pObj == pVar ? pFunc : pObj; + return; + } + Hop_Compose_rec( p, Hop_ObjFanin0(pObj), pFunc, pVar ); + Hop_Compose_rec( p, Hop_ObjFanin1(pObj), pFunc, pVar ); + pObj->pData = Hop_And( p, Hop_ObjChild0Copy(pObj), Hop_ObjChild1Copy(pObj) ); + assert( !Hop_ObjIsMarkA(pObj) ); // loop detection + Hop_ObjSetMarkA( pObj ); +} + +/**Function************************************************************* + + Synopsis [Composes the AIG (pRoot) with the function (pFunc) using PI var (iVar).] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Hop_Obj_t * Hop_Compose( Hop_Man_t * p, Hop_Obj_t * pRoot, Hop_Obj_t * pFunc, int iVar ) +{ + // quit if the PI variable is not defined + if ( iVar >= Hop_ManPiNum(p) ) + { + printf( "Hop_Compose(): The PI variable %d is not defined.\n", iVar ); + return NULL; + } + // recursively perform composition + Hop_Compose_rec( p, Hop_Regular(pRoot), pFunc, Hop_ManPi(p, iVar) ); + // clear the markings + Hop_ConeUnmark_rec( Hop_Regular(pRoot) ); + return Hop_NotCond( Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/hop/hopMan.c b/src/aig/hop/hopMan.c new file mode 100644 index 00000000..99f5d316 --- /dev/null +++ b/src/aig/hop/hopMan.c @@ -0,0 +1,164 @@ +/**CFile**************************************************************** + + FileName [hopMan.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Minimalistic And-Inverter Graph package.] + + Synopsis [AIG manager.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: hopMan.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "hop.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Starts the AIG manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Hop_Man_t * Hop_ManStart() +{ + Hop_Man_t * p; + // start the manager + p = ALLOC( Hop_Man_t, 1 ); + memset( p, 0, sizeof(Hop_Man_t) ); + // perform initializations + p->nTravIds = 1; + p->fRefCount = 1; + p->fCatchExor = 0; + // allocate arrays for nodes + p->vPis = Vec_PtrAlloc( 100 ); + p->vPos = Vec_PtrAlloc( 100 ); + // prepare the internal memory manager + Hop_ManStartMemory( p ); + // create the constant node + p->pConst1 = Hop_ManFetchMemory( p ); + p->pConst1->Type = AIG_CONST1; + p->pConst1->fPhase = 1; + p->nCreated = 1; + // start the table +// p->nTableSize = 107; + p->nTableSize = 10007; + p->pTable = ALLOC( Hop_Obj_t *, p->nTableSize ); + memset( p->pTable, 0, sizeof(Hop_Obj_t *) * p->nTableSize ); + return p; +} + +/**Function************************************************************* + + Synopsis [Stops the AIG manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Hop_ManStop( Hop_Man_t * p ) +{ + Hop_Obj_t * pObj; + int i; + // make sure the nodes have clean marks + pObj = Hop_ManConst1(p); + assert( !pObj->fMarkA && !pObj->fMarkB ); + Hop_ManForEachPi( p, pObj, i ) + assert( !pObj->fMarkA && !pObj->fMarkB ); + Hop_ManForEachPo( p, pObj, i ) + assert( !pObj->fMarkA && !pObj->fMarkB ); + Hop_ManForEachNode( p, pObj, i ) + assert( !pObj->fMarkA && !pObj->fMarkB ); + // print time + if ( p->time1 ) { PRT( "time1", p->time1 ); } + if ( p->time2 ) { PRT( "time2", p->time2 ); } +// Hop_TableProfile( p ); + if ( p->vChunks ) Hop_ManStopMemory( p ); + if ( p->vPis ) Vec_PtrFree( p->vPis ); + if ( p->vPos ) Vec_PtrFree( p->vPos ); + if ( p->vObjs ) Vec_PtrFree( p->vObjs ); + free( p->pTable ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [Returns the number of dangling nodes removed.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Hop_ManCleanup( Hop_Man_t * p ) +{ + Vec_Ptr_t * vObjs; + Hop_Obj_t * pNode; + int i, nNodesOld; + assert( p->fRefCount ); + nNodesOld = Hop_ManNodeNum(p); + // collect roots of dangling nodes + vObjs = Vec_PtrAlloc( 100 ); + Hop_ManForEachNode( p, pNode, i ) + if ( Hop_ObjRefs(pNode) == 0 ) + Vec_PtrPush( vObjs, pNode ); + // recursively remove dangling nodes + Vec_PtrForEachEntry( vObjs, pNode, i ) + Hop_ObjDelete_rec( p, pNode ); + Vec_PtrFree( vObjs ); + return nNodesOld - Hop_ManNodeNum(p); +} + +/**Function************************************************************* + + Synopsis [Stops the AIG manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Hop_ManPrintStats( Hop_Man_t * p ) +{ + printf( "PI/PO = %d/%d. ", Hop_ManPiNum(p), Hop_ManPoNum(p) ); + printf( "A = %7d. ", Hop_ManAndNum(p) ); + printf( "X = %5d. ", Hop_ManExorNum(p) ); + printf( "Cre = %7d. ", p->nCreated ); + printf( "Del = %7d. ", p->nDeleted ); + printf( "Lev = %3d. ", Hop_ManCountLevels(p) ); + printf( "\n" ); +} + + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/hop/hopMem.c b/src/aig/hop/hopMem.c new file mode 100644 index 00000000..0665470a --- /dev/null +++ b/src/aig/hop/hopMem.c @@ -0,0 +1,115 @@ +/**CFile**************************************************************** + + FileName [hopMem.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Minimalistic And-Inverter Graph package.] + + Synopsis [Memory management for the AIG nodes.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: hopMem.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "hop.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +// memory management +#define IVY_PAGE_SIZE 12 // page size containing 2^IVY_PAGE_SIZE nodes +#define IVY_PAGE_MASK 4095 // page bitmask (2^IVY_PAGE_SIZE)-1 + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Starts the internal memory manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Hop_ManStartMemory( Hop_Man_t * p ) +{ + p->vChunks = Vec_PtrAlloc( 128 ); + p->vPages = Vec_PtrAlloc( 128 ); +} + +/**Function************************************************************* + + Synopsis [Stops the internal memory manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Hop_ManStopMemory( Hop_Man_t * p ) +{ + void * pMemory; + int i; + Vec_PtrForEachEntry( p->vChunks, pMemory, i ) + free( pMemory ); + Vec_PtrFree( p->vChunks ); + Vec_PtrFree( p->vPages ); + p->pListFree = NULL; +} + +/**Function************************************************************* + + Synopsis [Allocates additional memory for the nodes.] + + Description [Allocates IVY_PAGE_SIZE nodes. Aligns memory by 32 bytes. + Records the pointer to the AIG manager in the -1 entry.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Hop_ManAddMemory( Hop_Man_t * p ) +{ + char * pMemory; + int i, nBytes; + assert( sizeof(Hop_Obj_t) <= 64 ); + assert( p->pListFree == NULL ); +// assert( (Hop_ManObjNum(p) & IVY_PAGE_MASK) == 0 ); + // allocate new memory page + nBytes = sizeof(Hop_Obj_t) * (1<vChunks, pMemory ); + // align memory at the 32-byte boundary + pMemory = pMemory + 64 - (((int)pMemory) & 63); + // remember the manager in the first entry + Vec_PtrPush( p->vPages, pMemory ); + // break the memory down into nodes + p->pListFree = (Hop_Obj_t *)pMemory; + for ( i = 1; i <= IVY_PAGE_MASK; i++ ) + { + *((char **)pMemory) = pMemory + sizeof(Hop_Obj_t); + pMemory += sizeof(Hop_Obj_t); + } + *((char **)pMemory) = NULL; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/hop/hopObj.c b/src/aig/hop/hopObj.c new file mode 100644 index 00000000..c8e70dd3 --- /dev/null +++ b/src/aig/hop/hopObj.c @@ -0,0 +1,271 @@ +/**CFile**************************************************************** + + FileName [hopObj.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Minimalistic And-Inverter Graph package.] + + Synopsis [Adding/removing objects.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: hopObj.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "hop.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Creates primary input.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Hop_Obj_t * Hop_ObjCreatePi( Hop_Man_t * p ) +{ + Hop_Obj_t * pObj; + pObj = Hop_ManFetchMemory( p ); + pObj->Type = AIG_PI; + Vec_PtrPush( p->vPis, pObj ); + p->nObjs[AIG_PI]++; + return pObj; +} + +/**Function************************************************************* + + Synopsis [Creates primary output with the given driver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Hop_Obj_t * Hop_ObjCreatePo( Hop_Man_t * p, Hop_Obj_t * pDriver ) +{ + Hop_Obj_t * pObj; + pObj = Hop_ManFetchMemory( p ); + pObj->Type = AIG_PO; + Vec_PtrPush( p->vPos, pObj ); + // add connections + pObj->pFanin0 = pDriver; + if ( p->fRefCount ) + Hop_ObjRef( Hop_Regular(pDriver) ); + else + pObj->nRefs = Hop_ObjLevel( Hop_Regular(pDriver) ); + // set the phase + pObj->fPhase = Hop_ObjFaninPhase(pDriver); + // update node counters of the manager + p->nObjs[AIG_PO]++; + return pObj; +} + +/**Function************************************************************* + + Synopsis [Create the new node assuming it does not exist.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Hop_Obj_t * Hop_ObjCreate( Hop_Man_t * p, Hop_Obj_t * pGhost ) +{ + Hop_Obj_t * pObj; + assert( !Hop_IsComplement(pGhost) ); + assert( Hop_ObjIsNode(pGhost) ); + assert( pGhost == &p->Ghost ); + // get memory for the new object + pObj = Hop_ManFetchMemory( p ); + pObj->Type = pGhost->Type; + // add connections + Hop_ObjConnect( p, pObj, pGhost->pFanin0, pGhost->pFanin1 ); + // update node counters of the manager + p->nObjs[Hop_ObjType(pObj)]++; + assert( pObj->pData == NULL ); + return pObj; +} + +/**Function************************************************************* + + Synopsis [Connect the object to the fanin.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Hop_ObjConnect( Hop_Man_t * p, Hop_Obj_t * pObj, Hop_Obj_t * pFan0, Hop_Obj_t * pFan1 ) +{ + assert( !Hop_IsComplement(pObj) ); + assert( Hop_ObjIsNode(pObj) ); + // add the first fanin + pObj->pFanin0 = pFan0; + pObj->pFanin1 = pFan1; + // increment references of the fanins and add their fanouts + if ( p->fRefCount ) + { + if ( pFan0 != NULL ) + Hop_ObjRef( Hop_ObjFanin0(pObj) ); + if ( pFan1 != NULL ) + Hop_ObjRef( Hop_ObjFanin1(pObj) ); + } + else + pObj->nRefs = Hop_ObjLevelNew( pObj ); + // set the phase + pObj->fPhase = Hop_ObjFaninPhase(pFan0) & Hop_ObjFaninPhase(pFan1); + // add the node to the structural hash table + Hop_TableInsert( p, pObj ); +} + +/**Function************************************************************* + + Synopsis [Connect the object to the fanin.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Hop_ObjDisconnect( Hop_Man_t * p, Hop_Obj_t * pObj ) +{ + assert( !Hop_IsComplement(pObj) ); + assert( Hop_ObjIsNode(pObj) ); + // remove connections + if ( pObj->pFanin0 != NULL ) + Hop_ObjDeref(Hop_ObjFanin0(pObj)); + if ( pObj->pFanin1 != NULL ) + Hop_ObjDeref(Hop_ObjFanin1(pObj)); + // remove the node from the structural hash table + Hop_TableDelete( p, pObj ); + // add the first fanin + pObj->pFanin0 = NULL; + pObj->pFanin1 = NULL; +} + +/**Function************************************************************* + + Synopsis [Deletes the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Hop_ObjDelete( Hop_Man_t * p, Hop_Obj_t * pObj ) +{ + assert( !Hop_IsComplement(pObj) ); + assert( !Hop_ObjIsTerm(pObj) ); + assert( Hop_ObjRefs(pObj) == 0 ); + // update node counters of the manager + p->nObjs[pObj->Type]--; + p->nDeleted++; + // remove connections + Hop_ObjDisconnect( p, pObj ); + // remove PIs/POs from the arrays + if ( Hop_ObjIsPi(pObj) ) + Vec_PtrRemove( p->vPis, pObj ); + // free the node + Hop_ManRecycleMemory( p, pObj ); +} + +/**Function************************************************************* + + Synopsis [Deletes the MFFC of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Hop_ObjDelete_rec( Hop_Man_t * p, Hop_Obj_t * pObj ) +{ + Hop_Obj_t * pFanin0, * pFanin1; + assert( !Hop_IsComplement(pObj) ); + if ( Hop_ObjIsConst1(pObj) || Hop_ObjIsPi(pObj) ) + return; + assert( Hop_ObjIsNode(pObj) ); + pFanin0 = Hop_ObjFanin0(pObj); + pFanin1 = Hop_ObjFanin1(pObj); + Hop_ObjDelete( p, pObj ); + if ( pFanin0 && !Hop_ObjIsNone(pFanin0) && Hop_ObjRefs(pFanin0) == 0 ) + Hop_ObjDelete_rec( p, pFanin0 ); + if ( pFanin1 && !Hop_ObjIsNone(pFanin1) && Hop_ObjRefs(pFanin1) == 0 ) + Hop_ObjDelete_rec( p, pFanin1 ); +} + +/**Function************************************************************* + + Synopsis [Returns the representative of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Hop_Obj_t * Hop_ObjRepr( Hop_Obj_t * pObj ) +{ + assert( !Hop_IsComplement(pObj) ); + if ( pObj->pData == NULL || pObj->pData == pObj ) + return pObj; + return Hop_ObjRepr( pObj->pData ); +} + +/**Function************************************************************* + + Synopsis [Sets an equivalence relation between the nodes.] + + Description [Makes the representative of pNew point to the representaive of pOld.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Hop_ObjCreateChoice( Hop_Obj_t * pOld, Hop_Obj_t * pNew ) +{ + Hop_Obj_t * pOldRepr; + Hop_Obj_t * pNewRepr; + assert( pOld != NULL && pNew != NULL ); + pOldRepr = Hop_ObjRepr(pOld); + pNewRepr = Hop_ObjRepr(pNew); + if ( pNewRepr != pOldRepr ) + pNewRepr->pData = pOldRepr; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/hop/hopOper.c b/src/aig/hop/hopOper.c new file mode 100644 index 00000000..a31ca0f2 --- /dev/null +++ b/src/aig/hop/hopOper.c @@ -0,0 +1,373 @@ +/**CFile**************************************************************** + + FileName [hopOper.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Minimalistic And-Inverter Graph package.] + + Synopsis [AIG operations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: hopOper.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "hop.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +// procedure to detect an EXOR gate +static inline int Hop_ObjIsExorType( Hop_Obj_t * p0, Hop_Obj_t * p1, Hop_Obj_t ** ppFan0, Hop_Obj_t ** ppFan1 ) +{ + if ( !Hop_IsComplement(p0) || !Hop_IsComplement(p1) ) + return 0; + p0 = Hop_Regular(p0); + p1 = Hop_Regular(p1); + if ( !Hop_ObjIsAnd(p0) || !Hop_ObjIsAnd(p1) ) + return 0; + if ( Hop_ObjFanin0(p0) != Hop_ObjFanin0(p1) || Hop_ObjFanin1(p0) != Hop_ObjFanin1(p1) ) + return 0; + if ( Hop_ObjFaninC0(p0) == Hop_ObjFaninC0(p1) || Hop_ObjFaninC1(p0) == Hop_ObjFaninC1(p1) ) + return 0; + *ppFan0 = Hop_ObjChild0(p0); + *ppFan1 = Hop_ObjChild1(p0); + return 1; +} + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Returns i-th elementary variable.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Hop_Obj_t * Hop_IthVar( Hop_Man_t * p, int i ) +{ + int v; + for ( v = Hop_ManPiNum(p); v <= i; v++ ) + Hop_ObjCreatePi( p ); + assert( i < Vec_PtrSize(p->vPis) ); + return Hop_ManPi( p, i ); +} + +/**Function************************************************************* + + Synopsis [Perform one operation.] + + Description [The argument nodes can be complemented.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Hop_Obj_t * Hop_Oper( Hop_Man_t * p, Hop_Obj_t * p0, Hop_Obj_t * p1, Hop_Type_t Type ) +{ + if ( Type == AIG_AND ) + return Hop_And( p, p0, p1 ); + if ( Type == AIG_EXOR ) + return Hop_Exor( p, p0, p1 ); + assert( 0 ); + return NULL; +} + +/**Function************************************************************* + + Synopsis [Performs canonicization step.] + + Description [The argument nodes can be complemented.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Hop_Obj_t * Hop_And( Hop_Man_t * p, Hop_Obj_t * p0, Hop_Obj_t * p1 ) +{ + Hop_Obj_t * pGhost, * pResult; +// Hop_Obj_t * pFan0, * pFan1; + // check trivial cases + if ( p0 == p1 ) + return p0; + if ( p0 == Hop_Not(p1) ) + return Hop_Not(p->pConst1); + if ( Hop_Regular(p0) == p->pConst1 ) + return p0 == p->pConst1 ? p1 : Hop_Not(p->pConst1); + if ( Hop_Regular(p1) == p->pConst1 ) + return p1 == p->pConst1 ? p0 : Hop_Not(p->pConst1); + // check if it can be an EXOR gate +// if ( Hop_ObjIsExorType( p0, p1, &pFan0, &pFan1 ) ) +// return Hop_Exor( p, pFan0, pFan1 ); + // check the table + pGhost = Hop_ObjCreateGhost( p, p0, p1, AIG_AND ); + if ( pResult = Hop_TableLookup( p, pGhost ) ) + return pResult; + return Hop_ObjCreate( p, pGhost ); +} + +/**Function************************************************************* + + Synopsis [Performs canonicization step.] + + Description [The argument nodes can be complemented.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Hop_Obj_t * Hop_Exor( Hop_Man_t * p, Hop_Obj_t * p0, Hop_Obj_t * p1 ) +{ +/* + Hop_Obj_t * pGhost, * pResult; + // check trivial cases + if ( p0 == p1 ) + return Hop_Not(p->pConst1); + if ( p0 == Hop_Not(p1) ) + return p->pConst1; + if ( Hop_Regular(p0) == p->pConst1 ) + return Hop_NotCond( p1, p0 == p->pConst1 ); + if ( Hop_Regular(p1) == p->pConst1 ) + return Hop_NotCond( p0, p1 == p->pConst1 ); + // check the table + pGhost = Hop_ObjCreateGhost( p, p0, p1, AIG_EXOR ); + if ( pResult = Hop_TableLookup( p, pGhost ) ) + return pResult; + return Hop_ObjCreate( p, pGhost ); +*/ + return Hop_Or( p, Hop_And(p, p0, Hop_Not(p1)), Hop_And(p, Hop_Not(p0), p1) ); +} + +/**Function************************************************************* + + Synopsis [Implements Boolean OR.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Hop_Obj_t * Hop_Or( Hop_Man_t * p, Hop_Obj_t * p0, Hop_Obj_t * p1 ) +{ + return Hop_Not( Hop_And( p, Hop_Not(p0), Hop_Not(p1) ) ); +} + +/**Function************************************************************* + + Synopsis [Implements ITE operation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Hop_Obj_t * Hop_Mux( Hop_Man_t * p, Hop_Obj_t * pC, Hop_Obj_t * p1, Hop_Obj_t * p0 ) +{ +/* + Hop_Obj_t * pTempA1, * pTempA2, * pTempB1, * pTempB2, * pTemp; + int Count0, Count1; + // consider trivial cases + if ( p0 == Hop_Not(p1) ) + return Hop_Exor( p, pC, p0 ); + // other cases can be added + // implement the first MUX (F = C * x1 + C' * x0) + + // check for constants here!!! + + pTempA1 = Hop_TableLookup( p, Hop_ObjCreateGhost(p, pC, p1, AIG_AND) ); + pTempA2 = Hop_TableLookup( p, Hop_ObjCreateGhost(p, Hop_Not(pC), p0, AIG_AND) ); + if ( pTempA1 && pTempA2 ) + { + pTemp = Hop_TableLookup( p, Hop_ObjCreateGhost(p, Hop_Not(pTempA1), Hop_Not(pTempA2), AIG_AND) ); + if ( pTemp ) return Hop_Not(pTemp); + } + Count0 = (pTempA1 != NULL) + (pTempA2 != NULL); + // implement the second MUX (F' = C * x1' + C' * x0') + pTempB1 = Hop_TableLookup( p, Hop_ObjCreateGhost(p, pC, Hop_Not(p1), AIG_AND) ); + pTempB2 = Hop_TableLookup( p, Hop_ObjCreateGhost(p, Hop_Not(pC), Hop_Not(p0), AIG_AND) ); + if ( pTempB1 && pTempB2 ) + { + pTemp = Hop_TableLookup( p, Hop_ObjCreateGhost(p, Hop_Not(pTempB1), Hop_Not(pTempB2), AIG_AND) ); + if ( pTemp ) return pTemp; + } + Count1 = (pTempB1 != NULL) + (pTempB2 != NULL); + // compare and decide which one to implement + if ( Count0 >= Count1 ) + { + pTempA1 = pTempA1? pTempA1 : Hop_And(p, pC, p1); + pTempA2 = pTempA2? pTempA2 : Hop_And(p, Hop_Not(pC), p0); + return Hop_Or( p, pTempA1, pTempA2 ); + } + pTempB1 = pTempB1? pTempB1 : Hop_And(p, pC, Hop_Not(p1)); + pTempB2 = pTempB2? pTempB2 : Hop_And(p, Hop_Not(pC), Hop_Not(p0)); + return Hop_Not( Hop_Or( p, pTempB1, pTempB2 ) ); +*/ + return Hop_Or( p, Hop_And(p, pC, p1), Hop_And(p, Hop_Not(pC), p0) ); +} + +/**Function************************************************************* + + Synopsis [Implements ITE operation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Hop_Obj_t * Hop_Maj( Hop_Man_t * p, Hop_Obj_t * pA, Hop_Obj_t * pB, Hop_Obj_t * pC ) +{ + return Hop_Or( p, Hop_Or(p, Hop_And(p, pA, pB), Hop_And(p, pA, pC)), Hop_And(p, pB, pC) ); +} + +/**Function************************************************************* + + Synopsis [Constructs the well-balanced tree of gates.] + + Description [Disregards levels and possible logic sharing.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Hop_Obj_t * Hop_Multi_rec( Hop_Man_t * p, Hop_Obj_t ** ppObjs, int nObjs, Hop_Type_t Type ) +{ + Hop_Obj_t * pObj1, * pObj2; + if ( nObjs == 1 ) + return ppObjs[0]; + pObj1 = Hop_Multi_rec( p, ppObjs, nObjs/2, Type ); + pObj2 = Hop_Multi_rec( p, ppObjs + nObjs/2, nObjs - nObjs/2, Type ); + return Hop_Oper( p, pObj1, pObj2, Type ); +} + +/**Function************************************************************* + + Synopsis [Old code.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Hop_Obj_t * Hop_Multi( Hop_Man_t * p, Hop_Obj_t ** pArgs, int nArgs, Hop_Type_t Type ) +{ + assert( Type == AIG_AND || Type == AIG_EXOR ); + assert( nArgs > 0 ); + return Hop_Multi_rec( p, pArgs, nArgs, Type ); +} + +/**Function************************************************************* + + Synopsis [Implements the miter.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Hop_Obj_t * Hop_Miter( Hop_Man_t * p, 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] = Hop_Not( Hop_Exor( p, vPairs->pArray[i], vPairs->pArray[i+1] ) ); + vPairs->nSize = vPairs->nSize/2; + return Hop_Not( Hop_Multi_rec( p, (Hop_Obj_t **)vPairs->pArray, vPairs->nSize, AIG_AND ) ); +} + +/**Function************************************************************* + + Synopsis [Creates AND function with nVars inputs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Hop_Obj_t * Hop_CreateAnd( Hop_Man_t * p, int nVars ) +{ + Hop_Obj_t * pFunc; + int i; + pFunc = Hop_ManConst1( p ); + for ( i = 0; i < nVars; i++ ) + pFunc = Hop_And( p, pFunc, Hop_IthVar(p, i) ); + return pFunc; +} + +/**Function************************************************************* + + Synopsis [Creates AND function with nVars inputs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Hop_Obj_t * Hop_CreateOr( Hop_Man_t * p, int nVars ) +{ + Hop_Obj_t * pFunc; + int i; + pFunc = Hop_ManConst0( p ); + for ( i = 0; i < nVars; i++ ) + pFunc = Hop_Or( p, pFunc, Hop_IthVar(p, i) ); + return pFunc; +} + +/**Function************************************************************* + + Synopsis [Creates AND function with nVars inputs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Hop_Obj_t * Hop_CreateExor( Hop_Man_t * p, int nVars ) +{ + Hop_Obj_t * pFunc; + int i; + pFunc = Hop_ManConst0( p ); + for ( i = 0; i < nVars; i++ ) + pFunc = Hop_Exor( p, pFunc, Hop_IthVar(p, i) ); + return pFunc; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/hop/hopTable.c b/src/aig/hop/hopTable.c new file mode 100644 index 00000000..76390054 --- /dev/null +++ b/src/aig/hop/hopTable.c @@ -0,0 +1,262 @@ +/**CFile**************************************************************** + + FileName [hopTable.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Minimalistic And-Inverter Graph package.] + + Synopsis [Structural hashing table.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006. ] + + Revision [$Id: hopTable.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "hop.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +// hashing the node +static unsigned long Hop_Hash( Hop_Obj_t * pObj, int TableSize ) +{ + unsigned long Key = Hop_ObjIsExor(pObj) * 1699; + Key ^= Hop_ObjFanin0(pObj)->Id * 7937; + Key ^= Hop_ObjFanin1(pObj)->Id * 2971; + Key ^= Hop_ObjFaninC0(pObj) * 911; + Key ^= Hop_ObjFaninC1(pObj) * 353; + return Key % TableSize; +} + +// returns the place where this node is stored (or should be stored) +static Hop_Obj_t ** Hop_TableFind( Hop_Man_t * p, Hop_Obj_t * pObj ) +{ + Hop_Obj_t ** ppEntry; + assert( Hop_ObjChild0(pObj) && Hop_ObjChild1(pObj) ); + assert( Hop_ObjFanin0(pObj)->Id < Hop_ObjFanin1(pObj)->Id ); + for ( ppEntry = p->pTable + Hop_Hash(pObj, p->nTableSize); *ppEntry; ppEntry = &(*ppEntry)->pNext ) + if ( *ppEntry == pObj ) + return ppEntry; + assert( *ppEntry == NULL ); + return ppEntry; +} + +static void Hop_TableResize( Hop_Man_t * p ); +static unsigned int Cudd_PrimeAig( unsigned int p ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Checks if a node with the given attributes is in the hash table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Hop_Obj_t * Hop_TableLookup( Hop_Man_t * p, Hop_Obj_t * pGhost ) +{ + Hop_Obj_t * pEntry; + assert( !Hop_IsComplement(pGhost) ); + assert( Hop_ObjChild0(pGhost) && Hop_ObjChild1(pGhost) ); + assert( Hop_ObjFanin0(pGhost)->Id < Hop_ObjFanin1(pGhost)->Id ); + if ( p->fRefCount && (!Hop_ObjRefs(Hop_ObjFanin0(pGhost)) || !Hop_ObjRefs(Hop_ObjFanin1(pGhost))) ) + return NULL; + for ( pEntry = p->pTable[Hop_Hash(pGhost, p->nTableSize)]; pEntry; pEntry = pEntry->pNext ) + { + if ( Hop_ObjChild0(pEntry) == Hop_ObjChild0(pGhost) && + Hop_ObjChild1(pEntry) == Hop_ObjChild1(pGhost) && + Hop_ObjType(pEntry) == Hop_ObjType(pGhost) ) + return pEntry; + } + return NULL; +} + +/**Function************************************************************* + + Synopsis [Adds the new node to the hash table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Hop_TableInsert( Hop_Man_t * p, Hop_Obj_t * pObj ) +{ + Hop_Obj_t ** ppPlace; + assert( !Hop_IsComplement(pObj) ); + assert( Hop_TableLookup(p, pObj) == NULL ); + if ( (pObj->Id & 0xFF) == 0 && 2 * p->nTableSize < Hop_ManNodeNum(p) ) + Hop_TableResize( p ); + ppPlace = Hop_TableFind( p, pObj ); + assert( *ppPlace == NULL ); + *ppPlace = pObj; +} + +/**Function************************************************************* + + Synopsis [Deletes the node from the hash table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Hop_TableDelete( Hop_Man_t * p, Hop_Obj_t * pObj ) +{ + Hop_Obj_t ** ppPlace; + assert( !Hop_IsComplement(pObj) ); + ppPlace = Hop_TableFind( p, pObj ); + assert( *ppPlace == pObj ); // node should be in the table + // remove the node + *ppPlace = pObj->pNext; + pObj->pNext = NULL; +} + +/**Function************************************************************* + + Synopsis [Count the number of nodes in the table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Hop_TableCountEntries( Hop_Man_t * p ) +{ + Hop_Obj_t * pEntry; + int i, Counter = 0; + for ( i = 0; i < p->nTableSize; i++ ) + for ( pEntry = p->pTable[i]; pEntry; pEntry = pEntry->pNext ) + Counter++; + return Counter; +} + +/**Function************************************************************* + + Synopsis [Resizes the table.] + + Description [Typically this procedure should not be called.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Hop_TableResize( Hop_Man_t * p ) +{ + Hop_Obj_t * pEntry, * pNext; + Hop_Obj_t ** pTableOld, ** ppPlace; + int nTableSizeOld, Counter, nEntries, i, clk; +clk = clock(); + // save the old table + pTableOld = p->pTable; + nTableSizeOld = p->nTableSize; + // get the new table + p->nTableSize = Cudd_PrimeAig( 2 * Hop_ManNodeNum(p) ); + p->pTable = ALLOC( Hop_Obj_t *, p->nTableSize ); + memset( p->pTable, 0, sizeof(Hop_Obj_t *) * p->nTableSize ); + // rehash the entries from the old table + Counter = 0; + for ( i = 0; i < nTableSizeOld; i++ ) + for ( pEntry = pTableOld[i], pNext = pEntry? pEntry->pNext : NULL; pEntry; pEntry = pNext, pNext = pEntry? pEntry->pNext : NULL ) + { + // get the place where this entry goes in the table + ppPlace = Hop_TableFind( p, pEntry ); + assert( *ppPlace == NULL ); // should not be there + // add the entry to the list + *ppPlace = pEntry; + pEntry->pNext = NULL; + Counter++; + } + nEntries = Hop_ManNodeNum(p); + assert( Counter == nEntries ); +// printf( "Increasing the structural table size from %6d to %6d. ", nTableSizeOld, p->nTableSize ); +// PRT( "Time", clock() - clk ); + // replace the table and the parameters + free( pTableOld ); +} + +/**Function******************************************************************** + + Synopsis [Profiles the hash table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +void Hop_TableProfile( Hop_Man_t * p ) +{ + Hop_Obj_t * pEntry; + int i, Counter; + for ( i = 0; i < p->nTableSize; i++ ) + { + Counter = 0; + for ( pEntry = p->pTable[i]; pEntry; pEntry = pEntry->pNext ) + Counter++; + if ( Counter ) + printf( "%d ", Counter ); + } +} + +/**Function******************************************************************** + + Synopsis [Returns the next prime >= p.] + + Description [Copied from CUDD, for stand-aloneness.] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +unsigned int Cudd_PrimeAig( unsigned int p) +{ + int i,pn; + p--; + do { + p++; + if (p&1) { + pn = 1; + i = 3; + while ((unsigned) (i * i) <= p) { + if (p % i == 0) { + pn = 0; + break; + } + i += 2; + } + } else { + pn = 0; + } + } while (!pn); + return(p); + +} /* end of Cudd_Prime */ + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/hop/hopUtil.c b/src/aig/hop/hopUtil.c new file mode 100644 index 00000000..87fdb15e --- /dev/null +++ b/src/aig/hop/hopUtil.c @@ -0,0 +1,572 @@ +/**CFile**************************************************************** + + FileName [hopUtil.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: hopUtil.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "hop.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Increments the current traversal ID of the network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Hop_ManIncrementTravId( Hop_Man_t * p ) +{ + if ( p->nTravIds >= (1<<30)-1 ) + Hop_ManCleanData( p ); + p->nTravIds++; +} + +/**Function************************************************************* + + Synopsis [Cleans the data pointers for the nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Hop_ManCleanData( Hop_Man_t * p ) +{ + Hop_Obj_t * pObj; + int i; + p->nTravIds = 1; + Hop_ManConst1(p)->pData = NULL; + Hop_ManForEachPi( p, pObj, i ) + pObj->pData = NULL; + Hop_ManForEachPo( p, pObj, i ) + pObj->pData = NULL; + Hop_ManForEachNode( p, pObj, i ) + pObj->pData = NULL; +} + +/**Function************************************************************* + + Synopsis [Recursively cleans the data pointers in the cone of the node.] + + Description [Applicable to small AIGs only because no caching is performed.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Hop_ObjCleanData_rec( Hop_Obj_t * pObj ) +{ + assert( !Hop_IsComplement(pObj) ); + assert( !Hop_ObjIsPo(pObj) ); + if ( Hop_ObjIsAnd(pObj) ) + { + Hop_ObjCleanData_rec( Hop_ObjFanin0(pObj) ); + Hop_ObjCleanData_rec( Hop_ObjFanin1(pObj) ); + } + pObj->pData = NULL; +} + +/**Function************************************************************* + + Synopsis [Detects multi-input gate rooted at this node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Hop_ObjCollectMulti_rec( Hop_Obj_t * pRoot, Hop_Obj_t * pObj, Vec_Ptr_t * vSuper ) +{ + if ( pRoot != pObj && (Hop_IsComplement(pObj) || Hop_ObjIsPi(pObj) || Hop_ObjType(pRoot) != Hop_ObjType(pObj)) ) + { + Vec_PtrPushUnique(vSuper, pObj); + return; + } + Hop_ObjCollectMulti_rec( pRoot, Hop_ObjChild0(pObj), vSuper ); + Hop_ObjCollectMulti_rec( pRoot, Hop_ObjChild1(pObj), vSuper ); +} + +/**Function************************************************************* + + Synopsis [Detects multi-input gate rooted at this node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Hop_ObjCollectMulti( Hop_Obj_t * pRoot, Vec_Ptr_t * vSuper ) +{ + assert( !Hop_IsComplement(pRoot) ); + Vec_PtrClear( vSuper ); + Hop_ObjCollectMulti_rec( pRoot, pRoot, vSuper ); +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the node is the root of MUX or EXOR/NEXOR.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Hop_ObjIsMuxType( Hop_Obj_t * pNode ) +{ + Hop_Obj_t * pNode0, * pNode1; + // check that the node is regular + assert( !Hop_IsComplement(pNode) ); + // if the node is not AND, this is not MUX + if ( !Hop_ObjIsAnd(pNode) ) + return 0; + // if the children are not complemented, this is not MUX + if ( !Hop_ObjFaninC0(pNode) || !Hop_ObjFaninC1(pNode) ) + return 0; + // get children + pNode0 = Hop_ObjFanin0(pNode); + pNode1 = Hop_ObjFanin1(pNode); + // if the children are not ANDs, this is not MUX + if ( !Hop_ObjIsAnd(pNode0) || !Hop_ObjIsAnd(pNode1) ) + return 0; + // otherwise the node is MUX iff it has a pair of equal grandchildren + return (Hop_ObjFanin0(pNode0) == Hop_ObjFanin0(pNode1) && (Hop_ObjFaninC0(pNode0) ^ Hop_ObjFaninC0(pNode1))) || + (Hop_ObjFanin0(pNode0) == Hop_ObjFanin1(pNode1) && (Hop_ObjFaninC0(pNode0) ^ Hop_ObjFaninC1(pNode1))) || + (Hop_ObjFanin1(pNode0) == Hop_ObjFanin0(pNode1) && (Hop_ObjFaninC1(pNode0) ^ Hop_ObjFaninC0(pNode1))) || + (Hop_ObjFanin1(pNode0) == Hop_ObjFanin1(pNode1) && (Hop_ObjFaninC1(pNode0) ^ Hop_ObjFaninC1(pNode1))); +} + + +/**Function************************************************************* + + Synopsis [Recognizes what nodes are inputs of the EXOR.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Hop_ObjRecognizeExor( Hop_Obj_t * pObj, Hop_Obj_t ** ppFan0, Hop_Obj_t ** ppFan1 ) +{ + Hop_Obj_t * p0, * p1; + assert( !Hop_IsComplement(pObj) ); + if ( !Hop_ObjIsNode(pObj) ) + return 0; + if ( Hop_ObjIsExor(pObj) ) + { + *ppFan0 = Hop_ObjChild0(pObj); + *ppFan1 = Hop_ObjChild1(pObj); + return 1; + } + assert( Hop_ObjIsAnd(pObj) ); + p0 = Hop_ObjChild0(pObj); + p1 = Hop_ObjChild1(pObj); + if ( !Hop_IsComplement(p0) || !Hop_IsComplement(p1) ) + return 0; + p0 = Hop_Regular(p0); + p1 = Hop_Regular(p1); + if ( !Hop_ObjIsAnd(p0) || !Hop_ObjIsAnd(p1) ) + return 0; + if ( Hop_ObjFanin0(p0) != Hop_ObjFanin0(p1) || Hop_ObjFanin1(p0) != Hop_ObjFanin1(p1) ) + return 0; + if ( Hop_ObjFaninC0(p0) == Hop_ObjFaninC0(p1) || Hop_ObjFaninC1(p0) == Hop_ObjFaninC1(p1) ) + return 0; + *ppFan0 = Hop_ObjChild0(p0); + *ppFan1 = Hop_ObjChild1(p0); + return 1; +} + +/**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 [] + +***********************************************************************/ +Hop_Obj_t * Hop_ObjRecognizeMux( Hop_Obj_t * pNode, Hop_Obj_t ** ppNodeT, Hop_Obj_t ** ppNodeE ) +{ + Hop_Obj_t * pNode0, * pNode1; + assert( !Hop_IsComplement(pNode) ); + assert( Hop_ObjIsMuxType(pNode) ); + // get children + pNode0 = Hop_ObjFanin0(pNode); + pNode1 = Hop_ObjFanin1(pNode); + + // find the control variable + if ( Hop_ObjFanin1(pNode0) == Hop_ObjFanin1(pNode1) && (Hop_ObjFaninC1(pNode0) ^ Hop_ObjFaninC1(pNode1)) ) + { +// if ( Fraig_IsComplement(pNode1->p2) ) + if ( Hop_ObjFaninC1(pNode0) ) + { // pNode2->p2 is positive phase of C + *ppNodeT = Hop_Not(Hop_ObjChild0(pNode1));//pNode2->p1); + *ppNodeE = Hop_Not(Hop_ObjChild0(pNode0));//pNode1->p1); + return Hop_ObjChild1(pNode1);//pNode2->p2; + } + else + { // pNode1->p2 is positive phase of C + *ppNodeT = Hop_Not(Hop_ObjChild0(pNode0));//pNode1->p1); + *ppNodeE = Hop_Not(Hop_ObjChild0(pNode1));//pNode2->p1); + return Hop_ObjChild1(pNode0);//pNode1->p2; + } + } + else if ( Hop_ObjFanin0(pNode0) == Hop_ObjFanin0(pNode1) && (Hop_ObjFaninC0(pNode0) ^ Hop_ObjFaninC0(pNode1)) ) + { +// if ( Fraig_IsComplement(pNode1->p1) ) + if ( Hop_ObjFaninC0(pNode0) ) + { // pNode2->p1 is positive phase of C + *ppNodeT = Hop_Not(Hop_ObjChild1(pNode1));//pNode2->p2); + *ppNodeE = Hop_Not(Hop_ObjChild1(pNode0));//pNode1->p2); + return Hop_ObjChild0(pNode1);//pNode2->p1; + } + else + { // pNode1->p1 is positive phase of C + *ppNodeT = Hop_Not(Hop_ObjChild1(pNode0));//pNode1->p2); + *ppNodeE = Hop_Not(Hop_ObjChild1(pNode1));//pNode2->p2); + return Hop_ObjChild0(pNode0);//pNode1->p1; + } + } + else if ( Hop_ObjFanin0(pNode0) == Hop_ObjFanin1(pNode1) && (Hop_ObjFaninC0(pNode0) ^ Hop_ObjFaninC1(pNode1)) ) + { +// if ( Fraig_IsComplement(pNode1->p1) ) + if ( Hop_ObjFaninC0(pNode0) ) + { // pNode2->p2 is positive phase of C + *ppNodeT = Hop_Not(Hop_ObjChild0(pNode1));//pNode2->p1); + *ppNodeE = Hop_Not(Hop_ObjChild1(pNode0));//pNode1->p2); + return Hop_ObjChild1(pNode1);//pNode2->p2; + } + else + { // pNode1->p1 is positive phase of C + *ppNodeT = Hop_Not(Hop_ObjChild1(pNode0));//pNode1->p2); + *ppNodeE = Hop_Not(Hop_ObjChild0(pNode1));//pNode2->p1); + return Hop_ObjChild0(pNode0);//pNode1->p1; + } + } + else if ( Hop_ObjFanin1(pNode0) == Hop_ObjFanin0(pNode1) && (Hop_ObjFaninC1(pNode0) ^ Hop_ObjFaninC0(pNode1)) ) + { +// if ( Fraig_IsComplement(pNode1->p2) ) + if ( Hop_ObjFaninC1(pNode0) ) + { // pNode2->p1 is positive phase of C + *ppNodeT = Hop_Not(Hop_ObjChild1(pNode1));//pNode2->p2); + *ppNodeE = Hop_Not(Hop_ObjChild0(pNode0));//pNode1->p1); + return Hop_ObjChild0(pNode1);//pNode2->p1; + } + else + { // pNode1->p2 is positive phase of C + *ppNodeT = Hop_Not(Hop_ObjChild0(pNode0));//pNode1->p1); + *ppNodeE = Hop_Not(Hop_ObjChild1(pNode1));//pNode2->p2); + return Hop_ObjChild1(pNode0);//pNode1->p2; + } + } + assert( 0 ); // this is not MUX + return NULL; +} + + +/**Function************************************************************* + + Synopsis [Prints Eqn formula for the AIG rooted at this node.] + + Description [The formula is in terms of PIs, which should have + their names assigned in pObj->pData fields.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Hop_ObjPrintEqn( FILE * pFile, Hop_Obj_t * pObj, Vec_Vec_t * vLevels, int Level ) +{ + Vec_Ptr_t * vSuper; + Hop_Obj_t * pFanin; + int fCompl, i; + // store the complemented attribute + fCompl = Hop_IsComplement(pObj); + pObj = Hop_Regular(pObj); + // constant case + if ( Hop_ObjIsConst1(pObj) ) + { + fprintf( pFile, "%d", !fCompl ); + return; + } + // PI case + if ( Hop_ObjIsPi(pObj) ) + { + fprintf( pFile, "%s%s", fCompl? "!" : "", pObj->pData ); + return; + } + // AND case + Vec_VecExpand( vLevels, Level ); + vSuper = Vec_VecEntry(vLevels, Level); + Hop_ObjCollectMulti( pObj, vSuper ); + fprintf( pFile, "%s", (Level==0? "" : "(") ); + Vec_PtrForEachEntry( vSuper, pFanin, i ) + { + Hop_ObjPrintEqn( pFile, Hop_NotCond(pFanin, fCompl), vLevels, Level+1 ); + if ( i < Vec_PtrSize(vSuper) - 1 ) + fprintf( pFile, " %s ", fCompl? "+" : "*" ); + } + fprintf( pFile, "%s", (Level==0? "" : ")") ); + return; +} + +/**Function************************************************************* + + Synopsis [Prints Verilog formula for the AIG rooted at this node.] + + Description [The formula is in terms of PIs, which should have + their names assigned in pObj->pData fields.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Hop_ObjPrintVerilog( FILE * pFile, Hop_Obj_t * pObj, Vec_Vec_t * vLevels, int Level ) +{ + Vec_Ptr_t * vSuper; + Hop_Obj_t * pFanin, * pFanin0, * pFanin1, * pFaninC; + int fCompl, i; + // store the complemented attribute + fCompl = Hop_IsComplement(pObj); + pObj = Hop_Regular(pObj); + // constant case + if ( Hop_ObjIsConst1(pObj) ) + { + fprintf( pFile, "1\'b%d", !fCompl ); + return; + } + // PI case + if ( Hop_ObjIsPi(pObj) ) + { + fprintf( pFile, "%s%s", fCompl? "~" : "", pObj->pData ); + return; + } + // EXOR case + if ( Hop_ObjIsExor(pObj) ) + { + Vec_VecExpand( vLevels, Level ); + vSuper = Vec_VecEntry( vLevels, Level ); + Hop_ObjCollectMulti( pObj, vSuper ); + fprintf( pFile, "%s", (Level==0? "" : "(") ); + Vec_PtrForEachEntry( vSuper, pFanin, i ) + { + Hop_ObjPrintVerilog( pFile, Hop_NotCond(pFanin, (fCompl && i==0)), vLevels, Level+1 ); + if ( i < Vec_PtrSize(vSuper) - 1 ) + fprintf( pFile, " ^ " ); + } + fprintf( pFile, "%s", (Level==0? "" : ")") ); + return; + } + // MUX case + if ( Hop_ObjIsMuxType(pObj) ) + { + if ( Hop_ObjRecognizeExor( pObj, &pFanin0, &pFanin1 ) ) + { + fprintf( pFile, "%s", (Level==0? "" : "(") ); + Hop_ObjPrintVerilog( pFile, Hop_NotCond(pFanin0, fCompl), vLevels, Level+1 ); + fprintf( pFile, " ^ " ); + Hop_ObjPrintVerilog( pFile, pFanin1, vLevels, Level+1 ); + fprintf( pFile, "%s", (Level==0? "" : ")") ); + } + else + { + pFaninC = Hop_ObjRecognizeMux( pObj, &pFanin1, &pFanin0 ); + fprintf( pFile, "%s", (Level==0? "" : "(") ); + Hop_ObjPrintVerilog( pFile, pFaninC, vLevels, Level+1 ); + fprintf( pFile, " ? " ); + Hop_ObjPrintVerilog( pFile, Hop_NotCond(pFanin1, fCompl), vLevels, Level+1 ); + fprintf( pFile, " : " ); + Hop_ObjPrintVerilog( pFile, Hop_NotCond(pFanin0, fCompl), vLevels, Level+1 ); + fprintf( pFile, "%s", (Level==0? "" : ")") ); + } + return; + } + // AND case + Vec_VecExpand( vLevels, Level ); + vSuper = Vec_VecEntry(vLevels, Level); + Hop_ObjCollectMulti( pObj, vSuper ); + fprintf( pFile, "%s", (Level==0? "" : "(") ); + Vec_PtrForEachEntry( vSuper, pFanin, i ) + { + Hop_ObjPrintVerilog( pFile, Hop_NotCond(pFanin, fCompl), vLevels, Level+1 ); + if ( i < Vec_PtrSize(vSuper) - 1 ) + fprintf( pFile, " %s ", fCompl? "|" : "&" ); + } + fprintf( pFile, "%s", (Level==0? "" : ")") ); + return; +} + + +/**Function************************************************************* + + Synopsis [Prints node in HAIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Hop_ObjPrintVerbose( Hop_Obj_t * pObj, int fHaig ) +{ + assert( !Hop_IsComplement(pObj) ); + printf( "Node %p : ", pObj ); + if ( Hop_ObjIsConst1(pObj) ) + printf( "constant 1" ); + else if ( Hop_ObjIsPi(pObj) ) + printf( "PI" ); + else + printf( "AND( %p%s, %p%s )", + Hop_ObjFanin0(pObj), (Hop_ObjFaninC0(pObj)? "\'" : " "), + Hop_ObjFanin1(pObj), (Hop_ObjFaninC1(pObj)? "\'" : " ") ); + printf( " (refs = %3d)", Hop_ObjRefs(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Prints node in HAIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Hop_ManPrintVerbose( Hop_Man_t * p, int fHaig ) +{ + Vec_Ptr_t * vNodes; + Hop_Obj_t * pObj; + int i; + printf( "PIs: " ); + Hop_ManForEachPi( p, pObj, i ) + printf( " %p", pObj ); + printf( "\n" ); + vNodes = Hop_ManDfs( p ); + Vec_PtrForEachEntry( vNodes, pObj, i ) + Hop_ObjPrintVerbose( pObj, fHaig ), printf( "\n" ); + printf( "\n" ); +} + +/**Function************************************************************* + + Synopsis [Writes the AIG into the BLIF file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Hop_ManDumpBlif( Hop_Man_t * p, char * pFileName ) +{ + FILE * pFile; + Vec_Ptr_t * vNodes; + Hop_Obj_t * pObj, * pConst1 = NULL; + int i, nDigits, Counter = 0; + if ( Hop_ManPoNum(p) == 0 ) + { + printf( "Hop_ManDumpBlif(): AIG manager does not have POs.\n" ); + return; + } + // collect nodes in the DFS order + vNodes = Hop_ManDfs( p ); + // assign IDs to objects + Hop_ManConst1(p)->pData = (void *)Counter++; + Hop_ManForEachPi( p, pObj, i ) + pObj->pData = (void *)Counter++; + Hop_ManForEachPo( p, pObj, i ) + pObj->pData = (void *)Counter++; + Vec_PtrForEachEntry( vNodes, pObj, i ) + pObj->pData = (void *)Counter++; + nDigits = Hop_Base10Log( Counter ); + // write the file + pFile = fopen( pFileName, "w" ); + fprintf( pFile, "# BLIF file written by procedure Hop_ManDumpBlif() in ABC\n" ); + fprintf( pFile, "# http://www.eecs.berkeley.edu/~alanmi/abc/\n" ); + fprintf( pFile, ".model test\n" ); + // write PIs + fprintf( pFile, ".inputs" ); + Hop_ManForEachPi( p, pObj, i ) + fprintf( pFile, " n%0*d", nDigits, (int)pObj->pData ); + fprintf( pFile, "\n" ); + // write POs + fprintf( pFile, ".outputs" ); + Hop_ManForEachPo( p, pObj, i ) + fprintf( pFile, " n%0*d", nDigits, (int)pObj->pData ); + fprintf( pFile, "\n" ); + // write nodes + Vec_PtrForEachEntry( vNodes, pObj, i ) + { + fprintf( pFile, ".names n%0*d n%0*d n%0*d\n", + nDigits, (int)Hop_ObjFanin0(pObj)->pData, + nDigits, (int)Hop_ObjFanin1(pObj)->pData, + nDigits, (int)pObj->pData ); + fprintf( pFile, "%d%d 1\n", !Hop_ObjFaninC0(pObj), !Hop_ObjFaninC1(pObj) ); + } + // write POs + Hop_ManForEachPo( p, pObj, i ) + { + fprintf( pFile, ".names n%0*d n%0*d\n", + nDigits, (int)Hop_ObjFanin0(pObj)->pData, + nDigits, (int)pObj->pData ); + fprintf( pFile, "%d 1\n", !Hop_ObjFaninC0(pObj) ); + if ( Hop_ObjIsConst1(Hop_ObjFanin0(pObj)) ) + pConst1 = Hop_ManConst1(p); + } + if ( pConst1 ) + fprintf( pFile, ".names n%0*d\n 1\n", nDigits, (int)pConst1->pData ); + fprintf( pFile, ".end\n\n" ); + fclose( pFile ); + Vec_PtrFree( vNodes ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/hop/hop_.c b/src/aig/hop/hop_.c new file mode 100644 index 00000000..468413fa --- /dev/null +++ b/src/aig/hop/hop_.c @@ -0,0 +1,48 @@ +/**CFile**************************************************************** + + FileName [ivy_.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Minimalistic 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/aig/hop/module.make b/src/aig/hop/module.make new file mode 100644 index 00000000..b06d91fd --- /dev/null +++ b/src/aig/hop/module.make @@ -0,0 +1,9 @@ +SRC += src/aig/hop/hopBalance.c \ + src/aig/hop/hopCheck.c \ + src/aig/hop/hopDfs.c \ + src/aig/hop/hopMan.c \ + src/aig/hop/hopMem.c \ + src/aig/hop/hopObj.c \ + src/aig/hop/hopOper.c \ + src/aig/hop/hopTable.c \ + src/aig/hop/hopUtil.c -- cgit v1.2.3