/**CFile**************************************************************** FileName [aig.h] SystemName [ABC: Logic synthesis and verification system.] PackageName [And-Inverter Graph package.] Synopsis [External declarations.] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - June 20, 2005.] Revision [$Id: aig.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ #ifndef __AIG_H__ #define __AIG_H__ /* AIG is an And-Inv Graph with structural hashing. It is always structurally hashed. It means that at any time: - for each AND gate, there are no other AND gates with the same children - the constants are propagated - there is no single-input nodes (inverters/buffers) Additionally the following invariants are satisfied: - there are no dangling nodes (the nodes without fanout) - the level of each AND gate reflects the levels of this fanins - the AND nodes are in the topological order - the constant 1 node has always number 0 in the object list The operations that are performed on AIGs: - building new nodes (Aig_And) - performing elementary Boolean operations (Aig_Or, Aig_Xor, etc) - replacing one node by another (Abc_AigReplace) - propagating constants (Abc_AigReplace) - deleting dangling nodes (Abc_AigDelete) When AIG is duplicated, the new graph is structurally hashed too. If this repeated hashing leads to fewer nodes, it means the original AIG was not strictly hashed (one of the conditions above is violated). */ //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// #include #include "vec.h" //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////// /// BASIC TYPES /// //////////////////////////////////////////////////////////////////////// //typedef int bool; #ifndef bool #define bool int #endif typedef struct Aig_Param_t_ Aig_Param_t; typedef struct Aig_Man_t_ Aig_Man_t; typedef struct Aig_Node_t_ Aig_Node_t; typedef struct Aig_Edge_t_ Aig_Edge_t; typedef struct Aig_MemFixed_t_ Aig_MemFixed_t; typedef struct Aig_SimInfo_t_ Aig_SimInfo_t; typedef struct Aig_Table_t_ Aig_Table_t; // network types typedef enum { AIG_NONE = 0, // 0: unknown AIG_PI, // 1: primary input AIG_PO, // 2: primary output AIG_AND // 3: internal node } Aig_NodeType_t; // the AIG parameters struct Aig_Param_t_ { int nPatsRand; // the number of random patterns int nBTLimit; // backtrack limit at the intermediate nodes int nSeconds; // the runtime limit at the final miter }; // the AIG edge struct Aig_Edge_t_ { unsigned iNode : 31; // the node unsigned fComp : 1; // the complemented attribute }; // the AIG node struct Aig_Node_t_ // 8 words { // various numbers associated with the node int Id; // the unique number (SAT var number) of this node int nRefs; // the reference counter unsigned Type : 2; // the node type unsigned fPhase : 1; // the phase of this node unsigned fMarkA : 1; // the mask unsigned fMarkB : 1; // the mask unsigned fMarkC : 1; // the mask unsigned TravId : 26; // the traversal ID unsigned Level : 16; // the direct level of the node unsigned LevelR : 16; // the reverse level of the node Aig_Edge_t Fans[2]; // the fanins int NextH; // next node in the hash table int Data; // miscelleneous data Aig_Man_t * pMan; // the parent manager }; // the AIG manager struct Aig_Man_t_ { // the AIG parameters Aig_Param_t Param; // the full set of AIG parameters Aig_Param_t * pParam; // the pointer to the above set // the nodes Aig_Node_t * pConst1; // the constant 1 node (ID=0) Vec_Ptr_t * vNodes; // all nodes by ID Vec_Ptr_t * vPis; // all PIs Vec_Ptr_t * vPos; // all POs Aig_Table_t * pTable; // structural hash table int nLevelMax; // the maximum level // fanout representation Vec_Ptr_t * vFanPivots; // fanout pivots Vec_Ptr_t * vFanFans0; // the next fanout of the first fanin Vec_Ptr_t * vFanFans1; // the next fanout of the second fanin // the memory managers Aig_MemFixed_t * mmNodes; // the memory manager for nodes int nTravIds; // the traversal ID // simulation info Aig_SimInfo_t * pInfo; // random and systematic sim info for PIs Aig_SimInfo_t * pInfoTemp; // temporary sim info for all nodes // simulation patterns int nPiWords; // the number of words in the PI info int nPatsMax; // the max number of patterns Vec_Ptr_t * vPats; // simulation patterns to try // equivalence classes Vec_Vec_t * vClasses; // the non-trival equivalence classes of nodes // temporary data Vec_Ptr_t * vFanouts; // temporary storage for fanouts of a node Vec_Ptr_t * vToReplace; // the nodes to replace }; // the AIG simulation info struct Aig_SimInfo_t_ { int Type; // the type (0 = PI, 1 = all) int nNodes; // the number of nodes for which allocated int nWords; // the number of words for each node int nPatsMax; // the maximum number of patterns int nPatsCur; // the current number of patterns unsigned * pData; // the simulation data }; // iterators over nodes, PIs, POs, ANDs #define Aig_ManForEachNode( pMan, pNode, i ) \ for ( i = 0; (i < Aig_ManNodeNum(pMan)) && (((pNode) = Aig_ManNode(pMan, i)), 1); i++ ) #define Aig_ManForEachPi( pMan, pNode, i ) \ for ( i = 0; (i < Aig_ManPiNum(pMan)) && (((pNode) = Aig_ManPi(pMan, i)), 1); i++ ) #define Aig_ManForEachPo( pMan, pNode, i ) \ for ( i = 0; (i < Aig_ManPoNum(pMan)) && (((pNode) = Aig_ManPo(pMan, i)), 1); i++ ) #define Aig_ManForEachAnd( pNtk, pNode, i ) \ for ( i = 0; (i < Aig_ManNodeNum(pMan)) && (((pNode) = Aig_ManNode(pMan, i)), 1); i++ ) \ if ( Aig_NodeIsAnd(pNode) ) {} else // maximum/minimum operators #define AIG_MIN(a,b) (((a) < (b))? (a) : (b)) #define AIG_MAX(a,b) (((a) > (b))? (a) : (b)) //////////////////////////////////////////////////////////////////////// /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// static inline int Aig_BitWordNum( int nBits ) { return nBits/32 + ((nBits%32) > 0); } static inline Aig_Node_t * Aig_ManNode( Aig_Man_t * pMan, int i ) { return Vec_PtrEntry(pMan->vNodes, i); } static inline Aig_Node_t * Aig_ManPi( Aig_Man_t * pMan, int i ) { return Vec_PtrEntry(pMan->vPis, i); } static inline Aig_Node_t * Aig_ManPo( Aig_Man_t * pMan, int i ) { return Vec_PtrEntry(pMan->vPos, i); } static inline int Aig_ManNodeNum( Aig_Man_t * pMan ) { return Vec_PtrSize(pMan->vNodes); } static inline int Aig_ManPiNum( Aig_Man_t * pMan ) { return Vec_PtrSize(pMan->vPis); } static inline int Aig_ManPoNum( Aig_Man_t * pMan ) { return Vec_PtrSize(pMan->vPos); } static inline int Aig_ManAndNum( Aig_Man_t * pMan ) { return Aig_ManNodeNum(pMan)-Aig_ManPiNum(pMan)-Aig_ManPoNum(pMan)-1; } static inline Aig_Node_t * Aig_Regular( Aig_Node_t * p ) { return (Aig_Node_t *)((unsigned)(p) & ~01); } static inline Aig_Node_t * Aig_Not( Aig_Node_t * p ) { return (Aig_Node_t *)((unsigned)(p) ^ 01); } static inline Aig_Node_t * Aig_NotCond( Aig_Node_t * p, int c ) { return (Aig_Node_t *)((unsigned)(p) ^ (c)); } static inline bool Aig_IsComplement( Aig_Node_t * p ) { return (bool)(((unsigned)p) & 01); } static inline bool Aig_NodeIsConst( Aig_Node_t * pNode ) { return Aig_Regular(pNode)->Id == 0; } static inline bool Aig_NodeIsPi( Aig_Node_t * pNode ) { return Aig_Regular(pNode)->Type == AIG_PI; } static inline bool Aig_NodeIsPo( Aig_Node_t * pNode ) { return Aig_Regular(pNode)->Type == AIG_PO; } static inline bool Aig_NodeIsAnd( Aig_Node_t * pNode ) { return Aig_Regular(pNode)->Type == AIG_AND; } static inline int Aig_NodeId( Aig_Node_t * pNode ) { assert( !Aig_IsComplement(pNode) ); return pNode->Id; } static inline int Aig_NodeRefs( Aig_Node_t * pNode ) { assert( !Aig_IsComplement(pNode) ); return pNode->nRefs; } static inline bool Aig_NodePhase( Aig_Node_t * pNode ) { assert( !Aig_IsComplement(pNode) ); return pNode->fPhase; } static inline int Aig_NodeLevel( Aig_Node_t * pNode ) { assert( !Aig_IsComplement(pNode) ); return pNode->Level; } static inline int Aig_NodeLevelR( Aig_Node_t * pNode ) { assert( !Aig_IsComplement(pNode) ); return pNode->LevelR; } static inline int Aig_NodeData( Aig_Node_t * pNode ) { assert( !Aig_IsComplement(pNode) ); return pNode->Data; } static inline Aig_Man_t * Aig_NodeMan( Aig_Node_t * pNode ) { assert( !Aig_IsComplement(pNode) ); return pNode->pMan; } static inline int Aig_NodeFaninId0( Aig_Node_t * pNode ) { assert( !Aig_IsComplement(pNode) ); return pNode->Fans[0].iNode; } static inline int Aig_NodeFaninId1( Aig_Node_t * pNode ) { assert( !Aig_IsComplement(pNode) ); return pNode->Fans[1].iNode; } static inline bool Aig_NodeFaninC0( Aig_Node_t * pNode ) { assert( !Aig_IsComplement(pNode) ); return pNode->Fans[0].fComp; } static inline bool Aig_NodeFaninC1( Aig_Node_t * pNode ) { assert( !Aig_IsComplement(pNode) ); return pNode->Fans[1].fComp; } static inline Aig_Node_t * Aig_NodeFanin0( Aig_Node_t * pNode ) { return Aig_ManNode( Aig_NodeMan(pNode), Aig_NodeFaninId0(pNode) ); } static inline Aig_Node_t * Aig_NodeFanin1( Aig_Node_t * pNode ) { return Aig_ManNode( Aig_NodeMan(pNode), Aig_NodeFaninId1(pNode) ); } static inline Aig_Node_t * Aig_NodeChild0( Aig_Node_t * pNode ) { return Aig_NotCond( Aig_NodeFanin0(pNode), Aig_NodeFaninC0(pNode) ); } static inline Aig_Node_t * Aig_NodeChild1( Aig_Node_t * pNode ) { return Aig_NotCond( Aig_NodeFanin1(pNode), Aig_NodeFaninC1(pNode) ); } static inline Aig_Node_t * Aig_NodeNextH( Aig_Node_t * pNode ) { return pNode->NextH? Aig_ManNode(pNode->pMan, pNode->NextH) : NULL; } static inline int Aig_NodeWhatFanin( Aig_Node_t * pNode, Aig_Node_t * pFanin ) { if ( Aig_NodeFaninId0(pNode) == pFanin->Id ) return 0; if ( Aig_NodeFaninId1(pNode) == pFanin->Id ) return 1; assert(0); return -1; } static inline int Aig_NodeGetLevelNew( Aig_Node_t * pNode ) { return 1 + AIG_MAX(Aig_NodeFanin0(pNode)->Level, Aig_NodeFanin1(pNode)->Level); } static inline unsigned * Aig_SimInfoForNode( Aig_SimInfo_t * p, Aig_Node_t * pNode ) { assert( p->Type ); return p->pData + p->nWords * pNode->Id; } static inline unsigned * Aig_SimInfoForPi( Aig_SimInfo_t * p, int Num ) { assert( !p->Type ); return p->pData + p->nWords * Num; } static inline void Aig_NodeSetTravId( Aig_Node_t * pNode, int TravId ) { pNode->TravId = TravId; } static inline void Aig_NodeSetTravIdCurrent( Aig_Node_t * pNode ) { pNode->TravId = pNode->pMan->nTravIds; } static inline void Aig_NodeSetTravIdPrevious( Aig_Node_t * pNode ) { pNode->TravId = pNode->pMan->nTravIds - 1; } static inline bool Aig_NodeIsTravIdCurrent( Aig_Node_t * pNode ) { return (bool)((int)pNode->TravId == pNode->pMan->nTravIds); } static inline bool Aig_NodeIsTravIdPrevious( Aig_Node_t * pNode ) { return (bool)((int)pNode->TravId == pNode->pMan->nTravIds - 1); } //////////////////////////////////////////////////////////////////////// /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// /*=== aigCheck.c ==========================================================*/ extern bool Aig_ManCheck( Aig_Man_t * pMan ); extern bool Aig_NodeIsAcyclic( Aig_Node_t * pNode, Aig_Node_t * pRoot ); /*=== aigFanout.c ==========================================================*/ extern void Aig_ManCreateFanouts( Aig_Man_t * p ); extern void Aig_NodeAddFaninFanout( Aig_Node_t * pFanin, Aig_Node_t * pFanout ); extern void Aig_NodeRemoveFaninFanout( Aig_Node_t * pFanin, Aig_Node_t * pFanoutToRemove ); extern int Aig_NodeGetFanoutNum( Aig_Node_t * pNode ); extern Vec_Ptr_t * Aig_NodeGetFanouts( Aig_Node_t * pNode ); extern int Aig_NodeGetLevelRNew( Aig_Node_t * pNode ); extern int Aig_ManSetLevelR( Aig_Man_t * pMan ); extern int Aig_ManGetLevelMax( Aig_Man_t * pMan ); extern int Aig_NodeUpdateLevel_int( Aig_Node_t * pNode ); extern int Aig_NodeUpdateLevelR_int( Aig_Node_t * pNode ); /*=== aigMem.c =============================================================*/ extern Aig_MemFixed_t * Aig_MemFixedStart( int nEntrySize ); extern void Aig_MemFixedStop( Aig_MemFixed_t * p, int fVerbose ); extern char * Aig_MemFixedEntryFetch( Aig_MemFixed_t * p ); extern void Aig_MemFixedEntryRecycle( Aig_MemFixed_t * p, char * pEntry ); extern void Aig_MemFixedRestart( Aig_MemFixed_t * p ); extern int Aig_MemFixedReadMemUsage( Aig_MemFixed_t * p ); /*=== aigMan.c =============================================================*/ extern void Aig_ManSetDefaultParams( Aig_Param_t * pParam ); extern Aig_Man_t * Aig_ManStart( Aig_Param_t * pParam ); extern int Aig_ManCleanup( Aig_Man_t * pMan ); extern void Aig_ManStop( Aig_Man_t * p ); /*=== aigNode.c =============================================================*/ extern Aig_Node_t * Aig_NodeCreateConst( Aig_Man_t * p ); extern Aig_Node_t * Aig_NodeCreatePi( Aig_Man_t * p ); extern Aig_Node_t * Aig_NodeCreatePo( Aig_Man_t * p, Aig_Node_t * pFanin ); extern Aig_Node_t * Aig_NodeCreateAnd( Aig_Man_t * p, Aig_Node_t * pFanin0, Aig_Node_t * pFanin1 ); extern void Aig_NodeConnectAnd( Aig_Node_t * pFanin0, Aig_Node_t * pFanin1, Aig_Node_t * pNode ); extern void Aig_NodeDisconnectAnd( Aig_Node_t * pNode ); extern void Aig_NodeDeleteAnd_rec( Aig_Man_t * pMan, Aig_Node_t * pRoot ); extern void Aig_NodePrint( Aig_Node_t * pNode ); extern char * Aig_NodeName( Aig_Node_t * pNode ); /*=== aigOper.c ==========================================================*/ extern Aig_Node_t * Aig_And( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1 ); extern Aig_Node_t * Aig_Or( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1 ); extern Aig_Node_t * Aig_Xor( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1 ); extern Aig_Node_t * Aig_Mux( Aig_Man_t * pMan, Aig_Node_t * pC, Aig_Node_t * p1, Aig_Node_t * p0 ); extern Aig_Node_t * Aig_Miter( Aig_Man_t * pMan, Vec_Ptr_t * vPairs ); /*=== aigReplace.c ==========================================================*/ extern void Aig_ManReplaceNode( Aig_Man_t * pMan, Aig_Node_t * pOld, Aig_Node_t * pNew, int fUpdateLevel ); /*=== aigTable.c ==========================================================*/ extern Aig_Table_t * Aig_TableCreate( int nSize ); extern void Aig_TableFree( Aig_Table_t * p ); extern int Aig_TableNumNodes( Aig_Table_t * p ); extern Aig_Node_t * Aig_TableLookupNode( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1 ); extern Aig_Node_t * Aig_TableInsertNode( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1, Aig_Node_t * pAnd ); extern void Aig_TableDeleteNode( Aig_Man_t * pMan, Aig_Node_t * pThis ); extern void Aig_TableResize( Aig_Man_t * pMan ); extern void Aig_TableRehash( Aig_Man_t * pMan ); /*=== aigUtil.c ==========================================================*/ extern void Aig_ManIncrementTravId( Aig_Man_t * pMan ); extern void Aig_PrintNode( Aig_Node_t * pNode ); /*=== fraigClasses.c ==========================================================*/ extern Vec_Vec_t * Aig_ManDeriveClassesFirst( Aig_Man_t * p, Aig_SimInfo_t * pInfoAll ); /*=== fraigSim.c ==========================================================*/ extern Aig_SimInfo_t * Aig_SimInfoAlloc( int nNodes, int nWords, int Type ); extern void Aig_SimInfoClean( Aig_SimInfo_t * p ); extern void Aig_SimInfoRandom( Aig_SimInfo_t * p ); extern void Aig_SimInfoResize( Aig_SimInfo_t * p ); extern void Aig_SimInfoFree( Aig_SimInfo_t * p ); extern Aig_SimInfo_t * Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi ); //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// #endif