diff options
Diffstat (limited to 'src/temp/ivy')
| -rw-r--r-- | src/temp/ivy/ivy.h | 76 | ||||
| -rw-r--r-- | src/temp/ivy/ivyBalance.c | 409 | ||||
| -rw-r--r-- | src/temp/ivy/ivyCut.c | 548 | ||||
| -rw-r--r-- | src/temp/ivy/ivyDfs.c | 133 | ||||
| -rw-r--r-- | src/temp/ivy/ivyMan.c | 8 | ||||
| -rw-r--r-- | src/temp/ivy/ivyMulti.c | 504 | ||||
| -rw-r--r-- | src/temp/ivy/ivyMulti8.c | 427 | ||||
| -rw-r--r-- | src/temp/ivy/ivyObj.c | 1 | ||||
| -rw-r--r-- | src/temp/ivy/ivyOper.c | 6 | ||||
| -rw-r--r-- | src/temp/ivy/ivyResyn.c | 96 | ||||
| -rw-r--r-- | src/temp/ivy/ivyRwrAlg.c | 408 | ||||
| -rw-r--r-- | src/temp/ivy/ivyRwrPre.c | 597 | ||||
| -rw-r--r-- | src/temp/ivy/ivyUtil.c | 216 | ||||
| -rw-r--r-- | src/temp/ivy/module.make | 3 |
14 files changed, 2695 insertions, 737 deletions
diff --git a/src/temp/ivy/ivy.h b/src/temp/ivy/ivy.h index 55ada384..57d8cfd2 100644 --- a/src/temp/ivy/ivy.h +++ b/src/temp/ivy/ivy.h @@ -42,6 +42,11 @@ extern "C" { typedef struct Ivy_Man_t_ Ivy_Man_t; typedef struct Ivy_Obj_t_ Ivy_Obj_t; +typedef int Ivy_Edge_t; + +// constant edges +#define IVY_CONST0 1 +#define IVY_CONST1 0 // object types typedef enum { @@ -102,10 +107,12 @@ struct Ivy_Man_t_ int * pTable; // structural hash table int nTableSize; // structural hash table size // various data members + int fCatchExor; // set to 1 to detect EXORs int fExtended; // set to 1 in extended mode int nTravIds; // the traversal ID int nLevelMax; // the maximum level void * pData; // the temporary data + Vec_Int_t * vRequired; // required times // truth table of the 8-LUTs unsigned * pMemory; // memory for truth tables Vec_Int_t * vTruths; // offset for truth table of each node @@ -118,6 +125,26 @@ struct Ivy_Man_t_ }; +#define IVY_CUT_LIMIT 256 +#define IVY_CUT_INPUT 6 + +typedef struct Ivy_Cut_t_ Ivy_Cut_t; +struct Ivy_Cut_t_ +{ + short nSize; + short nSizeMax; + int pArray[IVY_CUT_INPUT]; + unsigned uHash; +}; + +typedef struct Ivy_Store_t_ Ivy_Store_t; +struct Ivy_Store_t_ +{ + int nCuts; + int nCutsMax; + Ivy_Cut_t pCuts[IVY_CUT_LIMIT]; // storage for cuts +}; + //////////////////////////////////////////////////////////////////////// /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -133,14 +160,6 @@ static inline int Ivy_InfoHasBit( unsigned * p, int i ) { return (p[(i static inline void Ivy_InfoSetBit( unsigned * p, int i ) { p[(i)>>5] |= (1<<((i) & 31)); } static inline void Ivy_InfoXorBit( unsigned * p, int i ) { p[(i)>>5] ^= (1<<((i) & 31)); } -static inline int Ivy_FanCreate( int Id, int fCompl ) { return (Id << 1) | fCompl; } -static inline int Ivy_FanId( int Fan ) { return Fan >> 1; } -static inline int Ivy_FanCompl( int Fan ) { return Fan & 1; } - -static inline int Ivy_LeafCreate( int Id, int Lat ) { return (Id << 4) | Lat; } -static inline int Ivy_LeafId( int Leaf ) { return Leaf >> 4; } -static inline int Ivy_LeafLat( int Leaf ) { return Leaf & 15; } - static inline Ivy_Obj_t * Ivy_Regular( Ivy_Obj_t * p ) { return (Ivy_Obj_t *)((unsigned)(p) & ~01); } static inline Ivy_Obj_t * Ivy_Not( Ivy_Obj_t * p ) { return (Ivy_Obj_t *)((unsigned)(p) ^ 01); } static inline Ivy_Obj_t * Ivy_NotCond( Ivy_Obj_t * p, int c ) { return (Ivy_Obj_t *)((unsigned)(p) ^ (c)); } @@ -153,6 +172,19 @@ static inline Ivy_Obj_t * Ivy_ManPi( Ivy_Man_t * p, int i ) { return p->pO static inline Ivy_Obj_t * Ivy_ManPo( Ivy_Man_t * p, int i ) { return p->pObjs + Vec_IntEntry(p->vPos,i); } static inline Ivy_Obj_t * Ivy_ManObj( Ivy_Man_t * p, int i ) { return p->pObjs + i; } +static inline Ivy_Edge_t Ivy_EdgeCreate( int Id, int fCompl ) { return (Id << 1) | fCompl; } +static inline int Ivy_EdgeId( Ivy_Edge_t Edge ) { return Edge >> 1; } +static inline int Ivy_EdgeIsComplement( Ivy_Edge_t Edge ) { return Edge & 1; } +static inline Ivy_Edge_t Ivy_EdgeRegular( Ivy_Edge_t Edge ) { return (Edge >> 1) << 1; } +static inline Ivy_Edge_t Ivy_EdgeNot( Ivy_Edge_t Edge ) { return Edge ^ 1; } +static inline Ivy_Edge_t Ivy_EdgeNotCond( Ivy_Edge_t Edge, int fCond ) { return Edge ^ fCond; } +static inline Ivy_Edge_t Ivy_EdgeFromNode( Ivy_Obj_t * pNode ) { return Ivy_EdgeCreate( Ivy_Regular(pNode)->Id, Ivy_IsComplement(pNode) ); } +static inline Ivy_Obj_t * Ivy_EdgeToNode( Ivy_Man_t * p, Ivy_Edge_t Edge ){ return Ivy_NotCond( Ivy_ManObj(p, Ivy_EdgeId(Edge)), Ivy_EdgeIsComplement(Edge) ); } + +static inline int Ivy_LeafCreate( int Id, int Lat ) { return (Id << 4) | Lat; } +static inline int Ivy_LeafId( int Leaf ) { return Leaf >> 4; } +static inline int Ivy_LeafLat( int Leaf ) { return Leaf & 15; } + static inline int Ivy_ManPiNum( Ivy_Man_t * p ) { return p->nObjs[IVY_PI]; } static inline int Ivy_ManPoNum( Ivy_Man_t * p ) { return p->nObjs[IVY_PO]; } static inline int Ivy_ManAssertNum( Ivy_Man_t * p ) { return p->nObjs[IVY_ASSERT]; } @@ -185,9 +217,9 @@ static inline int Ivy_ObjIsAnd( Ivy_Obj_t * pObj ) { assert( !Ivy static inline int Ivy_ObjIsExor( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_EXOR; } static inline int Ivy_ObjIsBuf( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_BUF; } static inline int Ivy_ObjIsNode( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_AND || pObj->Type == IVY_EXOR; } -static inline int Ivy_ObjIsTerm( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_PI || pObj->Type == IVY_PO || pObj->Type == IVY_ASSERT; } +static inline int Ivy_ObjIsTerm( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_PI || pObj->Type == IVY_PO || pObj->Type == IVY_ASSERT; } static inline int Ivy_ObjIsHash( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_AND || pObj->Type == IVY_EXOR || pObj->Type == IVY_LATCH; } -static inline int Ivy_ObjIsOneFanin( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_PO || pObj->Type == IVY_ASSERT || pObj->Type == IVY_BUF || pObj->Type == IVY_LATCH; } +static inline int Ivy_ObjIsOneFanin( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_PO || pObj->Type == IVY_ASSERT || pObj->Type == IVY_BUF || pObj->Type == IVY_LATCH; } static inline int Ivy_ObjIsAndMulti( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_ANDM; } static inline int Ivy_ObjIsExorMulti( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_EXORM; } @@ -227,13 +259,9 @@ static inline Ivy_Obj_t * Ivy_ObjChild0( Ivy_Obj_t * pObj ) { assert( !Ivy static inline Ivy_Obj_t * Ivy_ObjChild1( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return Ivy_NotCond( Ivy_ObjFanin1(pObj), Ivy_ObjFaninC1(pObj) ); } static inline int Ivy_ObjLevelR( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->LevelR; } static inline int Ivy_ObjLevel( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Level; } -static inline int Ivy_ObjLevelNew( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return 1 + IVY_MAX(Ivy_ObjFanin0(pObj)->Level, Ivy_ObjFanin1(pObj)->Level); } +static inline int Ivy_ObjLevelNew( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return 1 + Ivy_ObjIsExor(pObj) + IVY_MAX(Ivy_ObjFanin0(pObj)->Level, Ivy_ObjFanin1(pObj)->Level); } static inline void Ivy_ObjClean( Ivy_Obj_t * pObj ) { int IdSaved = pObj->Id; - if ( IdSaved == 54 ) - { - int x = 0; - } memset( pObj, 0, sizeof(Ivy_Obj_t) ); pObj->Id = IdSaved; } @@ -339,6 +367,8 @@ static inline int Ivy_ObjFaninNum( Ivy_Obj_t * pObj ) // iterator over all objects, including those currently not used #define Ivy_ManForEachObj( p, pObj, i ) \ for ( i = 0, pObj = p->pObjs; i < p->ObjIdNext; i++, pObj++ ) +#define Ivy_ManForEachObjReverse( p, pObj, i ) \ + for ( i = p->ObjIdNext - 1, pObj = p->pObjs + i; i >= 0; i--, pObj-- ) // iterator over the primary inputs #define Ivy_ManForEachPi( p, pObj, i ) \ for ( i = 0; i < Vec_IntSize(p->vPis) && ((pObj) = Ivy_ManPi(p, i)); i++ ) @@ -369,6 +399,9 @@ static inline int Ivy_ObjFaninNum( Ivy_Obj_t * pObj ) /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +/*=== ivyBalance.c ========================================================*/ +extern Ivy_Man_t * Ivy_ManBalance( Ivy_Man_t * p, int fUpdateLevel ); +extern Ivy_Obj_t * Ivy_NodeBalanceBuildSuper( Vec_Ptr_t * vSuper, Ivy_Type_t Type, int fUpdateLevel ); /*=== ivyCanon.c ========================================================*/ extern Ivy_Obj_t * Ivy_CanonAnd( Ivy_Obj_t * p0, Ivy_Obj_t * p1 ); extern Ivy_Obj_t * Ivy_CanonExor( Ivy_Obj_t * p0, Ivy_Obj_t * p1 ); @@ -377,11 +410,13 @@ extern Ivy_Obj_t * Ivy_CanonLatch( Ivy_Obj_t * pObj, Ivy_Init_t Init ); extern int Ivy_ManCheck( Ivy_Man_t * p ); /*=== ivyCut.c ==========================================================*/ extern void Ivy_ManSeqFindCut( Ivy_Obj_t * pNode, Vec_Int_t * vFront, Vec_Int_t * vInside, int nSize ); -/*=== ivyBalance.c ======================================================*/ -extern int Ivy_ManBalance( Ivy_Man_t * p, int fUpdateLevel ); +extern Ivy_Store_t * Ivy_NodeFindCutsAll( Ivy_Obj_t * pObj, int nLeaves ); /*=== ivyDfs.c ==========================================================*/ extern Vec_Int_t * Ivy_ManDfs( Ivy_Man_t * p ); extern Vec_Int_t * Ivy_ManDfsExt( Ivy_Man_t * p ); +extern void Ivy_ManCollectCone( Ivy_Obj_t * pObj, Vec_Ptr_t * vFront, Vec_Ptr_t * vCone ); +extern Vec_Vec_t * Ivy_ManLevelize( Ivy_Man_t * p ); +extern Vec_Int_t * Ivy_ManRequiredLevels( Ivy_Man_t * p ); /*=== ivyDsd.c ==========================================================*/ extern int Ivy_TruthDsd( unsigned uTruth, Vec_Int_t * vTree ); extern void Ivy_TruthDsdPrint( FILE * pFile, Vec_Int_t * vTree ); @@ -399,6 +434,7 @@ extern Ivy_Obj_t * Ivy_Multi( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type extern Ivy_Obj_t * Ivy_Multi1( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ); extern Ivy_Obj_t * Ivy_Multi_rec( Ivy_Obj_t ** ppObjs, int nObjs, Ivy_Type_t Type ); extern Ivy_Obj_t * Ivy_MultiBalance_rec( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ); +extern int Ivy_MultiPlus( Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, Ivy_Type_t Type, int nLimit, Vec_Ptr_t * vSol ); /*=== ivyObj.c ==========================================================*/ extern Ivy_Obj_t * Ivy_ObjCreate( Ivy_Obj_t * pGhost ); extern Ivy_Obj_t * Ivy_ObjCreateExt( Ivy_Man_t * p, Ivy_Type_t Type ); @@ -415,8 +451,12 @@ extern Ivy_Obj_t * Ivy_Exor( Ivy_Obj_t * p0, Ivy_Obj_t * p1 ); extern Ivy_Obj_t * Ivy_Mux( Ivy_Obj_t * pC, Ivy_Obj_t * p1, Ivy_Obj_t * p0 ); extern Ivy_Obj_t * Ivy_Maj( Ivy_Obj_t * pA, Ivy_Obj_t * pB, Ivy_Obj_t * pC ); extern Ivy_Obj_t * Ivy_Miter( Vec_Ptr_t * vPairs ); +/*=== ivyResyn.c =========================================================*/ +extern Ivy_Man_t * Ivy_ManResyn( Ivy_Man_t * p, int fUpdateLevel ); /*=== ivyRewrite.c =========================================================*/ extern int Ivy_ManSeqRewrite( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost ); +extern int Ivy_ManRewriteAlg( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost ); +extern int Ivy_ManRewritePre( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost, int fVerbose ); /*=== ivyTable.c ========================================================*/ extern Ivy_Obj_t * Ivy_TableLookup( Ivy_Obj_t * pObj ); extern void Ivy_TableInsert( Ivy_Obj_t * pObj ); @@ -437,6 +477,8 @@ extern Ivy_Obj_t * Ivy_ObjRecognizeMux( Ivy_Obj_t * pObj, Ivy_Obj_t ** ppObj extern unsigned * Ivy_ManCutTruth( Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes, Vec_Int_t * vTruth ); extern Ivy_Obj_t * Ivy_NodeRealFanin_rec( Ivy_Obj_t * pNode, int iFanin ); extern Vec_Int_t * Ivy_ManLatches( Ivy_Man_t * p ); +extern int Ivy_ManReadLevels( Ivy_Man_t * p ); +extern Ivy_Obj_t * Ivy_ObjReal( Ivy_Obj_t * pObj ); #ifdef __cplusplus } diff --git a/src/temp/ivy/ivyBalance.c b/src/temp/ivy/ivyBalance.c index bbe69dd9..2e230ed2 100644 --- a/src/temp/ivy/ivyBalance.c +++ b/src/temp/ivy/ivyBalance.c @@ -17,32 +17,18 @@ Revision [$Id: ivyBalance.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] ***********************************************************************/ - + #include "ivy.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static void Ivy_NodeBalance( Ivy_Obj_t * pNode, int fUpdateLevel, Vec_Ptr_t * vFront, Vec_Ptr_t * vSpots ); - -// this procedure returns 1 if the node cannot be expanded -static inline int Ivy_NodeStopFanin( Ivy_Obj_t * pNode, int iFanin ) -{ - if ( iFanin == 0 ) - return Ivy_ObjFanin0(pNode)->Type != pNode->Type || Ivy_ObjRefs(Ivy_ObjFanin0(pNode)) > 1 || Ivy_ObjFaninC0(pNode); - else - return Ivy_ObjFanin1(pNode)->Type != pNode->Type || Ivy_ObjRefs(Ivy_ObjFanin1(pNode)) > 1 || Ivy_ObjFaninC1(pNode); -} - -// this procedure returns 1 if the node cannot be recursively dereferenced -static inline int Ivy_NodeBalanceDerefFanin( Ivy_Obj_t * pNode, int iFanin ) -{ - if ( iFanin == 0 ) - return Ivy_ObjFanin0(pNode)->Type == pNode->Type && Ivy_ObjRefs(Ivy_ObjFanin0(pNode)) == 0 && !Ivy_ObjFaninC0(pNode); - else - return Ivy_ObjFanin1(pNode)->Type == pNode->Type && Ivy_ObjRefs(Ivy_ObjFanin1(pNode)) == 0 && !Ivy_ObjFaninC1(pNode); -} +static int Ivy_NodeBalance_rec( Ivy_Man_t * pNew, Ivy_Obj_t * pObj, Vec_Vec_t * vStore, int Level, int fUpdateLevel ); +static Vec_Ptr_t * Ivy_NodeBalanceCone( Ivy_Obj_t * pObj, Vec_Vec_t * vStore, int Level ); +static int Ivy_NodeBalanceFindLeft( Vec_Ptr_t * vSuper ); +static void Ivy_NodeBalancePermute( Vec_Ptr_t * vSuper, int LeftBound, int fExor ); +static void Ivy_NodeBalancePushUniqueOrderByLevel( Vec_Ptr_t * vStore, Ivy_Obj_t * pObj ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -59,44 +45,41 @@ static inline int Ivy_NodeBalanceDerefFanin( Ivy_Obj_t * pNode, int iFanin ) SeeAlso [] ***********************************************************************/ -int Ivy_ManBalance( Ivy_Man_t * p, int fUpdateLevel ) +Ivy_Man_t * Ivy_ManBalance( Ivy_Man_t * p, int fUpdateLevel ) { - Vec_Int_t * vNodes; - Vec_Ptr_t * vFront, * vSpots; - Ivy_Obj_t * pNode; - int i; - vSpots = Vec_PtrAlloc( 50 ); - vFront = Vec_PtrAlloc( 50 ); - vNodes = Ivy_ManDfs( p ); - Ivy_ManForEachNodeVec( p, vNodes, pNode, i ) + Ivy_Man_t * pNew; + Ivy_Obj_t * pObj, * pDriver; + Vec_Vec_t * vStore; + int i, NewNodeId; + // clean the old manager + Ivy_ManCleanTravId( p ); + // create the new manager + pNew = Ivy_ManStart( Ivy_ManPiNum(p), Ivy_ManPoNum(p), Ivy_ManNodeNum(p) + 20000 ); + // map the nodes + Ivy_ManConst1(p)->TravId = Ivy_EdgeFromNode( Ivy_ManConst1(pNew) ); + Ivy_ManForEachPi( p, pObj, i ) + pObj->TravId = Ivy_EdgeFromNode( Ivy_ManPi(pNew, i) ); + // balance the AIG + vStore = Vec_VecAlloc( 50 ); + Ivy_ManForEachPo( p, pObj, i ) { - if ( Ivy_ObjIsBuf(pNode) ) - continue; - // fix the fanin buffer problem - Ivy_NodeFixBufferFanins( pNode ); - // skip node if it became a buffer - if ( Ivy_ObjIsBuf(pNode) ) - continue; - // skip nodes with one fanout if type of the node is the same as type of the fanout - // such nodes will be processed when the fanouts are processed - if ( Ivy_ObjRefs(pNode) == 1 && Ivy_ObjIsExor(pNode) == Ivy_ObjExorFanout(pNode) ) - continue; - assert( Ivy_ObjRefs(pNode) > 0 ); - // do not balance the node if both if its fanins have more than one fanout - if ( Ivy_NodeStopFanin(pNode, 0) && Ivy_NodeStopFanin(pNode, 1) ) - continue; - // try balancing this node - Ivy_NodeBalance( pNode, fUpdateLevel, vFront, vSpots ); + pDriver = Ivy_ObjReal( Ivy_ObjChild0(pObj) ); + NewNodeId = Ivy_NodeBalance_rec( pNew, Ivy_Regular(pDriver), vStore, 0, fUpdateLevel ); + NewNodeId = Ivy_EdgeNotCond( NewNodeId, Ivy_IsComplement(pDriver) ); + Ivy_ObjConnect( Ivy_ManPo(pNew, i), Ivy_EdgeToNode(pNew, NewNodeId) ); } - Vec_IntFree( vNodes ); - Vec_PtrFree( vSpots ); - Vec_PtrFree( vFront ); - return 1; + Vec_VecFree( vStore ); + if ( i = Ivy_ManCleanup( pNew ) ) + printf( "Cleanup after balancing removed %d dangling nodes.\n", i ); + // check the resulting AIG + if ( !Ivy_ManCheck(pNew) ) + printf( "Ivy_ManBalance(): The check has failed.\n" ); + return pNew; } /**Function************************************************************* - Synopsis [Dereferences MFFC of the node.] + Synopsis [Procedure used for sorting the nodes in decreasing order of levels.] Description [] @@ -105,24 +88,19 @@ int Ivy_ManBalance( Ivy_Man_t * p, int fUpdateLevel ) SeeAlso [] ***********************************************************************/ -void Ivy_NodeBalanceDeref_rec( Ivy_Obj_t * pNode ) +int Ivy_NodeCompareLevelsDecrease( Ivy_Obj_t ** pp1, Ivy_Obj_t ** pp2 ) { - Ivy_Obj_t * pFan; - // deref the first fanin - pFan = Ivy_ObjFanin0(pNode); - Ivy_ObjRefsDec( pFan ); - if ( Ivy_NodeBalanceDerefFanin(pNode, 0) ) - Ivy_NodeBalanceDeref_rec( pFan ); - // deref the second fanin - pFan = Ivy_ObjFanin1(pNode); - Ivy_ObjRefsDec( pFan ); - if ( Ivy_NodeBalanceDerefFanin(pNode, 1) ) - Ivy_NodeBalanceDeref_rec( pFan ); + int Diff = Ivy_Regular(*pp1)->Level - Ivy_Regular(*pp2)->Level; + if ( Diff > 0 ) + return -1; + if ( Diff < 0 ) + return 1; + return 0; } /**Function************************************************************* - Synopsis [Removes nodes inside supergate and determines frontier.] + Synopsis [Returns the ID of new node constructed.] Description [] @@ -131,35 +109,47 @@ void Ivy_NodeBalanceDeref_rec( Ivy_Obj_t * pNode ) SeeAlso [] ***********************************************************************/ -void Ivy_NodeBalanceCollect_rec( Ivy_Obj_t * pNode, Vec_Ptr_t * vSpots, Vec_Ptr_t * vFront ) +int Ivy_NodeBalance_rec( Ivy_Man_t * pNew, Ivy_Obj_t * pObjOld, Vec_Vec_t * vStore, int Level, int fUpdateLevel ) { - Ivy_Obj_t * pFanin; - // skip visited nodes - if ( Vec_PtrFind(vSpots, pNode) >= 0 ) - return; - // collect node - Vec_PtrPush( vSpots, pNode ); - // first fanin - pFanin = Ivy_ObjFanin0(pNode); - if ( Ivy_ObjRefs(pFanin) == 0 ) - Ivy_NodeBalanceCollect_rec( pFanin, vSpots, vFront ); - else if ( Ivy_ObjIsExor(pNode) && Vec_PtrFind(vFront, Ivy_ObjChild0(pNode)) >= 0 ) - Vec_PtrRemove( vFront, Ivy_ObjChild0(pNode) ); - else - Vec_PtrPushUnique( vFront, Ivy_ObjChild0(pNode) ); - // second fanin - pFanin = Ivy_ObjFanin1(pNode); - if ( Ivy_ObjRefs(pFanin) == 0 ) - Ivy_NodeBalanceCollect_rec( pFanin, vSpots, vFront ); - else if ( Ivy_ObjIsExor(pNode) && Vec_PtrFind(vFront, Ivy_ObjChild1(pNode)) >= 0 ) - Vec_PtrRemove( vFront, Ivy_ObjChild1(pNode) ); - else - Vec_PtrPushUnique( vFront, Ivy_ObjChild1(pNode) ); + Ivy_Obj_t * pObjNew; + Vec_Ptr_t * vSuper; + int i, NewNodeId; + assert( !Ivy_IsComplement(pObjOld) ); + assert( !Ivy_ObjIsBuf(pObjOld) ); + // return if the result is known + if ( Ivy_ObjIsConst1(pObjOld) ) + return pObjOld->TravId; + if ( pObjOld->TravId ) + return pObjOld->TravId; + assert( Ivy_ObjIsNode(pObjOld) ); + // get the implication supergate + vSuper = Ivy_NodeBalanceCone( pObjOld, vStore, Level ); + if ( vSuper->nSize == 0 ) + { // it means that the supergate contains two nodes in the opposite polarity + pObjOld->TravId = Ivy_EdgeFromNode( Ivy_ManConst0(pNew) ); + return pObjOld->TravId; + } + if ( vSuper->nSize < 2 ) + printf( "BUG!\n" ); + // for each old node, derive the new well-balanced node + for ( i = 0; i < vSuper->nSize; i++ ) + { + NewNodeId = Ivy_NodeBalance_rec( pNew, Ivy_Regular(vSuper->pArray[i]), vStore, Level + 1, fUpdateLevel ); + NewNodeId = Ivy_EdgeNotCond( NewNodeId, Ivy_IsComplement(vSuper->pArray[i]) ); + vSuper->pArray[i] = Ivy_EdgeToNode( pNew, NewNodeId ); + } + // build the supergate + pObjNew = Ivy_NodeBalanceBuildSuper( vSuper, Ivy_ObjType(pObjOld), fUpdateLevel ); + vSuper->nSize = 0; + // make sure the balanced node is not assigned + assert( pObjOld->TravId == 0 ); + pObjOld->TravId = Ivy_EdgeFromNode( pObjNew ); + return pObjOld->TravId; } /**Function************************************************************* - Synopsis [Comparison procedure for two nodes by level.] + Synopsis [Builds implication supergate.] Description [] @@ -168,89 +158,107 @@ void Ivy_NodeBalanceCollect_rec( Ivy_Obj_t * pNode, Vec_Ptr_t * vSpots, Vec_Ptr_ SeeAlso [] ***********************************************************************/ -int Ivy_BalanceCompareByLevel( Ivy_Obj_t ** pp1, Ivy_Obj_t ** pp2 ) +Ivy_Obj_t * Ivy_NodeBalanceBuildSuper( Vec_Ptr_t * vSuper, Ivy_Type_t Type, int fUpdateLevel ) { - int Level1 = Ivy_ObjLevel( *pp1 ); - int Level2 = Ivy_ObjLevel( *pp2 ); - if ( Level1 > Level2 ) - return -1; - if ( Level1 < Level2 ) - return 1; - return 0; + Ivy_Obj_t * pObj1, * pObj2; + int LeftBound; + assert( vSuper->nSize > 1 ); + // sort the new nodes by level in the decreasing order + Vec_PtrSort( vSuper, Ivy_NodeCompareLevelsDecrease ); + // balance the nodes + while ( vSuper->nSize > 1 ) + { + // find the left bound on the node to be paired + LeftBound = (!fUpdateLevel)? 0 : Ivy_NodeBalanceFindLeft( vSuper ); + // find the node that can be shared (if no such node, randomize choice) + Ivy_NodeBalancePermute( vSuper, LeftBound, Type == IVY_EXOR ); + // pull out the last two nodes + pObj1 = Vec_PtrPop(vSuper); + pObj2 = Vec_PtrPop(vSuper); + Ivy_NodeBalancePushUniqueOrderByLevel( vSuper, Ivy_Oper(pObj1, pObj2, Type) ); + } + return Vec_PtrEntry(vSuper, 0); } /**Function************************************************************* - Synopsis [Removes nodes inside supergate and determines frontier.] + Synopsis [Collects the nodes of the supergate.] - Description [Return 1 if the output needs to be complemented.] + Description [] SideEffects [] SeeAlso [] ***********************************************************************/ -int Ivy_NodeBalancePrepare( Ivy_Obj_t * pNode, Vec_Ptr_t * vFront, Vec_Ptr_t * vSpots ) +int Ivy_NodeBalanceCone_rec( Ivy_Obj_t * pRoot, Ivy_Obj_t * pObj, Vec_Ptr_t * vSuper ) { - Ivy_Man_t * pMan = Ivy_ObjMan( pNode ); - Ivy_Obj_t * pObj, * pNext; - int i, k, Counter = 0; - // dereference the cone - Ivy_NodeBalanceDeref_rec( pNode ); - // collect the frontier and the internal nodes - Vec_PtrClear( vFront ); - Vec_PtrClear( vSpots ); - Ivy_NodeBalanceCollect_rec( pNode, vSpots, vFront ); - // remove all the nodes - Vec_PtrForEachEntry( vSpots, pObj, i ) - { - // skip the first entry (the node itself) - if ( i == 0 ) continue; - // collect the free entries - Vec_IntPush( pMan->vFree, pObj->Id ); - Ivy_ObjDelete( pObj, 1 ); - } - // sort nodes by level in decreasing order - qsort( (void *)Vec_PtrArray(vFront), Vec_PtrSize(vFront), sizeof(Ivy_Obj_t *), - (int (*)(const void *, const void *))Ivy_BalanceCompareByLevel ); - // check if there are nodes and their complements - Counter = 0; - Vec_PtrForEachEntry( vFront, pObj, i ) + int RetValue1, RetValue2, i; + // check if the node is visited + if ( Ivy_Regular(pObj)->fMarkB ) { - if ( i == Vec_PtrSize(vFront) - 1 ) - break; - pNext = Vec_PtrEntry( vFront, i+1 ); - if ( Ivy_Regular(pObj) == Ivy_Regular(pNext) ) - { - assert( pObj == Ivy_Not(pNext) ); - Vec_PtrWriteEntry( vFront, i, NULL ); - Vec_PtrWriteEntry( vFront, i+1, NULL ); - i++; - Counter++; - } - } - // if there are no complemented pairs, go ahead and balance - if ( Counter == 0 ) + // 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] == Ivy_Not(pObj) ) + return -1; + assert( 0 ); return 0; - // if there are complemented pairs and this is AND, create const 0 - if ( Counter > 0 && Ivy_ObjIsAnd(pNode) ) + } + // if the new node is complemented or a PI, another gate begins + if ( pObj != pRoot && (Ivy_IsComplement(pObj) || Ivy_ObjType(pObj) != Ivy_ObjType(pRoot) || Ivy_ObjRefs(pObj) > 1) ) { - Vec_PtrClear( vFront ); - Vec_PtrPush( vFront, Ivy_ManConst0(pMan) ); + Vec_PtrPush( vSuper, pObj ); + Ivy_Regular(pObj)->fMarkB = 1; return 0; } - assert( Counter > 0 && Ivy_ObjIsExor(pNode) ); - // remove the pairs - k = 0; - Vec_PtrForEachEntry( vFront, pObj, i ) - if ( pObj ) - Vec_PtrWriteEntry( vFront, k++, pObj ); - Vec_PtrShrink( vFront, k ); - // add constant zero node if nothing is left - if ( Vec_PtrSize(vFront) == 0 ) - Vec_PtrPush( vFront, Ivy_ManConst0(pMan) ); - // return 1 if the number of pairs is odd (need to complement the output) - return Counter & 1; + assert( !Ivy_IsComplement(pObj) ); + assert( Ivy_ObjIsNode(pObj) ); + // go through the branches + RetValue1 = Ivy_NodeBalanceCone_rec( pRoot, Ivy_ObjReal( Ivy_ObjChild0(pObj) ), vSuper ); + RetValue2 = Ivy_NodeBalanceCone_rec( pRoot, Ivy_ObjReal( Ivy_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 * Ivy_NodeBalanceCone( Ivy_Obj_t * pObj, Vec_Vec_t * vStore, int Level ) +{ + Vec_Ptr_t * vNodes; + int RetValue, i; + assert( !Ivy_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 = Ivy_NodeBalanceCone_rec( pObj, pObj, vNodes ); + assert( vNodes->nSize > 1 ); + // unmark the visited nodes + Vec_PtrForEachEntry( vNodes, pObj, i ) + Ivy_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************************************************************* @@ -270,27 +278,27 @@ int Ivy_NodeBalancePrepare( Ivy_Obj_t * pNode, Vec_Ptr_t * vFront, Vec_Ptr_t * v ***********************************************************************/ int Ivy_NodeBalanceFindLeft( Vec_Ptr_t * vSuper ) { - Ivy_Obj_t * pNodeRight, * pNodeLeft; + Ivy_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; - pNodeRight = Vec_PtrEntry( vSuper, Current ); + 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 - pNodeLeft = Vec_PtrEntry( vSuper, Current ); + pObjLeft = Vec_PtrEntry( vSuper, Current ); // if the level of this node is different, quit the loop - if ( Ivy_Regular(pNodeLeft)->Level != Ivy_Regular(pNodeRight)->Level ) + if ( Ivy_Regular(pObjLeft)->Level != Ivy_Regular(pObjRight)->Level ) break; } Current++; // get the node, for which the equality holds - pNodeLeft = Vec_PtrEntry( vSuper, Current ); - assert( Ivy_Regular(pNodeLeft)->Level == Ivy_Regular(pNodeRight)->Level ); + pObjLeft = Vec_PtrEntry( vSuper, Current ); + assert( Ivy_Regular(pObjLeft)->Level == Ivy_Regular(pObjRight)->Level ); return Current; } @@ -306,9 +314,9 @@ int Ivy_NodeBalanceFindLeft( Vec_Ptr_t * vSuper ) SeeAlso [] ***********************************************************************/ -void Ivy_NodeBalancePermute( Ivy_Man_t * pMan, Vec_Ptr_t * vSuper, int LeftBound, int fExor ) +void Ivy_NodeBalancePermute( Vec_Ptr_t * vSuper, int LeftBound, int fExor ) { - Ivy_Obj_t * pNode1, * pNode2, * pNode3, * pGhost; + Ivy_Obj_t * pObj1, * pObj2, * pObj3, * pGhost; int RightBound, i; // get the right bound RightBound = Vec_PtrSize(vSuper) - 2; @@ -316,19 +324,19 @@ void Ivy_NodeBalancePermute( Ivy_Man_t * pMan, Vec_Ptr_t * vSuper, int LeftBound if ( LeftBound == RightBound ) return; // get the two last nodes - pNode1 = Vec_PtrEntry( vSuper, RightBound + 1 ); - pNode2 = Vec_PtrEntry( vSuper, RightBound ); + pObj1 = Vec_PtrEntry( vSuper, RightBound + 1 ); + pObj2 = Vec_PtrEntry( vSuper, RightBound ); // find the first node that can be shared for ( i = RightBound; i >= LeftBound; i-- ) { - pNode3 = Vec_PtrEntry( vSuper, i ); - pGhost = Ivy_ObjCreateGhost( pNode1, pNode3, fExor? IVY_EXOR : IVY_AND, IVY_INIT_NONE ); + pObj3 = Vec_PtrEntry( vSuper, i ); + pGhost = Ivy_ObjCreateGhost( pObj1, pObj3, fExor? IVY_EXOR : IVY_AND, IVY_INIT_NONE ); if ( Ivy_TableLookup( pGhost ) ) { - if ( pNode3 == pNode2 ) + if ( pObj3 == pObj2 ) return; - Vec_PtrWriteEntry( vSuper, i, pNode2 ); - Vec_PtrWriteEntry( vSuper, RightBound, pNode3 ); + Vec_PtrWriteEntry( vSuper, i, pObj2 ); + Vec_PtrWriteEntry( vSuper, RightBound, pObj3 ); return; } } @@ -336,11 +344,11 @@ void Ivy_NodeBalancePermute( Ivy_Man_t * pMan, Vec_Ptr_t * vSuper, int LeftBound // we did not find the node to share, randomize choice { int Choice = rand() % (RightBound - LeftBound + 1); - pNode3 = Vec_PtrEntry( vSuper, LeftBound + Choice ); - if ( pNode3 == pNode2 ) + pObj3 = Vec_PtrEntry( vSuper, LeftBound + Choice ); + if ( pObj3 == pObj2 ) return; - Vec_PtrWriteEntry( vSuper, LeftBound + Choice, pNode2 ); - Vec_PtrWriteEntry( vSuper, RightBound, pNode3 ); + Vec_PtrWriteEntry( vSuper, LeftBound + Choice, pObj2 ); + Vec_PtrWriteEntry( vSuper, RightBound, pObj3 ); } */ } @@ -356,61 +364,22 @@ void Ivy_NodeBalancePermute( Ivy_Man_t * pMan, Vec_Ptr_t * vSuper, int LeftBound SeeAlso [] ***********************************************************************/ -void Ivy_NodeBalancePushUniqueOrderByLevel( Vec_Ptr_t * vFront, Ivy_Obj_t * pNode ) +void Ivy_NodeBalancePushUniqueOrderByLevel( Vec_Ptr_t * vStore, Ivy_Obj_t * pObj ) { - Ivy_Obj_t * pNode1, * pNode2; + Ivy_Obj_t * pObj1, * pObj2; int i; - if ( Vec_PtrPushUnique(vFront, pNode) ) + if ( Vec_PtrPushUnique(vStore, pObj) ) return; // find the p of the node - for ( i = vFront->nSize-1; i > 0; i-- ) + for ( i = vStore->nSize-1; i > 0; i-- ) { - pNode1 = vFront->pArray[i ]; - pNode2 = vFront->pArray[i-1]; - if ( Ivy_Regular(pNode1)->Level <= Ivy_Regular(pNode2)->Level ) + pObj1 = vStore->pArray[i ]; + pObj2 = vStore->pArray[i-1]; + if ( Ivy_Regular(pObj1)->Level <= Ivy_Regular(pObj2)->Level ) break; - vFront->pArray[i ] = pNode2; - vFront->pArray[i-1] = pNode1; - } -} - -/**Function************************************************************* - - Synopsis [Balances one node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ivy_NodeBalance( Ivy_Obj_t * pNode, int fUpdateLevel, Vec_Ptr_t * vFront, Vec_Ptr_t * vSpots ) -{ - Ivy_Man_t * pMan = Ivy_ObjMan( pNode ); - Ivy_Obj_t * pFan0, * pFan1, * pNodeNew; - int fCompl, LeftBound; - // remove internal nodes and derive the frontier - fCompl = Ivy_NodeBalancePrepare( pNode, vFront, vSpots ); - assert( Vec_PtrSize(vFront) > 0 ); - // balance the nodes - while ( Vec_PtrSize(vFront) > 1 ) - { - // find the left bound on the node to be paired - LeftBound = (!fUpdateLevel)? 0 : Ivy_NodeBalanceFindLeft( vFront ); - // find the node that can be shared (if no such node, randomize choice) - Ivy_NodeBalancePermute( pMan, vFront, LeftBound, Ivy_ObjIsExor(pNode) ); - // pull out the last two nodes - pFan0 = Vec_PtrPop(vFront); assert( !Ivy_ObjIsConst1(Ivy_Regular(pFan0)) ); - pFan1 = Vec_PtrPop(vFront); assert( !Ivy_ObjIsConst1(Ivy_Regular(pFan1)) ); - // create the new node - pNodeNew = Ivy_ObjCreate( Ivy_ObjCreateGhost(pFan0, pFan1, Ivy_ObjType(pNode), IVY_INIT_NONE) ); - // add the new node to the frontier - Ivy_NodeBalancePushUniqueOrderByLevel( vFront, pNodeNew ); + vStore->pArray[i ] = pObj2; + vStore->pArray[i-1] = pObj1; } - assert( Vec_PtrSize(vFront) == 1 ); - // perform the replacement - Ivy_ObjReplace( pNode, Ivy_NotCond(Vec_PtrPop(vFront), fCompl), 1, 1 ); } diff --git a/src/temp/ivy/ivyCut.c b/src/temp/ivy/ivyCut.c index 57720e17..71a3613c 100644 --- a/src/temp/ivy/ivyCut.c +++ b/src/temp/ivy/ivyCut.c @@ -200,180 +200,6 @@ void Ivy_ManSeqFindCut( Ivy_Obj_t * pRoot, Vec_Int_t * vFront, Vec_Int_t * vInsi -/**Function************************************************************* - - Synopsis [Comparison for node pointers.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Ivy_ManFindAlgCutCompare( Ivy_Obj_t ** pp1, Ivy_Obj_t ** pp2 ) -{ - if ( *pp1 < *pp2 ) - return -1; - if ( *pp1 > *pp2 ) - return 1; - return 0; -} - -/**Function************************************************************* - - Synopsis [Computing one algebraic cut.] - - Description [Returns 1 if the tree-leaves of this node where traversed - and found to have no external references (and have not been collected). - Returns 0 if the tree-leaves have external references and are collected.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Ivy_ManFindAlgCut_rec( Ivy_Obj_t * pRoot, Ivy_Type_t Type, Vec_Ptr_t * vFront ) -{ - int RetValue0, RetValue1; - Ivy_Obj_t * pRootR = Ivy_Regular(pRoot); - assert( Type != IVY_EXOR || !Ivy_IsComplement(pRoot) ); - // if the node is a buffer skip through it - if ( Ivy_ObjIsBuf(pRootR) ) - return Ivy_ManFindAlgCut_rec( Ivy_NotCond(Ivy_ObjChild0(pRootR), Ivy_IsComplement(pRoot)), Type, vFront ); - // if the node is the end of the tree, return - if ( Ivy_IsComplement(pRoot) || Ivy_ObjIsCi(pRoot) || Ivy_ObjType(pRoot) != Type ) - { - if ( Ivy_ObjRefs(pRootR) == 1 ) - return 1; - assert( Ivy_ObjRefs(pRootR) > 1 ); - Vec_PtrPush( vFront, pRoot ); - return 0; - } - // branch on the node - assert( Ivy_ObjIsNode(pRoot) ); - RetValue0 = Ivy_ManFindAlgCut_rec( Ivy_ObjChild0(pRoot), Type, vFront ); - RetValue1 = Ivy_ManFindAlgCut_rec( Ivy_ObjChild1(pRoot), Type, vFront ); - // the case when both have no external referenced - if ( RetValue0 && RetValue1 ) - { - if ( Ivy_ObjRefs(pRoot) == 1 ) - return 1; - assert( Ivy_ObjRefs(pRoot) > 1 ); - Vec_PtrPush( vFront, pRoot ); - return 0; - } - // the case when one of them has external references - if ( RetValue0 ) - Vec_PtrPush( vFront, Ivy_ObjChild0(pRoot) ); - if ( RetValue1 ) - Vec_PtrPush( vFront, Ivy_ObjChild1(pRoot) ); - return 0; -} - -/**Function************************************************************* - - Synopsis [Computing one algebraic cut.] - - Description [Algebraic cut stops when we hit (a) CI, (b) complemented edge, - (c) boundary of different gates. Returns 1 if this is a pure tree. - Returns -1 if the contant 0 is detected. Return 0 if the array can be used.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Ivy_ManFindAlgCut( Ivy_Obj_t * pRoot, Vec_Ptr_t * vFront ) -{ - Ivy_Obj_t * pObj, * pPrev; - int RetValue, i, k; - assert( !Ivy_IsComplement(pRoot) ); - // clear the frontier and collect the nodes - Vec_PtrClear( vFront ); - RetValue = Ivy_ManFindAlgCut_rec( pRoot, Ivy_ObjType(pRoot), vFront ); - // return if the node is the root of a tree - if ( RetValue == 1 ) - return 1; - // sort the entries to in increasing order - Vec_PtrSort( vFront, Ivy_ManFindAlgCutCompare ); - // remove duplicated - k = 1; - Vec_PtrForEachEntryStart( vFront, pObj, i, 1 ) - { - pPrev = (k == 0 ? NULL : Vec_PtrEntry(vFront, k-1)); - if ( pObj == pPrev ) - { - if ( Ivy_ObjIsExor(pRoot) ) - k--; - continue; - } - if ( pObj == Ivy_Not(pPrev) ) - return -1; - Vec_PtrWriteEntry( vFront, k++, pObj ); - } - if ( k == 0 ) - return -1; - Vec_PtrShrink( vFront, k ); - return 0; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ivy_ManTestCutsAlg( Ivy_Man_t * p ) -{ - Vec_Ptr_t * vFront; - Ivy_Obj_t * pObj, * pTemp; - int i, k, RetValue; - vFront = Vec_PtrAlloc( 100 ); - Ivy_ManForEachObj( p, pObj, i ) - { - if ( !Ivy_ObjIsNode(pObj) ) - continue; - if ( Ivy_ObjIsMuxType(pObj) ) - { - printf( "m " ); - continue; - } - if ( pObj->Id == 509 ) - { - int y = 0; - } - - RetValue = Ivy_ManFindAlgCut( pObj, vFront ); - if ( Ivy_ObjIsExor(pObj) ) - printf( "x" ); - if ( RetValue == -1 ) - printf( "Const0 " ); - else if ( RetValue == 1 || Vec_PtrSize(vFront) <= 2 ) - printf( ". " ); - else - printf( "%d ", Vec_PtrSize(vFront) ); - - printf( "( " ); - Vec_PtrForEachEntry( vFront, pTemp, k ) - printf( "%d ", Ivy_ObjRefs(Ivy_Regular(pTemp)) ); - printf( ")\n" ); - - if ( Vec_PtrSize(vFront) == 5 ) - { - int x = 0; - } - } - printf( "\n" ); - Vec_PtrFree( vFront ); -} - - /**Function************************************************************* @@ -639,8 +465,8 @@ int Ivy_ManFindBoolCut( Ivy_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vVolu void Ivy_ManTestCutsBool( Ivy_Man_t * p ) { Vec_Ptr_t * vFront, * vVolume, * vLeaves; - Ivy_Obj_t * pObj, * pTemp; - int i, k, RetValue; + Ivy_Obj_t * pObj;//, * pTemp; + int i, RetValue;//, k; vFront = Vec_PtrAlloc( 100 ); vVolume = Vec_PtrAlloc( 100 ); vLeaves = Vec_PtrAlloc( 100 ); @@ -673,6 +499,376 @@ void Ivy_ManTestCutsBool( Ivy_Man_t * p ) Vec_PtrFree( vLeaves ); } + + +/**Function************************************************************* + + Synopsis [Find the hash value of the cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline unsigned Ivy_NodeCutHash( Ivy_Cut_t * pCut ) +{ + int i; +// for ( i = 1; i < pCut->nSize; i++ ) +// assert( pCut->pArray[i-1] < pCut->pArray[i] ); + pCut->uHash = 0; + for ( i = 0; i < pCut->nSize; i++ ) + pCut->uHash |= (1 << (pCut->pArray[i] % 31)); + return pCut->uHash; +} + +/**Function************************************************************* + + Synopsis [Removes one node to the cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Ivy_NodeCutShrink( Ivy_Cut_t * pCut, int iOld ) +{ + int i, k; + for ( i = k = 0; i < pCut->nSize; i++ ) + if ( pCut->pArray[i] != iOld ) + pCut->pArray[k++] = pCut->pArray[i]; + assert( k == pCut->nSize - 1 ); + pCut->nSize--; +} + +/**Function************************************************************* + + Synopsis [Adds one node to the cut.] + + Description [Returns 1 if the cuts is still okay.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Ivy_NodeCutExtend( Ivy_Cut_t * pCut, int iNew ) +{ + int i; + for ( i = 0; i < pCut->nSize; i++ ) + if ( pCut->pArray[i] == iNew ) + return 1; + // check if there is room + if ( pCut->nSize == pCut->nSizeMax ) + return 0; + // add the new one + for ( i = pCut->nSize - 1; i >= 0; i-- ) + if ( pCut->pArray[i] > iNew ) + pCut->pArray[i+1] = pCut->pArray[i]; + else + { + assert( pCut->pArray[i] < iNew ); + break; + } + pCut->pArray[i+1] = iNew; + pCut->nSize++; + return 1; +} + +/**Function************************************************************* + + Synopsis [Check if the cut exists.] + + Description [Returns 1 if the cut exists.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_NodeCutFindOrAdd( Ivy_Store_t * pCutStore, Ivy_Cut_t * pCutNew ) +{ + Ivy_Cut_t * pCut; + int i, k; + assert( pCutNew->uHash ); + // try to find the cut + for ( i = 0; i < pCutStore->nCuts; i++ ) + { + pCut = pCutStore->pCuts + i; + if ( pCut->uHash == pCutNew->uHash && pCut->nSize == pCutNew->nSize ) + { + for ( k = 0; k < pCutNew->nSize; k++ ) + if ( pCut->pArray[k] != pCutNew->pArray[k] ) + break; + if ( k == pCutNew->nSize ) + return 1; + } + } + assert( pCutStore->nCuts < pCutStore->nCutsMax ); + // add the cut + pCut = pCutStore->pCuts + pCutStore->nCuts++; + *pCut = *pCutNew; + return 0; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if pDom is contained in pCut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Ivy_CutCheckDominance( Ivy_Cut_t * pDom, Ivy_Cut_t * pCut ) +{ + int i, k; + for ( i = 0; i < pDom->nSize; i++ ) + { + for ( k = 0; k < pCut->nSize; k++ ) + if ( pDom->pArray[i] == pCut->pArray[k] ) + break; + if ( k == pCut->nSize ) // node i in pDom is not contained in pCut + return 0; + } + // every node in pDom is contained in pCut + return 1; +} + +/**Function************************************************************* + + Synopsis [Check if the cut exists.] + + Description [Returns 1 if the cut exists.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_NodeCutFindOrAddFilter( Ivy_Store_t * pCutStore, Ivy_Cut_t * pCutNew ) +{ + Ivy_Cut_t * pCut; + int i, k; + assert( pCutNew->uHash ); + // try to find the cut + for ( i = 0; i < pCutStore->nCuts; i++ ) + { + pCut = pCutStore->pCuts + i; + if ( pCut->nSize == 0 ) + continue; + if ( pCut->nSize == pCutNew->nSize ) + { + if ( pCut->uHash == pCutNew->uHash ) + { + for ( k = 0; k < pCutNew->nSize; k++ ) + if ( pCut->pArray[k] != pCutNew->pArray[k] ) + break; + if ( k == pCutNew->nSize ) + return 1; + } + continue; + } + if ( pCut->nSize < pCutNew->nSize ) + { + // skip the non-contained cuts + if ( (pCut->uHash & pCutNew->uHash) != pCut->uHash ) + continue; + // check containment seriously + if ( Ivy_CutCheckDominance( pCut, pCutNew ) ) + return 1; + continue; + } + // check potential containment of other cut + + // skip the non-contained cuts + if ( (pCut->uHash & pCutNew->uHash) != pCutNew->uHash ) + continue; + // check containment seriously + if ( Ivy_CutCheckDominance( pCutNew, pCut ) ) + { + // remove the current cut +// --pCutStore->nCuts; +// for ( k = i; k < pCutStore->nCuts; k++ ) +// pCutStore->pCuts[k] = pCutStore->pCuts[k+1]; +// i--; + pCut->nSize = 0; + } + } + assert( pCutStore->nCuts < pCutStore->nCutsMax ); + // add the cut + pCut = pCutStore->pCuts + pCutStore->nCuts++; + *pCut = *pCutNew; + return 0; +} + +/**Function************************************************************* + + Synopsis [Print the cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_NodeCompactCuts( Ivy_Store_t * pCutStore ) +{ + Ivy_Cut_t * pCut; + int i, k; + for ( i = k = 0; i < pCutStore->nCuts; i++ ) + { + pCut = pCutStore->pCuts + i; + if ( pCut->nSize == 0 ) + continue; + pCutStore->pCuts[k++] = *pCut; + } + pCutStore->nCuts = k; +} + +/**Function************************************************************* + + Synopsis [Print the cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_NodePrintCut( Ivy_Cut_t * pCut ) +{ + int i; + assert( pCut->nSize > 0 ); + printf( "%d : {", pCut->nSize ); + for ( i = 0; i < pCut->nSize; i++ ) + printf( " %d", pCut->pArray[i] ); + printf( " }\n" ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_NodePrintCuts( Ivy_Store_t * pCutStore ) +{ + int i; + printf( "Node %d\n", pCutStore->pCuts[0].pArray[0] ); + for ( i = 0; i < pCutStore->nCuts; i++ ) + Ivy_NodePrintCut( pCutStore->pCuts + i ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Store_t * Ivy_NodeFindCutsAll( Ivy_Obj_t * pObj, int nLeaves ) +{ + static Ivy_Store_t CutStore, * pCutStore = &CutStore; + Ivy_Cut_t CutNew, * pCutNew = &CutNew, * pCut; + Ivy_Man_t * pMan = Ivy_ObjMan(pObj); + Ivy_Obj_t * pLeaf; + int i, k; + + assert( nLeaves <= IVY_CUT_INPUT ); + + // start the structure + pCutStore->nCuts = 0; + pCutStore->nCutsMax = IVY_CUT_LIMIT; + // start the trivial cut + pCutNew->uHash = 0; + pCutNew->nSize = 1; + pCutNew->nSizeMax = nLeaves; + pCutNew->pArray[0] = pObj->Id; + Ivy_NodeCutHash( pCutNew ); + // add the trivial cut + Ivy_NodeCutFindOrAdd( pCutStore, pCutNew ); + assert( pCutStore->nCuts == 1 ); + + // explore the cuts + for ( i = 0; i < pCutStore->nCuts; i++ ) + { + // expand this cut + pCut = pCutStore->pCuts + i; + if ( pCut->nSize == 0 ) + continue; + for ( k = 0; k < pCut->nSize; k++ ) + { + pLeaf = Ivy_ObjObj( pObj, pCut->pArray[k] ); + if ( Ivy_ObjIsCi(pLeaf) ) + continue; + *pCutNew = *pCut; + Ivy_NodeCutShrink( pCutNew, pLeaf->Id ); + if ( !Ivy_NodeCutExtend( pCutNew, Ivy_ObjFaninId0(pLeaf) ) ) + continue; + if ( Ivy_ObjIsNode(pLeaf) && !Ivy_NodeCutExtend( pCutNew, Ivy_ObjFaninId1(pLeaf) ) ) + continue; + Ivy_NodeCutHash( pCutNew ); + Ivy_NodeCutFindOrAddFilter( pCutStore, pCutNew ); + if ( pCutStore->nCuts == IVY_CUT_LIMIT ) + break; + } + if ( pCutStore->nCuts == IVY_CUT_LIMIT ) + break; + } + Ivy_NodeCompactCuts( pCutStore ); +// Ivy_NodePrintCuts( pCutStore ); + return pCutStore; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManTestCutsAll( Ivy_Man_t * p ) +{ + Ivy_Obj_t * pObj; + int i, nCutsCut, nCutsTotal, nNodeTotal, nNodeOver; + int clk = clock(); + nNodeTotal = nNodeOver = 0; + nCutsTotal = -Ivy_ManNodeNum(p); + Ivy_ManForEachObj( p, pObj, i ) + { + if ( !Ivy_ObjIsNode(pObj) ) + continue; + nCutsCut = Ivy_NodeFindCutsAll( pObj, 4 )->nCuts; + nCutsTotal += nCutsCut; + nNodeOver += (nCutsCut == IVY_CUT_LIMIT); + nNodeTotal++; + } + printf( "Total cuts = %6d. Trivial = %6d. Nodes = %6d. Satur = %6d. ", + nCutsTotal, Ivy_ManPiNum(p) + Ivy_ManNodeNum(p), nNodeTotal, nNodeOver ); + PRT( "Time", clock() - clk ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/temp/ivy/ivyDfs.c b/src/temp/ivy/ivyDfs.c index 2db80b00..2dc3bac8 100644 --- a/src/temp/ivy/ivyDfs.c +++ b/src/temp/ivy/ivyDfs.c @@ -69,6 +69,9 @@ Vec_Int_t * Ivy_ManDfs( Ivy_Man_t * p ) Vec_Int_t * vNodes; Ivy_Obj_t * pObj; int i; + // make sure the nodes are not marked + Ivy_ManForEachObj( p, pObj, i ) + assert( !pObj->fMarkA && !pObj->fMarkB ); // collect the nodes vNodes = Vec_IntAlloc( Ivy_ManNodeNum(p) ); if ( Ivy_ManLatchNum(p) > 0 ) @@ -107,7 +110,7 @@ void Ivy_ManDfsExt_rec( Ivy_Obj_t * pObj, Vec_Int_t * vNodes ) // traverse the fanins vFanins = Ivy_ObjGetFanins( pObj ); Vec_IntForEachEntry( vFanins, Fanin, i ) - Ivy_ManDfsExt_rec( Ivy_ObjObj(pObj, Ivy_FanId(Fanin)), vNodes ); + Ivy_ManDfsExt_rec( Ivy_ObjObj(pObj, Ivy_EdgeId(Fanin)), vNodes ); // add the node Vec_IntPush( vNodes, pObj->Id ); } @@ -134,7 +137,7 @@ Vec_Int_t * Ivy_ManDfsExt( Ivy_Man_t * p ) vNodes = Vec_IntAlloc( 10 ); Ivy_ManForEachPo( p, pObj, i ) { - pFanin = Ivy_ManObj( p, Ivy_FanId( Ivy_ObjReadFanin(pObj,0) ) ); + pFanin = Ivy_ManObj( p, Ivy_EdgeId( Ivy_ObjReadFanin(pObj,0) ) ); Ivy_ManDfsExt_rec( pFanin, vNodes ); } Ivy_ManForEachNodeVec( p, vNodes, pObj, i ) @@ -145,6 +148,132 @@ Vec_Int_t * Ivy_ManDfsExt( Ivy_Man_t * p ) return vNodes; } +/**Function************************************************************* + + Synopsis [Collects nodes in the cone.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManCollectCone_rec( Ivy_Obj_t * pObj, Vec_Ptr_t * vCone ) +{ + if ( pObj->fMarkA ) + return; + if ( Ivy_ObjIsBuf(pObj) ) + { + Ivy_ManCollectCone_rec( Ivy_ObjFanin0(pObj), vCone ); + Vec_PtrPush( vCone, pObj ); + return; + } + assert( Ivy_ObjIsNode(pObj) ); + Ivy_ManCollectCone_rec( Ivy_ObjFanin0(pObj), vCone ); + Ivy_ManCollectCone_rec( Ivy_ObjFanin1(pObj), vCone ); + Vec_PtrPushUnique( vCone, pObj ); +} + +/**Function************************************************************* + + Synopsis [Collects nodes in the cone.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManCollectCone( Ivy_Obj_t * pObj, Vec_Ptr_t * vFront, Vec_Ptr_t * vCone ) +{ + Ivy_Obj_t * pTemp; + int i; + assert( !Ivy_IsComplement(pObj) ); + assert( Ivy_ObjIsNode(pObj) ); + // mark the nodes + Vec_PtrForEachEntry( vFront, pTemp, i ) + Ivy_Regular(pTemp)->fMarkA = 1; + assert( pObj->fMarkA == 0 ); + // collect the cone + Vec_PtrClear( vCone ); + Ivy_ManCollectCone_rec( pObj, vCone ); + // unmark the nodes + Vec_PtrForEachEntry( vFront, pTemp, i ) + Ivy_Regular(pTemp)->fMarkA = 0; +} + +/**Function************************************************************* + + Synopsis [Returns the nodes by level.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Vec_t * Ivy_ManLevelize( Ivy_Man_t * p ) +{ + Vec_Vec_t * vNodes; + Ivy_Obj_t * pObj; + int i; + vNodes = Vec_VecAlloc( 100 ); + Ivy_ManForEachObj( p, pObj, i ) + { + assert( !Ivy_ObjIsBuf(pObj) ); + if ( Ivy_ObjIsNode(pObj) ) + Vec_VecPush( vNodes, pObj->Level, pObj ); + } + return vNodes; +} + +/**Function************************************************************* + + Synopsis [Computes required levels for each node.] + + Description [Assumes topological ordering of the nodes.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Ivy_ManRequiredLevels( Ivy_Man_t * p ) +{ + Ivy_Obj_t * pObj; + Vec_Int_t * vLevelsR; + Vec_Vec_t * vNodes; + int i, k, Level, LevelMax; + assert( p->vRequired == NULL ); + // start the required times + vLevelsR = Vec_IntStart( Ivy_ManObjIdNext(p) ); + // iterate through the nodes in the reverse order + vNodes = Ivy_ManLevelize( p ); + Vec_VecForEachEntryReverseReverse( vNodes, pObj, i, k ) + { + Level = Vec_IntEntry( vLevelsR, pObj->Id ) + 1 + Ivy_ObjIsExor(pObj); + if ( Vec_IntEntry( vLevelsR, Ivy_ObjFaninId0(pObj) ) < Level ) + Vec_IntWriteEntry( vLevelsR, Ivy_ObjFaninId0(pObj), Level ); + if ( Vec_IntEntry( vLevelsR, Ivy_ObjFaninId1(pObj) ) < Level ) + Vec_IntWriteEntry( vLevelsR, Ivy_ObjFaninId1(pObj), Level ); + } + Vec_VecFree( vNodes ); + // convert it into the required times + LevelMax = Ivy_ManReadLevels( p ); +//printf( "max %5d\n",LevelMax ); + Ivy_ManForEachObj( p, pObj, i ) + { + Level = Vec_IntEntry( vLevelsR, pObj->Id ); + Vec_IntWriteEntry( vLevelsR, pObj->Id, LevelMax - Level ); +//printf( "%5d : %5d %5d\n", pObj->Id, Level, LevelMax - Level ); + } + p->vRequired = vLevelsR; + return vLevelsR; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/temp/ivy/ivyMan.c b/src/temp/ivy/ivyMan.c index 04c31f3d..2ff90aa9 100644 --- a/src/temp/ivy/ivyMan.c +++ b/src/temp/ivy/ivyMan.c @@ -48,6 +48,7 @@ Ivy_Man_t * Ivy_ManStart( int nPis, int nPos, int nNodesMax ) p = ALLOC( Ivy_Man_t, 1 ); memset( p, 0, sizeof(Ivy_Man_t) ); p->nTravIds = 1; + p->fCatchExor = 1; // AIG nodes p->nObjsAlloc = 1 + nPis + nPos + nNodesMax; // p->nObjsAlloc += (p->nObjsAlloc & 1); // make it even @@ -191,12 +192,13 @@ void Ivy_ManPrintStats( Ivy_Man_t * p ) { printf( "A = %d. ", Ivy_ManAndNum(p) ); printf( "X = %d. ", Ivy_ManExorNum(p) ); - printf( "B = %d. ", Ivy_ManBufNum(p) ); + printf( "B = %4d. ", Ivy_ManBufNum(p) ); } - printf( "MaxID = %d. ", p->ObjIdNext-1 ); - printf( "All = %d. ", p->nObjsAlloc ); +// printf( "MaxID = %d. ", p->ObjIdNext-1 ); +// printf( "All = %d. ", p->nObjsAlloc ); printf( "Cre = %d. ", p->nCreated ); printf( "Del = %d. ", p->nDeleted ); + printf( "Lev = %d. ", Ivy_ManReadLevels(p) ); printf( "\n" ); } diff --git a/src/temp/ivy/ivyMulti.c b/src/temp/ivy/ivyMulti.c index 059d1500..e2a44e2d 100644 --- a/src/temp/ivy/ivyMulti.c +++ b/src/temp/ivy/ivyMulti.c @@ -24,22 +24,18 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -typedef struct Ivy_Eval_t_ Ivy_Eval_t; -struct Ivy_Eval_t_ +#define IVY_EVAL_LIMIT 128 + +typedef struct Ivy_Eva_t_ Ivy_Eva_t; +struct Ivy_Eva_t_ { - unsigned Mask : 5; // the mask of covered nodes - unsigned Weight : 3; // the number of covered nodes - unsigned Cost : 4; // the number of overlapping nodes - unsigned Level : 12; // the level of this node - unsigned Fan0 : 4; // the first fanin - unsigned Fan1 : 4; // the second fanin + Ivy_Obj_t * pArg; // the argument node + unsigned Mask; // the mask of covered nodes + int Weight; // the number of covered nodes }; -static Ivy_Obj_t * Ivy_MultiBuild_rec( Ivy_Eval_t * pEvals, int iNum, Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ); -static void Ivy_MultiSort( Ivy_Obj_t ** pArgs, int nArgs ); -static int Ivy_MultiPushUniqueOrderByLevel( Ivy_Obj_t ** pArray, int nArgs, Ivy_Obj_t * pNode ); -static Ivy_Obj_t * Ivy_MultiEval( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ); - +static void Ivy_MultiPrint( Ivy_Eva_t * pEvals, int nLeaves, int nEvals ); +static int Ivy_MultiCover( Ivy_Eva_t * pEvals, int nLeaves, int nEvals, int nLimit, Vec_Ptr_t * vSols ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -47,212 +43,121 @@ static Ivy_Obj_t * Ivy_MultiEval( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type /**Function************************************************************* - Synopsis [Constructs the well-balanced tree of gates.] - - Description [Disregards levels and possible logic sharing.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Ivy_Obj_t * Ivy_Multi_rec( Ivy_Obj_t ** ppObjs, int nObjs, Ivy_Type_t Type ) -{ - Ivy_Obj_t * pObj1, * pObj2; - if ( nObjs == 1 ) - return ppObjs[0]; - pObj1 = Ivy_Multi_rec( ppObjs, nObjs/2, Type ); - pObj2 = Ivy_Multi_rec( ppObjs + nObjs/2, nObjs - nObjs/2, Type ); - return Ivy_Oper( pObj1, pObj2, Type ); -} - -/**Function************************************************************* - Synopsis [Constructs a balanced tree while taking sharing into account.] - Description [] + Description [Returns 1 if the implementation exists.] SideEffects [] SeeAlso [] ***********************************************************************/ -Ivy_Obj_t * Ivy_Multi( Ivy_Obj_t ** pArgsInit, int nArgs, Ivy_Type_t Type ) +int Ivy_MultiPlus( Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, Ivy_Type_t Type, int nLimit, Vec_Ptr_t * vSols ) { - static char NumBits[32] = {0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5}; - static Ivy_Eval_t pEvals[15+15*14/2]; - static Ivy_Obj_t * pArgs[16]; - Ivy_Eval_t * pEva, * pEvaBest; - int nArgsNew, nEvals, i, k; - Ivy_Obj_t * pTemp; - - // consider the case of one argument - assert( nArgs > 0 ); - if ( nArgs == 1 ) - return pArgsInit[0]; - // consider the case of two arguments - if ( nArgs == 2 ) - return Ivy_Oper( pArgsInit[0], pArgsInit[1], Type ); - -//Ivy_MultiEval( pArgsInit, nArgs, Type ); printf( "\n" ); - - // set the initial ones - for ( i = 0; i < nArgs; i++ ) + static Ivy_Eva_t pEvals[IVY_EVAL_LIMIT]; + Ivy_Eva_t * pEval, * pFan0, * pFan1; + Ivy_Obj_t * pObj, * pTemp; + int nEvals, nEvalsOld, i, k, x, nLeaves; + unsigned uMaskAll; + + // consider special cases + nLeaves = Vec_PtrSize(vLeaves); + assert( nLeaves > 2 ); + if ( nLeaves > 32 || nLeaves + Vec_PtrSize(vCone) > IVY_EVAL_LIMIT ) + return 0; +// if ( nLeaves == 1 ) +// return Vec_PtrEntry( vLeaves, 0 ); +// if ( nLeaves == 2 ) +// return Ivy_Oper( Vec_PtrEntry(vLeaves, 0), Vec_PtrEntry(vLeaves, 1), Type ); + + // set the leaf entries + uMaskAll = ((1 << nLeaves) - 1); + nEvals = 0; + Vec_PtrForEachEntry( vLeaves, pObj, i ) { - pArgs[i] = pArgsInit[i]; - pEva = pEvals + i; - pEva->Mask = (1 << i); - pEva->Weight = 1; - pEva->Cost = 0; - pEva->Level = Ivy_Regular(pArgs[i])->Level; - pEva->Fan0 = 0; - pEva->Fan1 = 0; + pEval = pEvals + nEvals; + pEval->pArg = pObj; + pEval->Mask = (1 << nEvals); + pEval->Weight = 1; + // mark the leaf + Ivy_Regular(pObj)->TravId = nEvals; + nEvals++; } - // find the available nodes - pEvaBest = pEvals; - nArgsNew = nArgs; - for ( i = 1; i < nArgsNew; i++ ) - for ( k = 0; k < i; k++ ) - if ( pTemp = Ivy_TableLookup(Ivy_ObjCreateGhost(pArgs[k], pArgs[i], Type, IVY_INIT_NONE)) ) - { - pEva = pEvals + nArgsNew; - pEva->Mask = pEvals[k].Mask | pEvals[i].Mask; - pEva->Weight = NumBits[pEva->Mask]; - pEva->Cost = pEvals[k].Cost + pEvals[i].Cost + NumBits[pEvals[k].Mask & pEvals[i].Mask]; - pEva->Level = 1 + IVY_MAX(pEvals[k].Level, pEvals[i].Level); - pEva->Fan0 = k; - pEva->Fan1 = i; -// assert( pEva->Level == (unsigned)Ivy_ObjLevel(pTemp) ); - // compare - if ( pEvaBest->Weight < pEva->Weight || - pEvaBest->Weight == pEva->Weight && pEvaBest->Cost > pEva->Cost || - pEvaBest->Weight == pEva->Weight && pEvaBest->Cost == pEva->Cost && pEvaBest->Level > pEva->Level ) - pEvaBest = pEva; - // save the argument - pArgs[nArgsNew++] = pTemp; - if ( nArgsNew == 15 ) - goto Outside; - } -Outside: - -// printf( "Best = %d.\n", pEvaBest - pEvals ); - - // the case of no common nodes - if ( nArgsNew == nArgs ) + // propagate masks through the cone + Vec_PtrForEachEntry( vCone, pObj, i ) { - Ivy_MultiSort( pArgs, nArgs ); - return Ivy_MultiBalance_rec( pArgs, nArgs, Type ); + pObj->TravId = nEvals + i; + if ( Ivy_ObjIsBuf(pObj) ) + pEvals[pObj->TravId].Mask = pEvals[Ivy_ObjFanin0(pObj)->TravId].Mask; + else + pEvals[pObj->TravId].Mask = pEvals[Ivy_ObjFanin0(pObj)->TravId].Mask | pEvals[Ivy_ObjFanin1(pObj)->TravId].Mask; } - // the case of one common node - if ( nArgsNew == nArgs + 1 ) + + // set the internal entries + Vec_PtrForEachEntry( vCone, pObj, i ) { - assert( pEvaBest - pEvals == nArgs ); - k = 0; - for ( i = 0; i < nArgs; i++ ) - if ( i != (int)pEvaBest->Fan0 && i != (int)pEvaBest->Fan1 ) - pArgs[k++] = pArgs[i]; - pArgs[k++] = pArgs[nArgs]; - assert( k == nArgs - 1 ); - nArgs = k; - Ivy_MultiSort( pArgs, nArgs ); - return Ivy_MultiBalance_rec( pArgs, nArgs, Type ); + if ( i == Vec_PtrSize(vCone) - 1 ) + break; + // skip buffers + if ( Ivy_ObjIsBuf(pObj) ) + continue; + // skip nodes without external fanout + if ( Ivy_ObjRefs(pObj) == 0 ) + continue; + assert( !Ivy_IsComplement(pObj) ); + pEval = pEvals + nEvals; + pEval->pArg = pObj; + pEval->Mask = pEvals[pObj->TravId].Mask; + pEval->Weight = Extra_WordCountOnes(pEval->Mask); + // mark the node + pObj->TravId = nEvals; + nEvals++; } - // the case when there is a node that covers everything - if ( (int)pEvaBest->Mask == ((1 << nArgs) - 1) ) - return Ivy_MultiBuild_rec( pEvals, pEvaBest - pEvals, pArgs, nArgsNew, Type ); - // evaluate node pairs - nEvals = nArgsNew; - for ( i = 1; i < nArgsNew; i++ ) + // find the available nodes + nEvalsOld = nEvals; + for ( i = 1; i < nEvals; i++ ) for ( k = 0; k < i; k++ ) { - pEva = pEvals + nEvals; - pEva->Mask = pEvals[k].Mask | pEvals[i].Mask; - pEva->Weight = NumBits[pEva->Mask]; - pEva->Cost = pEvals[k].Cost + pEvals[i].Cost + NumBits[pEvals[k].Mask & pEvals[i].Mask]; - pEva->Level = 1 + IVY_MAX(pEvals[k].Level, pEvals[i].Level); - pEva->Fan0 = k; - pEva->Fan1 = i; - // compare - if ( pEvaBest->Weight < pEva->Weight || - pEvaBest->Weight == pEva->Weight && pEvaBest->Cost > pEva->Cost || - pEvaBest->Weight == pEva->Weight && pEvaBest->Cost == pEva->Cost && pEvaBest->Level > pEva->Level ) - pEvaBest = pEva; + pFan0 = pEvals + i; + pFan1 = pEvals + k; + pTemp = Ivy_TableLookup(Ivy_ObjCreateGhost(pFan0->pArg, pFan1->pArg, Type, IVY_INIT_NONE)); + // skip nodes in the cone + if ( pTemp == NULL || pTemp->fMarkB ) + continue; + // skip the leaves + for ( x = 0; x < nLeaves; x++ ) + if ( pTemp == Ivy_Regular(vLeaves->pArray[x]) ) + break; + if ( x < nLeaves ) + continue; + pEval = pEvals + nEvals; + pEval->pArg = pTemp; + pEval->Mask = pFan0->Mask | pFan1->Mask; + pEval->Weight = (pFan0->Mask & pFan1->Mask) ? Extra_WordCountOnes(pEval->Mask) : pFan0->Weight + pFan1->Weight; // save the argument + pObj->TravId = nEvals; nEvals++; + // quit if the number of entries exceeded the limit + if ( nEvals == IVY_EVAL_LIMIT ) + goto Outside; + // quit if we found an acceptable implementation + if ( pEval->Mask == uMaskAll ) + goto Outside; } - assert( pEvaBest - pEvals >= nArgsNew ); - -// printf( "Used (%d, %d).\n", pEvaBest->Fan0, pEvaBest->Fan1 ); - - // get the best implementation - pTemp = Ivy_MultiBuild_rec( pEvals, pEvaBest - pEvals, pArgs, nArgsNew, Type ); - - // collect those not covered by EvaBest - k = 0; - for ( i = 0; i < nArgs; i++ ) - if ( (pEvaBest->Mask & (1 << i)) == 0 ) - pArgs[k++] = pArgs[i]; - pArgs[k++] = pTemp; - assert( k == nArgs - (int)pEvaBest->Weight + 1 ); - nArgs = k; - Ivy_MultiSort( pArgs, nArgs ); - return Ivy_MultiBalance_rec( pArgs, nArgs, Type ); -} - -/**Function************************************************************* - - Synopsis [Implements multi-input AND/EXOR operation.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Ivy_Obj_t * Ivy_MultiBuild_rec( Ivy_Eval_t * pEvals, int iNum, Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ) -{ - Ivy_Obj_t * pNode0, * pNode1; - if ( iNum < nArgs ) - return pArgs[iNum]; - pNode0 = Ivy_MultiBuild_rec( pEvals, pEvals[iNum].Fan0, pArgs, nArgs, Type ); - pNode1 = Ivy_MultiBuild_rec( pEvals, pEvals[iNum].Fan1, pArgs, nArgs, Type ); - return Ivy_Oper( pNode0, pNode1, Type ); -} - -/**Function************************************************************* - - Synopsis [Selection-sorts the nodes in the decreasing over of level.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ivy_MultiSort( Ivy_Obj_t ** pArgs, int nArgs ) -{ - Ivy_Obj_t * pTemp; - int i, j, iBest; +Outside: - for ( i = 0; i < nArgs-1; i++ ) - { - iBest = i; - for ( j = i+1; j < nArgs; j++ ) - if ( Ivy_Regular(pArgs[j])->Level > Ivy_Regular(pArgs[iBest])->Level ) - iBest = j; - pTemp = pArgs[i]; - pArgs[i] = pArgs[iBest]; - pArgs[iBest] = pTemp; - } +// Ivy_MultiPrint( pEvals, nLeaves, nEvals ); + if ( !Ivy_MultiCover( pEvals, nLeaves, nEvals, nLimit, vSols ) ) + return 0; + assert( Vec_PtrSize( vSols ) > 0 ); + return 1; } /**Function************************************************************* - Synopsis [Inserts a new node in the order by levels.] + Synopsis [Computes how many uncovered ones this one covers.] Description [] @@ -261,32 +166,28 @@ void Ivy_MultiSort( Ivy_Obj_t ** pArgs, int nArgs ) SeeAlso [] ***********************************************************************/ -int Ivy_MultiPushUniqueOrderByLevel( Ivy_Obj_t ** pArray, int nArgs, Ivy_Obj_t * pNode ) +void Ivy_MultiPrint( Ivy_Eva_t * pEvals, int nLeaves, int nEvals ) { - Ivy_Obj_t * pNode1, * pNode2; - int i; - // try to find the node in the array - for ( i = 0; i < nArgs; i++ ) - if ( pArray[i] == pNode ) - return nArgs; - // put the node last - pArray[nArgs++] = pNode; - // find the place to put the new node - for ( i = nArgs-1; i > 0; i-- ) + Ivy_Eva_t * pEval; + int i, k; + for ( i = nLeaves; i < nEvals; i++ ) { - pNode1 = pArray[i ]; - pNode2 = pArray[i-1]; - if ( Ivy_Regular(pNode1)->Level <= Ivy_Regular(pNode2)->Level ) - break; - pArray[i ] = pNode2; - pArray[i-1] = pNode1; + pEval = pEvals + i; + printf( "%2d (id = %5d) : |", i-nLeaves, Ivy_ObjId(pEval->pArg) ); + for ( k = 0; k < nLeaves; k++ ) + { + if ( pEval->Mask & (1 << k) ) + printf( "+" ); + else + printf( " " ); + } + printf( "| Lev = %d.\n", Ivy_ObjLevel(pEval->pArg) ); } - return nArgs; } /**Function************************************************************* - Synopsis [Balances the array recursively.] + Synopsis [Computes how many uncovered ones this one covers.] Description [] @@ -295,129 +196,102 @@ int Ivy_MultiPushUniqueOrderByLevel( Ivy_Obj_t ** pArray, int nArgs, Ivy_Obj_t * SeeAlso [] ***********************************************************************/ -Ivy_Obj_t * Ivy_MultiBalance_rec( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ) +static inline int Ivy_MultiWeight( unsigned uMask, int nMaskOnes, unsigned uFound ) { - Ivy_Obj_t * pNodeNew; - // consider the case of one argument - assert( nArgs > 0 ); - if ( nArgs == 1 ) - return pArgs[0]; - // consider the case of two arguments - if ( nArgs == 2 ) - return Ivy_Oper( pArgs[0], pArgs[1], Type ); - // get the last two nodes - pNodeNew = Ivy_Oper( pArgs[nArgs-1], pArgs[nArgs-2], Type ); - // add the new node - nArgs = Ivy_MultiPushUniqueOrderByLevel( pArgs, nArgs - 2, pNodeNew ); - return Ivy_MultiBalance_rec( pArgs, nArgs, Type ); + assert( uMask & ~uFound ); + if ( (uMask & uFound) == 0 ) + return nMaskOnes; + return Extra_WordCountOnes( uMask & ~uFound ); } /**Function************************************************************* - Synopsis [Implements multi-input AND/EXOR operation.] + Synopsis [Finds the cover.] - Description [] + Description [Returns 1 if the cover is found.] SideEffects [] SeeAlso [] ***********************************************************************/ -Ivy_Obj_t * Ivy_MultiEval( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ) +int Ivy_MultiCover( Ivy_Eva_t * pEvals, int nLeaves, int nEvals, int nLimit, Vec_Ptr_t * vSols ) { - Ivy_Obj_t * pTemp; - int i, k; - int nArgsOld = nArgs; - for ( i = 0; i < nArgs; i++ ) - printf( "%d[%d] ", i, Ivy_Regular(pArgs[i])->Level ); - for ( i = 1; i < nArgs; i++ ) - for ( k = 0; k < i; k++ ) + int fVerbose = 0; + Ivy_Eva_t * pEval, * pEvalBest; + unsigned uMaskAll, uFound, uTemp; + int i, k, BestK, WeightBest, WeightCur, LevelBest, LevelCur; + uMaskAll = (nLeaves == 32)? (~(unsigned)0) : ((1 << nLeaves) - 1); + uFound = 0; + // solve the covering problem + if ( fVerbose ) + printf( "Solution: " ); + Vec_PtrClear( vSols ); + for ( i = 0; i < nLimit; i++ ) + { + BestK = -1; + for ( k = nEvals - 1; k >= 0; k-- ) { - pTemp = Ivy_TableLookup(Ivy_ObjCreateGhost(pArgs[k], pArgs[i], Type, IVY_INIT_NONE)); - if ( pTemp != NULL ) + pEval = pEvals + k; + if ( (pEval->Mask & ~uFound) == 0 ) + continue; + if ( BestK == -1 ) { - printf( "%d[%d]=(%d,%d) ", nArgs, Ivy_Regular(pTemp)->Level, k, i ); - pArgs[nArgs++] = pTemp; + BestK = k; + pEvalBest = pEval; + WeightBest = Ivy_MultiWeight( pEvalBest->Mask, pEvalBest->Weight, uFound ); + LevelBest = Ivy_ObjLevel( Ivy_Regular(pEvalBest->pArg) ); + continue; + } + // compare BestK and the new one (k) + WeightCur = Ivy_MultiWeight( pEval->Mask, pEval->Weight, uFound ); + LevelCur = Ivy_ObjLevel( Ivy_Regular(pEval->pArg) ); + if ( WeightBest < WeightCur || + (WeightBest == WeightCur && LevelBest > LevelCur) ) + { + BestK = k; + pEvalBest = pEval; + WeightBest = WeightCur; + LevelBest = LevelCur; } } - printf( " ((%d/%d)) ", nArgsOld, nArgs-nArgsOld ); - return NULL; -} - - - -/**Function************************************************************* - - Synopsis [Old code.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Ivy_Obj_t * Ivy_Multi1( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ) -{ - Ivy_Obj_t * pArgsRef[5], * pTemp; - int i, k, m, nArgsNew, Counter = 0; - - -//Ivy_MultiEval( pArgs, nArgs, Type ); printf( "\n" ); - - - assert( Type == IVY_AND || Type == IVY_EXOR ); - assert( nArgs > 0 ); - if ( nArgs == 1 ) - return pArgs[0]; - - // find the nodes with more than one fanout - nArgsNew = 0; - for ( i = 0; i < nArgs; i++ ) - if ( Ivy_ObjRefs( Ivy_Regular(pArgs[i]) ) > 0 ) - pArgsRef[nArgsNew++] = pArgs[i]; - - // go through pairs - if ( nArgsNew >= 2 ) - for ( i = 0; i < nArgsNew; i++ ) - for ( k = i + 1; k < nArgsNew; k++ ) - if ( pTemp = Ivy_TableLookup(Ivy_ObjCreateGhost(pArgsRef[i], pArgsRef[k], Type, IVY_INIT_NONE)) ) - Counter++; -// printf( "%d", Counter ); - - // go through pairs - if ( nArgsNew >= 2 ) - for ( i = 0; i < nArgsNew; i++ ) - for ( k = i + 1; k < nArgsNew; k++ ) - if ( pTemp = Ivy_TableLookup(Ivy_ObjCreateGhost(pArgsRef[i], pArgsRef[k], Type, IVY_INIT_NONE)) ) + assert( BestK != -1 ); + // if the cost is only 1, take the leaf + if ( WeightBest == 1 && BestK >= nLeaves ) { - nArgsNew = 0; - for ( m = 0; m < nArgs; m++ ) - if ( pArgs[m] != pArgsRef[i] && pArgs[m] != pArgsRef[k] ) - pArgs[nArgsNew++] = pArgs[m]; - pArgs[nArgsNew++] = pTemp; - assert( nArgsNew == nArgs - 1 ); - return Ivy_Multi1( pArgs, nArgsNew, Type ); + uTemp = (pEvalBest->Mask & ~uFound); + for ( k = 0; k < nLeaves; k++ ) + if ( uTemp & (1 << k) ) + break; + assert( k < nLeaves ); + BestK = k; + pEvalBest = pEvals + BestK; } - return Ivy_Multi_rec( pArgs, nArgs, Type ); -} - -/**Function************************************************************* - - Synopsis [Old code.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Ivy_Obj_t * Ivy_Multi2( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ) -{ - assert( Type == IVY_AND || Type == IVY_EXOR ); - assert( nArgs > 0 ); - return Ivy_Multi_rec( pArgs, nArgs, Type ); + if ( fVerbose ) + { + if ( BestK < nLeaves ) + printf( "L(%d) ", BestK ); + else + printf( "%d ", BestK - nLeaves ); + } + // update the found set + Vec_PtrPush( vSols, pEvalBest->pArg ); + uFound |= pEvalBest->Mask; + if ( uFound == uMaskAll ) + break; + } + if ( uFound == uMaskAll ) + { + if ( fVerbose ) + printf( " Found \n\n" ); + return 1; + } + else + { + if ( fVerbose ) + printf( " Not found \n\n" ); + return 0; + } } //////////////////////////////////////////////////////////////////////// diff --git a/src/temp/ivy/ivyMulti8.c b/src/temp/ivy/ivyMulti8.c new file mode 100644 index 00000000..059d1500 --- /dev/null +++ b/src/temp/ivy/ivyMulti8.c @@ -0,0 +1,427 @@ +/**CFile**************************************************************** + + FileName [ivyMulti.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [Constructing multi-input AND/EXOR gates.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: ivyMulti.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ivy.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Ivy_Eval_t_ Ivy_Eval_t; +struct Ivy_Eval_t_ +{ + unsigned Mask : 5; // the mask of covered nodes + unsigned Weight : 3; // the number of covered nodes + unsigned Cost : 4; // the number of overlapping nodes + unsigned Level : 12; // the level of this node + unsigned Fan0 : 4; // the first fanin + unsigned Fan1 : 4; // the second fanin +}; + +static Ivy_Obj_t * Ivy_MultiBuild_rec( Ivy_Eval_t * pEvals, int iNum, Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ); +static void Ivy_MultiSort( Ivy_Obj_t ** pArgs, int nArgs ); +static int Ivy_MultiPushUniqueOrderByLevel( Ivy_Obj_t ** pArray, int nArgs, Ivy_Obj_t * pNode ); +static Ivy_Obj_t * Ivy_MultiEval( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ); + + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Constructs the well-balanced tree of gates.] + + Description [Disregards levels and possible logic sharing.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_Multi_rec( Ivy_Obj_t ** ppObjs, int nObjs, Ivy_Type_t Type ) +{ + Ivy_Obj_t * pObj1, * pObj2; + if ( nObjs == 1 ) + return ppObjs[0]; + pObj1 = Ivy_Multi_rec( ppObjs, nObjs/2, Type ); + pObj2 = Ivy_Multi_rec( ppObjs + nObjs/2, nObjs - nObjs/2, Type ); + return Ivy_Oper( pObj1, pObj2, Type ); +} + +/**Function************************************************************* + + Synopsis [Constructs a balanced tree while taking sharing into account.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_Multi( Ivy_Obj_t ** pArgsInit, int nArgs, Ivy_Type_t Type ) +{ + static char NumBits[32] = {0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5}; + static Ivy_Eval_t pEvals[15+15*14/2]; + static Ivy_Obj_t * pArgs[16]; + Ivy_Eval_t * pEva, * pEvaBest; + int nArgsNew, nEvals, i, k; + Ivy_Obj_t * pTemp; + + // consider the case of one argument + assert( nArgs > 0 ); + if ( nArgs == 1 ) + return pArgsInit[0]; + // consider the case of two arguments + if ( nArgs == 2 ) + return Ivy_Oper( pArgsInit[0], pArgsInit[1], Type ); + +//Ivy_MultiEval( pArgsInit, nArgs, Type ); printf( "\n" ); + + // set the initial ones + for ( i = 0; i < nArgs; i++ ) + { + pArgs[i] = pArgsInit[i]; + pEva = pEvals + i; + pEva->Mask = (1 << i); + pEva->Weight = 1; + pEva->Cost = 0; + pEva->Level = Ivy_Regular(pArgs[i])->Level; + pEva->Fan0 = 0; + pEva->Fan1 = 0; + } + + // find the available nodes + pEvaBest = pEvals; + nArgsNew = nArgs; + for ( i = 1; i < nArgsNew; i++ ) + for ( k = 0; k < i; k++ ) + if ( pTemp = Ivy_TableLookup(Ivy_ObjCreateGhost(pArgs[k], pArgs[i], Type, IVY_INIT_NONE)) ) + { + pEva = pEvals + nArgsNew; + pEva->Mask = pEvals[k].Mask | pEvals[i].Mask; + pEva->Weight = NumBits[pEva->Mask]; + pEva->Cost = pEvals[k].Cost + pEvals[i].Cost + NumBits[pEvals[k].Mask & pEvals[i].Mask]; + pEva->Level = 1 + IVY_MAX(pEvals[k].Level, pEvals[i].Level); + pEva->Fan0 = k; + pEva->Fan1 = i; +// assert( pEva->Level == (unsigned)Ivy_ObjLevel(pTemp) ); + // compare + if ( pEvaBest->Weight < pEva->Weight || + pEvaBest->Weight == pEva->Weight && pEvaBest->Cost > pEva->Cost || + pEvaBest->Weight == pEva->Weight && pEvaBest->Cost == pEva->Cost && pEvaBest->Level > pEva->Level ) + pEvaBest = pEva; + // save the argument + pArgs[nArgsNew++] = pTemp; + if ( nArgsNew == 15 ) + goto Outside; + } +Outside: + +// printf( "Best = %d.\n", pEvaBest - pEvals ); + + // the case of no common nodes + if ( nArgsNew == nArgs ) + { + Ivy_MultiSort( pArgs, nArgs ); + return Ivy_MultiBalance_rec( pArgs, nArgs, Type ); + } + // the case of one common node + if ( nArgsNew == nArgs + 1 ) + { + assert( pEvaBest - pEvals == nArgs ); + k = 0; + for ( i = 0; i < nArgs; i++ ) + if ( i != (int)pEvaBest->Fan0 && i != (int)pEvaBest->Fan1 ) + pArgs[k++] = pArgs[i]; + pArgs[k++] = pArgs[nArgs]; + assert( k == nArgs - 1 ); + nArgs = k; + Ivy_MultiSort( pArgs, nArgs ); + return Ivy_MultiBalance_rec( pArgs, nArgs, Type ); + } + // the case when there is a node that covers everything + if ( (int)pEvaBest->Mask == ((1 << nArgs) - 1) ) + return Ivy_MultiBuild_rec( pEvals, pEvaBest - pEvals, pArgs, nArgsNew, Type ); + + // evaluate node pairs + nEvals = nArgsNew; + for ( i = 1; i < nArgsNew; i++ ) + for ( k = 0; k < i; k++ ) + { + pEva = pEvals + nEvals; + pEva->Mask = pEvals[k].Mask | pEvals[i].Mask; + pEva->Weight = NumBits[pEva->Mask]; + pEva->Cost = pEvals[k].Cost + pEvals[i].Cost + NumBits[pEvals[k].Mask & pEvals[i].Mask]; + pEva->Level = 1 + IVY_MAX(pEvals[k].Level, pEvals[i].Level); + pEva->Fan0 = k; + pEva->Fan1 = i; + // compare + if ( pEvaBest->Weight < pEva->Weight || + pEvaBest->Weight == pEva->Weight && pEvaBest->Cost > pEva->Cost || + pEvaBest->Weight == pEva->Weight && pEvaBest->Cost == pEva->Cost && pEvaBest->Level > pEva->Level ) + pEvaBest = pEva; + // save the argument + nEvals++; + } + assert( pEvaBest - pEvals >= nArgsNew ); + +// printf( "Used (%d, %d).\n", pEvaBest->Fan0, pEvaBest->Fan1 ); + + // get the best implementation + pTemp = Ivy_MultiBuild_rec( pEvals, pEvaBest - pEvals, pArgs, nArgsNew, Type ); + + // collect those not covered by EvaBest + k = 0; + for ( i = 0; i < nArgs; i++ ) + if ( (pEvaBest->Mask & (1 << i)) == 0 ) + pArgs[k++] = pArgs[i]; + pArgs[k++] = pTemp; + assert( k == nArgs - (int)pEvaBest->Weight + 1 ); + nArgs = k; + Ivy_MultiSort( pArgs, nArgs ); + return Ivy_MultiBalance_rec( pArgs, nArgs, Type ); +} + +/**Function************************************************************* + + Synopsis [Implements multi-input AND/EXOR operation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_MultiBuild_rec( Ivy_Eval_t * pEvals, int iNum, Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ) +{ + Ivy_Obj_t * pNode0, * pNode1; + if ( iNum < nArgs ) + return pArgs[iNum]; + pNode0 = Ivy_MultiBuild_rec( pEvals, pEvals[iNum].Fan0, pArgs, nArgs, Type ); + pNode1 = Ivy_MultiBuild_rec( pEvals, pEvals[iNum].Fan1, pArgs, nArgs, Type ); + return Ivy_Oper( pNode0, pNode1, Type ); +} + +/**Function************************************************************* + + Synopsis [Selection-sorts the nodes in the decreasing over of level.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_MultiSort( Ivy_Obj_t ** pArgs, int nArgs ) +{ + Ivy_Obj_t * pTemp; + int i, j, iBest; + + for ( i = 0; i < nArgs-1; i++ ) + { + iBest = i; + for ( j = i+1; j < nArgs; j++ ) + if ( Ivy_Regular(pArgs[j])->Level > Ivy_Regular(pArgs[iBest])->Level ) + iBest = j; + pTemp = pArgs[i]; + pArgs[i] = pArgs[iBest]; + pArgs[iBest] = pTemp; + } +} + +/**Function************************************************************* + + Synopsis [Inserts a new node in the order by levels.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_MultiPushUniqueOrderByLevel( Ivy_Obj_t ** pArray, int nArgs, Ivy_Obj_t * pNode ) +{ + Ivy_Obj_t * pNode1, * pNode2; + int i; + // try to find the node in the array + for ( i = 0; i < nArgs; i++ ) + if ( pArray[i] == pNode ) + return nArgs; + // put the node last + pArray[nArgs++] = pNode; + // find the place to put the new node + for ( i = nArgs-1; i > 0; i-- ) + { + pNode1 = pArray[i ]; + pNode2 = pArray[i-1]; + if ( Ivy_Regular(pNode1)->Level <= Ivy_Regular(pNode2)->Level ) + break; + pArray[i ] = pNode2; + pArray[i-1] = pNode1; + } + return nArgs; +} + +/**Function************************************************************* + + Synopsis [Balances the array recursively.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_MultiBalance_rec( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ) +{ + Ivy_Obj_t * pNodeNew; + // consider the case of one argument + assert( nArgs > 0 ); + if ( nArgs == 1 ) + return pArgs[0]; + // consider the case of two arguments + if ( nArgs == 2 ) + return Ivy_Oper( pArgs[0], pArgs[1], Type ); + // get the last two nodes + pNodeNew = Ivy_Oper( pArgs[nArgs-1], pArgs[nArgs-2], Type ); + // add the new node + nArgs = Ivy_MultiPushUniqueOrderByLevel( pArgs, nArgs - 2, pNodeNew ); + return Ivy_MultiBalance_rec( pArgs, nArgs, Type ); +} + +/**Function************************************************************* + + Synopsis [Implements multi-input AND/EXOR operation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_MultiEval( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ) +{ + Ivy_Obj_t * pTemp; + int i, k; + int nArgsOld = nArgs; + for ( i = 0; i < nArgs; i++ ) + printf( "%d[%d] ", i, Ivy_Regular(pArgs[i])->Level ); + for ( i = 1; i < nArgs; i++ ) + for ( k = 0; k < i; k++ ) + { + pTemp = Ivy_TableLookup(Ivy_ObjCreateGhost(pArgs[k], pArgs[i], Type, IVY_INIT_NONE)); + if ( pTemp != NULL ) + { + printf( "%d[%d]=(%d,%d) ", nArgs, Ivy_Regular(pTemp)->Level, k, i ); + pArgs[nArgs++] = pTemp; + } + } + printf( " ((%d/%d)) ", nArgsOld, nArgs-nArgsOld ); + return NULL; +} + + + +/**Function************************************************************* + + Synopsis [Old code.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_Multi1( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ) +{ + Ivy_Obj_t * pArgsRef[5], * pTemp; + int i, k, m, nArgsNew, Counter = 0; + + +//Ivy_MultiEval( pArgs, nArgs, Type ); printf( "\n" ); + + + assert( Type == IVY_AND || Type == IVY_EXOR ); + assert( nArgs > 0 ); + if ( nArgs == 1 ) + return pArgs[0]; + + // find the nodes with more than one fanout + nArgsNew = 0; + for ( i = 0; i < nArgs; i++ ) + if ( Ivy_ObjRefs( Ivy_Regular(pArgs[i]) ) > 0 ) + pArgsRef[nArgsNew++] = pArgs[i]; + + // go through pairs + if ( nArgsNew >= 2 ) + for ( i = 0; i < nArgsNew; i++ ) + for ( k = i + 1; k < nArgsNew; k++ ) + if ( pTemp = Ivy_TableLookup(Ivy_ObjCreateGhost(pArgsRef[i], pArgsRef[k], Type, IVY_INIT_NONE)) ) + Counter++; +// printf( "%d", Counter ); + + // go through pairs + if ( nArgsNew >= 2 ) + for ( i = 0; i < nArgsNew; i++ ) + for ( k = i + 1; k < nArgsNew; k++ ) + if ( pTemp = Ivy_TableLookup(Ivy_ObjCreateGhost(pArgsRef[i], pArgsRef[k], Type, IVY_INIT_NONE)) ) + { + nArgsNew = 0; + for ( m = 0; m < nArgs; m++ ) + if ( pArgs[m] != pArgsRef[i] && pArgs[m] != pArgsRef[k] ) + pArgs[nArgsNew++] = pArgs[m]; + pArgs[nArgsNew++] = pTemp; + assert( nArgsNew == nArgs - 1 ); + return Ivy_Multi1( pArgs, nArgsNew, Type ); + } + return Ivy_Multi_rec( pArgs, nArgs, Type ); +} + +/**Function************************************************************* + + Synopsis [Old code.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_Multi2( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type ) +{ + assert( Type == IVY_AND || Type == IVY_EXOR ); + assert( nArgs > 0 ); + return Ivy_Multi_rec( pArgs, nArgs, Type ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ivy/ivyObj.c b/src/temp/ivy/ivyObj.c index 5d063525..703218bb 100644 --- a/src/temp/ivy/ivyObj.c +++ b/src/temp/ivy/ivyObj.c @@ -51,6 +51,7 @@ Ivy_Obj_t * Ivy_ObjCreate( Ivy_Obj_t * pGhost ) // realloc the node array if ( p->ObjIdNext == p->nObjsAlloc ) { + printf( "AIG manager is being resized. In the current release, it is not allowed!\n" ); Ivy_ManGrow( p ); pGhost = Ivy_ManGhost( p ); } diff --git a/src/temp/ivy/ivyOper.c b/src/temp/ivy/ivyOper.c index a10ba343..96f78165 100644 --- a/src/temp/ivy/ivyOper.c +++ b/src/temp/ivy/ivyOper.c @@ -81,7 +81,7 @@ Ivy_Obj_t * Ivy_Oper( Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Type_t Type ) Ivy_Obj_t * Ivy_And( Ivy_Obj_t * p0, Ivy_Obj_t * p1 ) { Ivy_Obj_t * pConst1 = Ivy_ObjConst1(Ivy_Regular(p0)); - Ivy_Obj_t * pFan0, * pFan1; +// Ivy_Obj_t * pFan0, * pFan1; // check trivial cases if ( p0 == p1 ) return p0; @@ -92,8 +92,8 @@ Ivy_Obj_t * Ivy_And( Ivy_Obj_t * p0, Ivy_Obj_t * p1 ) if ( Ivy_Regular(p1) == pConst1 ) return p1 == pConst1 ? p0 : Ivy_Not(pConst1); // check if it can be an EXOR gate - if ( Ivy_ObjIsExorType( p0, p1, &pFan0, &pFan1 ) ) - return Ivy_CanonExor( pFan0, pFan1 ); +// if ( Ivy_ObjIsExorType( p0, p1, &pFan0, &pFan1 ) ) +// return Ivy_CanonExor( pFan0, pFan1 ); return Ivy_CanonAnd( p0, p1 ); } diff --git a/src/temp/ivy/ivyResyn.c b/src/temp/ivy/ivyResyn.c new file mode 100644 index 00000000..2d65e7f7 --- /dev/null +++ b/src/temp/ivy/ivyResyn.c @@ -0,0 +1,96 @@ +/**CFile**************************************************************** + + FileName [ivyResyn.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [AIG rewriting script.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: ivyResyn.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ivy.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Performs several passes of rewriting on the AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Man_t * Ivy_ManResyn( Ivy_Man_t * pMan, int fUpdateLevel ) +{ + int clk, fVerbose = 0; + Ivy_Man_t * pTemp; + +if ( fVerbose ) Ivy_ManPrintStats( pMan ); +clk = clock(); + pMan = Ivy_ManBalance( pMan, fUpdateLevel ); +if ( fVerbose ) { PRT( "Balance", clock() - clk ); } +if ( fVerbose ) Ivy_ManPrintStats( pMan ); + +// Ivy_ManRewriteAlg( pMan, fUpdateLevel, 0 ); +clk = clock(); + Ivy_ManRewritePre( pMan, fUpdateLevel, 0, 0 ); +if ( fVerbose ) { PRT( "Rewrite", clock() - clk ); } +if ( fVerbose ) Ivy_ManPrintStats( pMan ); + +clk = clock(); + pMan = Ivy_ManBalance( pTemp = pMan, fUpdateLevel ); + Ivy_ManStop( pTemp ); +if ( fVerbose ) { PRT( "Balance", clock() - clk ); } +if ( fVerbose ) Ivy_ManPrintStats( pMan ); + +// Ivy_ManRewriteAlg( pMan, fUpdateLevel, 1 ); +clk = clock(); +if ( fVerbose ) Ivy_ManRewritePre( pMan, fUpdateLevel, 1, 0 ); +if ( fVerbose ) { PRT( "Rewrite", clock() - clk ); } +if ( fVerbose ) Ivy_ManPrintStats( pMan ); + +clk = clock(); + pMan = Ivy_ManBalance( pTemp = pMan, fUpdateLevel ); + Ivy_ManStop( pTemp ); +if ( fVerbose ) { PRT( "Balance", clock() - clk ); } +if ( fVerbose ) Ivy_ManPrintStats( pMan ); + +// Ivy_ManRewriteAlg( pMan, fUpdateLevel, 1 ); +clk = clock(); + Ivy_ManRewritePre( pMan, fUpdateLevel, 1, 0 ); +if ( fVerbose ) { PRT( "Rewrite", clock() - clk ); } +if ( fVerbose ) Ivy_ManPrintStats( pMan ); + +clk = clock(); + pMan = Ivy_ManBalance( pTemp = pMan, fUpdateLevel ); + Ivy_ManStop( pTemp ); +if ( fVerbose ) { PRT( "Balance", clock() - clk ); } +if ( fVerbose ) Ivy_ManPrintStats( pMan ); + return pMan; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ivy/ivyRwrAlg.c b/src/temp/ivy/ivyRwrAlg.c new file mode 100644 index 00000000..234827ff --- /dev/null +++ b/src/temp/ivy/ivyRwrAlg.c @@ -0,0 +1,408 @@ +/**CFile**************************************************************** + + FileName [ivyRwrAlg.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [Algebraic AIG rewriting.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: ivyRwrAlg.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ivy.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static int Ivy_ManFindAlgCut( Ivy_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone ); +static Ivy_Obj_t * Ivy_NodeRewriteAlg( Ivy_Obj_t * pObj, Vec_Ptr_t * vFront, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, Vec_Ptr_t * vSols, int LevelR, int fUseZeroCost ); +static int Ivy_NodeCountMffc( Ivy_Obj_t * pNode ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Algebraic AIG rewriting.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_ManRewriteAlg( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost ) +{ + Vec_Int_t * vRequired; + Vec_Ptr_t * vFront, * vLeaves, * vCone, * vSol; + Ivy_Obj_t * pObj, * pResult; + int i, RetValue, LevelR, nNodesOld; + int CountUsed, CountUndo; + vRequired = fUpdateLevel? Ivy_ManRequiredLevels( p ) : NULL; + vFront = Vec_PtrAlloc( 100 ); + vLeaves = Vec_PtrAlloc( 100 ); + vCone = Vec_PtrAlloc( 100 ); + vSol = Vec_PtrAlloc( 100 ); + // go through the nodes in the topological order + CountUsed = CountUndo = 0; + nNodesOld = Ivy_ManObjIdNext(p); + Ivy_ManForEachObj( p, pObj, i ) + { + assert( !Ivy_ObjIsBuf(pObj) ); + if ( i >= nNodesOld ) + break; + // skip no-nodes and MUX roots + if ( !Ivy_ObjIsNode(pObj) || Ivy_ObjIsExor(pObj) || Ivy_ObjIsMuxType(pObj) ) + continue; +// if ( pObj->Id > 297 ) // 296 --- 297 +// break; + if ( pObj->Id == 297 ) + { + int x = 0; + } + // get the largest algebraic cut + RetValue = Ivy_ManFindAlgCut( pObj, vFront, vLeaves, vCone ); + // the case of a trivial tree cut + if ( RetValue == 1 ) + continue; + // the case of constant 0 cone + if ( RetValue == -1 ) + { + Ivy_ObjReplace( pObj, Ivy_ManConst0(p), 1, 0 ); + continue; + } + assert( Vec_PtrSize(vLeaves) > 2 ); + // get the required level for this node + LevelR = vRequired? Vec_IntEntry(vRequired, pObj->Id) : 1000000; + // create a new cone + pResult = Ivy_NodeRewriteAlg( pObj, vFront, vLeaves, vCone, vSol, LevelR, fUseZeroCost ); + if ( pResult == NULL || pResult == pObj ) + continue; + assert( Vec_PtrSize(vSol) == 1 || !Ivy_IsComplement(pResult) ); + if ( Ivy_ObjLevel(Ivy_Regular(pResult)) > LevelR && Ivy_ObjRefs(Ivy_Regular(pResult)) == 0 ) + Ivy_ObjDelete_rec(Ivy_Regular(pResult), 1), CountUndo++; + else + Ivy_ObjReplace( pObj, pResult, 1, 0 ), CountUsed++; + } + printf( "Used = %d. Undo = %d.\n", CountUsed, CountUndo ); + Vec_PtrFree( vFront ); + Vec_PtrFree( vCone ); + Vec_PtrFree( vSol ); + if ( vRequired ) Vec_IntFree( vRequired ); + if ( i = Ivy_ManCleanup(p) ) + printf( "Cleanup after rewriting removed %d dangling nodes.\n", i ); + if ( !Ivy_ManCheck(p) ) + printf( "Ivy_ManRewriteAlg(): The check has failed.\n" ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Analizes one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_NodeRewriteAlg( Ivy_Obj_t * pObj, Vec_Ptr_t * vFront, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, Vec_Ptr_t * vSols, int LevelR, int fUseZeroCost ) +{ + int fVerbose = 0; + Ivy_Obj_t * pTemp; + int k, Counter, nMffc, RetValue; + + if ( fVerbose ) + { + if ( Ivy_ObjIsExor(pObj) ) + printf( "x " ); + else + printf( " " ); + } + +/* + printf( "%d ", Vec_PtrSize(vFront) ); + printf( "( " ); + Vec_PtrForEachEntry( vFront, pTemp, k ) + printf( "%d ", Ivy_ObjRefs(Ivy_Regular(pTemp)) ); + printf( ")\n" ); +*/ + // collect nodes in the cone + if ( Ivy_ObjIsExor(pObj) ) + Ivy_ManCollectCone( pObj, vFront, vCone ); + else + Ivy_ManCollectCone( pObj, vLeaves, vCone ); + + // deref nodes in the cone + Vec_PtrForEachEntry( vCone, pTemp, k ) + { + Ivy_ObjRefsDec( Ivy_ObjFanin0(pTemp) ); + Ivy_ObjRefsDec( Ivy_ObjFanin1(pTemp) ); + pTemp->fMarkB = 1; + } + + // count the MFFC size + Vec_PtrForEachEntry( vFront, pTemp, k ) + Ivy_Regular(pTemp)->fMarkA = 1; + nMffc = Ivy_NodeCountMffc( pObj ); + Vec_PtrForEachEntry( vFront, pTemp, k ) + Ivy_Regular(pTemp)->fMarkA = 0; + + if ( fVerbose ) + { + Counter = 0; + Vec_PtrForEachEntry( vCone, pTemp, k ) + Counter += (Ivy_ObjRefs(pTemp) > 0); + printf( "%5d : Leaves = %2d. Cone = %2d. ConeRef = %2d. Mffc = %d. Lev = %d. LevR = %d.\n", + pObj->Id, Vec_PtrSize(vFront), Vec_PtrSize(vCone), Counter-1, nMffc, Ivy_ObjLevel(pObj), LevelR ); + } +/* + printf( "Leaves:" ); + Vec_PtrForEachEntry( vLeaves, pTemp, k ) + printf( " %d%s", Ivy_Regular(pTemp)->Id, Ivy_IsComplement(pTemp)? "\'" : "" ); + printf( "\n" ); + printf( "Cone:\n" ); + Vec_PtrForEachEntry( vCone, pTemp, k ) + printf( " %5d = %d%s %d%s\n", pTemp->Id, + Ivy_ObjFaninId0(pTemp), Ivy_ObjFaninC0(pTemp)? "\'" : "", + Ivy_ObjFaninId1(pTemp), Ivy_ObjFaninC1(pTemp)? "\'" : "" ); +*/ + + RetValue = Ivy_MultiPlus( vLeaves, vCone, Ivy_ObjType(pObj), nMffc + fUseZeroCost, vSols ); + + // ref nodes in the cone + Vec_PtrForEachEntry( vCone, pTemp, k ) + { + Ivy_ObjRefsInc( Ivy_ObjFanin0(pTemp) ); + Ivy_ObjRefsInc( Ivy_ObjFanin1(pTemp) ); + pTemp->fMarkA = 0; + pTemp->fMarkB = 0; + } + + if ( !RetValue ) + return NULL; + + if ( Vec_PtrSize( vSols ) == 1 ) + return Vec_PtrEntry( vSols, 0 ); + return Ivy_NodeBalanceBuildSuper( vSols, Ivy_ObjType(pObj), 1 ); +} + +/**Function************************************************************* + + Synopsis [Comparison for node pointers.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_NodeCountMffc_rec( Ivy_Obj_t * pNode ) +{ + if ( Ivy_ObjRefs(pNode) > 0 || Ivy_ObjIsCi(pNode) || pNode->fMarkA ) + return 0; + assert( pNode->fMarkB ); + pNode->fMarkA = 1; +// printf( "%d ", pNode->Id ); + if ( Ivy_ObjIsBuf(pNode) ) + return Ivy_NodeCountMffc_rec( Ivy_ObjFanin0(pNode) ); + return 1 + Ivy_NodeCountMffc_rec( Ivy_ObjFanin0(pNode) ) + Ivy_NodeCountMffc_rec( Ivy_ObjFanin1(pNode) ); +} + +/**Function************************************************************* + + Synopsis [Comparison for node pointers.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_NodeCountMffc( Ivy_Obj_t * pNode ) +{ + assert( pNode->fMarkB ); + return 1 + Ivy_NodeCountMffc_rec( Ivy_ObjFanin0(pNode) ) + Ivy_NodeCountMffc_rec( Ivy_ObjFanin1(pNode) ); +} + +/**Function************************************************************* + + Synopsis [Comparison for node pointers.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_ManFindAlgCutCompare( Ivy_Obj_t ** pp1, Ivy_Obj_t ** pp2 ) +{ + if ( *pp1 < *pp2 ) + return -1; + if ( *pp1 > *pp2 ) + return 1; + return 0; +} + +/**Function************************************************************* + + Synopsis [Computing one algebraic cut.] + + Description [Returns 1 if the tree-leaves of this node where traversed + and found to have no external references (and have not been collected). + Returns 0 if the tree-leaves have external references and are collected.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_ManFindAlgCut_rec( Ivy_Obj_t * pObj, Ivy_Type_t Type, Vec_Ptr_t * vFront, Vec_Ptr_t * vCone ) +{ + int RetValue0, RetValue1; + Ivy_Obj_t * pObjR = Ivy_Regular(pObj); + assert( !Ivy_ObjIsBuf(pObjR) ); + assert( Type != IVY_EXOR || !Ivy_IsComplement(pObj) ); + + // make sure the node is not visited twice in different polarities + if ( Ivy_IsComplement(pObj) ) + { // if complemented, mark B + if ( pObjR->fMarkA ) + return -1; + pObjR->fMarkB = 1; + } + else + { // if non-complicated, mark A + if ( pObjR->fMarkB ) + return -1; + pObjR->fMarkA = 1; + } + Vec_PtrPush( vCone, pObjR ); + + // if the node is the end of the tree, return + if ( Ivy_IsComplement(pObj) || Ivy_ObjType(pObj) != Type ) + { + if ( Ivy_ObjRefs(pObjR) == 1 ) + return 1; + assert( Ivy_ObjRefs(pObjR) > 1 ); + Vec_PtrPush( vFront, pObj ); + return 0; + } + + // branch on the node + assert( !Ivy_IsComplement(pObj) ); + assert( Ivy_ObjIsNode(pObj) ); + // what if buffer has more than one fanout??? + RetValue0 = Ivy_ManFindAlgCut_rec( Ivy_ObjReal( Ivy_ObjChild0(pObj) ), Type, vFront, vCone ); + RetValue1 = Ivy_ManFindAlgCut_rec( Ivy_ObjReal( Ivy_ObjChild1(pObj) ), Type, vFront, vCone ); + if ( RetValue0 == -1 || RetValue1 == -1 ) + return -1; + + // the case when both have no external references + if ( RetValue0 && RetValue1 ) + { + if ( Ivy_ObjRefs(pObj) == 1 ) + return 1; + assert( Ivy_ObjRefs(pObj) > 1 ); + Vec_PtrPush( vFront, pObj ); + return 0; + } + // the case when one of them has external references + if ( RetValue0 ) + Vec_PtrPush( vFront, Ivy_ObjReal( Ivy_ObjChild0(pObj) ) ); + if ( RetValue1 ) + Vec_PtrPush( vFront, Ivy_ObjReal( Ivy_ObjChild1(pObj) ) ); + return 0; +} + +/**Function************************************************************* + + Synopsis [Computing one algebraic cut.] + + Description [Algebraic cut stops when we hit (a) CI, (b) complemented edge, + (c) boundary of different gates. Returns 1 if this is a pure tree. + Returns -1 if the contant 0 is detected. Return 0 if the array can be used.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_ManFindAlgCut( Ivy_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone ) +{ + Ivy_Obj_t * pObj, * pPrev; + int RetValue, i; + assert( !Ivy_IsComplement(pRoot) ); + assert( Ivy_ObjIsNode(pRoot) ); + // clear the frontier and collect the nodes + Vec_PtrClear( vCone ); + Vec_PtrClear( vFront ); + Vec_PtrClear( vLeaves ); + RetValue = Ivy_ManFindAlgCut_rec( pRoot, Ivy_ObjType(pRoot), vFront, vCone ); + // clean the marks + Vec_PtrForEachEntry( vCone, pObj, i ) + pObj->fMarkA = pObj->fMarkB = 0; + // quit if the same node is found in both polarities + if ( RetValue == -1 ) + return -1; + // return if the node is the root of a tree + if ( RetValue == 1 ) + return 1; + // return if the cut is composed of two nodes + if ( Vec_PtrSize(vFront) <= 2 ) + return 1; + // sort the entries in increasing order + Vec_PtrSort( vFront, Ivy_ManFindAlgCutCompare ); + // remove duplicates from vFront and save the nodes in vLeaves + pPrev = Vec_PtrEntry(vFront, 0); + Vec_PtrPush( vLeaves, pPrev ); + Vec_PtrForEachEntryStart( vFront, pObj, i, 1 ) + { + // compare current entry and the previous entry + if ( pObj == pPrev ) + { + if ( Ivy_ObjIsExor(pRoot) ) // A <+> A = 0 + { + // vLeaves are no longer structural support of pRoot!!! + Vec_PtrPop(vLeaves); + pPrev = Vec_PtrSize(vLeaves) == 0 ? NULL : Vec_PtrEntryLast(vLeaves); + } + continue; + } + if ( pObj == Ivy_Not(pPrev) ) + { + assert( Ivy_ObjIsAnd(pRoot) ); + return -1; + } + pPrev = pObj; + Vec_PtrPush( vLeaves, pObj ); + } + if ( Vec_PtrSize(vLeaves) == 0 ) + return -1; + if ( Vec_PtrSize(vLeaves) <= 2 ) + return 1; + return 0; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ivy/ivyRwrPre.c b/src/temp/ivy/ivyRwrPre.c new file mode 100644 index 00000000..243ab261 --- /dev/null +++ b/src/temp/ivy/ivyRwrPre.c @@ -0,0 +1,597 @@ +/**CFile**************************************************************** + + FileName [ivyRwtPre.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [Rewriting based on precomputation.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: ivyRwtPre.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ivy.h" +#include "deco.h" +#include "rwt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static unsigned Ivy_NodeGetTruth( Ivy_Obj_t * pObj, int * pNums, int nNums ); +static int Ivy_NodeMffcLabel( Ivy_Obj_t * pObj ); +static int Rwt_NodeRewrite( Rwt_Man_t * p, Ivy_Obj_t * pNode, int fUpdateLevel, int fUseZeroCost ); +static Dec_Graph_t * Rwt_CutEvaluate( Rwt_Man_t * p, Ivy_Obj_t * pRoot, Ivy_Cut_t * pCut, + Vec_Ptr_t * vFaninsCur, int nNodesSaved, int LevelMax, int * pGainBest, unsigned uTruth ); + +static int Ivy_GraphToNetworkCount( Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax, int LevelMax ); +static void Ivy_GraphUpdateNetwork( Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Performs incremental rewriting of the AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_ManRewritePre( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost, int fVerbose ) +{ + Rwt_Man_t * pManRwt; + Ivy_Obj_t * pNode; + int i, nNodes, nGain; + int clk, clkStart = clock(); + // start the rewriting manager + pManRwt = Rwt_ManStart( 0 ); + if ( pManRwt == NULL ) + return 0; + // compute the reverse levels if level update is requested + if ( fUpdateLevel ) + Ivy_ManRequiredLevels( p ); + // resynthesize each node once + nNodes = Ivy_ManObjIdNext( p ); + Ivy_ManForEachObj( p, pNode, i ) + { + if ( !Ivy_ObjIsNode(pNode) ) + continue; + // fix the fanin buffer problem + Ivy_NodeFixBufferFanins( pNode ); + if ( Ivy_ObjIsBuf(pNode) ) + continue; + // stop if all nodes have been tried once + if ( i >= nNodes ) + break; + // skip the nodes with many fanouts +// if ( Ivy_ObjRefs(pNode) > 1000 ) +// continue; + // for each cut, try to resynthesize it + nGain = Rwt_NodeRewrite( pManRwt, pNode, fUpdateLevel, fUseZeroCost ); + if ( nGain > 0 || nGain == 0 && fUseZeroCost ) + { + Dec_Graph_t * pGraph = Rwt_ManReadDecs(pManRwt); + int fCompl = Rwt_ManReadCompl(pManRwt); +/* + { + Ivy_Obj_t * pObj; + int i; + printf( "USING: (" ); + Vec_PtrForEachEntry( Rwt_ManReadLeaves(pManRwt), pObj, i ) + printf( "%d ", Ivy_ObjFanoutNum(Ivy_Regular(pObj)) ); + printf( ") Gain = %d.\n", nGain ); + } + if ( nGain > 0 ) + { // print stats on the MFFC + extern void Ivy_NodeMffsConeSuppPrint( Ivy_Obj_t * pNode ); + printf( "Node %6d : Gain = %4d ", pNode->Id, nGain ); + Ivy_NodeMffsConeSuppPrint( pNode ); + } +*/ + // complement the FF if needed +clk = clock(); + if ( fCompl ) Dec_GraphComplement( pGraph ); + Ivy_GraphUpdateNetwork( pNode, pGraph, fUpdateLevel, nGain ); + if ( fCompl ) Dec_GraphComplement( pGraph ); +Rwt_ManAddTimeUpdate( pManRwt, clock() - clk ); + } + } +Rwt_ManAddTimeTotal( pManRwt, clock() - clkStart ); + // print stats + if ( fVerbose ) + Rwt_ManPrintStats( pManRwt ); + // delete the managers + Rwt_ManStop( pManRwt ); + // fix the levels + if ( fUpdateLevel ) + Vec_IntFree( p->vRequired ), p->vRequired = NULL; + // check + if ( i = Ivy_ManCleanup(p) ) + printf( "Cleanup after rewriting removed %d dangling nodes.\n", i ); + if ( !Ivy_ManCheck(p) ) + printf( "Ivy_ManRewritePre(): The check has failed.\n" ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Performs rewriting for one node.] + + Description [This procedure considers all the cuts computed for the node + and tries to rewrite each of them using the "forest" of different AIG + structures precomputed and stored in the RWR manager. + Determines the best rewriting and computes the gain in the number of AIG + nodes in the final network. In the end, p->vFanins contains information + about the best cut that can be used for rewriting, while p->pGraph gives + the decomposition dag (represented using decomposition graph data structure). + Returns gain in the number of nodes or -1 if node cannot be rewritten.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Rwt_NodeRewrite( Rwt_Man_t * p, Ivy_Obj_t * pNode, int fUpdateLevel, int fUseZeroCost ) +{ + int fVeryVerbose = 0; + Dec_Graph_t * pGraph; + Ivy_Store_t * pStore; + Ivy_Cut_t * pCut; + Ivy_Obj_t * pFanin; + unsigned uPhase, uTruthBest, uTruth; + char * pPerm; + int Required, nNodesSaved, nNodesSaveCur; + int i, c, GainCur, GainBest = -1; + int clk, clk2; + + p->nNodesConsidered++; + // get the required times + Required = fUpdateLevel? Vec_IntEntry( Ivy_ObjMan(pNode)->vRequired, pNode->Id ) : 1000000; + // get the node's cuts +clk = clock(); + pStore = Ivy_NodeFindCutsAll( pNode, 5 ); +p->timeCut += clock() - clk; + + // go through the cuts +clk = clock(); + for ( c = 1; c < pStore->nCuts; c++ ) + { + pCut = pStore->pCuts + c; + // consider only 4-input cuts + if ( pCut->nSize != 4 ) + continue; + // skip the cuts with buffers + for ( i = 0; i < (int)pCut->nSize; i++ ) + if ( Ivy_ObjIsBuf( Ivy_ObjObj(pNode, pCut->pArray[i]) ) ) + break; + if ( i != pCut->nSize ) + continue; + +// if ( pNode->Id == 82 ) +// Ivy_NodePrintCut( pCut ); + + // get the fanin permutation +clk2 = clock(); + uTruth = 0xFFFF & Ivy_NodeGetTruth( pNode, pCut->pArray, pCut->nSize ); // truth table +p->timeTruth += clock() - clk2; + pPerm = p->pPerms4[ p->pPerms[uTruth] ]; + uPhase = p->pPhases[uTruth]; + // collect fanins with the corresponding permutation/phase + Vec_PtrClear( p->vFaninsCur ); + Vec_PtrFill( p->vFaninsCur, (int)pCut->nSize, 0 ); + for ( i = 0; i < (int)pCut->nSize; i++ ) + { + pFanin = Ivy_ObjObj( pNode, pCut->pArray[pPerm[i]] ); + assert( Ivy_ObjIsNode(pFanin) || Ivy_ObjIsCi(pFanin) ); + pFanin = Ivy_NotCond(pFanin, ((uPhase & (1<<i)) > 0) ); + Vec_PtrWriteEntry( p->vFaninsCur, i, pFanin ); + } +clk2 = clock(); +/* + printf( "Considering: (" ); + Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i ) + printf( "%d ", Ivy_ObjFanoutNum(Ivy_Regular(pFanin)) ); + printf( ")\n" ); +*/ + // mark the fanin boundary + Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i ) + Ivy_ObjRefsInc( Ivy_Regular(pFanin) ); + // label MFFC with current ID + Ivy_ManIncrementTravId( Ivy_ObjMan(pNode) ); + nNodesSaved = Ivy_NodeMffcLabel( pNode ); + // unmark the fanin boundary + Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i ) + Ivy_ObjRefsDec( Ivy_Regular(pFanin) ); +p->timeMffc += clock() - clk2; + + // evaluate the cut +clk2 = clock(); + pGraph = Rwt_CutEvaluate( p, pNode, pCut, p->vFaninsCur, nNodesSaved, Required, &GainCur, uTruth ); +p->timeEval += clock() - clk2; + + // check if the cut is better than the current best one + if ( pGraph != NULL && GainBest < GainCur ) + { + // save this form + nNodesSaveCur = nNodesSaved; + GainBest = GainCur; + p->pGraph = pGraph; + p->fCompl = ((uPhase & (1<<4)) > 0); + uTruthBest = uTruth; + // collect fanins in the + Vec_PtrClear( p->vFanins ); + Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i ) + Vec_PtrPush( p->vFanins, pFanin ); + } + } +p->timeRes += clock() - clk; + + if ( GainBest == -1 ) + return -1; + +// printf( "%d", nNodesSaveCur - GainBest ); +/* + if ( GainBest > 0 ) + { + if ( Rwt_CutIsintean( pNode, p->vFanins ) ) + printf( "b" ); + else + { + printf( "Node %d : ", pNode->Id ); + Vec_PtrForEachEntry( p->vFanins, pFanin, i ) + printf( "%d ", Ivy_Regular(pFanin)->Id ); + printf( "a" ); + } + } +*/ +/* + if ( GainBest > 0 ) + if ( p->fCompl ) + printf( "c" ); + else + printf( "." ); +*/ + + // copy the leaves + Vec_PtrForEachEntry( p->vFanins, pFanin, i ) + Dec_GraphNode(p->pGraph, i)->pFunc = pFanin; + + p->nScores[p->pMap[uTruthBest]]++; + p->nNodesGained += GainBest; + if ( fUseZeroCost || GainBest > 0 ) + p->nNodesRewritten++; + + // report the progress + if ( fVeryVerbose && GainBest > 0 ) + { + printf( "Node %6d : ", Ivy_ObjId(pNode) ); + printf( "Fanins = %d. ", p->vFanins->nSize ); + printf( "Save = %d. ", nNodesSaveCur ); + printf( "Add = %d. ", nNodesSaveCur-GainBest ); + printf( "GAIN = %d. ", GainBest ); + printf( "Cone = %d. ", p->pGraph? Dec_GraphNodeNum(p->pGraph) : 0 ); + printf( "Class = %d. ", p->pMap[uTruthBest] ); + printf( "\n" ); + } + return GainBest; +} + + +/**Function************************************************************* + + Synopsis [References/references the node and returns MFFC size.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_NodeRefDeref( Ivy_Obj_t * pNode, int fReference, int fLabel ) +{ + Ivy_Obj_t * pNode0, * pNode1; + int Counter; + // label visited nodes + if ( fLabel ) + Ivy_ObjSetTravIdCurrent( pNode ); + // skip the CI + if ( Ivy_ObjIsCi(pNode) ) + return 0; + assert( Ivy_ObjIsNode(pNode) || Ivy_ObjIsBuf(pNode) ); + // process the internal node + pNode0 = Ivy_ObjFanin0(pNode); + pNode1 = Ivy_ObjFanin1(pNode); + Counter = Ivy_ObjIsNode(pNode); + if ( fReference ) + { + if ( pNode0->nRefs++ == 0 ) + Counter += Ivy_NodeRefDeref( pNode0, fReference, fLabel ); + if ( Ivy_ObjIsNode(pNode) && pNode1->nRefs++ == 0 ) + Counter += Ivy_NodeRefDeref( pNode1, fReference, fLabel ); + } + else + { + assert( pNode0->nRefs > 0 ); + assert( pNode1->nRefs > 0 ); + if ( --pNode0->nRefs == 0 ) + Counter += Ivy_NodeRefDeref( pNode0, fReference, fLabel ); + if ( Ivy_ObjIsNode(pNode) && --pNode1->nRefs == 0 ) + Counter += Ivy_NodeRefDeref( pNode1, fReference, fLabel ); + } + return Counter; +} + +/**Function************************************************************* + + Synopsis [Computes the size of MFFC and labels nodes with the current TravId.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_NodeMffcLabel( Ivy_Obj_t * pNode ) +{ + int nConeSize1, nConeSize2; + assert( !Ivy_IsComplement( pNode ) ); + assert( Ivy_ObjIsNode( pNode ) ); + nConeSize1 = Ivy_NodeRefDeref( pNode, 0, 1 ); // dereference + nConeSize2 = Ivy_NodeRefDeref( pNode, 1, 0 ); // reference + assert( nConeSize1 == nConeSize2 ); + assert( nConeSize1 > 0 ); + return nConeSize1; +} + +/**Function************************************************************* + + Synopsis [Computes the truth table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned Ivy_NodeGetTruth_rec( Ivy_Obj_t * pObj, int * pNums, int nNums ) +{ + static unsigned uMasks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 }; + unsigned uTruth0, uTruth1; + int i; + for ( i = 0; i < nNums; i++ ) + if ( pObj->Id == pNums[i] ) + return uMasks[i]; + assert( Ivy_ObjIsNode(pObj) || Ivy_ObjIsBuf(pObj) ); + uTruth0 = Ivy_NodeGetTruth_rec( Ivy_ObjFanin0(pObj), pNums, nNums ); + if ( Ivy_ObjFaninC0(pObj) ) + uTruth0 = ~uTruth0; + if ( Ivy_ObjIsBuf(pObj) ) + return uTruth0; + uTruth1 = Ivy_NodeGetTruth_rec( Ivy_ObjFanin1(pObj), pNums, nNums ); + if ( Ivy_ObjFaninC1(pObj) ) + uTruth1 = ~uTruth1; + return uTruth0 & uTruth1; +} + + +/**Function************************************************************* + + Synopsis [Computes the truth table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned Ivy_NodeGetTruth( Ivy_Obj_t * pObj, int * pNums, int nNums ) +{ + assert( nNums < 6 ); + return Ivy_NodeGetTruth_rec( pObj, pNums, nNums ); +} + +/**Function************************************************************* + + Synopsis [Evaluates the cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Graph_t * Rwt_CutEvaluate( Rwt_Man_t * p, Ivy_Obj_t * pRoot, Ivy_Cut_t * pCut, Vec_Ptr_t * vFaninsCur, int nNodesSaved, int LevelMax, int * pGainBest, unsigned uTruth ) +{ + Vec_Ptr_t * vSubgraphs; + Dec_Graph_t * pGraphBest, * pGraphCur; + Rwt_Node_t * pNode, * pFanin; + int nNodesAdded, GainBest, i, k; + // find the matching class of subgraphs + vSubgraphs = Vec_VecEntry( p->vClasses, p->pMap[uTruth] ); + p->nSubgraphs += vSubgraphs->nSize; + // determine the best subgraph + GainBest = -1; + Vec_PtrForEachEntry( vSubgraphs, pNode, i ) + { + // get the current graph + pGraphCur = (Dec_Graph_t *)pNode->pNext; + // copy the leaves + Vec_PtrForEachEntry( vFaninsCur, pFanin, k ) + Dec_GraphNode(pGraphCur, k)->pFunc = pFanin; + // detect how many unlabeled nodes will be reused + nNodesAdded = Ivy_GraphToNetworkCount( pRoot, pGraphCur, nNodesSaved, LevelMax ); + if ( nNodesAdded == -1 ) + continue; + assert( nNodesSaved >= nNodesAdded ); + // count the gain at this node + if ( GainBest < nNodesSaved - nNodesAdded ) + { + GainBest = nNodesSaved - nNodesAdded; + pGraphBest = pGraphCur; + } + } + if ( GainBest == -1 ) + return NULL; + *pGainBest = GainBest; + return pGraphBest; +} + + +/**Function************************************************************* + + Synopsis [Counts the number of new nodes added when using this graph.] + + Description [AIG nodes for the fanins should be assigned to pNode->pFunc + of the leaves of the graph before calling this procedure. + Returns -1 if the number of nodes and levels exceeded the given limit or + the number of levels exceeded the maximum allowed level.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_GraphToNetworkCount( Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax, int LevelMax ) +{ + Dec_Node_t * pNode, * pNode0, * pNode1; + Ivy_Obj_t * pAnd, * pAnd0, * pAnd1; + int i, Counter, LevelNew, LevelOld; + // check for constant function or a literal + if ( Dec_GraphIsConst(pGraph) || Dec_GraphIsVar(pGraph) ) + return 0; + // set the levels of the leaves + Dec_GraphForEachLeaf( pGraph, pNode, i ) + pNode->Level = Ivy_Regular(pNode->pFunc)->Level; + // compute the AIG size after adding the internal nodes + Counter = 0; + Dec_GraphForEachNode( pGraph, pNode, i ) + { + // get the children of this node + pNode0 = Dec_GraphNode( pGraph, pNode->eEdge0.Node ); + pNode1 = Dec_GraphNode( pGraph, pNode->eEdge1.Node ); + // get the AIG nodes corresponding to the children + pAnd0 = pNode0->pFunc; + pAnd1 = pNode1->pFunc; + if ( pAnd0 && pAnd1 ) + { + // if they are both present, find the resulting node + pAnd0 = Ivy_NotCond( pAnd0, pNode->eEdge0.fCompl ); + pAnd1 = Ivy_NotCond( pAnd1, pNode->eEdge1.fCompl ); + pAnd = Ivy_TableLookup( Ivy_ObjCreateGhost(pAnd0, pAnd1, IVY_AND, IVY_INIT_NONE) ); + // return -1 if the node is the same as the original root + if ( Ivy_Regular(pAnd) == pRoot ) + return -1; + } + else + pAnd = NULL; + // count the number of added nodes + if ( pAnd == NULL || Ivy_ObjIsTravIdCurrent(Ivy_Regular(pAnd)) ) + { + if ( ++Counter > NodeMax ) + return -1; + } + // count the number of new levels + LevelNew = 1 + RWT_MAX( pNode0->Level, pNode1->Level ); + if ( pAnd ) + { + if ( Ivy_Regular(pAnd) == Ivy_ObjConst1(pRoot) ) + LevelNew = 0; + else if ( Ivy_Regular(pAnd) == Ivy_Regular(pAnd0) ) + LevelNew = (int)Ivy_Regular(pAnd0)->Level; + else if ( Ivy_Regular(pAnd) == Ivy_Regular(pAnd1) ) + LevelNew = (int)Ivy_Regular(pAnd1)->Level; + LevelOld = (int)Ivy_Regular(pAnd)->Level; +// assert( LevelNew == LevelOld ); + } + if ( LevelNew > LevelMax ) + return -1; + pNode->pFunc = pAnd; + pNode->Level = LevelNew; + } + return Counter; +} + +/**Function************************************************************* + + Synopsis [Transforms the decomposition graph into the AIG.] + + Description [AIG nodes for the fanins should be assigned to pNode->pFunc + of the leaves of the graph before calling this procedure.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_GraphToNetwork( Ivy_Man_t * pMan, Dec_Graph_t * pGraph ) +{ + Ivy_Obj_t * pAnd0, * pAnd1; + Dec_Node_t * pNode; + int i; + // check for constant function + if ( Dec_GraphIsConst(pGraph) ) + return Ivy_NotCond( Ivy_ManConst1(pMan), Dec_GraphIsComplement(pGraph) ); + // check for a literal + if ( Dec_GraphIsVar(pGraph) ) + return Ivy_NotCond( Dec_GraphVar(pGraph)->pFunc, Dec_GraphIsComplement(pGraph) ); + // build the AIG nodes corresponding to the AND gates of the graph + Dec_GraphForEachNode( pGraph, pNode, i ) + { + pAnd0 = Ivy_NotCond( Dec_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl ); + pAnd1 = Ivy_NotCond( Dec_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl ); + pNode->pFunc = Ivy_And( pAnd0, pAnd1 ); + } + // complement the result if necessary + return Ivy_NotCond( pNode->pFunc, Dec_GraphIsComplement(pGraph) ); +} + +/**Function************************************************************* + + Synopsis [Replaces MFFC of the node by the new factored form.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_GraphUpdateNetwork( Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain ) +{ + Ivy_Obj_t * pRootNew; + int nNodesNew, nNodesOld; + nNodesOld = Ivy_ManNodeNum(Ivy_ObjMan(pRoot)); + // create the new structure of nodes + pRootNew = Ivy_GraphToNetwork( Ivy_ObjMan(pRoot), pGraph ); + // remove the old nodes +// Ivy_AigReplace( pMan->pManFunc, pRoot, pRootNew, fUpdateLevel ); + Ivy_ObjReplace( pRoot, pRootNew, 1, 0 ); + // compare the gains + nNodesNew = Ivy_ManNodeNum(Ivy_ObjMan(pRoot)); + assert( nGain <= nNodesOld - nNodesNew ); +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ivy/ivyUtil.c b/src/temp/ivy/ivyUtil.c index 590affd7..3d1ac335 100644 --- a/src/temp/ivy/ivyUtil.c +++ b/src/temp/ivy/ivyUtil.c @@ -362,6 +362,222 @@ Vec_Int_t * Ivy_ManLatches( Ivy_Man_t * p ) return vLatches; } +/**Function************************************************************* + + Synopsis [Collect the latches.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_ManReadLevels( Ivy_Man_t * p ) +{ + Ivy_Obj_t * pObj; + int i, LevelMax = 0; + Ivy_ManForEachPo( p, pObj, i ) + { + pObj = Ivy_ObjFanin0(pObj); + LevelMax = IVY_MAX( LevelMax, (int)pObj->Level ); + } + return LevelMax; +} + +/**Function************************************************************* + + Synopsis [Returns the real fanin.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_ObjReal( Ivy_Obj_t * pObj ) +{ + Ivy_Obj_t * pFanin; + if ( !Ivy_ObjIsBuf( Ivy_Regular(pObj) ) ) + return pObj; + pFanin = Ivy_ObjReal( Ivy_ObjChild0(Ivy_Regular(pObj)) ); + return Ivy_NotCond( pFanin, Ivy_IsComplement(pObj) ); +} + + + +/**Function************************************************************* + + Synopsis [Checks if the cube has exactly one 1.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Ivy_TruthHasOneOne( unsigned uCube ) +{ + return (uCube & (uCube - 1)) == 0; +} + +/**Function************************************************************* + + Synopsis [Checks if two cubes are distance-1.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Ivy_TruthCubesDist1( unsigned uCube1, unsigned uCube2 ) +{ + unsigned uTemp = uCube1 | uCube2; + return Ivy_TruthHasOneOne( (uTemp >> 1) & uTemp & 0x55555555 ); +} + +/**Function************************************************************* + + Synopsis [Checks if two cubes differ in only one literal.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Ivy_TruthCubesDiff1( unsigned uCube1, unsigned uCube2 ) +{ + unsigned uTemp = uCube1 ^ uCube2; + return Ivy_TruthHasOneOne( ((uTemp >> 1) | uTemp) & 0x55555555 ); +} + +/**Function************************************************************* + + Synopsis [Combines two distance 1 cubes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline unsigned Ivy_TruthCubesMerge( unsigned uCube1, unsigned uCube2 ) +{ + unsigned uTemp; + uTemp = uCube1 | uCube2; + uTemp &= (uTemp >> 1) & 0x55555555; + assert( Ivy_TruthHasOneOne(uTemp) ); + uTemp |= (uTemp << 1); + return (uCube1 | uCube2) ^ uTemp; +} + +/**Function************************************************************* + + Synopsis [Estimates the number of AIG nodes in the truth table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_TruthEstimateNodes( unsigned * pTruth, int nVars ) +{ + static unsigned short uResult[256]; + static unsigned short uCover[81*81]; + static char pVarCount[81*81]; + int nMints, uCube, uCubeNew, i, k, c, nCubes, nRes, Counter; + assert( nVars <= 8 ); + // create the cover + nCubes = 0; + nMints = (1 << nVars); + for ( i = 0; i < nMints; i++ ) + if ( pTruth[i/32] & (1 << (i & 31)) ) + { + uCube = 0; + for ( k = 0; k < nVars; k++ ) + if ( i & (1 << k) ) + uCube |= (1 << ((k<<1)+1)); + else + uCube |= (1 << ((k<<1)+0)); + uCover[nCubes] = uCube; + pVarCount[nCubes] = nVars; + nCubes++; +// Extra_PrintBinary( stdout, &uCube, 8 ); printf( "\n" ); + } + assert( nCubes <= 256 ); + // reduce the cover by building larger cubes + for ( i = 1; i < nCubes; i++ ) + for ( k = 0; k < i; k++ ) + if ( pVarCount[i] && pVarCount[i] == pVarCount[k] && Ivy_TruthCubesDist1(uCover[i], uCover[k]) ) + { + uCubeNew = Ivy_TruthCubesMerge(uCover[i], uCover[k]); + for ( c = i; c < nCubes; c++ ) + if ( uCubeNew == uCover[c] ) + break; + if ( c != nCubes ) + continue; + uCover[nCubes] = uCubeNew; + pVarCount[nCubes] = pVarCount[i] - 1; + nCubes++; + assert( nCubes < 81*81 ); +// Extra_PrintBinary( stdout, &uCubeNew, 8 ); printf( "\n" ); +// c = c; + } + // compact the cover + nRes = 0; + for ( i = nCubes -1; i >= 0; i-- ) + { + for ( k = 0; k < nRes; k++ ) + if ( (uCover[i] & uResult[k]) == uResult[k] ) + break; + if ( k != nRes ) + continue; + uResult[nRes++] = uCover[i]; + } + // count the number of literals + Counter = 0; + for ( i = 0; i < nRes; i++ ) + { + for ( k = 0; k < nVars; k++ ) + if ( uResult[i] & (3 << (k<<1)) ) + Counter++; + } + return Counter; +} + +/**Function************************************************************* + + Synopsis [Tests the cover procedure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_TruthEstimateNodesTest() +{ + unsigned uTruth[8]; + int i; + for ( i = 0; i < 8; i++ ) + uTruth[i] = ~(unsigned)0; + uTruth[3] ^= (1 << 13); +// uTruth[4] = 0xFFFFF; +// uTruth[0] = 0xFF; +// uTruth[0] ^= (1 << 3); + printf( "Number = %d.\n", Ivy_TruthEstimateNodes(uTruth, 8) ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/temp/ivy/module.make b/src/temp/ivy/module.make index beadb8b9..f697910b 100644 --- a/src/temp/ivy/module.make +++ b/src/temp/ivy/module.make @@ -8,7 +8,8 @@ SRC += src/temp/ivy/ivyBalance.c \ src/temp/ivy/ivyMulti.c \ src/temp/ivy/ivyObj.c \ src/temp/ivy/ivyOper.c \ - src/temp/ivy/ivyRewrite.c \ + src/temp/ivy/ivyResyn.c \ + src/temp/ivy/ivyRwrPre.c \ src/temp/ivy/ivySeq.c \ src/temp/ivy/ivyTable.c \ src/temp/ivy/ivyUndo.c \ |