diff options
Diffstat (limited to 'src/aig')
| -rw-r--r-- | src/aig/dar/dar.h | 38 | ||||
| -rw-r--r-- | src/aig/dar/darCheck.c | 13 | ||||
| -rw-r--r-- | src/aig/dar/darCore.c | 4 | ||||
| -rw-r--r-- | src/aig/dar/darDfs.c | 55 | ||||
| -rw-r--r-- | src/aig/dar/darMan.c | 26 | ||||
| -rw-r--r-- | src/aig/dar/darObj.c | 55 | ||||
| -rw-r--r-- | src/aig/dar/darOper.c | 64 | ||||
| -rw-r--r-- | src/aig/dar/darSeq.c | 471 | ||||
| -rw-r--r-- | src/aig/dar/darTable.c | 29 |
9 files changed, 669 insertions, 86 deletions
diff --git a/src/aig/dar/dar.h b/src/aig/dar/dar.h index 7c77bea5..9bb79262 100644 --- a/src/aig/dar/dar.h +++ b/src/aig/dar/dar.h @@ -65,7 +65,8 @@ typedef enum { DAR_AIG_BUF, // 4: buffer node DAR_AIG_AND, // 5: AND node DAR_AIG_EXOR, // 6: EXOR node - DAR_AIG_VOID // 7: unused object + DAR_AIG_LATCH, // 7: latch + DAR_AIG_VOID // 8: unused object } Dar_Type_t; // the parameters @@ -179,11 +180,13 @@ static inline Dar_Obj_t * Dar_ManObj( Dar_Man_t * p, int i ) { return p->vO static inline int Dar_ManPiNum( Dar_Man_t * p ) { return p->nObjs[DAR_AIG_PI]; } static inline int Dar_ManPoNum( Dar_Man_t * p ) { return p->nObjs[DAR_AIG_PO]; } +static inline int Dar_ManBufNum( Dar_Man_t * p ) { return p->nObjs[DAR_AIG_BUF]; } static inline int Dar_ManAndNum( Dar_Man_t * p ) { return p->nObjs[DAR_AIG_AND]; } static inline int Dar_ManExorNum( Dar_Man_t * p ) { return p->nObjs[DAR_AIG_EXOR]; } -static inline int Dar_ManNodeNum( Dar_Man_t * p ) { return p->nObjs[DAR_AIG_AND]+p->nObjs[DAR_AIG_EXOR];} +static inline int Dar_ManLatchNum( Dar_Man_t * p ) { return p->nObjs[DAR_AIG_LATCH]; } +static inline int Dar_ManNodeNum( Dar_Man_t * p ) { return p->nObjs[DAR_AIG_AND]+p->nObjs[DAR_AIG_EXOR]; } static inline int Dar_ManGetCost( Dar_Man_t * p ) { return p->nObjs[DAR_AIG_AND]+3*p->nObjs[DAR_AIG_EXOR]; } -static inline int Dar_ManObjNum( Dar_Man_t * p ) { return p->nCreated - p->nDeleted; } +static inline int Dar_ManObjNum( Dar_Man_t * p ) { return p->nCreated - p->nDeleted; } static inline Dar_Type_t Dar_ObjType( Dar_Obj_t * pObj ) { return (Dar_Type_t)pObj->Type; } static inline int Dar_ObjIsNone( Dar_Obj_t * pObj ) { return pObj->Type == DAR_AIG_NONE; } @@ -193,19 +196,20 @@ static inline int Dar_ObjIsPo( Dar_Obj_t * pObj ) { return pObj- static inline int Dar_ObjIsBuf( Dar_Obj_t * pObj ) { return pObj->Type == DAR_AIG_BUF; } static inline int Dar_ObjIsAnd( Dar_Obj_t * pObj ) { return pObj->Type == DAR_AIG_AND; } static inline int Dar_ObjIsExor( Dar_Obj_t * pObj ) { return pObj->Type == DAR_AIG_EXOR; } +static inline int Dar_ObjIsLatch( Dar_Obj_t * pObj ) { return pObj->Type == DAR_AIG_LATCH; } static inline int Dar_ObjIsNode( Dar_Obj_t * pObj ) { return pObj->Type == DAR_AIG_AND || pObj->Type == DAR_AIG_EXOR; } -static inline int Dar_ObjIsTerm( Dar_Obj_t * pObj ) { return pObj->Type == DAR_AIG_PI || pObj->Type == DAR_AIG_PO || pObj->Type == DAR_AIG_CONST1; } -static inline int Dar_ObjIsHash( Dar_Obj_t * pObj ) { return pObj->Type == DAR_AIG_AND || pObj->Type == DAR_AIG_EXOR; } +static inline int Dar_ObjIsTerm( Dar_Obj_t * pObj ) { return pObj->Type == DAR_AIG_PI || pObj->Type == DAR_AIG_PO || pObj->Type == DAR_AIG_CONST1; } +static inline int Dar_ObjIsHash( Dar_Obj_t * pObj ) { return pObj->Type == DAR_AIG_AND || pObj->Type == DAR_AIG_EXOR || pObj->Type == DAR_AIG_LATCH; } static inline int Dar_ObjIsMarkA( Dar_Obj_t * pObj ) { return pObj->fMarkA; } static inline void Dar_ObjSetMarkA( Dar_Obj_t * pObj ) { pObj->fMarkA = 1; } static inline void Dar_ObjClearMarkA( Dar_Obj_t * pObj ) { pObj->fMarkA = 0; } -static inline void Dar_ObjSetTravId( Dar_Obj_t * pObj, int TravId ) { pObj->pData = (void *)TravId; } -static inline void Dar_ObjSetTravIdCurrent( Dar_Man_t * p, Dar_Obj_t * pObj ) { pObj->pData = (void *)p->nTravIds; } -static inline void Dar_ObjSetTravIdPrevious( Dar_Man_t * p, Dar_Obj_t * pObj ) { pObj->pData = (void *)(p->nTravIds - 1); } -static inline int Dar_ObjIsTravIdCurrent( Dar_Man_t * p, Dar_Obj_t * pObj ) { return (int )((int)pObj->pData == p->nTravIds); } -static inline int Dar_ObjIsTravIdPrevious( Dar_Man_t * p, Dar_Obj_t * pObj ) { return (int )((int)pObj->pData == p->nTravIds - 1); } +static inline void Dar_ObjSetTravId( Dar_Obj_t * pObj, int TravId ) { pObj->TravId = TravId; } +static inline void Dar_ObjSetTravIdCurrent( Dar_Man_t * p, Dar_Obj_t * pObj ) { pObj->TravId = p->nTravIds; } +static inline void Dar_ObjSetTravIdPrevious( Dar_Man_t * p, Dar_Obj_t * pObj ) { pObj->TravId = p->nTravIds - 1; } +static inline int Dar_ObjIsTravIdCurrent( Dar_Man_t * p, Dar_Obj_t * pObj ) { return (int)(pObj->TravId == p->nTravIds); } +static inline int Dar_ObjIsTravIdPrevious( Dar_Man_t * p, Dar_Obj_t * pObj ) { return (int)(pObj->TravId == p->nTravIds - 1); } static inline int Dar_ObjTravId( Dar_Obj_t * pObj ) { return (int)pObj->pData; } static inline int Dar_ObjPhase( Dar_Obj_t * pObj ) { return pObj->fPhase; } @@ -247,7 +251,7 @@ static inline Dar_Obj_t * Dar_ObjCreateGhost( Dar_Man_t * p, Dar_Obj_t * p0, Da assert( Type == DAR_AIG_PI || Dar_Regular(p0) != Dar_Regular(p1) ); pGhost = Dar_ManGhost(p); pGhost->Type = Type; - if ( Dar_Regular(p0)->Id < Dar_Regular(p1)->Id ) + if ( p1 == NULL || Dar_Regular(p0)->Id < Dar_Regular(p1)->Id ) { pGhost->pFanin0 = p0; pGhost->pFanin1 = p1; @@ -274,7 +278,8 @@ static inline Dar_Obj_t * Dar_ManFetchMemory( Dar_Man_t * p ) static inline void Dar_ManRecycleMemory( Dar_Man_t * p, Dar_Obj_t * pEntry ) { extern void Dar_MmFixedEntryRecycle( Dar_MmFixed_t * p, char * pEntry ); - pEntry->Type = DAR_AIG_NONE; // distinquishes dead node from live node + p->nDeleted++; + pEntry->Type = DAR_AIG_NONE; // distinquishes a dead node from a live node Dar_MmFixedEntryRecycle( p->pMemObjs, (char *)pEntry ); } @@ -291,7 +296,7 @@ static inline void Dar_ManRecycleMemory( Dar_Man_t * p, Dar_Obj_t * pEntry ) Vec_PtrForEachEntry( p->vPos, pObj, i ) // iterator over all objects, including those currently not used #define Dar_ManForEachObj( p, pObj, i ) \ - Vec_PtrForEachEntry( p->vObjs, pObj, i ) + Vec_PtrForEachEntry( p->vObjs, pObj, i ) if ( (pObj) == NULL ) {} else //////////////////////////////////////////////////////////////////////// /// FUNCTION DECLARATIONS /// @@ -313,7 +318,6 @@ extern Vec_Int_t * Dar_LibReadNodes(); extern Vec_Int_t * Dar_LibReadOuts(); /*=== darDfs.c ==========================================================*/ extern Vec_Ptr_t * Dar_ManDfs( Dar_Man_t * p ); -extern Vec_Ptr_t * Dar_ManDfsNode( Dar_Man_t * p, Dar_Obj_t * pNode ); extern int Dar_ManCountLevels( Dar_Man_t * p ); extern void Dar_ManCreateRefs( Dar_Man_t * p ); extern int Dar_DagSize( Dar_Obj_t * pObj ); @@ -342,11 +346,13 @@ extern void Dar_ObjConnect( Dar_Man_t * p, Dar_Obj_t * pObj, Dar_Obj_ extern void Dar_ObjDisconnect( Dar_Man_t * p, Dar_Obj_t * pObj ); extern void Dar_ObjDelete( Dar_Man_t * p, Dar_Obj_t * pObj ); extern void Dar_ObjDelete_rec( Dar_Man_t * p, Dar_Obj_t * pObj, int fFreeTop ); -extern void Dar_ObjReplace( Dar_Man_t * p, Dar_Obj_t * pObjOld, Dar_Obj_t * pObjNew ); +extern void Dar_ObjPatchFanin0( Dar_Man_t * p, Dar_Obj_t * pObj, Dar_Obj_t * pFaninNew ); +extern void Dar_ObjReplace( Dar_Man_t * p, Dar_Obj_t * pObjOld, Dar_Obj_t * pObjNew, int fNodesOnly ); /*=== darOper.c =========================================================*/ extern Dar_Obj_t * Dar_IthVar( Dar_Man_t * p, int i ); extern Dar_Obj_t * Dar_Oper( Dar_Man_t * p, Dar_Obj_t * p0, Dar_Obj_t * p1, Dar_Type_t Type ); extern Dar_Obj_t * Dar_And( Dar_Man_t * p, Dar_Obj_t * p0, Dar_Obj_t * p1 ); +extern Dar_Obj_t * Dar_Latch( Dar_Man_t * p, Dar_Obj_t * pObj, int fInitOne ); extern Dar_Obj_t * Dar_Or( Dar_Man_t * p, Dar_Obj_t * p0, Dar_Obj_t * p1 ); extern Dar_Obj_t * Dar_Exor( Dar_Man_t * p, Dar_Obj_t * p0, Dar_Obj_t * p1 ); extern Dar_Obj_t * Dar_Mux( Dar_Man_t * p, Dar_Obj_t * pC, Dar_Obj_t * p1, Dar_Obj_t * p0 ); @@ -355,6 +361,8 @@ extern Dar_Obj_t * Dar_Miter( Dar_Man_t * p, Vec_Ptr_t * vPairs ); extern Dar_Obj_t * Dar_CreateAnd( Dar_Man_t * p, int nVars ); extern Dar_Obj_t * Dar_CreateOr( Dar_Man_t * p, int nVars ); extern Dar_Obj_t * Dar_CreateExor( Dar_Man_t * p, int nVars ); +/*=== darSeq.c ========================================================*/ +extern int Dar_ManSeqStrash( Dar_Man_t * p, int nLatches, int * pInits ); /*=== darTable.c ========================================================*/ extern Dar_Obj_t * Dar_TableLookup( Dar_Man_t * p, Dar_Obj_t * pGhost ); extern void Dar_TableInsert( Dar_Man_t * p, Dar_Obj_t * pObj ); diff --git a/src/aig/dar/darCheck.c b/src/aig/dar/darCheck.c index 6cfba787..5c7a2390 100644 --- a/src/aig/dar/darCheck.c +++ b/src/aig/dar/darCheck.c @@ -89,15 +89,24 @@ int Dar_ManCheck( Dar_Man_t * p ) } } // count the total number of nodes - if ( Dar_ManObjNum(p) != 1 + Dar_ManPiNum(p) + Dar_ManPoNum(p) + Dar_ManAndNum(p) + Dar_ManExorNum(p) ) + if ( Dar_ManObjNum(p) != 1 + Dar_ManPiNum(p) + Dar_ManPoNum(p) + Dar_ManBufNum(p) + Dar_ManAndNum(p) + Dar_ManExorNum(p) + Dar_ManLatchNum(p) ) { printf( "Dar_ManCheck: The number of created nodes is wrong.\n" ); + printf( "C1 = %d. Pi = %d. Po = %d. Buf = %d. And = %d. Xor = %d. Lat = %d. Total = %d.\n", + 1, Dar_ManPiNum(p), Dar_ManPoNum(p), Dar_ManBufNum(p), Dar_ManAndNum(p), Dar_ManExorNum(p), Dar_ManLatchNum(p), + 1 + Dar_ManPiNum(p) + Dar_ManPoNum(p) + Dar_ManBufNum(p) + Dar_ManAndNum(p) + Dar_ManExorNum(p) + Dar_ManLatchNum(p) ); + printf( "Created = %d. Deleted = %d. Existing = %d.\n", + p->nCreated, p->nDeleted, p->nCreated - p->nDeleted ); return 0; } // count the number of nodes in the table - if ( Dar_TableCountEntries(p) != Dar_ManAndNum(p) + Dar_ManExorNum(p) ) + if ( Dar_TableCountEntries(p) != Dar_ManAndNum(p) + Dar_ManExorNum(p) + Dar_ManLatchNum(p) ) { printf( "Dar_ManCheck: The number of nodes in the structural hashing table is wrong.\n" ); + printf( "Entries = %d. And = %d. Xor = %d. Lat = %d. Total = %d.\n", + Dar_TableCountEntries(p), Dar_ManAndNum(p), Dar_ManExorNum(p), Dar_ManLatchNum(p), + Dar_ManAndNum(p) + Dar_ManExorNum(p) + Dar_ManLatchNum(p) ); + return 0; } // if ( !Dar_ManIsAcyclic(p) ) diff --git a/src/aig/dar/darCore.c b/src/aig/dar/darCore.c index 9f0f58f6..d56cca45 100644 --- a/src/aig/dar/darCore.c +++ b/src/aig/dar/darCore.c @@ -76,7 +76,7 @@ int Dar_ManRewrite( Dar_Man_t * p ) pObjNew = Dar_LibBuildBest( p ); pObjNew = Dar_NotCond( pObjNew, pObjNew->fPhase ^ pObj->fPhase ); // remove the old nodes - Dar_ObjReplace( p, pObj, pObjNew ); + Dar_ObjReplace( p, pObj, pObjNew, 1 ); // compare the gains nNodeAfter = Dar_ManNodeNum( p ); assert( p->GainBest == nNodeBefore - nNodeAfter ); @@ -99,6 +99,8 @@ int Dar_ManRewrite( Dar_Man_t * p ) return 1; } + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/dar/darDfs.c b/src/aig/dar/darDfs.c index 1c2ab057..bdb23c9d 100644 --- a/src/aig/dar/darDfs.c +++ b/src/aig/dar/darDfs.c @@ -39,15 +39,18 @@ SeeAlso [] ***********************************************************************/ -void Dar_ManDfs_rec( Dar_Obj_t * pObj, Vec_Ptr_t * vNodes ) +void Dar_ManDfs_rec( Dar_Man_t * p, Dar_Obj_t * pObj, Vec_Ptr_t * vNodes ) { assert( !Dar_IsComplement(pObj) ); - if ( !Dar_ObjIsNode(pObj) || Dar_ObjIsMarkA(pObj) ) + if ( pObj == NULL ) return; - Dar_ManDfs_rec( Dar_ObjFanin0(pObj), vNodes ); - Dar_ManDfs_rec( Dar_ObjFanin1(pObj), vNodes ); - assert( !Dar_ObjIsMarkA(pObj) ); // loop detection - Dar_ObjSetMarkA(pObj); + if ( Dar_ObjIsTravIdCurrent(p, pObj) ) + return; + assert( Dar_ObjIsNode(pObj) || Dar_ObjIsBuf(pObj) ); + Dar_ManDfs_rec( p, Dar_ObjFanin0(pObj), vNodes ); + Dar_ManDfs_rec( p, Dar_ObjFanin1(pObj), vNodes ); + assert( !Dar_ObjIsTravIdCurrent(p, pObj) ); // loop detection + Dar_ObjSetTravIdCurrent(p, pObj); Vec_PtrPush( vNodes, pObj ); } @@ -67,35 +70,21 @@ Vec_Ptr_t * Dar_ManDfs( Dar_Man_t * p ) Vec_Ptr_t * vNodes; Dar_Obj_t * pObj; int i; + Dar_ManIncrementTravId( p ); + // mark constant and PIs + Dar_ObjSetTravIdCurrent( p, Dar_ManConst1(p) ); + Dar_ManForEachPi( p, pObj, i ) + Dar_ObjSetTravIdCurrent( p, pObj ); + // if there are latches, mark them + if ( Dar_ManLatchNum(p) > 0 ) + Dar_ManForEachObj( p, pObj, i ) + if ( Dar_ObjIsLatch(pObj) ) + Dar_ObjSetTravIdCurrent( p, pObj ); + // go through the nodes vNodes = Vec_PtrAlloc( Dar_ManNodeNum(p) ); Dar_ManForEachObj( p, pObj, i ) - Dar_ManDfs_rec( pObj, vNodes ); - Dar_ManForEachObj( p, pObj, i ) - Dar_ObjClearMarkA(pObj); - return vNodes; -} - -/**Function************************************************************* - - Synopsis [Collects internal nodes in the DFS order.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Ptr_t * Dar_ManDfsNode( Dar_Man_t * p, Dar_Obj_t * pNode ) -{ - Vec_Ptr_t * vNodes; - Dar_Obj_t * pObj; - int i; - assert( !Dar_IsComplement(pNode) ); - vNodes = Vec_PtrAlloc( 16 ); - Dar_ManDfs_rec( pNode, vNodes ); - Vec_PtrForEachEntry( vNodes, pObj, i ) - Dar_ObjClearMarkA(pObj); + if ( Dar_ObjIsNode(pObj) || Dar_ObjIsBuf(pObj) ) + Dar_ManDfs_rec( p, pObj, vNodes ); return vNodes; } diff --git a/src/aig/dar/darMan.c b/src/aig/dar/darMan.c index bbac1360..1b40bb39 100644 --- a/src/aig/dar/darMan.c +++ b/src/aig/dar/darMan.c @@ -55,6 +55,7 @@ Dar_Man_t * Dar_ManStart( int nNodesMax ) // allocate arrays for nodes p->vPis = Vec_PtrAlloc( 100 ); p->vPos = Vec_PtrAlloc( 100 ); + p->vObjs = Vec_PtrAlloc( 1000 ); // prepare the internal memory manager p->pMemObjs = Dar_MmFixedStart( sizeof(Dar_Obj_t), nNodesMax ); p->pMemCuts = Dar_MmFlexStart(); @@ -66,7 +67,7 @@ Dar_Man_t * Dar_ManStart( int nNodesMax ) p->pConst1 = Dar_ManFetchMemory( p ); p->pConst1->Type = DAR_AIG_CONST1; p->pConst1->fPhase = 1; - p->nCreated = 1; + p->nObjs[DAR_AIG_CONST1]++; // start the table p->nTableSize = nNodesMax; p->pTable = ALLOC( Dar_Obj_t *, p->nTableSize ); @@ -100,10 +101,10 @@ void Dar_ManStop( Dar_Man_t * p ) // Dar_TableProfile( p ); Dar_MmFixedStop( p->pMemObjs, 0 ); Dar_MmFlexStop( p->pMemCuts, 0 ); - if ( p->vPis ) Vec_PtrFree( p->vPis ); - if ( p->vPos ) Vec_PtrFree( p->vPos ); - if ( p->vObjs ) Vec_PtrFree( p->vObjs ); - if ( p->vRequired ) Vec_IntFree( p->vRequired ); + if ( p->vPis ) Vec_PtrFree( p->vPis ); + if ( p->vPos ) Vec_PtrFree( p->vPos ); + if ( p->vObjs ) Vec_PtrFree( p->vObjs ); + if ( p->vRequired ) Vec_IntFree( p->vRequired ); if ( p->vLeavesBest ) Vec_PtrFree( p->vLeavesBest ); free( p->pTable ); free( p ); @@ -151,12 +152,15 @@ int Dar_ManCleanup( Dar_Man_t * p ) ***********************************************************************/ void Dar_ManPrintStats( Dar_Man_t * p ) { - printf( "PI/PO = %d/%d. ", Dar_ManPiNum(p), Dar_ManPoNum(p) ); - printf( "A = %7d. ", Dar_ManAndNum(p) ); - printf( "X = %5d. ", Dar_ManExorNum(p) ); - printf( "Cre = %7d. ", p->nCreated ); - printf( "Del = %7d. ", p->nDeleted ); - printf( "Lev = %3d. ", Dar_ManCountLevels(p) ); + printf( "PI/PO/Lat = %5d/%5d/%5d ", Dar_ManPiNum(p), Dar_ManPoNum(p), Dar_ManLatchNum(p) ); + printf( "A = %6d. ", Dar_ManAndNum(p) ); + if ( Dar_ManExorNum(p) ) + printf( "X = %5d. ", Dar_ManExorNum(p) ); + if ( Dar_ManBufNum(p) ) + printf( "B = %3d. ", Dar_ManBufNum(p) ); + printf( "Cre = %6d. ", p->nCreated ); + printf( "Del = %6d. ", p->nDeleted ); +// printf( "Lev = %3d. ", Dar_ManCountLevels(p) ); printf( "\n" ); } diff --git a/src/aig/dar/darObj.c b/src/aig/dar/darObj.c index faf9336e..2db13c71 100644 --- a/src/aig/dar/darObj.c +++ b/src/aig/dar/darObj.c @@ -89,7 +89,7 @@ Dar_Obj_t * Dar_ObjCreate( Dar_Man_t * p, Dar_Obj_t * pGhost ) { Dar_Obj_t * pObj; assert( !Dar_IsComplement(pGhost) ); - assert( Dar_ObjIsNode(pGhost) ); + assert( Dar_ObjIsHash(pGhost) ); assert( pGhost == &p->Ghost ); // get memory for the new object pObj = Dar_ManFetchMemory( p ); @@ -116,7 +116,7 @@ Dar_Obj_t * Dar_ObjCreate( Dar_Man_t * p, Dar_Obj_t * pGhost ) void Dar_ObjConnect( Dar_Man_t * p, Dar_Obj_t * pObj, Dar_Obj_t * pFan0, Dar_Obj_t * pFan1 ) { assert( !Dar_IsComplement(pObj) ); - assert( Dar_ObjIsNode(pObj) ); + assert( !Dar_ObjIsPi(pObj) ); // add the first fanin pObj->pFanin0 = pFan0; pObj->pFanin1 = pFan1; @@ -137,7 +137,7 @@ void Dar_ObjConnect( Dar_Man_t * p, Dar_Obj_t * pObj, Dar_Obj_t * pFan0, Dar_Obj pObj->fPhase = Dar_ObjFaninPhase(pFan0); } // add the node to the structural hash table - if ( Dar_ObjIsNode(pObj) ) + if ( Dar_ObjIsHash(pObj) ) Dar_TableInsert( p, pObj ); } @@ -161,7 +161,7 @@ void Dar_ObjDisconnect( Dar_Man_t * p, Dar_Obj_t * pObj ) if ( pObj->pFanin1 != NULL ) Dar_ObjDeref(Dar_ObjFanin1(pObj)); // remove the node from the structural hash table - if ( Dar_ObjIsNode(pObj) ) + if ( Dar_ObjIsHash(pObj) ) Dar_TableDelete( p, pObj ); // add the first fanin pObj->pFanin0 = NULL; @@ -184,7 +184,7 @@ void Dar_ObjDelete( Dar_Man_t * p, Dar_Obj_t * pObj ) assert( !Dar_IsComplement(pObj) ); assert( !Dar_ObjIsTerm(pObj) ); assert( Dar_ObjRefs(pObj) == 0 ); - p->nDeleted++; + p->nObjs[pObj->Type]--; Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL ); Dar_ManRecycleMemory( p, pObj ); } @@ -206,11 +206,10 @@ void Dar_ObjDelete_rec( Dar_Man_t * p, Dar_Obj_t * pObj, int fFreeTop ) assert( !Dar_IsComplement(pObj) ); if ( Dar_ObjIsConst1(pObj) || Dar_ObjIsPi(pObj) ) return; - assert( Dar_ObjIsNode(pObj) ); + assert( !Dar_ObjIsPo(pObj) ); pFanin0 = Dar_ObjFanin0(pObj); pFanin1 = Dar_ObjFanin1(pObj); Dar_ObjDisconnect( p, pObj ); - p->nObjs[pObj->Type]--; if ( fFreeTop ) Dar_ObjDelete( p, pObj ); if ( pFanin0 && !Dar_ObjIsNone(pFanin0) && Dar_ObjRefs(pFanin0) == 0 ) @@ -221,6 +220,33 @@ void Dar_ObjDelete_rec( Dar_Man_t * p, Dar_Obj_t * pObj, int fFreeTop ) /**Function************************************************************* + Synopsis [Replaces the first fanin of the node by the new fanin.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dar_ObjPatchFanin0( Dar_Man_t * p, Dar_Obj_t * pObj, Dar_Obj_t * pFaninNew ) +{ + Dar_Obj_t * pFaninOld; + assert( !Dar_IsComplement(pObj) ); + pFaninOld = Dar_ObjFanin0(pObj); + // decrement ref and remove fanout + Dar_ObjDeref( pFaninOld ); + // update the fanin + pObj->pFanin0 = pFaninNew; + // increment ref and add fanout + Dar_ObjRef( Dar_Regular(pFaninNew) ); + // get rid of old fanin + if ( !Dar_ObjIsPi(pFaninOld) && !Dar_ObjIsConst1(pFaninOld) && Dar_ObjRefs(pFaninOld) == 0 ) + Dar_ObjDelete_rec( p, pFaninOld, 1 ); +} + +/**Function************************************************************* + Synopsis [Replaces one object by another.] Description [Both objects are currently in the manager. The new object @@ -232,27 +258,27 @@ void Dar_ObjDelete_rec( Dar_Man_t * p, Dar_Obj_t * pObj, int fFreeTop ) SeeAlso [] ***********************************************************************/ -void Dar_ObjReplace( Dar_Man_t * p, Dar_Obj_t * pObjOld, Dar_Obj_t * pObjNew ) +void Dar_ObjReplace( Dar_Man_t * p, Dar_Obj_t * pObjOld, Dar_Obj_t * pObjNew, int fNodesOnly ) { Dar_Obj_t * pObjNewR = Dar_Regular(pObjNew); // the object to be replaced cannot be complemented assert( !Dar_IsComplement(pObjOld) ); // the object to be replaced cannot be a terminal assert( !Dar_ObjIsPi(pObjOld) && !Dar_ObjIsPo(pObjOld) ); - // the object to be used cannot be a buffer + // the object to be used cannot be a buffer or a PO assert( !Dar_ObjIsBuf(pObjNewR) && !Dar_ObjIsPo(pObjNewR) ); // the object cannot be the same assert( pObjOld != pObjNewR ); // make sure object is not pointing to itself - assert( pObjOld != Dar_ObjFanin0(pObjNewR) ); +// assert( pObjOld != Dar_ObjFanin0(pObjNewR) ); assert( pObjOld != Dar_ObjFanin1(pObjNewR) ); - // delete the old node + // recursively delete the old node - but leave the object there Dar_ObjDelete_rec( p, pObjOld, 0 ); // if the new object is complemented or already used, create a buffer - if ( Dar_IsComplement(pObjNew) || Dar_ObjRefs(pObjNew) > 0 || !Dar_ObjIsNode(pObjNew) ) + p->nObjs[pObjOld->Type]--; + if ( Dar_IsComplement(pObjNew) || Dar_ObjRefs(pObjNew) > 0 || (fNodesOnly && !Dar_ObjIsNode(pObjNew)) ) { pObjOld->Type = DAR_AIG_BUF; - p->nObjs[pObjOld->Type]++; Dar_ObjConnect( p, pObjOld, pObjNew, NULL ); } else @@ -261,9 +287,10 @@ void Dar_ObjReplace( Dar_Man_t * p, Dar_Obj_t * pObjOld, Dar_Obj_t * pObjNew ) Dar_Obj_t * pFanin1 = pObjNew->pFanin1; pObjOld->Type = pObjNew->Type; Dar_ObjDisconnect( p, pObjNew ); - Dar_ObjDelete( p, pObjNew ); Dar_ObjConnect( p, pObjOld, pFanin0, pFanin1 ); + Dar_ObjDelete( p, pObjNew ); } + p->nObjs[pObjOld->Type]++; } //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/dar/darOper.c b/src/aig/dar/darOper.c index 8921fe33..cfb89e31 100644 --- a/src/aig/dar/darOper.c +++ b/src/aig/dar/darOper.c @@ -89,6 +89,43 @@ Dar_Obj_t * Dar_Oper( Dar_Man_t * p, Dar_Obj_t * p0, Dar_Obj_t * p1, Dar_Type_t /**Function************************************************************* + Synopsis [Creates the canonical form of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dar_Obj_t * Dar_CanonPair_rec( Dar_Man_t * p, Dar_Obj_t * pGhost ) +{ + Dar_Obj_t * pResult, * pLat0, * pLat1; + int fCompl0, fCompl1; + Dar_Type_t Type; + assert( Dar_ObjIsNode(pGhost) ); + // consider the case when the pair is canonical + if ( !Dar_ObjIsLatch(Dar_ObjFanin0(pGhost)) || !Dar_ObjIsLatch(Dar_ObjFanin1(pGhost)) ) + { + if ( pResult = Dar_TableLookup( p, pGhost ) ) + return pResult; + return Dar_ObjCreate( p, pGhost ); + } + /// remember the latches + pLat0 = Dar_ObjFanin0(pGhost); + pLat1 = Dar_ObjFanin1(pGhost); + // remember type and compls + Type = Dar_ObjType(pGhost); + fCompl0 = Dar_ObjFaninC0(pGhost); + fCompl1 = Dar_ObjFaninC1(pGhost); + // call recursively + pResult = Dar_Oper( p, Dar_NotCond(Dar_ObjChild0(pLat0), fCompl0), Dar_NotCond(Dar_ObjChild0(pLat1), fCompl1), Type ); + // build latch on top of this + return Dar_Latch( p, pResult, (Type == DAR_AIG_AND)? fCompl0 & fCompl1 : fCompl0 ^ fCompl1 ); +} + +/**Function************************************************************* + Synopsis [Performs canonicization step.] Description [The argument nodes can be complemented.] @@ -114,11 +151,30 @@ Dar_Obj_t * Dar_And( Dar_Man_t * p, Dar_Obj_t * p0, Dar_Obj_t * p1 ) // check if it can be an EXOR gate // if ( Dar_ObjIsExorType( p0, p1, &pFan0, &pFan1 ) ) // return Dar_Exor( p, pFan0, pFan1 ); - // check the table pGhost = Dar_ObjCreateGhost( p, p0, p1, DAR_AIG_AND ); - if ( pResult = Dar_TableLookup( p, pGhost ) ) - return pResult; - return Dar_ObjCreate( p, pGhost ); + pResult = Dar_CanonPair_rec( p, pGhost ); + return pResult; +} + +/**Function************************************************************* + + Synopsis [Creates the canonical form of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dar_Obj_t * Dar_Latch( Dar_Man_t * p, Dar_Obj_t * pObj, int fInitOne ) +{ + Dar_Obj_t * pGhost, * pResult; + pGhost = Dar_ObjCreateGhost( p, Dar_NotCond(pObj, fInitOne), NULL, DAR_AIG_LATCH ); + pResult = Dar_TableLookup( p, pGhost ); + if ( pResult == NULL ) + pResult = Dar_ObjCreate( p, pGhost ); + return Dar_NotCond( pResult, fInitOne ); } /**Function************************************************************* diff --git a/src/aig/dar/darSeq.c b/src/aig/dar/darSeq.c new file mode 100644 index 00000000..bf3807f4 --- /dev/null +++ b/src/aig/dar/darSeq.c @@ -0,0 +1,471 @@ +/**CFile**************************************************************** + + FileName [darSeq.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [DAG-aware AIG rewriting.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 28, 2007.] + + Revision [$Id: darSeq.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "dar.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Converts combinational AIG manager into a sequential one.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dar_ManSeqStrashConvert( Dar_Man_t * p, int nLatches, int * pInits ) +{ + Dar_Obj_t * pObjLi, * pObjLo, * pLatch; + int i; + // collect the POs to be converted into latches + for ( i = 0; i < nLatches; i++ ) + { + // get the corresponding PI/PO pair + pObjLi = Dar_ManPo( p, Dar_ManPoNum(p) - nLatches + i ); + pObjLo = Dar_ManPi( p, Dar_ManPiNum(p) - nLatches + i ); + // create latch + pLatch = Dar_Latch( p, Dar_ObjChild0(pObjLi), pInits? pInits[i] : 0 ); + // recycle the old PO object + Dar_ObjDisconnect( p, pObjLi ); + Vec_PtrWriteEntry( p->vObjs, pObjLi->Id, NULL ); + Dar_ManRecycleMemory( p, pObjLi ); + // convert the corresponding PI to be a buffer and connect it to the latch + pObjLo->Type = DAR_AIG_BUF; + Dar_ObjConnect( p, pObjLo, pLatch, NULL ); + } + // shrink the arrays + Vec_PtrShrink( p->vPis, Dar_ManPiNum(p) - nLatches ); + Vec_PtrShrink( p->vPos, Dar_ManPoNum(p) - nLatches ); + // update the counters of different objects + p->nObjs[DAR_AIG_PI] -= nLatches; + p->nObjs[DAR_AIG_PO] -= nLatches; + p->nObjs[DAR_AIG_BUF] += nLatches; +} + +/**Function************************************************************* + + Synopsis [Collects internal nodes in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dar_ManDfsSeq_rec( Dar_Man_t * p, Dar_Obj_t * pObj, Vec_Ptr_t * vNodes ) +{ + assert( !Dar_IsComplement(pObj) ); + if ( pObj == NULL ) + return; + if ( Dar_ObjIsTravIdCurrent( p, pObj ) ) + return; + Dar_ObjSetTravIdCurrent( p, pObj ); + if ( Dar_ObjIsPi(pObj) ) + return; + Dar_ManDfsSeq_rec( p, Dar_ObjFanin0(pObj), vNodes ); + Dar_ManDfsSeq_rec( p, Dar_ObjFanin1(pObj), vNodes ); + Vec_PtrPush( vNodes, pObj ); +} + +/**Function************************************************************* + + Synopsis [Collects internal nodes in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Dar_ManDfsSeq( Dar_Man_t * p ) +{ + Vec_Ptr_t * vNodes; + Dar_Obj_t * pObj; + int i; + Dar_ManIncrementTravId( p ); + vNodes = Vec_PtrAlloc( Dar_ManNodeNum(p) ); + Dar_ManForEachPo( p, pObj, i ) + Dar_ManDfsSeq_rec( p, Dar_ObjFanin0(pObj), vNodes ); + return vNodes; +} + +/**Function************************************************************* + + Synopsis [Collects internal nodes in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dar_ManDfsUnreach_rec( Dar_Man_t * p, Dar_Obj_t * pObj, Vec_Ptr_t * vNodes ) +{ + assert( !Dar_IsComplement(pObj) ); + if ( pObj == NULL ) + return; + if ( Dar_ObjIsTravIdPrevious(p, pObj) || Dar_ObjIsTravIdCurrent(p, pObj) ) + return; + Dar_ObjSetTravIdPrevious( p, pObj ); // assume unknown + Dar_ManDfsUnreach_rec( p, Dar_ObjFanin0(pObj), vNodes ); + Dar_ManDfsUnreach_rec( p, Dar_ObjFanin1(pObj), vNodes ); + if ( Dar_ObjIsTravIdPrevious(p, Dar_ObjFanin0(pObj)) && + (Dar_ObjFanin1(pObj) == NULL || Dar_ObjIsTravIdPrevious(p, Dar_ObjFanin1(pObj))) ) + Vec_PtrPush( vNodes, pObj ); + else + Dar_ObjSetTravIdCurrent( p, pObj ); +} + +/**Function************************************************************* + + Synopsis [Collects internal nodes unreachable from PIs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Dar_ManDfsUnreach( Dar_Man_t * p ) +{ + Vec_Ptr_t * vNodes; + Dar_Obj_t * pObj, * pFanin; + int i, k;//, RetValue; + // collect unreachable nodes + Dar_ManIncrementTravId( p ); + Dar_ManIncrementTravId( p ); + // mark the constant and PIs + Dar_ObjSetTravIdPrevious( p, Dar_ManConst1(p) ); + Dar_ManForEachPi( p, pObj, i ) + Dar_ObjSetTravIdCurrent( p, pObj ); + // curr marks visited nodes reachable from PIs + // prev marks visited nodes unreachable or unknown + + // collect the unreachable nodes + vNodes = Vec_PtrAlloc( 32 ); + Dar_ManForEachPo( p, pObj, i ) + Dar_ManDfsUnreach_rec( p, Dar_ObjFanin0(pObj), vNodes ); + + // refine resulting nodes + do + { + k = 0; + Vec_PtrForEachEntry( vNodes, pObj, i ) + { + assert( Dar_ObjIsTravIdPrevious(p, pObj) ); + if ( Dar_ObjIsLatch(pObj) || Dar_ObjIsBuf(pObj) ) + { + pFanin = Dar_ObjFanin0(pObj); + assert( Dar_ObjIsTravIdPrevious(p, pFanin) || Dar_ObjIsTravIdCurrent(p, pFanin) ); + if ( Dar_ObjIsTravIdCurrent(p, pFanin) ) + { + Dar_ObjSetTravIdCurrent( p, pObj ); + continue; + } + } + else // AND gate + { + assert( Dar_ObjIsNode(pObj) ); + pFanin = Dar_ObjFanin0(pObj); + assert( Dar_ObjIsTravIdPrevious(p, pFanin) || Dar_ObjIsTravIdCurrent(p, pFanin) ); + if ( Dar_ObjIsTravIdCurrent(p, pFanin) ) + { + Dar_ObjSetTravIdCurrent( p, pObj ); + continue; + } + pFanin = Dar_ObjFanin1(pObj); + assert( Dar_ObjIsTravIdPrevious(p, pFanin) || Dar_ObjIsTravIdCurrent(p, pFanin) ); + if ( Dar_ObjIsTravIdCurrent(p, pFanin) ) + { + Dar_ObjSetTravIdCurrent( p, pObj ); + continue; + } + } + // write it back + Vec_PtrWriteEntry( vNodes, k++, pObj ); + } + Vec_PtrShrink( vNodes, k ); + } + while ( k < i ); + + if ( Vec_PtrSize(vNodes) > 0 ) + printf( "Found %d unreachable.\n", Vec_PtrSize(vNodes) ); + return vNodes; + +/* + // the resulting array contains all unreachable nodes except const 1 + if ( Vec_PtrSize(vNodes) == 0 ) + { + Vec_PtrFree( vNodes ); + return 0; + } + RetValue = Vec_PtrSize(vNodes); + + // mark these nodes + Dar_ManIncrementTravId( p ); + Vec_PtrForEachEntry( vNodes, pObj, i ) + Dar_ObjSetTravIdCurrent( p, pObj ); + Vec_PtrFree( vNodes ); + return RetValue; +*/ +} + + +/**Function************************************************************* + + Synopsis [Removes nodes that do not fanout into POs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dar_ManRemoveUnmarked( Dar_Man_t * p ) +{ + Vec_Ptr_t * vNodes; + Dar_Obj_t * pObj; + int i, RetValue; + // collect unmarked nodes + vNodes = Vec_PtrAlloc( 100 ); + Dar_ManForEachObj( p, pObj, i ) + { + if ( Dar_ObjIsTerm(pObj) ) + continue; + if ( Dar_ObjIsTravIdCurrent(p, pObj) ) + continue; +//Dar_ObjPrintVerbose( pObj, 0 ); + Dar_ObjDisconnect( p, pObj ); + Vec_PtrPush( vNodes, pObj ); + } + if ( Vec_PtrSize(vNodes) == 0 ) + { + Vec_PtrFree( vNodes ); + return 0; + } + // remove the dangling objects + RetValue = Vec_PtrSize(vNodes); + Vec_PtrForEachEntry( vNodes, pObj, i ) + Dar_ObjDelete( p, pObj ); + printf( "Removes %d dangling.\n", Vec_PtrSize(vNodes) ); + Vec_PtrFree( vNodes ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Dar_Obj_t * Dar_ObjReal_rec( Dar_Obj_t * pObj ) +{ + Dar_Obj_t * pObjNew, * pObjR = Dar_Regular(pObj); + if ( !Dar_ObjIsBuf(pObjR) ) + return pObj; + pObjNew = Dar_ObjReal_rec( Dar_ObjChild0(pObjR) ); + return Dar_NotCond( pObjNew, Dar_IsComplement(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Rehashes the nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dar_ManSeqRehashOne( Dar_Man_t * p, Vec_Ptr_t * vNodes, Vec_Ptr_t * vUnreach ) +{ + Dar_Obj_t * pObj, * pObjNew, * pFanin0, * pFanin1; + int i, RetValue = 0; + // mark the unreachable nodes + Dar_ManIncrementTravId( p ); + Vec_PtrForEachEntry( vUnreach, pObj, i ) + Dar_ObjSetTravIdCurrent(p, pObj); + // go through the nodes while skipping unreachable + Vec_PtrForEachEntry( vNodes, pObj, i ) + { + // skip nodes unreachable from the PIs + if ( Dar_ObjIsTravIdCurrent(p, pObj) ) + continue; + // process the node + if ( Dar_ObjIsPo(pObj) ) + { + if ( !Dar_ObjIsBuf(Dar_ObjFanin0(pObj)) ) + continue; + pFanin0 = Dar_ObjReal_rec( Dar_ObjChild0(pObj) ); + Dar_ObjPatchFanin0( p, pObj, pFanin0 ); + continue; + } + if ( Dar_ObjIsLatch(pObj) ) + { + if ( !Dar_ObjIsBuf(Dar_ObjFanin0(pObj)) ) + continue; + pObjNew = Dar_ObjReal_rec( Dar_ObjChild0(pObj) ); + pObjNew = Dar_Latch( p, pObjNew, 0 ); + Dar_ObjReplace( p, pObj, pObjNew, 1 ); + RetValue = 1; + continue; + } + if ( Dar_ObjIsNode(pObj) ) + { + if ( !Dar_ObjIsBuf(Dar_ObjFanin0(pObj)) && !Dar_ObjIsBuf(Dar_ObjFanin1(pObj)) ) + continue; + pFanin0 = Dar_ObjReal_rec( Dar_ObjChild0(pObj) ); + pFanin1 = Dar_ObjReal_rec( Dar_ObjChild1(pObj) ); + pObjNew = Dar_And( p, pFanin0, pFanin1 ); + Dar_ObjReplace( p, pObj, pObjNew, 1 ); + RetValue = 1; + continue; + } + } + return RetValue; +} + +/**Function************************************************************* + + Synopsis [If AIG contains buffers, this procedure removes them.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dar_ManRemoveBuffers( Dar_Man_t * p ) +{ + Dar_Obj_t * pObj, * pObjNew, * pFanin0, * pFanin1; + int i; + if ( Dar_ManBufNum(p) == 0 ) + return; + Dar_ManForEachObj( p, pObj, i ) + { + if ( Dar_ObjIsPo(pObj) ) + { + if ( !Dar_ObjIsBuf(Dar_ObjFanin0(pObj)) ) + continue; + pFanin0 = Dar_ObjReal_rec( Dar_ObjChild0(pObj) ); + Dar_ObjPatchFanin0( p, pObj, pFanin0 ); + } + else if ( Dar_ObjIsLatch(pObj) ) + { + if ( !Dar_ObjIsBuf(Dar_ObjFanin0(pObj)) ) + continue; + pFanin0 = Dar_ObjReal_rec( Dar_ObjChild0(pObj) ); + pObjNew = Dar_Latch( p, pFanin0, 0 ); + Dar_ObjReplace( p, pObj, pObjNew, 0 ); + } + else if ( Dar_ObjIsAnd(pObj) ) + { + if ( !Dar_ObjIsBuf(Dar_ObjFanin0(pObj)) && !Dar_ObjIsBuf(Dar_ObjFanin1(pObj)) ) + continue; + pFanin0 = Dar_ObjReal_rec( Dar_ObjChild0(pObj) ); + pFanin1 = Dar_ObjReal_rec( Dar_ObjChild1(pObj) ); + pObjNew = Dar_And( p, pFanin0, pFanin1 ); + Dar_ObjReplace( p, pObj, pObjNew, 0 ); + } + } + assert( Dar_ManBufNum(p) == 0 ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dar_ManSeqStrash( Dar_Man_t * p, int nLatches, int * pInits ) +{ + Vec_Ptr_t * vNodes, * vUnreach; + Dar_Obj_t * pObj; + int i; + int RetValue = 1; + // create latches out of the additional PI/PO pairs + Dar_ManSeqStrashConvert( p, nLatches, pInits ); + // iteratively rehash the network + while ( RetValue ) + { + Dar_ManPrintStats( p ); + + Dar_ManForEachObj( p, pObj, i ) + assert( pObj->Type > 0 ); + + // mark nodes unreachable from the PIs + vUnreach = Dar_ManDfsUnreach( p ); + // collect nodes reachable from the POs + vNodes = Dar_ManDfsSeq( p ); + // remove nodes unreachable from the POs + Dar_ManRemoveUnmarked( p ); + // continue rehashing as long as there are changes + RetValue = Dar_ManSeqRehashOne( p, vNodes, vUnreach ); + Vec_PtrFree( vNodes ); + Vec_PtrFree( vUnreach ); + } + // perform the final cleanup + Dar_ManIncrementTravId( p ); + vNodes = Dar_ManDfsSeq( p ); + Dar_ManRemoveUnmarked( p ); + Vec_PtrFree( vNodes ); + // remove buffers if they are left +// Dar_ManRemoveBuffers( p ); + // clean up + if ( !Dar_ManCheck( p ) ) + { + printf( "Dar_ManSeqStrash: The network check has failed.\n" ); + return 0; + } + return 1; + +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/dar/darTable.c b/src/aig/dar/darTable.c index 8b4bfaf3..af9956ec 100644 --- a/src/aig/dar/darTable.c +++ b/src/aig/dar/darTable.c @@ -39,8 +39,15 @@ static unsigned long Dar_Hash( Dar_Obj_t * pObj, int TableSize ) static Dar_Obj_t ** Dar_TableFind( Dar_Man_t * p, Dar_Obj_t * pObj ) { Dar_Obj_t ** ppEntry; - assert( Dar_ObjChild0(pObj) && Dar_ObjChild1(pObj) ); - assert( Dar_ObjFanin0(pObj)->Id < Dar_ObjFanin1(pObj)->Id ); + if ( Dar_ObjIsLatch(pObj) ) + { + assert( Dar_ObjChild0(pObj) && Dar_ObjChild1(pObj) == NULL ); + } + else + { + assert( Dar_ObjChild0(pObj) && Dar_ObjChild1(pObj) ); + assert( Dar_ObjFanin0(pObj)->Id < Dar_ObjFanin1(pObj)->Id ); + } for ( ppEntry = p->pTable + Dar_Hash(pObj, p->nTableSize); *ppEntry; ppEntry = &(*ppEntry)->pNext ) if ( *ppEntry == pObj ) return ppEntry; @@ -70,10 +77,20 @@ Dar_Obj_t * Dar_TableLookup( Dar_Man_t * p, Dar_Obj_t * pGhost ) { Dar_Obj_t * pEntry; assert( !Dar_IsComplement(pGhost) ); - assert( Dar_ObjChild0(pGhost) && Dar_ObjChild1(pGhost) ); - assert( Dar_ObjFanin0(pGhost)->Id < Dar_ObjFanin1(pGhost)->Id ); - if ( !Dar_ObjRefs(Dar_ObjFanin0(pGhost)) || !Dar_ObjRefs(Dar_ObjFanin1(pGhost)) ) - return NULL; + if ( pGhost->Type == DAR_AIG_LATCH ) + { + assert( Dar_ObjChild0(pGhost) && Dar_ObjChild1(pGhost) == NULL ); + if ( !Dar_ObjRefs(Dar_ObjFanin0(pGhost)) ) + return NULL; + } + else + { + assert( pGhost->Type == DAR_AIG_AND ); + assert( Dar_ObjChild0(pGhost) && Dar_ObjChild1(pGhost) ); + assert( Dar_ObjFanin0(pGhost)->Id < Dar_ObjFanin1(pGhost)->Id ); + if ( !Dar_ObjRefs(Dar_ObjFanin0(pGhost)) || !Dar_ObjRefs(Dar_ObjFanin1(pGhost)) ) + return NULL; + } for ( pEntry = p->pTable[Dar_Hash(pGhost, p->nTableSize)]; pEntry; pEntry = pEntry->pNext ) { if ( Dar_ObjChild0(pEntry) == Dar_ObjChild0(pGhost) && |