diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2007-06-08 08:01:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2007-06-08 08:01:00 -0700 |
commit | d47752011d94805850f8713258634d1bde5e639f (patch) | |
tree | 81236dfb564a1d5c3f4a8e2f6cd56f5b5f88313e | |
parent | feb8fb692e09a2fc7c1da4f2fcf605d398e940f2 (diff) | |
download | abc-d47752011d94805850f8713258634d1bde5e639f.tar.gz abc-d47752011d94805850f8713258634d1bde5e639f.tar.bz2 abc-d47752011d94805850f8713258634d1bde5e639f.zip |
Version abc70608
-rw-r--r-- | abc.dsp | 4 | ||||
-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 | ||||
-rw-r--r-- | src/base/abc/abcDfs.c | 3 | ||||
-rw-r--r-- | src/base/abc/abcNtk.c | 2 | ||||
-rw-r--r-- | src/base/abci/abc.c | 56 | ||||
-rw-r--r-- | src/base/abci/abcDar.c | 209 | ||||
-rw-r--r-- | src/base/abci/abcFraig.c | 4 | ||||
-rw-r--r-- | src/base/abci/abcPart.c | 55 | ||||
-rw-r--r-- | src/base/io/ioReadAiger.c | 13 | ||||
-rw-r--r-- | src/base/io/ioReadBench.c | 8 | ||||
-rw-r--r-- | src/base/io/ioWriteVerilog.c | 10 | ||||
-rw-r--r-- | src/base/io/ioWriteVerilog.zip | bin | 0 -> 3662 bytes | |||
-rw-r--r-- | src/base/ver/ver.h | 1 | ||||
-rw-r--r-- | src/base/ver/verCore.c | 173 | ||||
-rw-r--r-- | src/base/ver/verCore.zip | bin | 14163 -> 14624 bytes | |||
-rw-r--r-- | src/map/if/ifUtil.c | 20 |
24 files changed, 1103 insertions, 210 deletions
@@ -858,6 +858,10 @@ SOURCE=.\src\aig\dar\darOper.c # End Source File # Begin Source File +SOURCE=.\src\aig\dar\darSeq.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\dar\darTable.c # End Source File # Begin Source File 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) && diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c index b682f8ae..39e985c0 100644 --- a/src/base/abc/abcDfs.c +++ b/src/base/abc/abcDfs.c @@ -55,7 +55,10 @@ void Abc_NtkDfs_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ) assert( Abc_ObjIsNode( pNode ) || Abc_ObjIsBox( pNode ) ); // visit the transitive fanin of the node Abc_ObjForEachFanin( pNode, pFanin, i ) + { +// pFanin = Abc_ObjFanin( pNode, Abc_ObjFaninNum(pNode)-1-i ); Abc_NtkDfs_rec( Abc_ObjFanin0Ntk(pFanin), vNodes ); + } // add the node after the fanins have been added Vec_PtrPush( vNodes, pNode ); } diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c index ce187f60..7d8d0f0f 100644 --- a/src/base/abc/abcNtk.c +++ b/src/base/abc/abcNtk.c @@ -987,7 +987,7 @@ void Abc_NtkFixNonDrivenNets( Abc_Ntk_t * pNtk ) Abc_Obj_t * pNet, * pNode; int i; - if ( Abc_NtkNodeNum(pNtk) == 0 ) + if ( Abc_NtkNodeNum(pNtk) == 0 && Abc_NtkBoxNum(pNtk) == 0 ) return; // check for non-driven nets diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 1e0fed0c..d5321e6d 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -330,7 +330,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) // Kit_TruthCountMintermsPrecomp(); // Kit_DsdPrecompute4Vars(); - Dar_LibStart(); +// Dar_LibStart(); } /**Function************************************************************* @@ -346,7 +346,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) ***********************************************************************/ void Abc_End() { - Dar_LibStop(); +// Dar_LibStop(); Abc_NtkFraigStoreClean(); // Rwt_Man4ExplorePrint(); @@ -5931,7 +5931,7 @@ usage: int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; - Abc_Ntk_t * pNtk;//, * pNtkRes; + Abc_Ntk_t * pNtk, * pNtkRes; int c; int nLevels; // extern Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk ); @@ -5940,6 +5940,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) // extern int Pr_ManProofTest( char * pFileName ); extern void Abc_NtkCompareSupports( Abc_Ntk_t * pNtk ); extern void Abc_NtkCompareCones( Abc_Ntk_t * pNtk ); + extern Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -6049,8 +6050,21 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) // Abc_Ntk4VarTable( pNtk ); // Dat_NtkGenerateArrays( pNtk ); - return 0; + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "Network should be strashed. Command has failed.\n" ); + return 1; + } + pNtkRes = Abc_NtkDar( pNtk ); + if ( pNtkRes == NULL ) + { + fprintf( pErr, "Command has failed.\n" ); + return 1; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; usage: fprintf( pErr, "usage: test [-h]\n" ); fprintf( pErr, "\t testbench for new procedures\n" ); @@ -7286,6 +7300,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) int fAllNodes; int fExdc; int c; + int fPartition = 0; pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -7307,7 +7322,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) pParams->fVerbose = 0; // the verbosiness flag pParams->fVerboseP = 0; // the verbosiness flag Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "RDCrscpvaeh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "RDCrscptvaeh" ) ) != EOF ) { switch ( c ) { @@ -7360,6 +7375,9 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'v': pParams->fVerbose ^= 1; break; + case 't': + fPartition ^= 1; + break; case 'a': fAllNodes ^= 1; break; @@ -7388,13 +7406,28 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) pParams->fVerboseP = pParams->fTryProve; // get the new network - if ( Abc_NtkIsStrash(pNtk) ) - pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes, fExdc ); + if ( fPartition ) + { + pNtkRes = Abc_NtkDup( pNtk ); + if ( Abc_NtkIsStrash(pNtk) ) + Abc_NtkFraigPartitionedTime( pNtk, &Params ); + else + { + pNtk = Abc_NtkStrash( pNtk, fAllNodes, !fAllNodes, 0 ); + Abc_NtkFraigPartitionedTime( pNtk, &Params ); + Abc_NtkDelete( pNtk ); + } + } else { - pNtk = Abc_NtkStrash( pNtk, fAllNodes, !fAllNodes, 0 ); - pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes, fExdc ); - Abc_NtkDelete( pNtk ); + if ( Abc_NtkIsStrash(pNtk) ) + pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes, fExdc ); + else + { + pNtk = Abc_NtkStrash( pNtk, fAllNodes, !fAllNodes, 0 ); + pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes, fExdc ); + Abc_NtkDelete( pNtk ); + } } if ( pNtkRes == NULL ) { @@ -7411,7 +7444,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) usage: sprintf( Buffer, "%d", pParams->nBTLimit ); - fprintf( pErr, "usage: fraig [-R num] [-D num] [-C num] [-rscpvah]\n" ); + fprintf( pErr, "usage: fraig [-R num] [-D num] [-C num] [-rscpvtah]\n" ); fprintf( pErr, "\t transforms a logic network into a functionally reduced AIG\n" ); fprintf( pErr, "\t-R num : number of random patterns (127 < num < 32769) [default = %d]\n", pParams->nPatsRand ); fprintf( pErr, "\t-D num : number of systematic patterns (127 < num < 32769) [default = %d]\n", pParams->nPatsDyna ); @@ -7423,6 +7456,7 @@ usage: fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", pParams->fVerbose? "yes": "no" ); fprintf( pErr, "\t-e : toggle functional sweeping using EXDC [default = %s]\n", fExdc? "yes": "no" ); fprintf( pErr, "\t-a : toggle between all nodes and DFS nodes [default = %s]\n", fAllNodes? "all": "dfs" ); + fprintf( pErr, "\t-t : toggle using partitioned representation [default = %s]\n", fPartition? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; } diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 0863061b..81278515 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -25,62 +25,12 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static Dar_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk ); -static Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Dar_Man_t * pMan ); - //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* - Synopsis [Gives the current ABC network to AIG manager for processing.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk ) -{ - Abc_Ntk_t * pNtkAig; - Dar_Man_t * pMan;//, * pTemp; - assert( Abc_NtkIsStrash(pNtk) ); - // convert to the AIG manager - pMan = Abc_NtkToDar( pNtk ); - if ( pMan == NULL ) - return NULL; - if ( !Dar_ManCheck( pMan ) ) - { - printf( "Abc_NtkDar: AIG check has failed.\n" ); - Dar_ManStop( pMan ); - return NULL; - } - // perform balance - Dar_ManPrintStats( pMan ); -// Dar_ManDumpBlif( pMan, "aig_temp.blif" ); - pMan->pPars = Dar_ManDefaultParams(); - Dar_ManRewrite( pMan ); - Dar_ManPrintStats( pMan ); - // convert from the AIG manager - pNtkAig = Abc_NtkFromDar( pNtk, pMan ); - if ( pNtkAig == NULL ) - return NULL; - Dar_ManStop( pMan ); - // make sure everything is okay - if ( !Abc_NtkCheck( pNtkAig ) ) - { - printf( "Abc_NtkDar: The network check has failed.\n" ); - Abc_NtkDelete( pNtkAig ); - return NULL; - } - return pNtkAig; -} - -/**Function************************************************************* - Synopsis [Converts the network from the AIG manager into ABC.] Description [] @@ -96,7 +46,7 @@ Dar_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk ) Abc_Obj_t * pObj; int i; // create the manager - pMan = Dar_ManStart( Abc_NtkNodeNum(pNtk) ); + pMan = Dar_ManStart( Abc_NtkNodeNum(pNtk) + 100 ); // transfer the pointers to the basic nodes Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Dar_ManConst1(pMan); Abc_NtkForEachCi( pNtk, pObj, i ) @@ -122,14 +72,14 @@ Dar_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtk, Dar_Man_t * pMan ) +Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Dar_Man_t * pMan ) { Vec_Ptr_t * vNodes; Abc_Ntk_t * pNtkNew; Dar_Obj_t * pObj; int i; // perform strashing - pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG ); + pNtkNew = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG ); // transfer the pointers to the basic nodes Dar_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew); Dar_ManForEachPi( pMan, pObj, i ) @@ -147,6 +97,159 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtk, Dar_Man_t * pMan ) return pNtkNew; } +/**Function************************************************************* + + Synopsis [Converts the network from the AIG manager into ABC.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkFromDarSeq( Abc_Ntk_t * pNtkOld, Dar_Man_t * pMan ) +{ + Vec_Ptr_t * vNodes; + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pObjNew, * pFaninNew, * pFaninNew0, * pFaninNew1; + Dar_Obj_t * pObj; + int i; +// assert( Dar_ManLatchNum(pMan) > 0 ); + // perform strashing + pNtkNew = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG ); + // transfer the pointers to the basic nodes + Dar_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew); + Dar_ManForEachPi( pMan, pObj, i ) + pObj->pData = Abc_NtkPi(pNtkNew, i); + // create latches of the new network + Dar_ManForEachObj( pMan, pObj, i ) + { + if ( !Dar_ObjIsLatch(pObj) ) + continue; + pObjNew = Abc_NtkCreateLatch( pNtkNew ); + pFaninNew0 = Abc_NtkCreateBi( pNtkNew ); + pFaninNew1 = Abc_NtkCreateBo( pNtkNew ); + Abc_ObjAddFanin( pObjNew, pFaninNew0 ); + Abc_ObjAddFanin( pFaninNew1, pObjNew ); + Abc_LatchSetInit0( pObjNew ); + pObj->pData = Abc_ObjFanout0( pObjNew ); + } + Abc_NtkAddDummyBoxNames( pNtkNew ); + // rebuild the AIG + vNodes = Dar_ManDfs( pMan ); + Vec_PtrForEachEntry( vNodes, pObj, i ) + { + // add the first fanin + pObj->pData = pFaninNew0 = (Abc_Obj_t *)Dar_ObjChild0Copy(pObj); + if ( Dar_ObjIsBuf(pObj) ) + continue; + // add the second fanin + pFaninNew1 = (Abc_Obj_t *)Dar_ObjChild1Copy(pObj); + // create the new node + if ( Dar_ObjIsExor(pObj) ) + pObj->pData = pObjNew = Abc_AigXor( pNtkNew->pManFunc, pFaninNew0, pFaninNew1 ); + else + pObj->pData = pObjNew = Abc_AigAnd( pNtkNew->pManFunc, pFaninNew0, pFaninNew1 ); + } + Vec_PtrFree( vNodes ); + // connect the PO nodes + Dar_ManForEachPo( pMan, pObj, i ) + { + pFaninNew = (Abc_Obj_t *)Dar_ObjChild0Copy( pObj ); + Abc_ObjAddFanin( Abc_NtkPo(pNtkNew, i), pFaninNew ); + } + // connect the latches + Dar_ManForEachObj( pMan, pObj, i ) + { + if ( !Dar_ObjIsLatch(pObj) ) + continue; + pFaninNew = (Abc_Obj_t *)Dar_ObjChild0Copy( pObj ); + Abc_ObjAddFanin( Abc_ObjFanin0(Abc_ObjFanin0(pObj->pData)), pFaninNew ); + } + if ( !Abc_NtkCheck( pNtkNew ) ) + fprintf( stdout, "Abc_NtkFromIvySeq(): Network check has failed.\n" ); + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Collect latch values.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int * Abc_NtkGetLatchValues( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pLatch; + int i, * pArray; + pArray = ALLOC( int, Abc_NtkLatchNum(pNtk) ); + Abc_NtkForEachLatch( pNtk, pLatch, i ) + pArray[i] = Abc_LatchIsInit1(pLatch); + return pArray; +} + +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk ) +{ + Abc_Ntk_t * pNtkAig; + Dar_Man_t * pMan;//, * pTemp; + int * pArray; + + assert( Abc_NtkIsStrash(pNtk) ); + // convert to the AIG manager + pMan = Abc_NtkToDar( pNtk ); + if ( pMan == NULL ) + return NULL; + if ( !Dar_ManCheck( pMan ) ) + { + printf( "Abc_NtkDar: AIG check has failed.\n" ); + Dar_ManStop( pMan ); + return NULL; + } + // perform balance + Dar_ManPrintStats( pMan ); + + pArray = Abc_NtkGetLatchValues(pNtk); + Dar_ManSeqStrash( pMan, Abc_NtkLatchNum(pNtk), pArray ); + free( pArray ); + +// Dar_ManDumpBlif( pMan, "aig_temp.blif" ); +// pMan->pPars = Dar_ManDefaultParams(); +// Dar_ManRewrite( pMan ); + Dar_ManPrintStats( pMan ); + // convert from the AIG manager + if ( Dar_ManLatchNum(pMan) ) + pNtkAig = Abc_NtkFromDarSeq( pNtk, pMan ); + else + pNtkAig = Abc_NtkFromDar( pNtk, pMan ); + if ( pNtkAig == NULL ) + return NULL; + Dar_ManStop( pMan ); + // make sure everything is okay + if ( !Abc_NtkCheck( pNtkAig ) ) + { + printf( "Abc_NtkDar: The network check has failed.\n" ); + Abc_NtkDelete( pNtkAig ); + return NULL; + } + return pNtkAig; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c index 30e49af2..fa6771b3 100644 --- a/src/base/abci/abcFraig.c +++ b/src/base/abci/abcFraig.c @@ -687,7 +687,7 @@ int Abc_NtkFraigStore( Abc_Ntk_t * pNtk ) // set the number of networks stored Abc_FrameSetNtkStoreSize( Abc_FrameReadNtkStoreSize() + 1 ); } -// printf( "The number of AIG nodes added to storage = %5d.\n", Abc_NtkNodeNum(pStore) - nAndsOld ); + printf( "The number of AIG nodes added to storage = %5d.\n", Abc_NtkNodeNum(pStore) - nAndsOld ); return 1; } @@ -734,7 +734,7 @@ Abc_Ntk_t * Abc_NtkFraigRestore() Fraig_ParamsSetDefault( &Params ); Params.nPatsRand = nWordsMin * 32; // the number of words of random simulation info Params.nPatsDyna = nWordsMin * 32; // the number of words of dynamic simulation info - Params.nBTLimit = 99; // the max number of backtracks to perform + Params.nBTLimit = 999999; // the max number of backtracks to perform Params.fFuncRed = 1; // performs only one level hashing Params.fFeedBack = 1; // enables solver feedback Params.fDist1Pats = 1; // enables distance-1 patterns diff --git a/src/base/abci/abcPart.c b/src/base/abci/abcPart.c index 748868de..787e3f88 100644 --- a/src/base/abci/abcPart.c +++ b/src/base/abci/abcPart.c @@ -698,12 +698,67 @@ Abc_Ntk_t * Abc_NtkFraigPartitioned( Abc_Ntk_t * pNtk, void * pParams ) // derive the final network pNtkFraig = Abc_NtkPartStitchChoices( pNtk, vFraigs ); Vec_PtrForEachEntry( vFraigs, pNtkAig, i ) + { +// Abc_NtkPrintStats( stdout, pNtkAig, 0 ); Abc_NtkDelete( pNtkAig ); + } Vec_PtrFree( vFraigs ); return pNtkFraig; } +/**Function************************************************************* + + Synopsis [Stitches together several networks with choice nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkFraigPartitionedTime( Abc_Ntk_t * pNtk, void * pParams ) +{ + extern int Cmd_CommandExecute( void * pAbc, char * sCommand ); + extern void * Abc_FrameGetGlobalFrame(); + + Vec_Vec_t * vParts; + Vec_Ptr_t * vFraigs, * vOne; + Abc_Ntk_t * pNtkAig, * pNtkFraig; + int i; + int clk = clock(); + + // perform partitioning + assert( Abc_NtkIsStrash(pNtk) ); +// vParts = Abc_NtkPartitionNaive( pNtk, 20 ); + vParts = Abc_NtkPartitionSmart( pNtk, 0, 0 ); + + Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "unset progressbar" ); + + // fraig each partition + vFraigs = Vec_PtrAlloc( Vec_VecSize(vParts) ); + Vec_VecForEachLevel( vParts, vOne, i ) + { + pNtkAig = Abc_NtkCreateConeArray( pNtk, vOne, 0 ); + pNtkFraig = Abc_NtkFraig( pNtkAig, pParams, 0, 0 ); + Vec_PtrPush( vFraigs, pNtkFraig ); + Abc_NtkDelete( pNtkAig ); + + printf( "Finished part %d (out of %d)\r", i+1, Vec_VecSize(vParts) ); + } + Vec_VecFree( vParts ); + + Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "set progressbar" ); + + // derive the final network + Vec_PtrForEachEntry( vFraigs, pNtkAig, i ) + Abc_NtkDelete( pNtkAig ); + Vec_PtrFree( vFraigs ); + + PRT( "Partitioned fraiging time", clock() - clk ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/io/ioReadAiger.c b/src/base/io/ioReadAiger.c index a54a00fe..fe519476 100644 --- a/src/base/io/ioReadAiger.c +++ b/src/base/io/ioReadAiger.c @@ -96,7 +96,7 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck ) // prepare the array of nodes vNodes = Vec_PtrAlloc( 1 + nInputs + nLatches + nAnds ); - Vec_PtrPush( vNodes, Abc_AigConst1(pNtkNew) ); + Vec_PtrPush( vNodes, Abc_ObjNot( Abc_AigConst1(pNtkNew) ) ); // create the PIs for ( i = 0; i < nInputs; i++ ) @@ -122,6 +122,8 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck ) Vec_PtrPush( vNodes, pNode1 ); // assign names to latch and its input Abc_ObjAssignName( pObj, Abc_ObjNameDummy("_L", i, nDigits), NULL ); + + printf( "Creating latch %s with input %d and output %d.\n", Abc_ObjName(pObj), pNode0->Id, pNode1->Id ); } // remember the beginning of latch/PO literals @@ -156,14 +158,17 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck ) Abc_NtkForEachLatchInput( pNtkNew, pObj, i ) { uLit0 = atoi( pCur ); while ( *pCur++ != '\n' ); - pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) ^ (uLit0 < 2) ); + pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) ); Abc_ObjAddFanin( pObj, pNode0 ); + + printf( "Adding input %d to latch input %d.\n", pNode0->Id, pObj->Id ); + } // read the PO driver literals Abc_NtkForEachPo( pNtkNew, pObj, i ) { uLit0 = atoi( pCur ); while ( *pCur++ != '\n' ); - pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) ^ (uLit0 < 2) ); + pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) ); Abc_ObjAddFanin( pObj, pNode0 ); } @@ -204,7 +209,7 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck ) Abc_ObjAssignName( Abc_ObjFanin0(Abc_ObjFanin0(pObj)), Abc_ObjName(pObj), "L" ); // mark the node as named pObj->pCopy = (Abc_Obj_t *)Abc_ObjName(pObj); - } + } // skipping the comments free( pContents ); Vec_PtrFree( vNodes ); diff --git a/src/base/io/ioReadBench.c b/src/base/io/ioReadBench.c index 2730ba69..ba622e40 100644 --- a/src/base/io/ioReadBench.c +++ b/src/base/io/ioReadBench.c @@ -118,7 +118,13 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p ) if ( strncmp(pType, "DFF", 3) == 0 ) // works for both DFF and DFFRSE { pNode = Io_ReadCreateLatch( pNtk, vTokens->pArray[2], vTokens->pArray[0] ); - Abc_LatchSetInit0( pNode ); +// Abc_LatchSetInit0( pNode ); + if ( pType[3] == '0' ) + Abc_LatchSetInit0( pNode ); + else if ( pType[3] == '1' ) + Abc_LatchSetInit1( pNode ); + else + Abc_LatchSetInitDc( pNode ); } else if ( strcmp(pType, "LUT") == 0 ) { diff --git a/src/base/io/ioWriteVerilog.c b/src/base/io/ioWriteVerilog.c index a02d53fd..a4eeb78f 100644 --- a/src/base/io/ioWriteVerilog.c +++ b/src/base/io/ioWriteVerilog.c @@ -113,7 +113,12 @@ void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk ) { // write inputs and outputs // fprintf( pFile, "module %s ( gclk,\n ", Abc_NtkName(pNtk) ); - fprintf( pFile, "module %s ( \n ", Abc_NtkName(pNtk) ); + fprintf( pFile, "module %s ( ", Abc_NtkName(pNtk) ); + // add the clock signal if it does not exist + if ( Abc_NtkLatchNum(pNtk) > 0 && Nm_ManFindIdByName(pNtk->pManName, "clock", ABC_OBJ_PI) == -1 ) + fprintf( pFile, "clock, " ); + // write other primary inputs + fprintf( pFile, "\n " ); if ( Abc_NtkPiNum(pNtk) > 0 ) { Io_WriteVerilogPis( pFile, pNtk, 3 ); @@ -435,7 +440,8 @@ void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk ) return; // write the latches // fprintf( pFile, " always @(posedge %s) begin\n", Io_WriteVerilogGetName(Abc_ObjFanout0(Abc_NtkPi(pNtk,0))) ); - fprintf( pFile, " always begin\n" ); +// fprintf( pFile, " always begin\n" ); + fprintf( pFile, " always @ (posedge clock) begin\n" ); Abc_NtkForEachLatch( pNtk, pLatch, i ) { fprintf( pFile, " %s", Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch)))) ); diff --git a/src/base/io/ioWriteVerilog.zip b/src/base/io/ioWriteVerilog.zip Binary files differnew file mode 100644 index 00000000..19e68a89 --- /dev/null +++ b/src/base/io/ioWriteVerilog.zip diff --git a/src/base/ver/ver.h b/src/base/ver/ver.h index cf2b7497..9c538ac4 100644 --- a/src/base/ver/ver.h +++ b/src/base/ver/ver.h @@ -66,6 +66,7 @@ struct Ver_Man_t_ Vec_Ptr_t * vNames; Vec_Ptr_t * vStackFn; Vec_Int_t * vStackOp; + Vec_Int_t * vPerm; }; diff --git a/src/base/ver/verCore.c b/src/base/ver/verCore.c index 12c54dba..6d7d230e 100644 --- a/src/base/ver/verCore.c +++ b/src/base/ver/verCore.c @@ -110,6 +110,7 @@ Ver_Man_t * Ver_ParseStart( char * pFileName, Abc_Lib_t * pGateLib ) p->vNames = Vec_PtrAlloc( 100 ); p->vStackFn = Vec_PtrAlloc( 100 ); p->vStackOp = Vec_IntAlloc( 100 ); + p->vPerm = Vec_IntAlloc( 100 ); // create the design library and assign the technology library p->pDesign = Abc_LibCreate( pFileName ); p->pDesign->pLibrary = pGateLib; @@ -136,6 +137,7 @@ void Ver_ParseStop( Ver_Man_t * p ) Vec_PtrFree( p->vNames ); Vec_PtrFree( p->vStackFn ); Vec_IntFree( p->vStackOp ); + Vec_IntFree( p->vPerm ); free( p ); } @@ -1193,6 +1195,12 @@ int Ver_ParseAssign( Ver_Man_t * pMan, Abc_Ntk_t * pNtk ) pFunc = (Hop_Obj_t *)Mio_LibraryReadConst1(Abc_FrameReadLibGen()); else { + // "assign foo = \bar ;" + if ( *pEquation == '\\' ) + { + pEquation++; + pEquation[strlen(pEquation) - 1] = 0; + } if ( Ver_ParseFindNet(pNtk, pEquation) == NULL ) { sprintf( pMan->sError, "Cannot read Verilog with non-trivial assignments in the mapped netlist." ); @@ -1358,6 +1366,29 @@ int Ver_ParseGateStandard( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_GateType_t Ga /**Function************************************************************* + Synopsis [Returns the index of the given pin the gate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ver_FindGateInput( Mio_Gate_t * pGate, char * pName ) +{ + Mio_Pin_t * pGatePin; + int i; + for ( i = 0, pGatePin = Mio_GateReadPins(pGate); pGatePin != NULL; pGatePin = Mio_PinReadNext(pGatePin), i++ ) + if ( strcmp(pName, Mio_PinReadName(pGatePin)) == 0 ) + return i; + if ( strcmp(pName, Mio_GateReadOutName(pGate)) == 0 ) + return i; + return -1; +} + +/**Function************************************************************* + Synopsis [Parses one directive.] Description [] @@ -1369,10 +1400,10 @@ int Ver_ParseGateStandard( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_GateType_t Ga ***********************************************************************/ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate ) { - Mio_Pin_t * pGatePin; Ver_Stream_t * p = pMan->pReader; Abc_Obj_t * pNetActual, * pNode; char * pWord, Symbol; + int Input, i, nFanins = Mio_GateReadInputs(pGate); // convert from the blackbox into the network with local functions representated by gates if ( 1 != pMan->fMapped ) @@ -1404,7 +1435,7 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate ) pNode->pData = pGate; // parse pairs of formal/actural inputs - pGatePin = Mio_GateReadPins(pGate); + Vec_IntClear( pMan->vPerm ); while ( 1 ) { // process one pair of formal/actual parameters @@ -1420,24 +1451,13 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate ) if ( pWord == NULL ) return 0; - // make sure that the formal name is the same as the gate's - if ( Mio_GateReadInputs(pGate) == Abc_ObjFaninNum(pNode) ) - { - if ( strcmp(pWord, Mio_GateReadOutName(pGate)) ) - { - sprintf( pMan->sError, "Formal output name listed %s is different from the name of the gate output %s.", pWord, Mio_GateReadOutName(pGate) ); - Ver_ParsePrintErrorMessage( pMan ); - return 0; - } - } - else + // find the corresponding pin of the gate + Input = Ver_FindGateInput( pGate, pWord ); + if ( Input == -1 ) { - if ( strcmp(pWord, Mio_PinReadName(pGatePin)) ) - { - sprintf( pMan->sError, "Formal input name listed %s is different from the name of the corresponding pin %s.", pWord, Mio_PinReadName(pGatePin) ); - Ver_ParsePrintErrorMessage( pMan ); - return 0; - } + sprintf( pMan->sError, "Formal input name %s cannot be found in the gate %s.", pWord, Mio_GateReadOutName(pGate) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; } // open the paranthesis @@ -1482,10 +1502,13 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate ) } // add the fanin - if ( Mio_GateReadInputs(pGate) == Abc_ObjFaninNum(pNode) ) - Abc_ObjAddFanin( pNetActual, pNode ); // fanout - else + if ( Input < nFanins ) + { + Vec_IntPush( pMan->vPerm, Input ); Abc_ObjAddFanin( pNode, pNetActual ); // fanin + } + else + Abc_ObjAddFanin( pNetActual, pNode ); // fanout // check if it is the end of gate Ver_ParseSkipComments( pMan ); @@ -1501,13 +1524,10 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate ) return 0; } Ver_ParseSkipComments( pMan ); - - // get the next pin - pGatePin = Mio_PinReadNext(pGatePin); } // check that the gate as the same number of input - if ( !(Abc_ObjFaninNum(pNode) == Mio_GateReadInputs(pGate) && Abc_ObjFanoutNum(pNode) == 1) ) + if ( !(Abc_ObjFaninNum(pNode) == nFanins && Abc_ObjFanoutNum(pNode) == 1) ) { sprintf( pMan->sError, "Parsing of gate %s has failed.", Mio_GateReadName(pGate) ); Ver_ParsePrintErrorMessage( pMan ); @@ -1522,6 +1542,20 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate ) Ver_ParsePrintErrorMessage( pMan ); return 0; } + + // check if we need to permute the inputs + Vec_IntForEachEntry( pMan->vPerm, Input, i ) + if ( Input != i ) + break; + if ( i < Vec_IntSize(pMan->vPerm) ) + { + // add the fanin numnbers to the end of the permuation array + for ( i = 0; i < nFanins; i++ ) + Vec_IntPush( pMan->vPerm, Abc_ObjFaninId(pNode, i) ); + // write the fanin numbers into their corresponding places (according to the gate) + for ( i = 0; i < nFanins; i++ ) + Vec_IntWriteEntry( &pNode->vFanins, Vec_IntEntry(pMan->vPerm, i), Vec_IntEntry(pMan->vPerm, i+nFanins) ); + } return 1; } @@ -1546,6 +1580,7 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox ) Abc_Obj_t * pNode; char * pWord, Symbol; int fCompl, fFormalIsGiven; + int i, k, Bit, Limit, nMsb, nLsb, fQuit, flag; // gate the name of the box pWord = Ver_ParseGetName( pMan ); @@ -1613,8 +1648,6 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox ) // consider the case of vector-inputs if ( Symbol == '{' ) { - int i, k, Bit, Limit, nMsb, nLsb, fQuit; - // skip this char Ver_StreamPopChar(p); @@ -1673,7 +1706,8 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox ) pNetActual = Ver_ParseFindNet( pNtk, pWord ); if ( pNetActual == NULL ) { - if ( !strncmp(pWord, "Open_", 5) ) + if ( !strncmp(pWord, "Open_", 5) || + !strncmp(pWord, "dct_unconnected", 15) ) pNetActual = Abc_NtkCreateNet( pNtk ); else { @@ -1697,7 +1731,8 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox ) pNetActual = Ver_ParseFindNet( pNtk, Buffer ); if ( pNetActual == NULL ) { - if ( !strncmp(pWord, "Open_", 5) ) + if ( !strncmp(pWord, "Open_", 5) || + !strncmp(pWord, "dct_unconnected", 15) ) pNetActual = Abc_NtkCreateNet( pNtk ); else { @@ -1738,34 +1773,72 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox ) if ( pWord[0] == 0 ) { pNetActual = Abc_NtkCreateNet( pNtk ); + Vec_PtrPush( pBundle->vNetsActual, Abc_ObjNotCond( pNetActual, fCompl ) ); } else { -/* - // check if the name is complemented - fCompl = (pWord[0] == '~'); - if ( fCompl ) - { - pWord++; - if ( pNtk->pData == NULL ) - pNtk->pData = Extra_MmFlexStart(); - } -*/ // get the actual net + flag=0; pNetActual = Ver_ParseFindNet( pNtk, pWord ); - if ( pNetActual == NULL ) + if ( pNetActual == NULL ) { - if ( !strncmp(pWord, "Open_", 5) ) - pNetActual = Abc_NtkCreateNet( pNtk ); - else + Ver_ParseLookupSuffix( pMan, pWord, &nMsb, &nLsb ); + if ( nMsb == -1 && nLsb == -1 ) { - sprintf( pMan->sError, "Actual net \"%s\" is missing in box \"%s\".", pWord, Abc_ObjName(pNode) ); - Ver_ParsePrintErrorMessage( pMan ); - return 0; + Ver_ParseSignalSuffix( pMan, pWord, &nMsb, &nLsb ); + if ( nMsb == -1 && nLsb == -1 ) + { + if ( !strncmp(pWord, "Open_", 5) || + !strncmp(pWord, "dct_unconnected", 15) ) + { + pNetActual = Abc_NtkCreateNet( pNtk ); + Vec_PtrPush( pBundle->vNetsActual, pNetActual ); + } + else + { + sprintf( pMan->sError, "Actual net \"%s\" is missing in box \"%s\".", pWord, Abc_ObjName(pNode) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + } + else + { + flag=1; + } + } + else + { + flag=1; } + if (flag) + { + Limit = (nMsb > nLsb) ? nMsb - nLsb + 1: nLsb - nMsb + 1; + for ( Bit = nMsb, k = Limit - 1; k >= 0; Bit = (nMsb > nLsb ? Bit - 1: Bit + 1), k--) + { + // get the actual net + sprintf( Buffer, "%s[%d]", pWord, Bit ); + pNetActual = Ver_ParseFindNet( pNtk, Buffer ); + if ( pNetActual == NULL ) + { + if ( !strncmp(pWord, "Open_", 5) || + !strncmp(pWord, "dct_unconnected", 15)) + pNetActual = Abc_NtkCreateNet( pNtk ); + else + { + sprintf( pMan->sError, "Actual net \"%s\" is missing in box \"%s\".", pWord, Abc_ObjName(pNode) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + } + Vec_PtrPush( pBundle->vNetsActual, pNetActual ); + } + } + } + else + { + Vec_PtrPush( pBundle->vNetsActual, Abc_ObjNotCond( pNetActual, fCompl ) ); } } - Vec_PtrPush( pBundle->vNetsActual, Abc_ObjNotCond( pNetActual, fCompl ) ); } if ( fFormalIsGiven ) @@ -2000,8 +2073,8 @@ int Ver_ParseConnectBox( Ver_Man_t * pMan, Abc_Obj_t * pBox ) } if ( pBundle == NULL ) { - printf( "Warning: The formal output %s is not driven when instantiating network %s in box %s.", - pNameFormal, pNtkBox->pName, Abc_ObjName(pBox) ); +// printf( "Warning: The formal output %s is not driven when instantiating network %s in box %s.", +// pNameFormal, pNtkBox->pName, Abc_ObjName(pBox) ); continue; } } diff --git a/src/base/ver/verCore.zip b/src/base/ver/verCore.zip Binary files differindex 45574008..cdfcf5a4 100644 --- a/src/base/ver/verCore.zip +++ b/src/base/ver/verCore.zip diff --git a/src/map/if/ifUtil.c b/src/map/if/ifUtil.c index f4ffa4c1..f3fa049e 100644 --- a/src/map/if/ifUtil.c +++ b/src/map/if/ifUtil.c @@ -427,6 +427,26 @@ int If_ManCrossCut( If_Man_t * p ) return nCutSizeMax; } +/**Function************************************************************* + + Synopsis [Computes cross-cut of the circuit.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int If_ManCountTrueArea( If_Man_t * p ) +{ + If_Obj_t * pObj; + int i, Area = 0; + Vec_PtrForEachEntry( p->vMapped, pObj, i ) + Area += 1 + (If_ObjCutBest(pObj)->nLeaves > (unsigned)p->pPars->nLutSize / 2); + return Area; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |