From 1647addf5e3ce4f82cc35cd4983bc5f7b9730290 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 14 Jul 2007 08:01:00 -0700 Subject: Version abc70714 --- abc.dsp | 20 ++++ src/aig/aig/aig.h | 45 ++++++-- src/aig/aig/aigDfs.c | 59 ++++++++++ src/aig/aig/aigFanout.c | 189 +++++++++++++++++++++++++++++++ src/aig/aig/aigMan.c | 68 ++++++++--- src/aig/aig/aigMem.c | 3 +- src/aig/aig/aigObj.c | 130 ++++++++++++++++++--- src/aig/aig/aigSeq.c | 11 +- src/aig/aig/aigTable.c | 133 ++++++++-------------- src/aig/aig/aigTiming.c | 275 +++++++++++++++++++++++++++++++++++++++++++++ src/aig/aig/module.make | 2 + src/aig/dar/darBalance.c | 18 +-- src/aig/dar/darCore.c | 47 ++++---- src/aig/dar/darCut.c | 50 +++++++-- src/aig/dar/darInt.h | 16 +-- src/aig/dar/darLib.c | 268 +++++++++++++++++++++++++++++++++++-------- src/aig/dar/darMan.c | 21 +++- src/aig/dar/darRefact.c | 48 ++++++++ src/aig/dar/darResub.c | 48 ++++++++ src/aig/dar/darScript.c | 48 ++++++++ src/aig/dar/dar_.c | 2 +- src/aig/dar/module.make | 3 + src/aig/fra/fraCore.c | 2 +- src/base/abci/abc.c | 2 +- src/base/abci/abcDar.c | 12 +- src/base/abci/abcRewrite.c | 4 + src/base/abci/abcTiming.c | 4 +- 27 files changed, 1294 insertions(+), 234 deletions(-) create mode 100644 src/aig/aig/aigFanout.c create mode 100644 src/aig/aig/aigTiming.c create mode 100644 src/aig/dar/darRefact.c create mode 100644 src/aig/dar/darResub.c create mode 100644 src/aig/dar/darScript.c diff --git a/abc.dsp b/abc.dsp index 095c8ebd..7bb16175 100644 --- a/abc.dsp +++ b/abc.dsp @@ -2534,6 +2534,18 @@ SOURCE=.\src\aig\dar\darMan.c # End Source File # Begin Source File +SOURCE=.\src\aig\dar\darRefact.c +# End Source File +# Begin Source File + +SOURCE=.\src\aig\dar\darResub.c +# End Source File +# Begin Source File + +SOURCE=.\src\aig\dar\darScript.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\dar\darTruth.c # End Source File # End Group @@ -2722,6 +2734,10 @@ SOURCE=.\src\aig\aig\aigDfs.c # End Source File # Begin Source File +SOURCE=.\src\aig\aig\aigFanout.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\aig\aigMan.c # End Source File # Begin Source File @@ -2746,6 +2762,10 @@ SOURCE=.\src\aig\aig\aigTable.c # End Source File # Begin Source File +SOURCE=.\src\aig\aig\aigTiming.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\aig\aigUtil.c # End Source File # End Group diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h index 4d9f9819..6725f4a6 100644 --- a/src/aig/aig/aig.h +++ b/src/aig/aig/aig.h @@ -89,6 +89,7 @@ struct Aig_Man_t_ Vec_Ptr_t * vPis; // the array of PIs Vec_Ptr_t * vPos; // the array of POs Vec_Ptr_t * vObjs; // the array of all nodes (optional) + Vec_Ptr_t * vBufs; // the array of buffers Aig_Obj_t * pConst1; // the constant 1 node Aig_Obj_t Ghost; // the ghost node // AIG node counters @@ -98,9 +99,16 @@ struct Aig_Man_t_ // structural hash table Aig_Obj_t ** pTable; // structural hash table int nTableSize; // structural hash table size + // representation of fanouts + int * pFanData; // the database to store fanout information + int nFansAlloc; // the size of fanout representation + Vec_Vec_t * vLevels; // used to update timing information + int nBufReplaces; // the number of times replacement led to a buffer + int nBufFixes; // the number of times buffers were propagated + int nBufMax; // the maximum number of buffers during computation // various data members Aig_MmFixed_t * pMemObjs; // memory manager for objects - Vec_Int_t * vRequired; // the required times + Vec_Int_t * vLevelR; // the reverse level of the nodes int nLevelMax; // maximum number of levels void * pData; // the temporary data int nTravIds; // the current traversal ID @@ -190,9 +198,10 @@ static inline Aig_Obj_t * Aig_ObjChild1( Aig_Obj_t * pObj ) { return pObj- static inline Aig_Obj_t * Aig_ObjChild0Copy( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj)) : NULL; } static inline Aig_Obj_t * Aig_ObjChild1Copy( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj)) : NULL; } static inline int Aig_ObjLevel( Aig_Obj_t * pObj ) { return pObj->nRefs; } -static inline int Aig_ObjLevelNew( Aig_Obj_t * pObj ) { return 1 + Aig_ObjIsExor(pObj) + AIG_MAX(Aig_ObjFanin0(pObj)->Level, Aig_ObjFanin1(pObj)->Level); } -static inline int Aig_ObjFaninPhase( Aig_Obj_t * pObj ) { return Aig_Regular(pObj)->fPhase ^ Aig_IsComplement(pObj); } -static inline void Aig_ObjClean( Aig_Obj_t * pObj ) { memset( pObj, 0, sizeof(Aig_Obj_t) ); } +static inline int Aig_ObjLevelNew( Aig_Obj_t * pObj ) { return Aig_ObjFanin1(pObj)? 1 + Aig_ObjIsExor(pObj) + AIG_MAX(Aig_ObjFanin0(pObj)->Level, Aig_ObjFanin1(pObj)->Level) : Aig_ObjFanin0(pObj)->Level; } +static inline int Aig_ObjFaninPhase( Aig_Obj_t * pObj ) { return pObj? Aig_Regular(pObj)->fPhase ^ Aig_IsComplement(pObj) : 0; } +static inline void Aig_ObjClean( Aig_Obj_t * pObj ) { memset( pObj, 0, sizeof(Aig_Obj_t) ); } +static inline Aig_Obj_t * Aig_ObjFanout0( Aig_Man_t * p, Aig_Obj_t * pObj ) { assert(p->pFanData && pObj->Id < p->nFansAlloc); return Aig_ManObj(p, p->pFanData[5*pObj->Id] >> 1); } static inline int Aig_ObjWhatFanin( Aig_Obj_t * pObj, Aig_Obj_t * pFanin ) { if ( Aig_ObjFanin0(pObj) == pFanin ) return 0; @@ -263,9 +272,18 @@ static inline void Aig_ManRecycleMemory( Aig_Man_t * p, Aig_Obj_t * pEntry ) #define Aig_ManForEachObj( p, pObj, i ) \ Vec_PtrForEachEntry( p->vObjs, pObj, i ) if ( (pObj) == NULL ) {} else // iterator over all nodes -#define Aig_ManForEachNode( p, pObj, i ) \ +#define Aig_ManForEachNode( p, pObj, i ) \ Vec_PtrForEachEntry( p->vObjs, pObj, i ) if ( (pObj) == NULL || !Aig_ObjIsNode(pObj) ) {} else +// these two procedures are only here for the use inside the iterator +static inline int Aig_ObjFanout0Int( Aig_Man_t * p, int ObjId ) { assert(ObjId < p->nFansAlloc); return p->pFanData[5*ObjId]; } +static inline int Aig_ObjFanoutNext( Aig_Man_t * p, int iFan ) { assert(iFan/2 < p->nFansAlloc); return p->pFanData[5*(iFan >> 1) + 3 + (iFan & 1)]; } +// iterator over the fanouts +#define Aig_ObjForEachFanout( p, pObj, pFanout, iFan, i ) \ + for ( assert(p->pFanData), i = 0; (i < (int)(pObj)->nRefs) && \ + (((iFan) = i? Aig_ObjFanoutNext(p, iFan) : Aig_ObjFanout0Int(p, pObj->Id)), 1) && \ + (((pFanout) = Aig_ManObj(p, iFan>>1)), 1); i++ ) + //////////////////////////////////////////////////////////////////////// /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -275,16 +293,21 @@ extern int Aig_ManCheck( Aig_Man_t * p ); /*=== aigDfs.c ==========================================================*/ extern Vec_Ptr_t * Aig_ManDfs( Aig_Man_t * p ); extern Vec_Ptr_t * Aig_ManDfsNodes( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes ); +extern Vec_Ptr_t * Aig_ManDfsReverse( Aig_Man_t * p ); extern int Aig_ManCountLevels( Aig_Man_t * p ); -extern void Aig_ManCreateRefs( Aig_Man_t * p ); extern int Aig_DagSize( Aig_Obj_t * pObj ); extern void Aig_ConeUnmark_rec( Aig_Obj_t * pObj ); extern Aig_Obj_t * Aig_Transfer( Aig_Man_t * pSour, Aig_Man_t * pDest, Aig_Obj_t * pObj, int nVars ); extern Aig_Obj_t * Aig_Compose( Aig_Man_t * p, Aig_Obj_t * pRoot, Aig_Obj_t * pFunc, int iVar ); +/*=== aigFanout.c ==========================================================*/ +extern void Aig_ObjAddFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout ); +extern void Aig_ObjRemoveFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout ); +extern void Aig_ManCreateFanout( Aig_Man_t * p ); +extern void Aig_ManDeleteFanout( Aig_Man_t * p ); /*=== aigMan.c ==========================================================*/ extern Aig_Man_t * Aig_ManStart(); extern Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p ); -extern Aig_Man_t * Aig_ManDup( Aig_Man_t * p ); +extern Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered ); extern void Aig_ManStop( Aig_Man_t * p ); extern int Aig_ManCleanup( Aig_Man_t * p ); extern void Aig_ManPrintStats( Aig_Man_t * p ); @@ -300,7 +323,7 @@ extern void Aig_ObjDisconnect( Aig_Man_t * p, Aig_Obj_t * pObj ); extern void Aig_ObjDelete( Aig_Man_t * p, Aig_Obj_t * pObj ); extern void Aig_ObjDelete_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int fFreeTop ); extern void Aig_ObjPatchFanin0( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFaninNew ); -extern void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, int fNodesOnly ); +extern void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, int fNodesOnly, int fUpdateLevel ); /*=== aigOper.c =========================================================*/ extern Aig_Obj_t * Aig_IthVar( Aig_Man_t * p, int i ); extern Aig_Obj_t * Aig_Oper( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1, Aig_Type_t Type ); @@ -322,6 +345,12 @@ extern void Aig_TableInsert( Aig_Man_t * p, Aig_Obj_t * pObj ); extern void Aig_TableDelete( Aig_Man_t * p, Aig_Obj_t * pObj ); extern int Aig_TableCountEntries( Aig_Man_t * p ); extern void Aig_TableProfile( Aig_Man_t * p ); +/*=== aigTiming.c ========================================================*/ +extern int Aig_ObjRequiredLevel( Aig_Man_t * p, Aig_Obj_t * pObj ); +extern void Aig_ManStartReverseLevels( Aig_Man_t * p, int nMaxLevelIncrease ); +extern void Aig_ManStopReverseLevels( Aig_Man_t * p ); +extern void Aig_ManUpdateLevel( Aig_Man_t * p, Aig_Obj_t * pObjNew ); +extern void Aig_ManUpdateReverseLevel( Aig_Man_t * p, Aig_Obj_t * pObjNew ); /*=== aigUtil.c =========================================================*/ extern unsigned Aig_PrimeCudd( unsigned p ); extern void Aig_ManIncrementTravId( Aig_Man_t * p ); diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c index 0f2d9401..a71afec6 100644 --- a/src/aig/aig/aigDfs.c +++ b/src/aig/aig/aigDfs.c @@ -117,6 +117,65 @@ Vec_Ptr_t * Aig_ManDfsNodes( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes ) return vNodes; } +/**Function************************************************************* + + Synopsis [Collects internal nodes in the reverse DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManDfsReverse_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes ) +{ + Aig_Obj_t * pFanout; + int iFanout, i; + assert( !Aig_IsComplement(pObj) ); + if ( Aig_ObjIsTravIdCurrent(p, pObj) ) + return; + assert( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) ); + Aig_ObjForEachFanout( p, pObj, pFanout, iFanout, i ) + Aig_ManDfsReverse_rec( p, pFanout, vNodes ); + assert( !Aig_ObjIsTravIdCurrent(p, pObj) ); // loop detection + Aig_ObjSetTravIdCurrent(p, pObj); + Vec_PtrPush( vNodes, pObj ); +} + +/**Function************************************************************* + + Synopsis [Collects internal nodes in the reverse DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Aig_ManDfsReverse( Aig_Man_t * p ) +{ + Vec_Ptr_t * vNodes; + Aig_Obj_t * pObj; + int i; + Aig_ManIncrementTravId( p ); + // mark POs + Aig_ManForEachPo( p, pObj, i ) + Aig_ObjSetTravIdCurrent( p, pObj ); + // if there are latches, mark them + if ( Aig_ManLatchNum(p) > 0 ) + Aig_ManForEachObj( p, pObj, i ) + if ( Aig_ObjIsLatch(pObj) ) + Aig_ObjSetTravIdCurrent( p, pObj ); + // go through the nodes + vNodes = Vec_PtrAlloc( Aig_ManNodeNum(p) ); + Aig_ManForEachObj( p, pObj, i ) + if ( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) ) + Aig_ManDfsReverse_rec( p, pObj, vNodes ); + return vNodes; +} + /**Function************************************************************* Synopsis [Computes the max number of levels in the manager.] diff --git a/src/aig/aig/aigFanout.c b/src/aig/aig/aigFanout.c new file mode 100644 index 00000000..e7d5f216 --- /dev/null +++ b/src/aig/aig/aigFanout.c @@ -0,0 +1,189 @@ +/**CFile**************************************************************** + + FileName [aigFanout.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [AIG package.] + + Synopsis [Fanout manipulation.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 28, 2007.] + + Revision [$Id: aigFanout.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "aig.h" + +// 0: first iFan +// 1: prev iFan0 +// 2: prev iFan1 +// 3: next iFan0 +// 4: next iFan1 + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline int Aig_FanoutCreate( int FanId, int Num ) { assert( Num < 2 ); return (FanId << 1) | Num; } +static inline int * Aig_FanoutObj( int * pData, int ObjId ) { return pData + 5*ObjId; } +static inline int * Aig_FanoutPrev( int * pData, int iFan ) { return pData + 5*(iFan >> 1) + 1 + (iFan & 1); } +static inline int * Aig_FanoutNext( int * pData, int iFan ) { return pData + 5*(iFan >> 1) + 3 + (iFan & 1); } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + + +/**Function************************************************************* + + Synopsis [Adds fanout (pFanout) of node (pObj).] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ObjAddFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout ) +{ + int iFan, * pFirst, * pPrevC, * pNextC, * pPrev, * pNext; + assert( p->pFanData ); + assert( !Aig_IsComplement(pObj) && !Aig_IsComplement(pFanout) ); + assert( pFanout->Id > 0 ); + if ( pObj->Id >= p->nFansAlloc || pFanout->Id >= p->nFansAlloc ) + { + int nFansAlloc = 2 * AIG_MAX( pObj->Id, pFanout->Id ); + p->pFanData = REALLOC( int, p->pFanData, 5 * nFansAlloc ); + memset( p->pFanData + 5 * p->nFansAlloc, 0, sizeof(int) * 5 * (nFansAlloc - p->nFansAlloc) ); + p->nFansAlloc = nFansAlloc; + } + assert( pObj->Id < p->nFansAlloc && pFanout->Id < p->nFansAlloc ); + iFan = Aig_FanoutCreate( pFanout->Id, Aig_ObjWhatFanin(pFanout, pObj) ); + pPrevC = Aig_FanoutPrev( p->pFanData, iFan ); + pNextC = Aig_FanoutNext( p->pFanData, iFan ); + pFirst = Aig_FanoutObj( p->pFanData, pObj->Id ); + if ( *pFirst == 0 ) + { + *pFirst = iFan; + *pPrevC = iFan; + *pNextC = iFan; + } + else + { + pPrev = Aig_FanoutPrev( p->pFanData, *pFirst ); + pNext = Aig_FanoutNext( p->pFanData, *pPrev ); + assert( *pNext == *pFirst ); + *pPrevC = *pPrev; + *pNextC = *pFirst; + *pPrev = iFan; + *pNext = iFan; + } +} + +/**Function************************************************************* + + Synopsis [Removes fanout (pFanout) of node (pObj).] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ObjRemoveFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout ) +{ + int iFan, * pFirst, * pPrevC, * pNextC, * pPrev, * pNext; + assert( p->pFanData && pObj->Id < p->nFansAlloc && pFanout->Id < p->nFansAlloc ); + assert( !Aig_IsComplement(pObj) && !Aig_IsComplement(pFanout) ); + assert( pFanout->Id > 0 ); + iFan = Aig_FanoutCreate( pFanout->Id, Aig_ObjWhatFanin(pFanout, pObj) ); + pPrevC = Aig_FanoutPrev( p->pFanData, iFan ); + pNextC = Aig_FanoutNext( p->pFanData, iFan ); + pPrev = Aig_FanoutPrev( p->pFanData, *pNextC ); + pNext = Aig_FanoutNext( p->pFanData, *pPrevC ); + assert( *pPrev == iFan ); + assert( *pNext == iFan ); + pFirst = Aig_FanoutObj( p->pFanData, pObj->Id ); + assert( *pFirst > 0 ); + if ( *pFirst == iFan ) + { + if ( *pNextC == iFan ) + { + *pFirst = 0; + *pPrev = 0; + *pNext = 0; + *pPrevC = 0; + *pNextC = 0; + return; + } + *pFirst = *pNextC; + } + *pPrev = *pPrevC; + *pNext = *pNextC; + *pPrevC = 0; + *pNextC = 0; +} + +/**Function************************************************************* + + Synopsis [Create fanout for all objects in the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManCreateFanout( Aig_Man_t * p ) +{ + Aig_Obj_t * pObj; + int i; + // allocate fanout datastructure + assert( p->pFanData == NULL ); + p->nFansAlloc = 2 * Aig_ManObjIdMax(p); + if ( p->nFansAlloc < (1<<12) ) + p->nFansAlloc = (1<<12); + p->pFanData = ALLOC( int, 5 * p->nFansAlloc ); + memset( p->pFanData, 0, sizeof(int) * 5 * p->nFansAlloc ); + // add fanouts for all objects + Aig_ManForEachObj( p, pObj, i ) + { + if ( Aig_ObjChild0(pObj) ) + Aig_ObjAddFanout( p, Aig_ObjFanin0(pObj), pObj ); + if ( Aig_ObjChild1(pObj) ) + Aig_ObjAddFanout( p, Aig_ObjFanin1(pObj), pObj ); + } +} + +/**Function************************************************************* + + Synopsis [Deletes fanout for all objects in the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManDeleteFanout( Aig_Man_t * p ) +{ + assert( p->pFanData != NULL ); + FREE( p->pFanData ); + p->nFansAlloc = 0; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c index 1b0ea548..562260d3 100644 --- a/src/aig/aig/aigMan.c +++ b/src/aig/aig/aigMan.c @@ -55,6 +55,7 @@ Aig_Man_t * Aig_ManStart( int nNodesMax ) p->vPis = Vec_PtrAlloc( 100 ); p->vPos = Vec_PtrAlloc( 100 ); p->vObjs = Vec_PtrAlloc( 1000 ); + p->vBufs = Vec_PtrAlloc( 100 ); // prepare the internal memory manager p->pMemObjs = Aig_MmFixedStart( sizeof(Aig_Obj_t), nNodesMax ); // create the constant node @@ -94,6 +95,28 @@ Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p ) return pNew; } +/**Function************************************************************* + + Synopsis [Duplicates the AIG manager recursively.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t * Aig_ManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj ) +{ + if ( pObj->pData ) + return pObj->pData; + Aig_ManDup_rec( pNew, p, Aig_ObjFanin0(pObj) ); + if ( Aig_ObjIsBuf(pObj) ) + return pObj->pData = Aig_ObjChild0Copy(pObj); + Aig_ManDup_rec( pNew, p, Aig_ObjFanin1(pObj) ); + return pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); +} + /**Function************************************************************* Synopsis [Duplicates the AIG manager.] @@ -105,7 +128,7 @@ Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Aig_ManDup( Aig_Man_t * p ) +Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered ) { Aig_Man_t * pNew; Aig_Obj_t * pObj; @@ -113,15 +136,25 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p ) // create the new manager pNew = Aig_ManStart( Aig_ManObjIdMax(p) + 1 ); // create the PIs + Aig_ManCleanData( p ); Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); Aig_ManForEachPi( p, pObj, i ) pObj->pData = Aig_ObjCreatePi(pNew); // duplicate internal nodes - Aig_ManForEachObj( p, pObj, i ) - if ( Aig_ObjIsBuf(pObj) ) - pObj->pData = Aig_ObjChild0Copy(pObj); - else if ( Aig_ObjIsNode(pObj) ) - pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + if ( fOrdered ) + { + Aig_ManForEachObj( p, pObj, i ) + if ( Aig_ObjIsBuf(pObj) ) + pObj->pData = Aig_ObjChild0Copy(pObj); + else if ( Aig_ObjIsNode(pObj) ) + pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + } + else + { + Aig_ManForEachObj( p, pObj, i ) + if ( !Aig_ObjIsPo(pObj) ) + Aig_ManDup_rec( pNew, p, pObj ); + } // add the POs Aig_ManForEachPo( p, pObj, i ) Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); @@ -149,15 +182,20 @@ void Aig_ManStop( Aig_Man_t * p ) // print time if ( p->time1 ) { PRT( "time1", p->time1 ); } if ( p->time2 ) { PRT( "time2", p->time2 ); } + // delete fanout + if ( p->pFanData ) + Aig_ManDeleteFanout( p ); // make sure the nodes have clean marks Aig_ManForEachObj( p, pObj, i ) assert( !pObj->fMarkA && !pObj->fMarkB ); // Aig_TableProfile( p ); Aig_MmFixedStop( p->pMemObjs, 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->vBufs ) Vec_PtrFree( p->vBufs ); + if ( p->vLevelR ) Vec_IntFree( p->vLevelR ); + if ( p->vLevels ) Vec_VecFree( p->vLevels ); free( p->pTable ); free( p ); } @@ -205,14 +243,16 @@ int Aig_ManCleanup( Aig_Man_t * p ) void Aig_ManPrintStats( Aig_Man_t * p ) { printf( "PI/PO/Lat = %5d/%5d/%5d ", Aig_ManPiNum(p), Aig_ManPoNum(p), Aig_ManLatchNum(p) ); - printf( "A = %6d. ", Aig_ManAndNum(p) ); + printf( "A = %7d. ", Aig_ManAndNum(p) ); if ( Aig_ManExorNum(p) ) printf( "X = %5d. ", Aig_ManExorNum(p) ); // if ( Aig_ManBufNum(p) ) - printf( "B = %3d. ", Aig_ManBufNum(p) ); - printf( "Cre = %6d. ", p->nCreated ); - printf( "Del = %6d. ", p->nDeleted ); + printf( "B = %5d. ", Aig_ManBufNum(p) ); +// printf( "Cre = %6d. ", p->nCreated ); +// printf( "Del = %6d. ", p->nDeleted ); // printf( "Lev = %3d. ", Aig_ManCountLevels(p) ); + printf( "Max = %7d. ", Aig_ManObjIdMax(p) ); + printf( "Lev = %3d. ", Aig_ManLevels(p) ); printf( "\n" ); } diff --git a/src/aig/aig/aigMem.c b/src/aig/aig/aigMem.c index 20663e6f..dab90777 100644 --- a/src/aig/aig/aigMem.c +++ b/src/aig/aig/aigMem.c @@ -232,7 +232,8 @@ void Aig_MmFixedRestart( Aig_MmFixed_t * p ) { int i; char * pTemp; - + if ( p->nChunks == 0 ) + return; // deallocate all chunks except the first one for ( i = 1; i < p->nChunks; i++ ) free( p->pChunks[i] ); diff --git a/src/aig/aig/aigObj.c b/src/aig/aig/aigObj.c index a261ab40..542b90f9 100644 --- a/src/aig/aig/aigObj.c +++ b/src/aig/aig/aigObj.c @@ -66,9 +66,7 @@ Aig_Obj_t * Aig_ObjCreatePo( Aig_Man_t * p, Aig_Obj_t * pDriver ) pObj = Aig_ManFetchMemory( p ); pObj->Type = AIG_OBJ_PO; Vec_PtrPush( p->vPos, pObj ); - // add connections Aig_ObjConnect( p, pObj, pDriver, NULL ); - // update node counters of the manager p->nObjs[AIG_OBJ_PO]++; return pObj; } @@ -125,23 +123,19 @@ void Aig_ObjConnect( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFan0, Aig_Obj { assert( Aig_ObjFanin0(pObj)->Type > 0 ); Aig_ObjRef( Aig_ObjFanin0(pObj) ); + if ( p->pFanData ) + Aig_ObjAddFanout( p, Aig_ObjFanin0(pObj), pObj ); } if ( pFan1 != NULL ) { assert( Aig_ObjFanin1(pObj)->Type > 0 ); Aig_ObjRef( Aig_ObjFanin1(pObj) ); + if ( p->pFanData ) + Aig_ObjAddFanout( p, Aig_ObjFanin1(pObj), pObj ); } // set level and phase - if ( pFan1 != NULL ) - { - pObj->Level = Aig_ObjLevelNew( pObj ); - pObj->fPhase = Aig_ObjFaninPhase(pFan0) & Aig_ObjFaninPhase(pFan1); - } - else - { - pObj->Level = pFan0->Level; - pObj->fPhase = Aig_ObjFaninPhase(pFan0); - } + pObj->Level = Aig_ObjLevelNew( pObj ); + pObj->fPhase = Aig_ObjFaninPhase(pFan0) & Aig_ObjFaninPhase(pFan1); // add the node to the structural hash table if ( Aig_ObjIsHash(pObj) ) Aig_TableInsert( p, pObj ); @@ -163,9 +157,17 @@ void Aig_ObjDisconnect( Aig_Man_t * p, Aig_Obj_t * pObj ) assert( !Aig_IsComplement(pObj) ); // remove connections if ( pObj->pFanin0 != NULL ) + { + if ( p->pFanData ) + Aig_ObjRemoveFanout( p, Aig_ObjFanin0(pObj), pObj ); Aig_ObjDeref(Aig_ObjFanin0(pObj)); + } if ( pObj->pFanin1 != NULL ) + { + if ( p->pFanData ) + Aig_ObjRemoveFanout( p, Aig_ObjFanin1(pObj), pObj ); Aig_ObjDeref(Aig_ObjFanin1(pObj)); + } // remove the node from the structural hash table if ( Aig_ObjIsHash(pObj) ) Aig_TableDelete( p, pObj ); @@ -190,6 +192,8 @@ void Aig_ObjDelete( Aig_Man_t * p, Aig_Obj_t * pObj ) assert( !Aig_IsComplement(pObj) ); assert( !Aig_ObjIsTerm(pObj) ); assert( Aig_ObjRefs(pObj) == 0 ); + if ( p->pFanData && Aig_ObjIsBuf(pObj) ) + Vec_PtrRemove( p->vBufs, pObj ); p->nObjs[pObj->Type]--; Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL ); Aig_ManRecycleMemory( p, pObj ); @@ -241,30 +245,105 @@ void Aig_ObjPatchFanin0( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFaninNew assert( !Aig_IsComplement(pObj) ); pFaninOld = Aig_ObjFanin0(pObj); // decrement ref and remove fanout + if ( p->pFanData ) + Aig_ObjRemoveFanout( p, pFaninOld, pObj ); Aig_ObjDeref( pFaninOld ); // update the fanin pObj->pFanin0 = pFaninNew; // increment ref and add fanout - Aig_ObjRef( Aig_Regular(pFaninNew) ); + if ( p->pFanData ) + Aig_ObjAddFanout( p, Aig_ObjFanin0(pObj), pObj ); + Aig_ObjRef( Aig_ObjFanin0(pObj) ); // get rid of old fanin if ( !Aig_ObjIsPi(pFaninOld) && !Aig_ObjIsConst1(pFaninOld) && Aig_ObjRefs(pFaninOld) == 0 ) Aig_ObjDelete_rec( p, pFaninOld, 1 ); } +/**Function************************************************************* + + Synopsis [Replaces node with a buffer fanin by a node without them.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_NodeFixBufferFanins( Aig_Man_t * p, Aig_Obj_t * pObj, int fNodesOnly, int fUpdateLevel ) +{ + Aig_Obj_t * pFanReal0, * pFanReal1, * pResult; + p->nBufFixes++; + if ( Aig_ObjIsPo(pObj) ) + { + assert( Aig_ObjIsBuf(Aig_ObjFanin0(pObj)) ); + pFanReal0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) ); + Aig_ObjPatchFanin0( p, pObj, pFanReal0 ); + return; + } + assert( Aig_ObjIsNode(pObj) ); + assert( Aig_ObjIsBuf(Aig_ObjFanin0(pObj)) || Aig_ObjIsBuf(Aig_ObjFanin1(pObj)) ); + // get the real fanins + pFanReal0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) ); + pFanReal1 = Aig_ObjReal_rec( Aig_ObjChild1(pObj) ); + // get the new node + if ( Aig_ObjIsNode(pObj) ) + pResult = Aig_Oper( p, pFanReal0, pFanReal1, Aig_ObjType(pObj) ); +// else if ( Aig_ObjIsLatch(pObj) ) +// pResult = Aig_Latch( p, pFanReal0, Aig_ObjInit(pObj) ); + else + assert( 0 ); + // replace the node with buffer by the node without buffer + Aig_ObjReplace( p, pObj, pResult, fNodesOnly, fUpdateLevel ); +} + +/**Function************************************************************* + + Synopsis [Returns the number of dangling nodes removed.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ManPropagateBuffers( Aig_Man_t * p, int fNodesOnly, int fUpdateLevel ) +{ + Aig_Obj_t * pObj; + int nSteps; + assert( p->pFanData ); + for ( nSteps = 0; Vec_PtrSize(p->vBufs) > 0; nSteps++ ) + { + // get the node with a buffer fanin + for ( pObj = Vec_PtrEntryLast(p->vBufs); Aig_ObjIsBuf(pObj); pObj = Aig_ObjFanout0(p, pObj) ); + // replace this node by a node without buffer + Aig_NodeFixBufferFanins( p, pObj, fNodesOnly, fUpdateLevel ); + // stop if a cycle occured + if ( nSteps > 1000000 ) + { + printf( "Error: A cycle is encountered while propagating buffers.\n" ); + break; + } + } + return nSteps; +} + /**Function************************************************************* Synopsis [Replaces one object by another.] - Description [Both objects are currently in the manager. The new object - (pObjNew) should be used instead of the old object (pObjOld). If the - new object is complemented or used, the buffer is added.] + Description [The new object (pObjNew) should be used instead of the old + object (pObjOld). If the new object is complemented or used, the buffer + is added and the new object remains in the manager; otherwise, the new + object is deleted.] SideEffects [] SeeAlso [] ***********************************************************************/ -void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, int fNodesOnly ) +void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, int fNodesOnly, int fUpdateLevel ) { Aig_Obj_t * pObjNewR = Aig_Regular(pObjNew); // the object to be replaced cannot be complemented @@ -288,17 +367,34 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in { pObjOld->Type = AIG_OBJ_BUF; Aig_ObjConnect( p, pObjOld, pObjNew, NULL ); + p->nBufReplaces++; } else { Aig_Obj_t * pFanin0 = pObjNew->pFanin0; Aig_Obj_t * pFanin1 = pObjNew->pFanin1; + int LevelOld = pObjOld->Level; pObjOld->Type = pObjNew->Type; Aig_ObjDisconnect( p, pObjNew ); Aig_ObjConnect( p, pObjOld, pFanin0, pFanin1 ); + // delete the new object Aig_ObjDelete( p, pObjNew ); + // update levels + if ( fUpdateLevel ) + { + pObjOld->Level = LevelOld; + Aig_ManUpdateLevel( p, pObjOld ); + Aig_ManUpdateReverseLevel( p, pObjOld ); + } } p->nObjs[pObjOld->Type]++; + // store buffers if fanout is allocated + if ( p->pFanData && Aig_ObjIsBuf(pObjOld) ) + { + Vec_PtrPush( p->vBufs, pObjOld ); + p->nBufMax = AIG_MAX( p->nBufMax, Vec_PtrSize(p->vBufs) ); + Aig_ManPropagateBuffers( p, fNodesOnly, fUpdateLevel ); + } } //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/aig/aigSeq.c b/src/aig/aig/aigSeq.c index 98b7d195..19466996 100644 --- a/src/aig/aig/aigSeq.c +++ b/src/aig/aig/aigSeq.c @@ -43,6 +43,7 @@ void Aig_ManSeqStrashConvert( Aig_Man_t * p, int nLatches, int * pInits ) { Aig_Obj_t * pObjLi, * pObjLo, * pLatch; int i; + assert( Vec_PtrSize( p->vBufs ) == 0 ); // collect the POs to be converted into latches for ( i = 0; i < nLatches; i++ ) { @@ -58,6 +59,8 @@ void Aig_ManSeqStrashConvert( Aig_Man_t * p, int nLatches, int * pInits ) // convert the corresponding PI to be a buffer and connect it to the latch pObjLo->Type = AIG_OBJ_BUF; Aig_ObjConnect( p, pObjLo, pLatch, NULL ); + // save the buffer +// Vec_PtrPush( p->vBufs, pObjLo ); } // shrink the arrays Vec_PtrShrink( p->vPis, Aig_ManPiNum(p) - nLatches ); @@ -353,7 +356,7 @@ int Aig_ManSeqRehashOne( Aig_Man_t * p, Vec_Ptr_t * vNodes, Vec_Ptr_t * vUnreach continue; pObjNew = Aig_ObjReal_rec( Aig_ObjChild0(pObj) ); pObjNew = Aig_Latch( p, pObjNew, 0 ); - Aig_ObjReplace( p, pObj, pObjNew, 1 ); + Aig_ObjReplace( p, pObj, pObjNew, 1, 0 ); RetValue = 1; Counter++; continue; @@ -365,7 +368,7 @@ int Aig_ManSeqRehashOne( Aig_Man_t * p, Vec_Ptr_t * vNodes, Vec_Ptr_t * vUnreach pFanin0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) ); pFanin1 = Aig_ObjReal_rec( Aig_ObjChild1(pObj) ); pObjNew = Aig_And( p, pFanin0, pFanin1 ); - Aig_ObjReplace( p, pObj, pObjNew, 1 ); + Aig_ObjReplace( p, pObj, pObjNew, 1, 0 ); RetValue = 1; Counter++; continue; @@ -407,7 +410,7 @@ void Aig_ManRemoveBuffers( Aig_Man_t * p ) continue; pFanin0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) ); pObjNew = Aig_Latch( p, pFanin0, 0 ); - Aig_ObjReplace( p, pObj, pObjNew, 0 ); + Aig_ObjReplace( p, pObj, pObjNew, 0, 0 ); } else if ( Aig_ObjIsAnd(pObj) ) { @@ -416,7 +419,7 @@ void Aig_ManRemoveBuffers( Aig_Man_t * p ) pFanin0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) ); pFanin1 = Aig_ObjReal_rec( Aig_ObjChild1(pObj) ); pObjNew = Aig_And( p, pFanin0, pFanin1 ); - Aig_ObjReplace( p, pObj, pObjNew, 0 ); + Aig_ObjReplace( p, pObj, pObjNew, 0, 0 ); } } assert( Aig_ManBufNum(p) == 0 ); diff --git a/src/aig/aig/aigTable.c b/src/aig/aig/aigTable.c index e8cfb480..bba7650a 100644 --- a/src/aig/aig/aigTable.c +++ b/src/aig/aig/aigTable.c @@ -28,8 +28,8 @@ static unsigned long Aig_Hash( Aig_Obj_t * pObj, int TableSize ) { unsigned long Key = Aig_ObjIsExor(pObj) * 1699; - Key ^= (long)Aig_ObjFanin0(pObj) * 7937; - Key ^= (long)Aig_ObjFanin1(pObj) * 2971; + Key ^= Aig_ObjFanin0(pObj)->Id * 7937; + Key ^= Aig_ObjFanin1(pObj)->Id * 2971; Key ^= Aig_ObjFaninC0(pObj) * 911; Key ^= Aig_ObjFaninC1(pObj) * 353; return Key % TableSize; @@ -55,13 +55,56 @@ static Aig_Obj_t ** Aig_TableFind( Aig_Man_t * p, Aig_Obj_t * pObj ) return ppEntry; } -static void Aig_TableResize( Aig_Man_t * p ); -static unsigned int Cudd_PrimeAig( unsigned int p ); - //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [Resizes the table.] + + Description [Typically this procedure should not be called.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_TableResize( Aig_Man_t * p ) +{ + Aig_Obj_t * pEntry, * pNext; + Aig_Obj_t ** pTableOld, ** ppPlace; + int nTableSizeOld, Counter, nEntries, i, clk; +clk = clock(); + // save the old table + pTableOld = p->pTable; + nTableSizeOld = p->nTableSize; + // get the new table + p->nTableSize = Aig_PrimeCudd( 2 * Aig_ManNodeNum(p) ); + p->pTable = ALLOC( Aig_Obj_t *, p->nTableSize ); + memset( p->pTable, 0, sizeof(Aig_Obj_t *) * p->nTableSize ); + // rehash the entries from the old table + Counter = 0; + for ( i = 0; i < nTableSizeOld; i++ ) + for ( pEntry = pTableOld[i], pNext = pEntry? pEntry->pNext : NULL; + pEntry; pEntry = pNext, pNext = pEntry? pEntry->pNext : NULL ) + { + // get the place where this entry goes in the table + ppPlace = Aig_TableFind( p, pEntry ); + assert( *ppPlace == NULL ); // should not be there + // add the entry to the list + *ppPlace = pEntry; + pEntry->pNext = NULL; + Counter++; + } + nEntries = Aig_ManNodeNum(p); + assert( Counter == nEntries ); + printf( "Increasing the structural table size from %6d to %6d. ", nTableSizeOld, p->nTableSize ); + PRT( "Time", clock() - clk ); + // replace the table and the parameters + free( pTableOld ); +} + /**Function************************************************************* Synopsis [Checks if node with the given attributes is in the hash table.] @@ -167,51 +210,6 @@ int Aig_TableCountEntries( Aig_Man_t * p ) return Counter; } -/**Function************************************************************* - - Synopsis [Resizes the table.] - - Description [Typically this procedure should not be called.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Aig_TableResize( Aig_Man_t * p ) -{ - Aig_Obj_t * pEntry, * pNext; - Aig_Obj_t ** pTableOld, ** ppPlace; - int nTableSizeOld, Counter, nEntries, i, clk; -clk = clock(); - // save the old table - pTableOld = p->pTable; - nTableSizeOld = p->nTableSize; - // get the new table - p->nTableSize = Cudd_PrimeAig( 2 * Aig_ManNodeNum(p) ); - p->pTable = ALLOC( Aig_Obj_t *, p->nTableSize ); - memset( p->pTable, 0, sizeof(Aig_Obj_t *) * p->nTableSize ); - // rehash the entries from the old table - Counter = 0; - for ( i = 0; i < nTableSizeOld; i++ ) - for ( pEntry = pTableOld[i], pNext = pEntry? pEntry->pNext : NULL; pEntry; pEntry = pNext, pNext = pEntry? pEntry->pNext : NULL ) - { - // get the place where this entry goes in the table - ppPlace = Aig_TableFind( p, pEntry ); - assert( *ppPlace == NULL ); // should not be there - // add the entry to the list - *ppPlace = pEntry; - pEntry->pNext = NULL; - Counter++; - } - nEntries = Aig_ManNodeNum(p); - assert( Counter == nEntries ); - printf( "Increasing the structural table size from %6d to %6d. ", nTableSizeOld, p->nTableSize ); - PRT( "Time", clock() - clk ); - // replace the table and the parameters - free( pTableOld ); -} - /**Function******************************************************************** Synopsis [Profiles the hash table.] @@ -237,41 +235,6 @@ void Aig_TableProfile( Aig_Man_t * p ) } } -/**Function******************************************************************** - - Synopsis [Returns the next prime >= p.] - - Description [Copied from CUDD, for stand-aloneness.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -unsigned int Cudd_PrimeAig( unsigned int p) -{ - int i,pn; - p--; - do { - p++; - if (p&1) { - pn = 1; - i = 3; - while ((unsigned) (i * i) <= p) { - if (p % i == 0) { - pn = 0; - break; - } - i += 2; - } - } else { - pn = 0; - } - } while (!pn); - return(p); - -} /* end of Cudd_Prime */ - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/aig/aigTiming.c b/src/aig/aig/aigTiming.c new file mode 100644 index 00000000..dfb4c306 --- /dev/null +++ b/src/aig/aig/aigTiming.c @@ -0,0 +1,275 @@ +/**CFile**************************************************************** + + FileName [aigTiming.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [AIG package.] + + Synopsis [Incremental updating of direct/reverse AIG levels.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 28, 2007.] + + Revision [$Id: aigTiming.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "aig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Returns the reverse level of the node.] + + Description [The reverse level is the level of the node in reverse + topological order, starting from the COs.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Aig_ObjReverseLevel( Aig_Man_t * p, Aig_Obj_t * pObj ) +{ + assert( p->vLevelR ); + Vec_IntFillExtra( p->vLevelR, pObj->Id + 1, 0 ); + return Vec_IntEntry(p->vLevelR, pObj->Id); +} + +/**Function************************************************************* + + Synopsis [Sets the reverse level of the node.] + + Description [The reverse level is the level of the node in reverse + topological order, starting from the COs.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Aig_ObjSetReverseLevel( Aig_Man_t * p, Aig_Obj_t * pObj, int LevelR ) +{ + assert( p->vLevelR ); + Vec_IntFillExtra( p->vLevelR, pObj->Id + 1, 0 ); + Vec_IntWriteEntry( p->vLevelR, pObj->Id, LevelR ); +} + +/**Function************************************************************* + + Synopsis [Returns required level of the node.] + + Description [Converts the reverse levels of the node into its required + level as follows: ReqLevel(Node) = MaxLevels(Ntk) + 1 - LevelR(Node).] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ObjRequiredLevel( Aig_Man_t * p, Aig_Obj_t * pObj ) +{ + assert( p->vLevelR ); + return p->nLevelMax + 1 - Aig_ObjReverseLevel(p, pObj); +} + +/**Function************************************************************* + + Synopsis [Computes the reverse level of the node using its fanout levels.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ObjReverseLevelNew( Aig_Man_t * p, Aig_Obj_t * pObj ) +{ + Aig_Obj_t * pFanout; + int i, iFanout, LevelCur, Level = 0; + Aig_ObjForEachFanout( p, pObj, pFanout, iFanout, i ) + { + LevelCur = Aig_ObjReverseLevel( p, pFanout ); + Level = AIG_MAX( Level, LevelCur ); + } + return Level + 1; +} + +/**Function************************************************************* + + Synopsis [Prepares for the computation of required levels.] + + Description [This procedure should be called before the required times + are used. It starts internal data structures, which records the level + from the COs of the network nodes in reverse topologogical order.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManStartReverseLevels( Aig_Man_t * p, int nMaxLevelIncrease ) +{ + Vec_Ptr_t * vNodes; + Aig_Obj_t * pObj; + int i; + assert( p->pFanData != NULL ); + assert( p->vLevelR == NULL ); + // remember the maximum number of direct levels + p->nLevelMax = Aig_ManLevels(p) + nMaxLevelIncrease; + // start the reverse levels + p->vLevelR = Vec_IntAlloc( 0 ); + Vec_IntFill( p->vLevelR, 1 + Aig_ManObjIdMax(p), 0 ); + // compute levels in reverse topological order + vNodes = Aig_ManDfsReverse( p ); + Vec_PtrForEachEntry( vNodes, pObj, i ) + { + assert( pObj->fMarkA == 0 ); + Aig_ObjSetReverseLevel( p, pObj, Aig_ObjReverseLevelNew(p, pObj) ); + } + Vec_PtrFree( vNodes ); +} + +/**Function************************************************************* + + Synopsis [Cleans the data structures used to compute required levels.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManStopReverseLevels( Aig_Man_t * p ) +{ + assert( p->vLevelR != NULL ); + Vec_IntFree( p->vLevelR ); + p->vLevelR = NULL; + p->nLevelMax = 0; + +} + +/**Function************************************************************* + + Synopsis [Incrementally updates level of the nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManUpdateLevel( Aig_Man_t * p, Aig_Obj_t * pObjNew ) +{ + Aig_Obj_t * pFanout, * pTemp; + int iFanout, LevelOld, Lev, k, m; + assert( p->pFanData != NULL ); + // allocate level if needed + if ( p->vLevels == NULL ) + p->vLevels = Vec_VecAlloc( Aig_ManLevels(p) + 8 ); + // check if level has changed + LevelOld = Aig_ObjLevel(pObjNew); + if ( LevelOld == Aig_ObjLevelNew(pObjNew) ) + return; + // start the data structure for level update + // we cannot fail to visit a node when using this structure because the + // nodes are stored by their _old_ levels, which are assumed to be correct + Vec_VecClear( p->vLevels ); + Vec_VecPush( p->vLevels, LevelOld, pObjNew ); + pObjNew->fMarkA = 1; + // recursively update level + Vec_VecForEachEntryStart( p->vLevels, pTemp, Lev, k, LevelOld ) + { + pTemp->fMarkA = 0; + assert( Aig_ObjLevel(pTemp) == Lev ); + pTemp->Level = Aig_ObjLevelNew(pTemp); + // if the level did not change, no need to check the fanout levels + if ( Aig_ObjLevel(pTemp) == Lev ) + continue; + // schedule fanout for level update + Aig_ObjForEachFanout( p, pTemp, pFanout, iFanout, m ) + { + if ( !Aig_ObjIsPo(pFanout) && !pFanout->fMarkA ) + { + Vec_VecPush( p->vLevels, Aig_ObjLevel(pFanout), pFanout ); + pFanout->fMarkA = 1; + } + } + } +} + +/**Function************************************************************* + + Synopsis [Incrementally updates level of the nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManUpdateReverseLevel( Aig_Man_t * p, Aig_Obj_t * pObjNew ) +{ + Aig_Obj_t * pFanin, * pTemp; + int LevelOld, Lev, k; + assert( p->vLevelR != NULL ); + // allocate level if needed + if ( p->vLevels == NULL ) + p->vLevels = Vec_VecAlloc( Aig_ManLevels(p) + 8 ); + // check if level has changed + LevelOld = Aig_ObjReverseLevel(p, pObjNew); + if ( LevelOld == Aig_ObjReverseLevelNew(p, pObjNew) ) + return; + // start the data structure for level update + // we cannot fail to visit a node when using this structure because the + // nodes are stored by their _old_ levels, which are assumed to be correct + Vec_VecClear( p->vLevels ); + Vec_VecPush( p->vLevels, LevelOld, pObjNew ); + pObjNew->fMarkA = 1; + // recursively update level + Vec_VecForEachEntryStart( p->vLevels, pTemp, Lev, k, LevelOld ) + { + pTemp->fMarkA = 0; + LevelOld = Aig_ObjReverseLevel(p, pTemp); + assert( LevelOld == Lev ); + Aig_ObjSetReverseLevel( p, pTemp, Aig_ObjReverseLevelNew(p, pTemp) ); + // if the level did not change, to need to check the fanout levels + if ( Aig_ObjReverseLevel(p, pTemp) == Lev ) + continue; + // schedule fanins for level update + pFanin = Aig_ObjFanin0(pTemp); + if ( pFanin && !Aig_ObjIsPi(pFanin) && !pFanin->fMarkA ) + { + Vec_VecPush( p->vLevels, Aig_ObjReverseLevel(p, pFanin), pFanin ); + pFanin->fMarkA = 1; + } + pFanin = Aig_ObjFanin1(pTemp); + if ( pFanin && !Aig_ObjIsPi(pFanin) && !pFanin->fMarkA ) + { + Vec_VecPush( p->vLevels, Aig_ObjReverseLevel(p, pFanin), pFanin ); + pFanin->fMarkA = 1; + } + } +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/aig/module.make b/src/aig/aig/module.make index f1e83fe6..f9afc4ee 100644 --- a/src/aig/aig/module.make +++ b/src/aig/aig/module.make @@ -1,9 +1,11 @@ SRC += src/aig/aig/aigCheck.c \ src/aig/aig/aigDfs.c \ + src/aig/aig/aigFanout.c \ src/aig/aig/aigMan.c \ src/aig/aig/aigMem.c \ src/aig/aig/aigObj.c \ src/aig/aig/aigOper.c \ src/aig/aig/aigSeq.c \ src/aig/aig/aigTable.c \ + src/aig/aig/aigTiming.c \ src/aig/aig/aigUtil.c diff --git a/src/aig/dar/darBalance.c b/src/aig/dar/darBalance.c index a1502382..969e5253 100644 --- a/src/aig/dar/darBalance.c +++ b/src/aig/dar/darBalance.c @@ -49,7 +49,7 @@ static Aig_Obj_t * Dar_BalanceBuildSuper( Aig_Man_t * p, Vec_Ptr_t * vSuper, Aig Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel ) { Aig_Man_t * pNew; - Aig_Obj_t * pObj, * pObjNew; + Aig_Obj_t * pObj, * pDriver, * pObjNew; Vec_Vec_t * vStore; int i; // create the new manager @@ -63,14 +63,15 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel ) vStore = Vec_VecAlloc( 50 ); Aig_ManForEachPo( p, pObj, i ) { - pObjNew = Dar_Balance_rec( pNew, Aig_ObjFanin0(pObj), vStore, 0, fUpdateLevel ); - Aig_ObjCreatePo( pNew, Aig_NotCond( pObjNew, Aig_ObjFaninC0(pObj) ) ); + pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) ); + pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel ); + pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) ); + Aig_ObjCreatePo( pNew, pObjNew ); } Vec_VecFree( vStore ); // remove dangling nodes -// Aig_ManCreateRefs( pNew ); -// if ( i = Aig_ManCleanup( pNew ) ) -// printf( "Cleanup after balancing removed %d dangling nodes.\n", i ); + if ( i = Aig_ManCleanup( pNew ) ) + printf( "Cleanup after balancing removed %d dangling nodes.\n", i ); // check the resulting AIG if ( !Aig_ManCheck(pNew) ) printf( "Dar_ManBalance(): The check has failed.\n" ); @@ -94,6 +95,7 @@ Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjOld, Vec_Vec_t * Vec_Ptr_t * vSuper; int i; assert( !Aig_IsComplement(pObjOld) ); + assert( !Aig_ObjIsBuf(pObjOld) ); // return if the result is known if ( pObjOld->pData ) return pObjOld->pData; @@ -157,8 +159,8 @@ int Dar_BalanceCone_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper assert( !Aig_IsComplement(pObj) ); assert( Aig_ObjIsNode(pObj) ); // go through the branches - RetValue1 = Dar_BalanceCone_rec( pRoot, Aig_ObjChild0(pObj), vSuper ); - RetValue2 = Dar_BalanceCone_rec( pRoot, Aig_ObjChild1(pObj), vSuper ); + RetValue1 = Dar_BalanceCone_rec( pRoot, Aig_ObjReal_rec( Aig_ObjChild0(pObj) ), vSuper ); + RetValue2 = Dar_BalanceCone_rec( pRoot, Aig_ObjReal_rec( Aig_ObjChild1(pObj) ), vSuper ); if ( RetValue1 == -1 || RetValue2 == -1 ) return -1; // return 1 if at least one branch has a duplicate diff --git a/src/aig/dar/darCore.c b/src/aig/dar/darCore.c index a617f5d6..e7186e83 100644 --- a/src/aig/dar/darCore.c +++ b/src/aig/dar/darCore.c @@ -43,7 +43,7 @@ void Dar_ManDefaultParams( Dar_Par_t * pPars ) { memset( pPars, 0, sizeof(Dar_Par_t) ); pPars->nCutsMax = 8; - pPars->nSubgMax = 4; + pPars->nSubgMax = 5; // 5 is a "magic number" pPars->fUpdateLevel = 0; pPars->fUseZeros = 0; pPars->fVerbose = 0; @@ -69,18 +69,18 @@ int Dar_ManRewrite( Aig_Man_t * pAig, Dar_Par_t * pPars ) Aig_Obj_t * pObj, * pObjNew; int i, k, nNodesOld, nNodeBefore, nNodeAfter, Required; int clk = 0, clkStart; + // prepare the library + Dar_LibPrepare( pPars->nSubgMax ); // create rewriting manager p = Dar_ManStart( pAig, pPars ); // remove dangling nodes Aig_ManCleanup( pAig ); + // if updating levels is requested, start fanout and timing + Aig_ManCreateFanout( pAig ); + if ( p->pPars->fUpdateLevel ) + Aig_ManStartReverseLevels( pAig, 0 ); // set elementary cuts for the PIs -// Dar_ManSetupPis( p ); - Aig_ManCleanData( pAig ); - Dar_ObjPrepareCuts( p, Aig_ManConst1(pAig) ); - Aig_ManForEachPi( pAig, pObj, i ) - Dar_ObjPrepareCuts( p, pObj ); -// if ( p->pPars->fUpdateLevel ) -// Aig_NtkStartReverseLevels( p ); + Dar_ManCutsStart( p ); // resynthesize each node once clkStart = clock(); p->nNodesInit = Aig_ManNodeNum(pAig); @@ -93,6 +93,10 @@ int Dar_ManRewrite( Aig_Man_t * pAig, Dar_Par_t * pPars ) continue; if ( i > nNodesOld ) break; + // consider freeing the cuts +// if ( (i & 0xFFF) == 0 && Aig_MmFixedReadMemUsage(p->pMemCuts)/(1<<20) > 100 ) +// Dar_ManCutsStart( p ); + // compute cuts for the node clk = clock(); Dar_ObjComputeCuts_rec( p, pObj ); @@ -100,7 +104,7 @@ p->timeCuts += clock() - clk; // check if there is a trivial cut Dar_ObjForEachCut( pObj, pCut, k ) - if ( pCut->nLeaves == 0 || (pCut->nLeaves == 1 && pCut->pLeaves[0] != pObj->Id) ) + if ( pCut->nLeaves == 0 || (pCut->nLeaves == 1 && pCut->pLeaves[0] != pObj->Id && Aig_ManObj(p->pAig, pCut->pLeaves[0])) ) break; if ( k < (int)pObj->nCuts ) { @@ -115,10 +119,10 @@ p->timeCuts += clock() - clk; assert( pCut->uTruth == 0xAAAA || pCut->uTruth == 0x5555 ); pObjNew = Aig_NotCond( Aig_ManObj(p->pAig, pCut->pLeaves[0]), pCut->uTruth==0x5555 ); } - // replace the node - Aig_ObjReplace( pAig, pObj, pObjNew, 1 ); // remove the old cuts Dar_ObjSetCuts( pObj, NULL ); + // replace the node + Aig_ObjReplace( pAig, pObj, pObjNew, 1, p->pPars->fUpdateLevel ); continue; } @@ -128,17 +132,17 @@ p->timeCuts += clock() - clk; Dar_ObjForEachCut( pObj, pCut, k ) Dar_LibEval( p, pObj, pCut, Required ); // check the best gain - if ( !(p->GainBest > 0 || p->GainBest == 0 && p->pPars->fUseZeros) ) + if ( !(p->GainBest > 0 || (p->GainBest == 0 && p->pPars->fUseZeros)) ) continue; + // remove the old cuts + Dar_ObjSetCuts( pObj, NULL ); // if we end up here, a rewriting step is accepted nNodeBefore = Aig_ManNodeNum( pAig ); pObjNew = Dar_LibBuildBest( p ); pObjNew = Aig_NotCond( pObjNew, pObjNew->fPhase ^ pObj->fPhase ); assert( (int)Aig_Regular(pObjNew)->Level <= Required ); // replace the node - Aig_ObjReplace( pAig, pObj, pObjNew, 1 ); - // remove the old cuts - Dar_ObjSetCuts( pObj, NULL ); + Aig_ObjReplace( pAig, pObj, pObjNew, 1, p->pPars->fUpdateLevel ); // compare the gains nNodeAfter = Aig_ManNodeNum( pAig ); assert( p->GainBest <= nNodeBefore - nNodeAfter ); @@ -151,13 +155,14 @@ p->timeOther = p->timeTotal - p->timeCuts - p->timeEval; Extra_ProgressBarStop( pProgress ); p->nCutMemUsed = Aig_MmFixedReadMemUsage(p->pMemCuts)/(1<<20); Dar_ManCutsFree( p ); - // stop the rewriting manager - Dar_ManStop( p ); // put the nodes into the DFS order and reassign their IDs // Aig_NtkReassignIds( p ); // fix the levels -// if ( p->pPars->fUpdateLevel ) -// Aig_NtkStopReverseLevels( p ); + Aig_ManDeleteFanout( pAig ); + if ( p->pPars->fUpdateLevel ) + Aig_ManStopReverseLevels( pAig ); + // stop the rewriting manager + Dar_ManStop( p ); // check if ( !Aig_ManCheck( pAig ) ) { @@ -190,9 +195,7 @@ Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig ) // remove dangling nodes Aig_ManCleanup( pAig ); // set elementary cuts for the PIs -// Dar_ManSetupPis( p ); - Aig_ManForEachPi( pAig, pObj, i ) - Dar_ObjPrepareCuts( p, pObj ); + Dar_ManCutsStart( p ); // compute cuts for each nodes in the topological order Aig_ManForEachObj( pAig, pObj, i ) { diff --git a/src/aig/dar/darCut.c b/src/aig/dar/darCut.c index af9d1227..08bd77a9 100644 --- a/src/aig/dar/darCut.c +++ b/src/aig/dar/darCut.c @@ -62,20 +62,25 @@ static inline int Dar_WordCountOnes( unsigned uWord ) static inline int Dar_CutFindValue( Dar_Man_t * p, Dar_Cut_t * pCut ) { Aig_Obj_t * pLeaf; - int i, Value; + int i, Value, nOnes; assert( pCut->fUsed ); - if ( pCut->nLeaves < 2 ) - return 1001; Value = 0; + nOnes = 0; Dar_CutForEachLeaf( p->pAig, pCut, pLeaf, i ) { if ( pLeaf == NULL ) return 0; assert( pLeaf != NULL ); Value += pLeaf->nRefs; + nOnes += (pLeaf->nRefs == 1); } + if ( pCut->nLeaves < 2 ) + return 1001; +// Value = Value * 100 / pCut->nLeaves; if ( Value > 1000 ) Value = 1000; + if ( nOnes > 3 ) + Value = 5 - nOnes; return Value; } @@ -83,7 +88,7 @@ static inline int Dar_CutFindValue( Dar_Man_t * p, Dar_Cut_t * pCut ) Synopsis [Returns the next free cut to use.] - Description [] + Description [Uses the cut with the smallest value.] SideEffects [] @@ -114,6 +119,14 @@ static inline Dar_Cut_t * Dar_CutFindFree( Dar_Man_t * p, Aig_Obj_t * pObj ) pCutMax = pCut; } } + if ( pCutMax == NULL ) + { + Dar_ObjForEachCutAll( pObj, pCut, i ) + { + if ( pCutMax == NULL || pCutMax->Value > pCut->Value ) + pCutMax = pCut; + } + } assert( pCutMax != NULL ); pCutMax->fUsed = 0; return pCutMax; @@ -466,7 +479,6 @@ static inline int Dar_CutSuppMinimize( Dar_Cut_t * pCut ) unsigned uPhase = 0, uTruth = 0xFFFF & pCut->uTruth; int i, k, nLeaves; assert( pCut->fUsed ); - assert( pCut->nLeaves > 0 ); // compute the truth support of the cut's function nLeaves = pCut->nLeaves; for ( i = 0; i < (int)pCut->nLeaves; i++ ) @@ -555,6 +567,28 @@ Dar_Cut_t * Dar_ObjPrepareCuts( Dar_Man_t * p, Aig_Obj_t * pObj ) return pCutSet; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dar_ManCutsStart( Dar_Man_t * p ) +{ + Aig_Obj_t * pObj; + int i; + Aig_ManCleanData( p->pAig ); + Aig_MmFixedRestart( p->pMemCuts ); + Dar_ObjPrepareCuts( p, Aig_ManConst1(p->pAig) ); + Aig_ManForEachPi( p->pAig, pObj, i ) + Dar_ObjPrepareCuts( p, pObj ); +} + /**Function************************************************************* Synopsis [] @@ -612,10 +646,6 @@ Dar_Cut_t * Dar_ObjComputeCuts( Dar_Man_t * p, Aig_Obj_t * pObj ) // minimize support of the cut if ( Dar_CutSuppMinimize( pCut ) ) { - // if a simple cut is found return immediately - if ( pCut->nLeaves < 2 ) - return pCutSet; - // otherwise, filter the cuts again RetValue = Dar_CutFilter( pObj, pCut ); assert( !RetValue ); } @@ -628,6 +658,8 @@ Dar_Cut_t * Dar_ObjComputeCuts( Dar_Man_t * p, Aig_Obj_t * pObj ) p->nCutsSkipped++; pCut->fUsed = 0; } + else if ( pCut->nLeaves < 2 ) + return pCutSet; } // count the number of nontrivial cuts cuts Dar_ObjForEachCut( pObj, pCut, i ) diff --git a/src/aig/dar/darInt.h b/src/aig/dar/darInt.h index 0eb8f9fe..f496a73f 100644 --- a/src/aig/dar/darInt.h +++ b/src/aig/dar/darInt.h @@ -101,7 +101,7 @@ struct Dar_Man_t_ }; static inline Dar_Cut_t * Dar_ObjCuts( Aig_Obj_t * pObj ) { return pObj->pData; } -static inline void Dar_ObjSetCuts( Aig_Obj_t * pObj, Dar_Cut_t * pCuts ) { pObj->pData = pCuts; } +static inline void Dar_ObjSetCuts( Aig_Obj_t * pObj, Dar_Cut_t * pCuts ) { assert( !Aig_ObjIsNone(pObj) ); pObj->pData = pCuts; } //////////////////////////////////////////////////////////////////////// /// MACRO DEFINITIONS /// @@ -126,22 +126,24 @@ static inline void Dar_ObjSetCuts( Aig_Obj_t * pObj, Dar_Cut_t * pCuts ) /*=== darBalance.c ========================================================*/ extern Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel ); -/*=== darCore.c ========================================================*/ -/*=== darCut.c ========================================================*/ -extern Dar_Cut_t * Dar_ObjPrepareCuts( Dar_Man_t * p, Aig_Obj_t * pObj ); +/*=== darCore.c ===========================================================*/ +/*=== darCut.c ============================================================*/ +extern void Dar_ManCutsStart( Dar_Man_t * p ); extern void Dar_ManCutsFree( Dar_Man_t * p ); extern Dar_Cut_t * Dar_ObjComputeCuts_rec( Dar_Man_t * p, Aig_Obj_t * pObj ); extern Dar_Cut_t * Dar_ObjComputeCuts( Dar_Man_t * p, Aig_Obj_t * pObj ); -/*=== darData.c ========================================================*/ +/*=== darData.c ===========================================================*/ extern Vec_Int_t * Dar_LibReadNodes(); extern Vec_Int_t * Dar_LibReadOuts(); extern Vec_Int_t * Dar_LibReadPrios(); -/*=== darLib.c ==========================================================*/ +/*=== darLib.c ============================================================*/ extern void Dar_LibStart(); extern void Dar_LibStop(); +extern void Dar_LibPrepare( int nSubgraphs ); +extern void Dar_LibReturnCanonicals( unsigned * pCanons ); extern void Dar_LibEval( Dar_Man_t * p, Aig_Obj_t * pRoot, Dar_Cut_t * pCut, int Required ); extern Aig_Obj_t * Dar_LibBuildBest( Dar_Man_t * p ); -/*=== darMan.c ==========================================================*/ +/*=== darMan.c ============================================================*/ extern Dar_Man_t * Dar_ManStart( Aig_Man_t * pAig, Dar_Par_t * pPars ); extern void Dar_ManStop( Dar_Man_t * p ); extern void Dar_ManPrintStats( Dar_Man_t * p ); diff --git a/src/aig/dar/darLib.c b/src/aig/dar/darLib.c index fce6155b..c3d57b52 100644 --- a/src/aig/dar/darLib.c +++ b/src/aig/dar/darLib.c @@ -44,7 +44,7 @@ struct Dar_LibDat_t_ // library object data Aig_Obj_t * pFunc; // the corresponding AIG node if it exists int Level; // level of this node after it is constructured int TravId; // traversal ID of the library object data - unsigned char Area; // area of the node + unsigned char fMffc; // set to one if node is part of MFFC unsigned char nLats[3]; // the number of latches on the input/output stem }; @@ -54,9 +54,6 @@ struct Dar_Lib_t_ // library Dar_LibObj_t * pObjs; // the set of library objects int nObjs; // the number of objects used int iObj; // the current object - // object data - Dar_LibDat_t * pDatas; - int nDatas; // structures by class int nSubgr[222]; // the number of subgraphs by class int * pSubgr[222]; // the subgraphs for each class @@ -75,8 +72,24 @@ struct Dar_Lib_t_ // library int nNodes[222]; // the number of nodes by class int * pNodes[222]; // the nodes for each class int * pNodesMem; // memory for nodes pointers - int pNodesTotal; // the total number of nodes - // information by NPN classes + int nNodesTotal; // the total number of nodes + // prepared library + int nSubgraphs; + int nNodes0Max; + // nodes by class + int nNodes0[222]; // the number of nodes by class + int * pNodes0[222]; // the nodes for each class + int * pNodes0Mem; // memory for nodes pointers + int nNodes0Total; // the total number of nodes + // structures by class + int nSubgr0[222]; // the number of subgraphs by class + int * pSubgr0[222]; // the subgraphs for each class + int * pSubgr0Mem; // memory for subgraph pointers + int nSubgr0Total; // the total number of subgraph + // object data + Dar_LibDat_t * pDatas; + int nDatas; + // information about NPN classes char ** pPerms4; unsigned short * puCanons; char * pPhases; @@ -104,7 +117,7 @@ static inline int Dar_LibObjTruth( Dar_LibObj_t * pObj ) { return pOb SeeAlso [] ***********************************************************************/ -Dar_Lib_t * Dar_LibAlloc( int nObjs, int nDatas ) +Dar_Lib_t * Dar_LibAlloc( int nObjs ) { unsigned uTruths[4] = { 0xAAAA, 0xCCCC, 0xF0F0, 0xFF00 }; Dar_Lib_t * p; @@ -115,10 +128,6 @@ Dar_Lib_t * Dar_LibAlloc( int nObjs, int nDatas ) p->nObjs = nObjs; p->pObjs = ALLOC( Dar_LibObj_t, nObjs ); memset( p->pObjs, 0, sizeof(Dar_LibObj_t) * nObjs ); - // allocate datas - p->nDatas = nDatas; - p->pDatas = ALLOC( Dar_LibDat_t, nDatas ); - memset( p->pObjs, 0, sizeof(Dar_LibDat_t) * nDatas ); // allocate canonical data p->pPerms4 = Extra_Permutations( 4 ); Extra_Truth4VarNPN( &p->puCanons, &p->pPhases, &p->pPerms, &p->pMap ); @@ -149,7 +158,9 @@ void Dar_LibFree( Dar_Lib_t * p ) free( p->pObjs ); free( p->pDatas ); free( p->pNodesMem ); + free( p->pNodes0Mem ); free( p->pSubgrMem ); + free( p->pSubgr0Mem ); free( p->pPriosMem ); FREE( p->pPlaceMem ); FREE( p->pScoreMem ); @@ -161,6 +172,31 @@ void Dar_LibFree( Dar_Lib_t * p ) free( p ); } +/**Function************************************************************* + + Synopsis [Returns canonical truth tables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dar_LibReturnCanonicals( unsigned * pCanons ) +{ + int Visits[222] = {0}; + int i, k; + // find canonical truth tables + for ( i = k = 0; i < (1<<16); i++ ) + if ( !Visits[s_DarLib->pMap[i]] ) + { + Visits[s_DarLib->pMap[i]] = 1; + pCanons[k++] = ((i<<16) | i); + } + assert( k == 222 ); +} + /**Function************************************************************* Synopsis [Adds one AND to the library.] @@ -196,14 +232,14 @@ void Dar_LibAddNode( Dar_Lib_t * p, int Id0, int Id1, int fCompl0, int fCompl1 ) SeeAlso [] ***********************************************************************/ -void Dar_LibSetup_rec( Dar_Lib_t * p, Dar_LibObj_t * pObj, int Class ) +void Dar_LibSetup_rec( Dar_Lib_t * p, Dar_LibObj_t * pObj, int Class, int fCollect ) { if ( pObj->fTerm || (int)pObj->Num == Class ) return; pObj->Num = Class; - Dar_LibSetup_rec( p, Dar_LibObj(p, pObj->Fan0), Class ); - Dar_LibSetup_rec( p, Dar_LibObj(p, pObj->Fan1), Class ); - if ( p->pNodesMem ) + Dar_LibSetup_rec( p, Dar_LibObj(p, pObj->Fan0), Class, fCollect ); + Dar_LibSetup_rec( p, Dar_LibObj(p, pObj->Fan1), Class, fCollect ); + if ( fCollect ) p->pNodes[Class][ p->nNodes[Class]++ ] = pObj-p->pObjs; else p->nNodes[Class]++; @@ -239,10 +275,12 @@ void Dar_LibSetup( Dar_Lib_t * p, Vec_Int_t * vOuts, Vec_Int_t * vPrios ) } // allocate memory for the roots of each class p->pSubgrMem = ALLOC( int, Vec_IntSize(vOuts) ); + p->pSubgr0Mem = ALLOC( int, Vec_IntSize(vOuts) ); p->nSubgrTotal = 0; for ( i = 0; i < 222; i++ ) { p->pSubgr[i] = p->pSubgrMem + p->nSubgrTotal; + p->pSubgr0[i] = p->pSubgr0Mem + p->nSubgrTotal; p->nSubgrTotal += p->nSubgr[i]; p->nSubgr[i] = 0; } @@ -321,18 +359,20 @@ void Dar_LibSetup( Dar_Lib_t * p, Vec_Int_t * vOuts, Vec_Int_t * vPrios ) // count nodes in each class for ( i = 0; i < 222; i++ ) for ( k = 0; k < p->nSubgr[i]; k++ ) - Dar_LibSetup_rec( p, Dar_LibObj(p, p->pSubgr[i][k]), i ); + Dar_LibSetup_rec( p, Dar_LibObj(p, p->pSubgr[i][k]), i, 0 ); // count the total number of nodes - p->pNodesTotal = 0; + p->nNodesTotal = 0; for ( i = 0; i < 222; i++ ) - p->pNodesTotal += p->nNodes[i]; + p->nNodesTotal += p->nNodes[i]; // allocate memory for the nodes of each class - p->pNodesMem = ALLOC( int, p->pNodesTotal ); - p->pNodesTotal = 0; + p->pNodesMem = ALLOC( int, p->nNodesTotal ); + p->pNodes0Mem = ALLOC( int, p->nNodesTotal ); + p->nNodesTotal = 0; for ( i = 0; i < 222; i++ ) { - p->pNodes[i] = p->pNodesMem + p->pNodesTotal; - p->pNodesTotal += p->nNodes[i]; + p->pNodes[i] = p->pNodesMem + p->nNodesTotal; + p->pNodes0[i] = p->pNodes0Mem + p->nNodesTotal; + p->nNodesTotal += p->nNodes[i]; p->nNodes[i] = 0; } // create traversal IDs @@ -343,16 +383,143 @@ void Dar_LibSetup( Dar_Lib_t * p, Vec_Int_t * vOuts, Vec_Int_t * vPrios ) for ( i = 0; i < 222; i++ ) { for ( k = 0; k < p->nSubgr[i]; k++ ) - Dar_LibSetup_rec( p, Dar_LibObj(p, p->pSubgr[i][k]), i ); + Dar_LibSetup_rec( p, Dar_LibObj(p, p->pSubgr[i][k]), i, 1 ); nNodesTotal += p->nNodes[i]; //printf( "Class %3d : Subgraphs = %4d. Nodes = %5d.\n", i, p->nSubgr[i], p->nNodes[i] ); } - assert( nNodesTotal == p->pNodesTotal ); + assert( nNodesTotal == p->nNodesTotal ); // prepare the number of the PI nodes for ( i = 0; i < 4; i++ ) Dar_LibObj(p, i)->Num = i; } +/**Function************************************************************* + + Synopsis [Starts the library.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dar_LibCreateData( Dar_Lib_t * p, int nDatas ) +{ + if ( p->nDatas == nDatas ) + return; + FREE( p->pDatas ); + // allocate datas + p->nDatas = nDatas; + p->pDatas = ALLOC( Dar_LibDat_t, nDatas ); + memset( p->pDatas, 0, sizeof(Dar_LibDat_t) * nDatas ); +} + +/**Function************************************************************* + + Synopsis [Adds one AND to the library.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dar_LibSetup0_rec( Dar_Lib_t * p, Dar_LibObj_t * pObj, int Class, int fCollect ) +{ + if ( pObj->fTerm || (int)pObj->Num == Class ) + return; + pObj->Num = Class; + Dar_LibSetup0_rec( p, Dar_LibObj(p, pObj->Fan0), Class, fCollect ); + Dar_LibSetup0_rec( p, Dar_LibObj(p, pObj->Fan1), Class, fCollect ); + if ( fCollect ) + p->pNodes0[Class][ p->nNodes0[Class]++ ] = pObj-p->pObjs; + else + p->nNodes0[Class]++; +} + +/**Function************************************************************* + + Synopsis [Starts the library.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dar_LibPrepare( int nSubgraphs ) +{ + Dar_Lib_t * p = s_DarLib; + int i, k, nNodes0Total; + if ( p->nSubgraphs == nSubgraphs ) + return; + + // favor special classes: + // 1 : F = (!d*!c*!b*!a) + // 4 : F = (!d*!c*!(b*a)) + // 12 : F = (!d*!(c*!(!b*!a))) + // 20 : F = (!d*!(c*b*a)) + + // set the subgraph counters + p->nSubgr0Total = 0; + for ( i = 0; i < 222; i++ ) + { +// if ( i == 1 || i == 4 || i == 12 || i == 20 ) // special classes + if ( i == 1 ) // special classes + p->nSubgr0[i] = p->nSubgr[i]; + else + p->nSubgr0[i] = AIG_MIN( p->nSubgr[i], nSubgraphs ); + p->nSubgr0Total += p->nSubgr0[i]; + for ( k = 0; k < p->nSubgr0[i]; k++ ) + p->pSubgr0[i][k] = p->pSubgr[i][ p->pPrios[i][k] ]; + } + + // count the number of nodes + // clean node counters + for ( i = 0; i < 222; i++ ) + p->nNodes0[i] = 0; + // create traversal IDs + for ( i = 0; i < p->iObj; i++ ) + Dar_LibObj(p, i)->Num = 0xff; + // count nodes in each class + // count the total number of nodes and the largest class + p->nNodes0Total = 0; + p->nNodes0Max = 0; + for ( i = 0; i < 222; i++ ) + { + for ( k = 0; k < p->nSubgr0[i]; k++ ) + Dar_LibSetup0_rec( p, Dar_LibObj(p, p->pSubgr0[i][k]), i, 0 ); + p->nNodes0Total += p->nNodes0[i]; + p->nNodes0Max = AIG_MAX( p->nNodes0Max, p->nNodes0[i] ); + } + + // clean node counters + for ( i = 0; i < 222; i++ ) + p->nNodes0[i] = 0; + // create traversal IDs + for ( i = 0; i < p->iObj; i++ ) + Dar_LibObj(p, i)->Num = 0xff; + // add the nodes to storage + nNodes0Total = 0; + for ( i = 0; i < 222; i++ ) + { + for ( k = 0; k < p->nSubgr0[i]; k++ ) + Dar_LibSetup0_rec( p, Dar_LibObj(p, p->pSubgr0[i][k]), i, 1 ); + nNodes0Total += p->nNodes0[i]; + } + assert( nNodes0Total == p->nNodes0Total ); + // prepare the number of the PI nodes + for ( i = 0; i < 4; i++ ) + Dar_LibObj(p, i)->Num = i; + + // realloc the datas + Dar_LibCreateData( p, p->nNodes0Max + 32 ); + // allocated more because Dar_LibBuildBest() sometimes requires more entries +} + /**Function************************************************************* Synopsis [Reads library from array.] @@ -374,7 +541,7 @@ Dar_Lib_t * Dar_LibRead() vOuts = Dar_LibReadOuts(); vPrios = Dar_LibReadPrios(); // create library - p = Dar_LibAlloc( Vec_IntSize(vObjs)/2 + 4, 6000 ); + p = Dar_LibAlloc( Vec_IntSize(vObjs)/2 + 4 ); // create nodes for ( i = 0; i < vObjs->nSize; i += 2 ) Dar_LibAddNode( p, vObjs->pArray[i] >> 1, vObjs->pArray[i+1] >> 1, @@ -383,6 +550,7 @@ Dar_Lib_t * Dar_LibRead() Dar_LibSetup( p, vOuts, vPrios ); Vec_IntFree( vObjs ); Vec_IntFree( vOuts ); + Vec_IntFree( vPrios ); return p; } @@ -670,15 +838,20 @@ void Dar_LibEvalAssignNums( Dar_Man_t * p, int Class ) Dar_LibDat_t * pData, * pData0, * pData1; Aig_Obj_t * pGhost, * pFanin0, * pFanin1; int i; - for ( i = 0; i < s_DarLib->nNodes[Class]; i++ ) + for ( i = 0; i < s_DarLib->nNodes0[Class]; i++ ) { // get one class node, assign its temporary number and set its data - pObj = Dar_LibObj(s_DarLib, s_DarLib->pNodes[Class][i]); + pObj = Dar_LibObj(s_DarLib, s_DarLib->pNodes0[Class][i]); pObj->Num = 4 + i; + assert( (int)pObj->Num < s_DarLib->nNodes0Max + 4 ); pData = s_DarLib->pDatas + pObj->Num; + pData->fMffc = 0; pData->pFunc = NULL; pData->TravId = 0xFFFF; + // explore the fanins + assert( (int)Dar_LibObj(s_DarLib, pObj->Fan0)->Num < s_DarLib->nNodes0Max + 4 ); + assert( (int)Dar_LibObj(s_DarLib, pObj->Fan1)->Num < s_DarLib->nNodes0Max + 4 ); pData0 = s_DarLib->pDatas + Dar_LibObj(s_DarLib, pObj->Fan0)->Num; pData1 = s_DarLib->pDatas + Dar_LibObj(s_DarLib, pObj->Fan1)->Num; pData->Level = 1 + AIG_MAX(pData0->Level, pData1->Level); @@ -704,9 +877,7 @@ void Dar_LibEvalAssignNums( Dar_Man_t * p, int Class ) // clear the node if it is part of MFFC if ( pData->pFunc != NULL && Aig_ObjIsTravIdCurrent(p->pAig, pData->pFunc) ) - pData->pFunc = NULL; -//if ( Class == 7 ) -//printf( "Evaling node %d at data %d\n", pData->pFunc? pData->pFunc->Id : -1, pObj->Num ); + pData->fMffc = 1; } } @@ -729,20 +900,22 @@ int Dar_LibEval_rec( Dar_LibObj_t * pObj, int Out, int nNodesSaved, int Required return 0; assert( pObj->Num > 3 ); pData = s_DarLib->pDatas + pObj->Num; - if ( pData->pFunc ) + if ( pData->pFunc && !pData->fMffc ) return 0; if ( pData->Level > Required ) return 0xff; if ( pData->TravId == Out ) - return pData->Area; + return 0; pData->TravId = Out; - Area = 1 + Dar_LibEval_rec( Dar_LibObj(s_DarLib, pObj->Fan0), Out, nNodesSaved, Required ); + // this is a new node - get a bound on the area of its branches + nNodesSaved--; + Area = Dar_LibEval_rec( Dar_LibObj(s_DarLib, pObj->Fan0), Out, nNodesSaved, Required+1 ); if ( Area > nNodesSaved ) - return pData->Area = 0xff; - Area += Dar_LibEval_rec( Dar_LibObj(s_DarLib, pObj->Fan1), Out, nNodesSaved, Required ); + return 0xff; + Area += Dar_LibEval_rec( Dar_LibObj(s_DarLib, pObj->Fan1), Out, nNodesSaved, Required+1 ); if ( Area > nNodesSaved ) - return pData->Area = 0xff; - return pData->Area = Area; + return 0xff; + return Area + 1; } /**Function************************************************************* @@ -773,25 +946,27 @@ void Dar_LibEval( Dar_Man_t * p, Aig_Obj_t * pRoot, Dar_Cut_t * pCut, int Requir Class = s_DarLib->pMap[pCut->uTruth]; Dar_LibEvalAssignNums( p, Class ); // profile outputs by their savings - p->nTotalSubgs += s_DarLib->nSubgr[Class]; - p->ClassSubgs[Class] += s_DarLib->nSubgr[Class]; - for ( Out = 0; Out < s_DarLib->nSubgr[Class]; Out++ ) + p->nTotalSubgs += s_DarLib->nSubgr0[Class]; + p->ClassSubgs[Class] += s_DarLib->nSubgr0[Class]; + for ( Out = 0; Out < s_DarLib->nSubgr0[Class]; Out++ ) { - pObj = Dar_LibObj(s_DarLib, s_DarLib->pSubgr[Class][Out]); - nNodesAdded = Dar_LibEval_rec( pObj, Out, nNodesSaved, Required ); + pObj = Dar_LibObj(s_DarLib, s_DarLib->pSubgr0[Class][Out]); + if ( Aig_Regular(s_DarLib->pDatas[pObj->Num].pFunc) == pRoot ) + continue; + nNodesAdded = Dar_LibEval_rec( pObj, Out, nNodesSaved - !p->pPars->fUseZeros, Required ); nNodesGained = nNodesSaved - nNodesAdded; if ( fTraining && nNodesGained >= 0 ) Dar_LibIncrementScore( Class, Out, nNodesGained + 1 ); - if ( nNodesGained <= 0 ) + if ( nNodesGained < 0 || (nNodesGained == 0 && !p->pPars->fUseZeros) ) continue; - if ( nNodesGained < p->GainBest || - (nNodesGained == p->GainBest && s_DarLib->pDatas[pObj->Num].Level >= p->GainBest) ) + if ( nNodesGained < p->GainBest || + (nNodesGained == p->GainBest && s_DarLib->pDatas[pObj->Num].Level >= p->LevelBest) ) continue; // remember this possibility Vec_PtrClear( p->vLeavesBest ); for ( k = 0; k < (int)pCut->nLeaves; k++ ) Vec_PtrPush( p->vLeavesBest, s_DarLib->pDatas[k].pFunc ); - p->OutBest = s_DarLib->pSubgr[Class][Out]; + p->OutBest = s_DarLib->pSubgr0[Class][Out]; p->OutNumBest = Out; p->LevelBest = s_DarLib->pDatas[pObj->Num].Level; p->GainBest = nNodesGained; @@ -845,7 +1020,6 @@ Aig_Obj_t * Dar_LibBuildBest_rec( Dar_Man_t * p, Dar_LibObj_t * pObj ) pFanin0 = Aig_NotCond( pFanin0, pObj->fCompl0 ); pFanin1 = Aig_NotCond( pFanin1, pObj->fCompl1 ); pData->pFunc = Aig_And( p->pAig, pFanin0, pFanin1 ); -//printf( "Adding node %d for data %d\n", pData->pFunc->Id, pObj->Num ); return pData->pFunc; } diff --git a/src/aig/dar/darMan.c b/src/aig/dar/darMan.c index a209503a..8b7c5afb 100644 --- a/src/aig/dar/darMan.c +++ b/src/aig/dar/darMan.c @@ -48,7 +48,7 @@ Dar_Man_t * Dar_ManStart( Aig_Man_t * pAig, Dar_Par_t * pPars ) p->pPars = pPars; p->pAig = pAig; // prepare the internal memory manager - p->pMemCuts = Aig_MmFixedStart( p->pPars->nCutsMax * sizeof(Dar_Cut_t), 512 ); + p->pMemCuts = Aig_MmFixedStart( p->pPars->nCutsMax * sizeof(Dar_Cut_t), 1024 ); // other data p->vLeavesBest = Vec_PtrAlloc( 4 ); return p; @@ -89,18 +89,27 @@ void Dar_ManStop( Dar_Man_t * p ) ***********************************************************************/ void Dar_ManPrintStats( Dar_Man_t * p ) { - int i, Gain; + unsigned pCanons[222]; + int Gain, i; + extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars ); + Gain = p->nNodesInit - Aig_ManNodeNum(p->pAig); printf( "NodesBeg = %8d. NodesEnd = %8d. Gain = %6d. (%6.2f %%). Cut mem = %d Mb\n", p->nNodesInit, Aig_ManNodeNum(p->pAig), Gain, 100.0*Gain/p->nNodesInit, p->nCutMemUsed ); printf( "Cuts = %8d. Tried = %8d. Used = %8d. Bad = %5d. Skipped = %5d. Ave = %.2f.\n", p->nCutsAll, p->nCutsTried, p->nCutsUsed, p->nCutsBad, p->nCutsSkipped, (float)p->nCutsUsed/Aig_ManNodeNum(p->pAig) ); + + printf( "Bufs = %5d. BufMax = %5d. BufReplace = %6d. BufFix = %6d.\n", + Aig_ManBufNum(p->pAig), p->pAig->nBufMax, p->pAig->nBufReplaces, p->pAig->nBufFixes ); PRT( "Cuts ", p->timeCuts ); PRT( "Eval ", p->timeEval ); PRT( "Other ", p->timeOther ); PRT( "TOTAL ", p->timeTotal ); -/* + + if ( !p->pPars->fVeryVerbose ) + return; + Dar_LibReturnCanonicals( pCanons ); for ( i = 0; i < 222; i++ ) { if ( p->ClassGains[i] == 0 && p->ClassTimes[i] == 0 ) @@ -108,10 +117,10 @@ void Dar_ManPrintStats( Dar_Man_t * p ) printf( "%3d : ", i ); printf( "G = %6d (%5.2f %%) ", p->ClassGains[i], Gain? 100.0*p->ClassGains[i]/Gain : 0.0 ); printf( "S = %8d (%5.2f %%) ", p->ClassSubgs[i], p->nTotalSubgs? 100.0*p->ClassSubgs[i]/p->nTotalSubgs : 0.0 ); - printf( "R = %7d ", p->ClassGains[i]? p->ClassSubgs[i]/p->ClassGains[i] : 9999999 ); - PRTP( "T", p->ClassTimes[i], p->timeEval ); + printf( "R = %7d ", p->ClassGains[i]? p->ClassSubgs[i]/p->ClassGains[i] : 9999999 ); + Kit_DsdPrintFromTruth( pCanons + i, 4 ); +// PRTP( "T", p->ClassTimes[i], p->timeEval ); } -*/ } diff --git a/src/aig/dar/darRefact.c b/src/aig/dar/darRefact.c new file mode 100644 index 00000000..1bcc0466 --- /dev/null +++ b/src/aig/dar/darRefact.c @@ -0,0 +1,48 @@ +/**CFile**************************************************************** + + FileName [darRefact.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [DAG-aware AIG rewriting.] + + Synopsis [Refactoring.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 28, 2007.] + + Revision [$Id: darRefact.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "darInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/dar/darResub.c b/src/aig/dar/darResub.c new file mode 100644 index 00000000..f819934e --- /dev/null +++ b/src/aig/dar/darResub.c @@ -0,0 +1,48 @@ +/**CFile**************************************************************** + + FileName [darResub.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: darResub.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "darInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/dar/darScript.c b/src/aig/dar/darScript.c new file mode 100644 index 00000000..c98a263e --- /dev/null +++ b/src/aig/dar/darScript.c @@ -0,0 +1,48 @@ +/**CFile**************************************************************** + + FileName [darScript.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [DAG-aware AIG rewriting.] + + Synopsis [Rewriting scripts.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 28, 2007.] + + Revision [$Id: darScript.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "darInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/dar/dar_.c b/src/aig/dar/dar_.c index 08bd8c3e..12fd7d17 100644 --- a/src/aig/dar/dar_.c +++ b/src/aig/dar/dar_.c @@ -18,7 +18,7 @@ ***********************************************************************/ -#include "dar.h" +#include "darInt.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// diff --git a/src/aig/dar/module.make b/src/aig/dar/module.make index bcf9a2e6..09b45171 100644 --- a/src/aig/dar/module.make +++ b/src/aig/dar/module.make @@ -4,4 +4,7 @@ SRC += src/aig/dar/darBalance.c \ src/aig/dar/darData.c \ src/aig/dar/darLib.c \ src/aig/dar/darMan.c \ + src/aig/dar/darRefact.c \ + src/aig/dar/darResub.c \ + src/aig/dar/darScript.c \ src/aig/dar/darTruth.c diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c index 5338d662..9e1a9a1a 100644 --- a/src/aig/fra/fraCore.c +++ b/src/aig/fra/fraCore.c @@ -45,7 +45,7 @@ Aig_Man_t * Fra_Perform( Aig_Man_t * pManAig, Fra_Par_t * pPars ) Aig_Man_t * pManAigNew; int clk; if ( Aig_ManNodeNum(pManAig) == 0 ) - return Aig_ManDup(pManAig); + return Aig_ManDup(pManAig, 1); clk = clock(); assert( Aig_ManLatchNum(pManAig) == 0 ); p = Fra_ManStart( pManAig, pPars ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 6b305033..c9761783 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -1532,7 +1532,7 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults nCofLevel = 1; - fCofactor = 1; + fCofactor = 0; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "Nch" ) ) != EOF ) { diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index c4020127..ba0705ed 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -521,14 +521,24 @@ Abc_Ntk_t * Abc_NtkCSweep( Abc_Ntk_t * pNtk, int nCutsMax, int nLeafMax, int fVe ***********************************************************************/ Abc_Ntk_t * Abc_NtkDRewrite( Abc_Ntk_t * pNtk, Dar_Par_t * pPars ) { - Aig_Man_t * pMan; + Aig_Man_t * pMan, * pTemp; Abc_Ntk_t * pNtkAig; + int clk; assert( Abc_NtkIsStrash(pNtk) ); pMan = Abc_NtkToDar( pNtk ); if ( pMan == NULL ) return NULL; // Aig_ManPrintStats( pMan ); + Dar_ManRewrite( pMan, pPars ); +// pMan = Dar_ManBalance( pTemp = pMan, pPars->fUpdateLevel ); +// Aig_ManStop( pTemp ); + +clk = clock(); + pMan = Aig_ManDup( pTemp = pMan, 0 ); + Aig_ManStop( pTemp ); +PRT( "time", clock() - clk ); + // Aig_ManPrintStats( pMan ); pNtkAig = Abc_NtkFromDar( pNtk, pMan ); Aig_ManStop( pMan ); diff --git a/src/base/abci/abcRewrite.c b/src/base/abci/abcRewrite.c index 7760b2d1..613741a8 100644 --- a/src/base/abci/abcRewrite.c +++ b/src/base/abci/abcRewrite.c @@ -155,7 +155,11 @@ Rwr_ManAddTimeTotal( pManRwr, clock() - clkStart ); } // put the nodes into the DFS order and reassign their IDs + { +// int clk = clock(); Abc_NtkReassignIds( pNtk ); +// PRT( "time", clock() - clk ); + } // Abc_AigCheckFaninOrder( pNtk->pManFunc ); // fix the levels if ( fUpdateLevel ) diff --git a/src/base/abci/abcTiming.c b/src/base/abci/abcTiming.c index fd54f519..5d5e6e93 100644 --- a/src/base/abci/abcTiming.c +++ b/src/base/abci/abcTiming.c @@ -811,7 +811,7 @@ void Abc_NtkUpdateLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels ) pTemp->fMarkA = 0; assert( Abc_ObjLevel(pTemp) == Lev ); Abc_ObjSetLevel( pTemp, Abc_ObjLevelNew(pTemp) ); - // if the level did not change, to need to check the fanout levels + // if the level did not change, no need to check the fanout levels if ( Abc_ObjLevel(pTemp) == Lev ) continue; // schedule fanout for level update @@ -858,7 +858,7 @@ void Abc_NtkUpdateReverseLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels ) LevelOld = Abc_ObjReverseLevel(pTemp); assert( LevelOld == Lev ); Abc_ObjSetReverseLevel( pTemp, Abc_ObjReverseLevelNew(pTemp) ); - // if the level did not change, to need to check the fanout levels + // if the level did not change, no need to check the fanout levels if ( Abc_ObjReverseLevel(pTemp) == Lev ) continue; // schedule fanins for level update -- cgit v1.2.3