diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2007-07-23 08:01:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2007-07-23 08:01:00 -0700 |
commit | 64dc240b904adafee78e2a66a1fc31b717f8985f (patch) | |
tree | 3632887450b37c4dcac6f6cbac08d42e9512c440 /src/aig | |
parent | 1647addf5e3ce4f82cc35cd4983bc5f7b9730290 (diff) | |
download | abc-64dc240b904adafee78e2a66a1fc31b717f8985f.tar.gz abc-64dc240b904adafee78e2a66a1fc31b717f8985f.tar.bz2 abc-64dc240b904adafee78e2a66a1fc31b717f8985f.zip |
Version abc70723
Diffstat (limited to 'src/aig')
-rw-r--r-- | src/aig/aig/aig.h | 17 | ||||
-rw-r--r-- | src/aig/aig/aigDfs.c | 58 | ||||
-rw-r--r-- | src/aig/aig/aigMffc.c | 297 | ||||
-rw-r--r-- | src/aig/aig/aigObj.c | 5 | ||||
-rw-r--r-- | src/aig/aig/aigTable.c | 27 | ||||
-rw-r--r-- | src/aig/aig/aigTruth.c | 98 | ||||
-rw-r--r-- | src/aig/aig/aigUtil.c | 20 | ||||
-rw-r--r-- | src/aig/aig/aigWin.c | 184 | ||||
-rw-r--r-- | src/aig/aig/module.make | 5 | ||||
-rw-r--r-- | src/aig/dar/dar.h | 29 | ||||
-rw-r--r-- | src/aig/dar/darCore.c | 20 | ||||
-rw-r--r-- | src/aig/dar/darInt.h | 7 | ||||
-rw-r--r-- | src/aig/dar/darLib.c | 87 | ||||
-rw-r--r-- | src/aig/dar/darMan.c | 2 | ||||
-rw-r--r-- | src/aig/dar/darRefact.c | 532 | ||||
-rw-r--r-- | src/aig/dar/darScript.c | 204 | ||||
-rw-r--r-- | src/aig/kit/kit.h | 1 |
17 files changed, 1486 insertions, 107 deletions
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h index 6725f4a6..8c9400be 100644 --- a/src/aig/aig/aig.h +++ b/src/aig/aig/aig.h @@ -274,6 +274,9 @@ static inline void Aig_ManRecycleMemory( Aig_Man_t * p, Aig_Obj_t * pEntry ) // iterator over all nodes #define Aig_ManForEachNode( p, pObj, i ) \ Vec_PtrForEachEntry( p->vObjs, pObj, i ) if ( (pObj) == NULL || !Aig_ObjIsNode(pObj) ) {} else +// iterator over the nodes whose IDs are stored in the array +#define Aig_ManForEachNodeVec( p, vIds, pObj, i ) \ + for ( i = 0; i < Vec_IntSize(vIds) && ((pObj) = Aig_ManObj(p, Vec_IntEntry(vIds,i))); i++ ) // 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]; } @@ -299,6 +302,7 @@ 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 ); +extern void Aig_ManCollectCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes ); /*=== 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 ); @@ -314,6 +318,13 @@ extern void Aig_ManPrintStats( Aig_Man_t * p ); /*=== aigMem.c ==========================================================*/ extern void Aig_ManStartMemory( Aig_Man_t * p ); extern void Aig_ManStopMemory( Aig_Man_t * p ); +/*=== aigMffc.c ==========================================================*/ +extern int Aig_NodeRef_rec( Aig_Obj_t * pNode, unsigned LevelMin ); +extern int Aig_NodeDeref_rec( Aig_Obj_t * pNode, unsigned LevelMin ); +extern int Aig_NodeMffsSupp( Aig_Man_t * p, Aig_Obj_t * pNode, int LevelMin, Vec_Ptr_t * vSupp ); +extern int Aig_NodeMffsLabel( Aig_Man_t * p, Aig_Obj_t * pNode ); +extern int Aig_NodeMffsLabelCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves ); +extern int Aig_NodeMffsExtendCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vResult ); /*=== aigObj.c ==========================================================*/ extern Aig_Obj_t * Aig_ObjCreatePi( Aig_Man_t * p ); extern Aig_Obj_t * Aig_ObjCreatePo( Aig_Man_t * p, Aig_Obj_t * pDriver ); @@ -341,6 +352,7 @@ extern Aig_Obj_t * Aig_CreateExor( Aig_Man_t * p, int nVars ); extern int Aig_ManSeqStrash( Aig_Man_t * p, int nLatches, int * pInits ); /*=== aigTable.c ========================================================*/ extern Aig_Obj_t * Aig_TableLookup( Aig_Man_t * p, Aig_Obj_t * pGhost ); +extern Aig_Obj_t * Aig_TableLookupTwo( Aig_Man_t * p, Aig_Obj_t * pFanin0, Aig_Obj_t * pFanin1 ); 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 ); @@ -351,10 +363,13 @@ extern void Aig_ManStartReverseLevels( Aig_Man_t * p, int nMaxLevelIn 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 ); +/*=== aigTruth.c ========================================================*/ +extern unsigned * Aig_ManCutTruth( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes, Vec_Ptr_t * vTruthElem, Vec_Ptr_t * vTruthStore ); /*=== aigUtil.c =========================================================*/ extern unsigned Aig_PrimeCudd( unsigned p ); extern void Aig_ManIncrementTravId( Aig_Man_t * p ); extern int Aig_ManLevels( Aig_Man_t * p ); +extern void Aig_ManCheckMarkA( Aig_Man_t * p ); extern void Aig_ManCleanData( Aig_Man_t * p ); extern void Aig_ObjCleanData_rec( Aig_Obj_t * pObj ); extern void Aig_ObjCollectMulti( Aig_Obj_t * pFunc, Vec_Ptr_t * vSuper ); @@ -367,6 +382,8 @@ extern void Aig_ObjPrintVerilog( FILE * pFile, Aig_Obj_t * pObj, Vec_ extern void Aig_ObjPrintVerbose( Aig_Obj_t * pObj, int fHaig ); extern void Aig_ManPrintVerbose( Aig_Man_t * p, int fHaig ); extern void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName ); +/*=== aigWin.c =========================================================*/ +extern void Aig_ManFindCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vVisited, int nSizeLimit, int nFanoutLimit ); /*=== aigMem.c ===========================================================*/ // fixed-size-block memory manager diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c index a71afec6..62900bb5 100644 --- a/src/aig/aig/aigDfs.c +++ b/src/aig/aig/aigDfs.c @@ -433,6 +433,64 @@ Aig_Obj_t * Aig_Compose( Aig_Man_t * p, Aig_Obj_t * pRoot, Aig_Obj_t * pFunc, in return Aig_NotCond( Aig_Regular(pRoot)->pData, Aig_IsComplement(pRoot) ); } +/**Function************************************************************* + + Synopsis [Computes the internal nodes of the cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManCollectCut_rec( Aig_Obj_t * pNode, Vec_Ptr_t * vNodes ) +{ +// Aig_Obj_t * pFan0 = Aig_ObjFanin0(pNode); +// Aig_Obj_t * pFan1 = Aig_ObjFanin1(pNode); + if ( pNode->fMarkA ) + return; + pNode->fMarkA = 1; + assert( Aig_ObjIsNode(pNode) ); + Aig_ManCollectCut_rec( Aig_ObjFanin0(pNode), vNodes ); + Aig_ManCollectCut_rec( Aig_ObjFanin1(pNode), vNodes ); + Vec_PtrPush( vNodes, pNode ); +//printf( "added %d ", pNode->Id ); +} + +/**Function************************************************************* + + Synopsis [Computes the internal nodes of the cut.] + + Description [Does not include the leaves of the cut.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManCollectCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes ) +{ + Aig_Obj_t * pObj; + int i; + // collect and mark the leaves + Vec_PtrClear( vNodes ); + Vec_PtrForEachEntry( vLeaves, pObj, i ) + { + assert( pObj->fMarkA == 0 ); + pObj->fMarkA = 1; +// printf( "%d " , pObj->Id ); + } +//printf( "\n" ); + // collect and mark the nodes + Aig_ManCollectCut_rec( pRoot, vNodes ); + // clean the nodes + Vec_PtrForEachEntry( vNodes, pObj, i ) + pObj->fMarkA = 0; + Vec_PtrForEachEntry( vLeaves, pObj, i ) + pObj->fMarkA = 0; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/aig/aigMffc.c b/src/aig/aig/aigMffc.c new file mode 100644 index 00000000..47ce896d --- /dev/null +++ b/src/aig/aig/aigMffc.c @@ -0,0 +1,297 @@ +/**CFile**************************************************************** + + FileName [aigMffc.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [AIG package.] + + Synopsis [Computation of MFFCs.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 28, 2007.] + + Revision [$Id: aigMffc.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "aig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Dereferences the node's MFFC.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_NodeDeref_rec( Aig_Obj_t * pNode, unsigned LevelMin ) +{ + Aig_Obj_t * pFanin; + int Counter = 0; + if ( Aig_ObjIsPi(pNode) ) + return 0; + // consider the first fanin + pFanin = Aig_ObjFanin0(pNode); + assert( pFanin->nRefs > 0 ); + if ( --pFanin->nRefs == 0 && (!LevelMin || pFanin->Level > LevelMin) ) + Counter += Aig_NodeDeref_rec( pFanin, LevelMin ); + // skip the buffer + if ( Aig_ObjIsBuf(pNode) ) + return Counter; + assert( Aig_ObjIsNode(pNode) ); + // consider the second fanin + pFanin = Aig_ObjFanin1(pNode); + assert( pFanin->nRefs > 0 ); + if ( --pFanin->nRefs == 0 && (!LevelMin || pFanin->Level > LevelMin) ) + Counter += Aig_NodeDeref_rec( pFanin, LevelMin ); + return Counter + 1; +} + +/**Function************************************************************* + + Synopsis [References the node's MFFC.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_NodeRef_rec( Aig_Obj_t * pNode, unsigned LevelMin ) +{ + Aig_Obj_t * pFanin; + int Counter = 0; + if ( Aig_ObjIsPi(pNode) ) + return 0; + // consider the first fanin + pFanin = Aig_ObjFanin0(pNode); + if ( pFanin->nRefs++ == 0 && (!LevelMin || pFanin->Level > LevelMin) ) + Counter += Aig_NodeRef_rec( pFanin, LevelMin ); + // skip the buffer + if ( Aig_ObjIsBuf(pNode) ) + return Counter; + assert( Aig_ObjIsNode(pNode) ); + // consider the second fanin + pFanin = Aig_ObjFanin1(pNode); + if ( pFanin->nRefs++ == 0 && (!LevelMin || pFanin->Level > LevelMin) ) + Counter += Aig_NodeRef_rec( pFanin, LevelMin ); + return Counter + 1; +} + +/**Function************************************************************* + + Synopsis [References the node's MFFC.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_NodeRefLabel_rec( Aig_Man_t * p, Aig_Obj_t * pNode, unsigned LevelMin ) +{ + Aig_Obj_t * pFanin; + int Counter = 0; + if ( Aig_ObjIsPi(pNode) ) + return 0; + Aig_ObjSetTravIdCurrent( p, pNode ); + // consider the first fanin + pFanin = Aig_ObjFanin0(pNode); + if ( pFanin->nRefs++ == 0 && (!LevelMin || pFanin->Level > LevelMin) ) + Counter += Aig_NodeRefLabel_rec( p, pFanin, LevelMin ); + if ( Aig_ObjIsBuf(pNode) ) + return Counter; + assert( Aig_ObjIsNode(pNode) ); + // consider the second fanin + pFanin = Aig_ObjFanin1(pNode); + if ( pFanin->nRefs++ == 0 && (!LevelMin || pFanin->Level > LevelMin) ) + Counter += Aig_NodeRefLabel_rec( p, pFanin, LevelMin ); + return Counter + 1; +} + +/**Function************************************************************* + + Synopsis [Collects the internal and boundary nodes in the derefed MFFC.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_NodeMffsSupp_rec( Aig_Man_t * p, Aig_Obj_t * pNode, unsigned LevelMin, Vec_Ptr_t * vSupp, int fTopmost, Aig_Obj_t * pObjSkip ) +{ + // skip visited nodes + if ( Aig_ObjIsTravIdCurrent(p, pNode) ) + return; + Aig_ObjSetTravIdCurrent(p, pNode); + // add to the new support nodes + if ( !fTopmost && pNode != pObjSkip && (Aig_ObjIsPi(pNode) || pNode->nRefs > 0 || pNode->Level <= LevelMin) ) + { + if ( vSupp ) Vec_PtrPush( vSupp, pNode ); + return; + } + assert( Aig_ObjIsNode(pNode) ); + // recur on the children + Aig_NodeMffsSupp_rec( p, Aig_ObjFanin0(pNode), LevelMin, vSupp, 0, pObjSkip ); + Aig_NodeMffsSupp_rec( p, Aig_ObjFanin1(pNode), LevelMin, vSupp, 0, pObjSkip ); +} + +/**Function************************************************************* + + Synopsis [Collects the support of depth-limited MFFC.] + + Description [Returns the number of internal nodes in the MFFC.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_NodeMffsSupp( Aig_Man_t * p, Aig_Obj_t * pNode, int LevelMin, Vec_Ptr_t * vSupp ) +{ + int ConeSize1, ConeSize2; + assert( !Aig_IsComplement(pNode) ); + assert( Aig_ObjIsNode(pNode) ); + if ( vSupp ) Vec_PtrClear( vSupp ); + Aig_ManIncrementTravId( p ); + ConeSize1 = Aig_NodeDeref_rec( pNode, LevelMin ); + Aig_NodeMffsSupp_rec( p, pNode, LevelMin, vSupp, 1, NULL ); + ConeSize2 = Aig_NodeRef_rec( pNode, LevelMin ); + assert( ConeSize1 == ConeSize2 ); + assert( ConeSize1 > 0 ); + return ConeSize1; +} + +/**Function************************************************************* + + Synopsis [Labels the nodes in the MFFC.] + + Description [Returns the number of internal nodes in the MFFC.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_NodeMffsLabel( Aig_Man_t * p, Aig_Obj_t * pNode ) +{ + int ConeSize1, ConeSize2; + assert( !Aig_IsComplement(pNode) ); + assert( Aig_ObjIsNode(pNode) ); + Aig_ManIncrementTravId( p ); + ConeSize1 = Aig_NodeDeref_rec( pNode, 0 ); + ConeSize2 = Aig_NodeRefLabel_rec( p, pNode, 0 ); + assert( ConeSize1 == ConeSize2 ); + assert( ConeSize1 > 0 ); + return ConeSize1; +} + +/**Function************************************************************* + + Synopsis [Labels the nodes in the MFFC.] + + Description [Returns the number of internal nodes in the MFFC.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_NodeMffsLabelCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves ) +{ + Aig_Obj_t * pObj; + int i, ConeSize1, ConeSize2; + assert( !Aig_IsComplement(pNode) ); + assert( Aig_ObjIsNode(pNode) ); + Aig_ManIncrementTravId( p ); + Vec_PtrForEachEntry( vLeaves, pObj, i ) + pObj->nRefs++; + ConeSize1 = Aig_NodeDeref_rec( pNode, 0 ); + ConeSize2 = Aig_NodeRefLabel_rec( p, pNode, 0 ); + Vec_PtrForEachEntry( vLeaves, pObj, i ) + pObj->nRefs--; + assert( ConeSize1 == ConeSize2 ); + assert( ConeSize1 > 0 ); + return ConeSize1; +} + +/**Function************************************************************* + + Synopsis [Expands the cut by adding the most closely related node.] + + Description [Returns 1 if the cut exists.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_NodeMffsExtendCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vResult ) +{ + Aig_Obj_t * pObj, * pLeafBest; + int i, LevelMax, ConeSize1, ConeSize2, ConeCur1, ConeCur2, ConeBest; + // dereference the current cut + LevelMax = 0; + Vec_PtrForEachEntry( vLeaves, pObj, i ) + LevelMax = AIG_MAX( LevelMax, (int)pObj->Level ); + if ( LevelMax == 0 ) + return 0; + // dereference the cut + ConeSize1 = Aig_NodeDeref_rec( pNode, 0 ); + // try expanding each node in the boundary + ConeBest = AIG_INFINITY; + pLeafBest = NULL; + Vec_PtrForEachEntry( vLeaves, pObj, i ) + { + if ( (int)pObj->Level != LevelMax ) + continue; + ConeCur1 = Aig_NodeDeref_rec( pObj, 0 ); + if ( ConeBest > ConeCur1 ) + { + ConeBest = ConeCur1; + pLeafBest = pObj; + } + ConeCur2 = Aig_NodeRef_rec( pObj, 0 ); + assert( ConeCur1 == ConeCur2 ); + } + assert( pLeafBest != NULL ); + assert( Aig_ObjIsNode(pLeafBest) ); + // deref the best leaf + ConeCur1 = Aig_NodeDeref_rec( pLeafBest, 0 ); + // collect the cut nodes + Vec_PtrClear( vResult ); + Aig_ManIncrementTravId( p ); + Aig_NodeMffsSupp_rec( p, pNode, 0, vResult, 1, pLeafBest ); + // ref the nodes + ConeCur2 = Aig_NodeRef_rec( pLeafBest, 0 ); + assert( ConeCur1 == ConeCur2 ); + // ref the original node + ConeSize2 = Aig_NodeRef_rec( pNode, 0 ); + assert( ConeSize1 == ConeSize2 ); + return 1; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/aig/aigObj.c b/src/aig/aig/aigObj.c index 542b90f9..f2296e01 100644 --- a/src/aig/aig/aigObj.c +++ b/src/aig/aig/aigObj.c @@ -380,12 +380,13 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in // delete the new object Aig_ObjDelete( p, pObjNew ); // update levels - if ( fUpdateLevel ) + if ( p->pFanData ) { pObjOld->Level = LevelOld; Aig_ManUpdateLevel( p, pObjOld ); - Aig_ManUpdateReverseLevel( p, pObjOld ); } + if ( fUpdateLevel ) + Aig_ManUpdateReverseLevel( p, pObjOld ); } p->nObjs[pObjOld->Type]++; // store buffers if fanout is allocated diff --git a/src/aig/aig/aigTable.c b/src/aig/aig/aigTable.c index bba7650a..ba359c09 100644 --- a/src/aig/aig/aigTable.c +++ b/src/aig/aig/aigTable.c @@ -146,6 +146,33 @@ Aig_Obj_t * Aig_TableLookup( Aig_Man_t * p, Aig_Obj_t * pGhost ) /**Function************************************************************* + Synopsis [Checks if node with the given attributes is in the hash table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t * Aig_TableLookupTwo( Aig_Man_t * p, Aig_Obj_t * pFanin0, Aig_Obj_t * pFanin1 ) +{ + Aig_Obj_t * pGhost; + // consider simple cases + if ( pFanin0 == pFanin1 ) + return pFanin0; + if ( pFanin0 == Aig_Not(pFanin1) ) + return Aig_ManConst0(p); + if ( Aig_Regular(pFanin0) == Aig_ManConst1(p) ) + return pFanin0 == Aig_ManConst1(p) ? pFanin1 : Aig_ManConst0(p); + if ( Aig_Regular(pFanin1) == Aig_ManConst1(p) ) + return pFanin1 == Aig_ManConst1(p) ? pFanin0 : Aig_ManConst0(p); + pGhost = Aig_ObjCreateGhost( p, pFanin0, pFanin1, AIG_OBJ_AND ); + return Aig_TableLookup( p, pGhost ); +} + +/**Function************************************************************* + Synopsis [Adds the new node to the hash table.] Description [] diff --git a/src/aig/aig/aigTruth.c b/src/aig/aig/aigTruth.c new file mode 100644 index 00000000..a92f9e1d --- /dev/null +++ b/src/aig/aig/aigTruth.c @@ -0,0 +1,98 @@ +/**CFile**************************************************************** + + FileName [aigTruth.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [AIG package.] + + Synopsis [Computes truth table for the cut.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 28, 2007.] + + Revision [$Id: aigTruth.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "aig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Computes truth table of the cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned * Aig_ManCutTruthOne( Aig_Obj_t * pNode, unsigned * pTruth, int nWords ) +{ + unsigned * pTruth0, * pTruth1; + int i; + pTruth0 = Aig_ObjFanin0(pNode)->pData; + pTruth1 = Aig_ObjFanin1(pNode)->pData; + if ( Aig_ObjIsExor(pNode) ) + for ( i = 0; i < nWords; i++ ) + pTruth[i] = pTruth0[i] ^ pTruth1[i]; + else if ( !Aig_ObjFaninC0(pNode) && !Aig_ObjFaninC1(pNode) ) + for ( i = 0; i < nWords; i++ ) + pTruth[i] = pTruth0[i] & pTruth1[i]; + else if ( !Aig_ObjFaninC0(pNode) && Aig_ObjFaninC1(pNode) ) + for ( i = 0; i < nWords; i++ ) + pTruth[i] = pTruth0[i] & ~pTruth1[i]; + else if ( Aig_ObjFaninC0(pNode) && !Aig_ObjFaninC1(pNode) ) + for ( i = 0; i < nWords; i++ ) + pTruth[i] = ~pTruth0[i] & pTruth1[i]; + else // if ( Aig_ObjFaninC0(pNode) && Aig_ObjFaninC1(pNode) ) + for ( i = 0; i < nWords; i++ ) + pTruth[i] = ~pTruth0[i] & ~pTruth1[i]; + return pTruth; +} + +/**Function************************************************************* + + Synopsis [Computes truth table of the cut.] + + Description [The returned pointer should be used immediately.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned * Aig_ManCutTruth( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes, Vec_Ptr_t * vTruthElem, Vec_Ptr_t * vTruthStore ) +{ + Aig_Obj_t * pObj; + int i, nWords; + assert( Vec_PtrSize(vLeaves) <= Vec_PtrSize(vTruthElem) ); + assert( Vec_PtrSize(vNodes) <= Vec_PtrSize(vTruthStore) ); + assert( Vec_PtrSize(vNodes) == 0 || pRoot == Vec_PtrEntryLast(vNodes) ); + // assign elementary truth tables + Vec_PtrForEachEntry( vLeaves, pObj, i ) + pObj->pData = Vec_PtrEntry( vTruthElem, i ); + // compute truths for other nodes + nWords = Aig_TruthWordNum( Vec_PtrSize(vLeaves) ); + Vec_PtrForEachEntry( vNodes, pObj, i ) + pObj->pData = Aig_ManCutTruthOne( pObj, Vec_PtrEntry(vTruthStore, i), nWords ); + return pRoot->pData; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c index 1e45bca1..a1c68371 100644 --- a/src/aig/aig/aigUtil.c +++ b/src/aig/aig/aigUtil.c @@ -104,6 +104,25 @@ int Aig_ManLevels( Aig_Man_t * p ) /**Function************************************************************* + Synopsis [Checks if the markA is reset.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManCheckMarkA( Aig_Man_t * p ) +{ + Aig_Obj_t * pObj; + int i; + Aig_ManForEachObj( p, pObj, i ) + assert( pObj->fMarkA == 0 ); +} + +/**Function************************************************************* + Synopsis [Cleans the data pointers for the nodes.] Description [] @@ -144,6 +163,7 @@ void Aig_ObjCleanData_rec( Aig_Obj_t * pObj ) pObj->pData = NULL; } + /**Function************************************************************* Synopsis [Detects multi-input gate rooted at this node.] diff --git a/src/aig/aig/aigWin.c b/src/aig/aig/aigWin.c new file mode 100644 index 00000000..0485b243 --- /dev/null +++ b/src/aig/aig/aigWin.c @@ -0,0 +1,184 @@ +/**CFile**************************************************************** + + FileName [aigWin.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [AIG package.] + + Synopsis [Window computation.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 28, 2007.] + + Revision [$Id: aigWin.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "aig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Evaluate the cost of removing the node from the set of leaves.] + + Description [Returns the number of new leaves that will be brought in. + Returns large number if the node cannot be removed from the set of leaves.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Aig_NodeGetLeafCostOne( Aig_Obj_t * pNode, int nFanoutLimit ) +{ + int Cost; + // make sure the node is in the construction zone + assert( pNode->fMarkA ); + // cannot expand over the PI node + if ( Aig_ObjIsPi(pNode) ) + return 999; + // get the cost of the cone + Cost = (!Aig_ObjFanin0(pNode)->fMarkA) + (!Aig_ObjFanin1(pNode)->fMarkA); + // always accept if the number of leaves does not increase + if ( Cost < 2 ) + return Cost; + // skip nodes with many fanouts + if ( (int)pNode->nRefs > nFanoutLimit ) + return 999; + // return the number of nodes that will be on the leaves if this node is removed + return Cost; +} + +/**Function************************************************************* + + Synopsis [Builds reconvergence-driven cut by changing one leaf at a time.] + + Description [This procedure looks at the current leaves and tries to change + one leaf at a time in such a way that the cut grows as little as possible. + In evaluating the fanins, this procedure looks only at their immediate + predecessors (this is why it is called a one-level construction procedure).] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ManFindCut_int( Vec_Ptr_t * vFront, Vec_Ptr_t * vVisited, int nSizeLimit, int nFanoutLimit ) +{ + Aig_Obj_t * pNode, * pFaninBest, * pNext; + int CostBest, CostCur, i; + // find the best fanin + CostBest = 100; + pFaninBest = NULL; +//printf( "Evaluating fanins of the cut:\n" ); + Vec_PtrForEachEntry( vFront, pNode, i ) + { + CostCur = Aig_NodeGetLeafCostOne( pNode, nFanoutLimit ); +//printf( " Fanin %s has cost %d.\n", Aig_ObjName(pNode), CostCur ); + if ( CostBest > CostCur || + (CostBest == CostCur && pNode->Level > pFaninBest->Level) ) + { + CostBest = CostCur; + pFaninBest = pNode; + } + if ( CostBest == 0 ) + break; + } + if ( pFaninBest == NULL ) + return 0; + assert( CostBest < 3 ); + if ( Vec_PtrSize(vFront) - 1 + CostBest > nSizeLimit ) + return 0; + assert( Aig_ObjIsNode(pFaninBest) ); + // remove the node from the array + Vec_PtrRemove( vFront, pFaninBest ); +//printf( "Removing fanin %s.\n", Aig_ObjName(pFaninBest) ); + + // add the left child to the fanins + pNext = Aig_ObjFanin0(pFaninBest); + if ( !pNext->fMarkA ) + { +//printf( "Adding fanin %s.\n", Aig_ObjName(pNext) ); + pNext->fMarkA = 1; + Vec_PtrPush( vFront, pNext ); + Vec_PtrPush( vVisited, pNext ); + } + // add the right child to the fanins + pNext = Aig_ObjFanin1(pFaninBest); + if ( !pNext->fMarkA ) + { +//printf( "Adding fanin %s.\n", Aig_ObjName(pNext) ); + pNext->fMarkA = 1; + Vec_PtrPush( vFront, pNext ); + Vec_PtrPush( vVisited, pNext ); + } + assert( Vec_PtrSize(vFront) <= nSizeLimit ); + // keep doing this + return 1; +} + +/**Function************************************************************* + + Synopsis [Computes one sequential cut of the given size.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManFindCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vVisited, int nSizeLimit, int nFanoutLimit ) +{ + Aig_Obj_t * pNode; + int i; + + assert( !Aig_IsComplement(pRoot) ); + assert( Aig_ObjIsNode(pRoot) ); + assert( Aig_ObjChild0(pRoot) ); + assert( Aig_ObjChild1(pRoot) ); + + // start the cut + Vec_PtrClear( vFront ); + Vec_PtrPush( vFront, Aig_ObjFanin0(pRoot) ); + Vec_PtrPush( vFront, Aig_ObjFanin1(pRoot) ); + + // start the visited nodes + Vec_PtrClear( vVisited ); + Vec_PtrPush( vVisited, pRoot ); + Vec_PtrPush( vVisited, Aig_ObjFanin0(pRoot) ); + Vec_PtrPush( vVisited, Aig_ObjFanin1(pRoot) ); + + // mark these nodes + assert( !pRoot->fMarkA ); + assert( !Aig_ObjFanin0(pRoot)->fMarkA ); + assert( !Aig_ObjFanin1(pRoot)->fMarkA ); + pRoot->fMarkA = 1; + Aig_ObjFanin0(pRoot)->fMarkA = 1; + Aig_ObjFanin1(pRoot)->fMarkA = 1; + + // compute the cut + while ( Aig_ManFindCut_int( vFront, vVisited, nSizeLimit, nFanoutLimit ) ); + assert( Vec_PtrSize(vFront) <= nSizeLimit ); + + // clean the visit markings + Vec_PtrForEachEntry( vVisited, pNode, i ) + pNode->fMarkA = 0; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/aig/module.make b/src/aig/aig/module.make index f9afc4ee..83e4c413 100644 --- a/src/aig/aig/module.make +++ b/src/aig/aig/module.make @@ -2,10 +2,13 @@ SRC += src/aig/aig/aigCheck.c \ src/aig/aig/aigDfs.c \ src/aig/aig/aigFanout.c \ src/aig/aig/aigMan.c \ + src/aig/aig/aigMffc.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 + src/aig/aig/aigTruth.c \ + src/aig/aig/aigUtil.c \ + src/aig/aig/aigWin.c diff --git a/src/aig/dar/dar.h b/src/aig/dar/dar.h index cff2785b..3106c7ad 100644 --- a/src/aig/dar/dar.h +++ b/src/aig/dar/dar.h @@ -37,10 +37,10 @@ extern "C" { /// BASIC TYPES /// //////////////////////////////////////////////////////////////////////// -typedef struct Dar_Par_t_ Dar_Par_t; +typedef struct Dar_RwrPar_t_ Dar_RwrPar_t; +typedef struct Dar_RefPar_t_ Dar_RefPar_t; -// the rewriting parameters -struct Dar_Par_t_ +struct Dar_RwrPar_t_ { int nCutsMax; // the maximum number of cuts to try int nSubgMax; // the maximum number of subgraphs to try @@ -50,6 +50,18 @@ struct Dar_Par_t_ int fVeryVerbose; // enables very verbose output }; +struct Dar_RefPar_t_ +{ + int nMffcMin; // the min MFFC size for which refactoring is used + int nLeafMax; // the max number of leaves of a cut + int nCutsMax; // the max number of cuts to consider + int fExtend; // extends the cut below MFFC + int fUpdateLevel; // updates the level after each move + int fUseZeros; // perform zero-cost replacements + int fVerbose; // verbosity level + int fVeryVerbose; // enables very verbose output +}; + //////////////////////////////////////////////////////////////////////// /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -62,10 +74,17 @@ struct Dar_Par_t_ /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +/*=== darBalance.c ========================================================*/ +extern Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel ); /*=== darCore.c ========================================================*/ -extern void Dar_ManDefaultParams( Dar_Par_t * pPars ); -extern int Dar_ManRewrite( Aig_Man_t * pAig, Dar_Par_t * pPars ); +extern void Dar_ManDefaultRwrParams( Dar_RwrPar_t * pPars ); +extern int Dar_ManRewrite( Aig_Man_t * pAig, Dar_RwrPar_t * pPars ); extern Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig ); +/*=== darRefact.c ========================================================*/ +extern void Dar_ManDefaultRefParams( Dar_RefPar_t * pPars ); +extern int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars ); +/*=== darScript.c ========================================================*/ +extern Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fVerbose ); #ifdef __cplusplus } diff --git a/src/aig/dar/darCore.c b/src/aig/dar/darCore.c index e7186e83..7546df0b 100644 --- a/src/aig/dar/darCore.c +++ b/src/aig/dar/darCore.c @@ -39,15 +39,15 @@ SeeAlso [] ***********************************************************************/ -void Dar_ManDefaultParams( Dar_Par_t * pPars ) +void Dar_ManDefaultRwrParams( Dar_RwrPar_t * pPars ) { - memset( pPars, 0, sizeof(Dar_Par_t) ); - pPars->nCutsMax = 8; - pPars->nSubgMax = 5; // 5 is a "magic number" - pPars->fUpdateLevel = 0; - pPars->fUseZeros = 0; - pPars->fVerbose = 0; - pPars->fVeryVerbose = 0; + memset( pPars, 0, sizeof(Dar_RwrPar_t) ); + pPars->nCutsMax = 8; + pPars->nSubgMax = 5; // 5 is a "magic number" + pPars->fUpdateLevel = 0; + pPars->fUseZeros = 0; + pPars->fVerbose = 0; + pPars->fVeryVerbose = 0; } /**Function************************************************************* @@ -61,7 +61,7 @@ void Dar_ManDefaultParams( Dar_Par_t * pPars ) SeeAlso [] ***********************************************************************/ -int Dar_ManRewrite( Aig_Man_t * pAig, Dar_Par_t * pPars ) +int Dar_ManRewrite( Aig_Man_t * pAig, Dar_RwrPar_t * pPars ) { Dar_Man_t * p; ProgressBar * pProgress; @@ -128,7 +128,7 @@ p->timeCuts += clock() - clk; // evaluate the cuts p->GainBest = -1; - Required = 1000000; + Required = pAig->vLevelR? Aig_ObjRequiredLevel(pAig, pObj) : AIG_INFINITY; Dar_ObjForEachCut( pObj, pCut, k ) Dar_LibEval( p, pObj, pCut, Required ); // check the best gain diff --git a/src/aig/dar/darInt.h b/src/aig/dar/darInt.h index f496a73f..0acd272c 100644 --- a/src/aig/dar/darInt.h +++ b/src/aig/dar/darInt.h @@ -64,8 +64,8 @@ struct Dar_Cut_t_ // 6 words // the AIG manager struct Dar_Man_t_ { - // input data; - Dar_Par_t * pPars; // rewriting parameters + // input data + Dar_RwrPar_t * pPars; // rewriting parameters Aig_Man_t * pAig; // AIG manager // various data members Aig_MmFixed_t * pMemCuts; // memory manager for cuts @@ -125,7 +125,6 @@ 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 void Dar_ManCutsStart( Dar_Man_t * p ); @@ -144,7 +143,7 @@ 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 ============================================================*/ -extern Dar_Man_t * Dar_ManStart( Aig_Man_t * pAig, Dar_Par_t * pPars ); +extern Dar_Man_t * Dar_ManStart( Aig_Man_t * pAig, Dar_RwrPar_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 c3d57b52..72ce0cde 100644 --- a/src/aig/dar/darLib.c +++ b/src/aig/dar/darLib.c @@ -707,65 +707,6 @@ int Dar_LibCutMatch( Dar_Man_t * p, Dar_Cut_t * pCut ) /**Function************************************************************* - Synopsis [Dereferences the node's MFFC.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Aig_NodeDeref_rec( Aig_Man_t * p, Aig_Obj_t * pNode ) -{ - Aig_Obj_t * pFanin; - int Counter = 0; - if ( Aig_ObjIsPi(pNode) ) - return Counter; - pFanin = Aig_ObjFanin0( pNode ); - assert( pFanin->nRefs > 0 ); - if ( --pFanin->nRefs == 0 ) - Counter += Aig_NodeDeref_rec( p, pFanin ); - if ( Aig_ObjIsBuf(pNode) ) - return Counter; - pFanin = Aig_ObjFanin1( pNode ); - assert( pFanin->nRefs > 0 ); - if ( --pFanin->nRefs == 0 ) - Counter += Aig_NodeDeref_rec( p, pFanin ); - return 1 + Counter; -} - -/**Function************************************************************* - - Synopsis [References the node's MFFC.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Aig_NodeRef_rec( Aig_Man_t * p, Aig_Obj_t * pNode ) -{ - Aig_Obj_t * pFanin; - int Counter = 0; - if ( Aig_ObjIsPi(pNode) ) - return Counter; - Aig_ObjSetTravIdCurrent( p, pNode ); - pFanin = Aig_ObjFanin0( pNode ); - if ( pFanin->nRefs++ == 0 ) - Counter += Aig_NodeRef_rec( p, pFanin ); - if ( Aig_ObjIsBuf(pNode) ) - return Counter; - pFanin = Aig_ObjFanin1( pNode ); - if ( pFanin->nRefs++ == 0 ) - Counter += Aig_NodeRef_rec( p, pFanin ); - return 1 + Counter; -} - -/**Function************************************************************* - Synopsis [Marks the MFFC of the node.] Description [] @@ -777,19 +718,16 @@ int Aig_NodeRef_rec( Aig_Man_t * p, Aig_Obj_t * pNode ) ***********************************************************************/ int Dar_LibCutMarkMffc( Aig_Man_t * p, Aig_Obj_t * pRoot, int nLeaves ) { - int i, nNodes1, nNodes2; + int i, nNodes; // mark the cut leaves for ( i = 0; i < nLeaves; i++ ) Aig_Regular(s_DarLib->pDatas[i].pFunc)->nRefs++; // label MFFC with current ID - Aig_ManIncrementTravId( p ); - nNodes1 = Aig_NodeDeref_rec( p, pRoot ); - nNodes2 = Aig_NodeRef_rec( p, pRoot ); - assert( nNodes1 == nNodes2 ); + nNodes = Aig_NodeMffsLabel( p, pRoot ); // unmark the cut leaves for ( i = 0; i < nLeaves; i++ ) Aig_Regular(s_DarLib->pDatas[i].pFunc)->nRefs--; - return nNodes1; + return nNodes; } /**Function************************************************************* @@ -836,7 +774,7 @@ void Dar_LibEvalAssignNums( Dar_Man_t * p, int Class ) { Dar_LibObj_t * pObj; Dar_LibDat_t * pData, * pData0, * pData1; - Aig_Obj_t * pGhost, * pFanin0, * pFanin1; + Aig_Obj_t * pFanin0, * pFanin1; int i; for ( i = 0; i < s_DarLib->nNodes0[Class]; i++ ) { @@ -859,22 +797,7 @@ void Dar_LibEvalAssignNums( Dar_Man_t * p, int Class ) continue; pFanin0 = Aig_NotCond( pData0->pFunc, pObj->fCompl0 ); pFanin1 = Aig_NotCond( pData1->pFunc, pObj->fCompl1 ); - - // consider simple cases - if ( pFanin0 == pFanin1 ) - pData->pFunc = pFanin0; - else if ( pFanin0 == Aig_Not(pFanin1) ) - pData->pFunc = Aig_ManConst0(p->pAig); - else if ( Aig_Regular(pFanin0) == Aig_ManConst1(p->pAig) ) - pData->pFunc = pFanin0 == Aig_ManConst1(p->pAig) ? pFanin1 : Aig_ManConst0(p->pAig); - else if ( Aig_Regular(pFanin1) == Aig_ManConst1(p->pAig) ) - pData->pFunc = pFanin1 == Aig_ManConst1(p->pAig) ? pFanin0 : Aig_ManConst0(p->pAig); - else - { - pGhost = Aig_ObjCreateGhost( p->pAig, pFanin0, pFanin1, AIG_OBJ_AND ); - pData->pFunc = Aig_TableLookup( p->pAig, pGhost ); - } - + pData->pFunc = Aig_TableLookupTwo( p->pAig, pFanin0, pFanin1 ); // clear the node if it is part of MFFC if ( pData->pFunc != NULL && Aig_ObjIsTravIdCurrent(p->pAig, pData->pFunc) ) pData->fMffc = 1; diff --git a/src/aig/dar/darMan.c b/src/aig/dar/darMan.c index 8b7c5afb..ef898ea2 100644 --- a/src/aig/dar/darMan.c +++ b/src/aig/dar/darMan.c @@ -39,7 +39,7 @@ SeeAlso [] ***********************************************************************/ -Dar_Man_t * Dar_ManStart( Aig_Man_t * pAig, Dar_Par_t * pPars ) +Dar_Man_t * Dar_ManStart( Aig_Man_t * pAig, Dar_RwrPar_t * pPars ) { Dar_Man_t * p; // start the manager diff --git a/src/aig/dar/darRefact.c b/src/aig/dar/darRefact.c index 1bcc0466..cdfbaa01 100644 --- a/src/aig/dar/darRefact.c +++ b/src/aig/dar/darRefact.c @@ -19,17 +19,151 @@ ***********************************************************************/ #include "darInt.h" +#include "kit.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +// the refactoring manager +typedef struct Ref_Man_t_ Ref_Man_t; +struct Ref_Man_t_ +{ + // input data + Dar_RefPar_t * pPars; // rewriting parameters + Aig_Man_t * pAig; // AIG manager + // computed cuts + Vec_Vec_t * vCuts; // the storage for cuts + // truth table and ISOP + Vec_Ptr_t * vTruthElem; // elementary truth tables + Vec_Ptr_t * vTruthStore; // storage for truth tables + Vec_Int_t * vMemory; // storage for ISOP + Vec_Ptr_t * vCutNodes; // storage for internal nodes of the cut + // various data members + Vec_Ptr_t * vLeavesBest; // the best set of leaves + Kit_Graph_t * pGraphBest; // the best factored form + int GainBest; // the best gain + int LevelBest; // the level of node with the best gain + // node statistics + int nNodesInit; // the initial number of nodes + int nNodesTried; // the number of nodes tried + int nNodesBelow; // the number of nodes below the level limit + int nNodesExten; // the number of nodes with extended cut + int nCutsUsed; // the number of rewriting steps + int nCutsTried; // the number of cuts tries + // timing statistics + int timeCuts; + int timeEval; + int timeOther; + int timeTotal; +}; + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* + Synopsis [Returns the structure with default assignment of parameters.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dar_ManDefaultRefParams( Dar_RefPar_t * pPars ) +{ + memset( pPars, 0, sizeof(Dar_RefPar_t) ); + pPars->nMffcMin = 2; // the min MFFC size for which refactoring is used + pPars->nLeafMax = 12; // the max number of leaves of a cut + pPars->nCutsMax = 5; // the max number of cuts to consider + pPars->fUpdateLevel = 0; + pPars->fUseZeros = 0; + pPars->fVerbose = 0; + pPars->fVeryVerbose = 0; +} + +/**Function************************************************************* + + Synopsis [Starts the rewriting manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ref_Man_t * Dar_ManRefStart( Aig_Man_t * pAig, Dar_RefPar_t * pPars ) +{ + Ref_Man_t * p; + // start the manager + p = ALLOC( Ref_Man_t, 1 ); + memset( p, 0, sizeof(Ref_Man_t) ); + p->pAig = pAig; + p->pPars = pPars; + // other data + p->vCuts = Vec_VecStart( pPars->nCutsMax ); + p->vTruthElem = Vec_PtrAllocTruthTables( pPars->nLeafMax ); + p->vTruthStore = Vec_PtrAllocSimInfo( 256, Kit_TruthWordNum(pPars->nLeafMax) ); + p->vMemory = Vec_IntAlloc( 1 << 16 ); + p->vCutNodes = Vec_PtrAlloc( 256 ); + p->vLeavesBest = Vec_PtrAlloc( pPars->nLeafMax ); + return p; +} + +/**Function************************************************************* + + Synopsis [Prints out the statistics of the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dar_ManRefPrintStats( Ref_Man_t * p ) +{ + int Gain = p->nNodesInit - Aig_ManNodeNum(p->pAig); + printf( "NodesBeg = %8d. NodesEnd = %8d. Gain = %6d. (%6.2f %%).\n", + p->nNodesInit, Aig_ManNodeNum(p->pAig), Gain, 100.0*Gain/p->nNodesInit ); + printf( "Tried = %6d. Below = %5d. Extended = %5d. Used = %5d.\n", + p->nNodesTried, p->nNodesBelow, p->nNodesExten, p->nCutsUsed ); + PRT( "Cuts ", p->timeCuts ); + PRT( "Eval ", p->timeEval ); + PRT( "Other ", p->timeOther ); + PRT( "TOTAL ", p->timeTotal ); +} + +/**Function************************************************************* + + Synopsis [Stops the rewriting manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dar_ManRefStop( Ref_Man_t * p ) +{ + if ( p->pPars->fVerbose ) + Dar_ManRefPrintStats( p ); + Vec_VecFree( p->vCuts ); + Vec_PtrFree( p->vTruthElem ); + Vec_PtrFree( p->vTruthStore ); + Vec_PtrFree( p->vLeavesBest ); + Vec_IntFree( p->vMemory ); + Vec_PtrFree( p->vCutNodes ); + free( p ); +} + +/**Function************************************************************* + Synopsis [] Description [] @@ -39,7 +173,405 @@ SeeAlso [] ***********************************************************************/ +void Ref_ObjComputeCuts( Aig_Man_t * pAig, Aig_Obj_t * pRoot, Vec_Vec_t * vCuts ) +{ +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ref_ObjPrint( Aig_Obj_t * pObj ) +{ + printf( "%d", pObj? Aig_Regular(pObj)->Id : -1 ); + if ( pObj ) + printf( "(%d) ", Aig_IsComplement(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Counts the number of new nodes added when using this graph.] + + Description [AIG nodes for the fanins should be assigned to pNode->pFunc + of the leaves of the graph before calling this procedure. + Returns -1 if the number of nodes and levels exceeded the given limit or + the number of levels exceeded the maximum allowed level.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dar_RefactTryGraph( Aig_Man_t * pAig, Aig_Obj_t * pRoot, Vec_Ptr_t * vCut, Kit_Graph_t * pGraph, int NodeMax, int LevelMax ) +{ + Kit_Node_t * pNode, * pNode0, * pNode1; + Aig_Obj_t * pAnd, * pAnd0, * pAnd1; + int i, Counter, LevelNew, LevelOld; + // check for constant function or a literal + if ( Kit_GraphIsConst(pGraph) || Kit_GraphIsVar(pGraph) ) + return 0; + // set the levels of the leaves + Kit_GraphForEachLeaf( pGraph, pNode, i ) + { + pNode->pFunc = Vec_PtrEntry(vCut, i); + pNode->Level = Aig_Regular(pNode->pFunc)->Level; + assert( Aig_Regular(pNode->pFunc)->Level < (1<<14)-1 ); + } +//printf( "Trying:\n" ); + // compute the AIG size after adding the internal nodes + Counter = 0; + Kit_GraphForEachNode( pGraph, pNode, i ) + { + // get the children of this node + pNode0 = Kit_GraphNode( pGraph, pNode->eEdge0.Node ); + pNode1 = Kit_GraphNode( pGraph, pNode->eEdge1.Node ); + // get the AIG nodes corresponding to the children + pAnd0 = pNode0->pFunc; + pAnd1 = pNode1->pFunc; + if ( pAnd0 && pAnd1 ) + { + // if they are both present, find the resulting node + pAnd0 = Aig_NotCond( pAnd0, pNode->eEdge0.fCompl ); + pAnd1 = Aig_NotCond( pAnd1, pNode->eEdge1.fCompl ); + pAnd = Aig_TableLookupTwo( pAig, pAnd0, pAnd1 ); + // return -1 if the node is the same as the original root + if ( Aig_Regular(pAnd) == pRoot ) + return -1; + } + else + pAnd = NULL; + // count the number of added nodes + if ( pAnd == NULL || Aig_ObjIsTravIdCurrent(pAig, Aig_Regular(pAnd)) ) + { + if ( ++Counter > NodeMax ) + return -1; + } + // count the number of new levels + LevelNew = 1 + AIG_MAX( pNode0->Level, pNode1->Level ); + if ( pAnd ) + { + if ( Aig_Regular(pAnd) == Aig_ManConst1(pAig) ) + LevelNew = 0; + else if ( Aig_Regular(pAnd) == Aig_Regular(pAnd0) ) + LevelNew = (int)Aig_Regular(pAnd0)->Level; + else if ( Aig_Regular(pAnd) == Aig_Regular(pAnd1) ) + LevelNew = (int)Aig_Regular(pAnd1)->Level; + LevelOld = (int)Aig_Regular(pAnd)->Level; +// assert( LevelNew == LevelOld ); + } + if ( LevelNew > LevelMax ) + return -1; + pNode->pFunc = pAnd; + pNode->Level = LevelNew; +/* +printf( "Checking " ); +Ref_ObjPrint( pAnd0 ); +printf( " and " ); +Ref_ObjPrint( pAnd1 ); +printf( " Result " ); +Ref_ObjPrint( pNode->pFunc ); +printf( "\n" ); +*/ + } + return Counter; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t * Dar_RefactBuildGraph( Aig_Man_t * pAig, Vec_Ptr_t * vCut, Kit_Graph_t * pGraph ) +{ + Aig_Obj_t * pAnd0, * pAnd1; + Kit_Node_t * pNode; + int i; + // check for constant function + if ( Kit_GraphIsConst(pGraph) ) + return Aig_NotCond( Aig_ManConst1(pAig), Kit_GraphIsComplement(pGraph) ); + // set the leaves + Kit_GraphForEachLeaf( pGraph, pNode, i ) + pNode->pFunc = Vec_PtrEntry(vCut, i); + // check for a literal + if ( Kit_GraphIsVar(pGraph) ) + return Aig_NotCond( Kit_GraphVar(pGraph)->pFunc, Kit_GraphIsComplement(pGraph) ); + // build the AIG nodes corresponding to the AND gates of the graph +//printf( "Building (current number %d):\n", Aig_ManObjIdMax(pAig) ); + Kit_GraphForEachNode( pGraph, pNode, i ) + { + pAnd0 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl ); + pAnd1 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl ); + pNode->pFunc = Aig_And( pAig, pAnd0, pAnd1 ); +/* +printf( "Checking " ); +Ref_ObjPrint( pAnd0 ); +printf( " and " ); +Ref_ObjPrint( pAnd1 ); +printf( " Result " ); +Ref_ObjPrint( pNode->pFunc ); +printf( "\n" ); +*/ + } + // complement the result if necessary + return Aig_NotCond( pNode->pFunc, Kit_GraphIsComplement(pGraph) ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dar_ManRefactorTryCuts( Ref_Man_t * p, Aig_Obj_t * pObj, int nNodesSaved, int Required ) +{ + Vec_Ptr_t * vCut; + Kit_Graph_t * pGraphCur; + int k, RetValue, GainCur, nNodesAdded; + unsigned * pTruth; + + p->GainBest = -1; + p->pGraphBest = NULL; + Vec_VecForEachLevel( p->vCuts, vCut, k ) + { + if ( Vec_PtrSize(vCut) == 0 ) + continue; +// if ( Vec_PtrSize(vCut) != 0 && Vec_PtrSize(Vec_VecEntry(p->vCuts, k+1)) != 0 ) +// continue; + + p->nCutsTried++; + // get the cut nodes + Aig_ManCollectCut( pObj, vCut, p->vCutNodes ); + // get the truth table + pTruth = Aig_ManCutTruth( pObj, vCut, p->vCutNodes, p->vTruthElem, p->vTruthStore ); + // try the positive phase + RetValue = Kit_TruthIsop( pTruth, Vec_PtrSize(vCut), p->vMemory, 0 ); + if ( RetValue > -1 ) + { + pGraphCur = Kit_SopFactor( p->vMemory, 0, Vec_PtrSize(vCut), p->vMemory ); + nNodesAdded = Dar_RefactTryGraph( p->pAig, pObj, vCut, pGraphCur, nNodesSaved - !p->pPars->fUseZeros, Required ); + if ( nNodesAdded > -1 ) + { + GainCur = nNodesSaved - nNodesAdded; + if ( p->GainBest < GainCur || (p->GainBest == GainCur && + (Kit_GraphIsConst(pGraphCur) || Kit_GraphRootLevel(pGraphCur) < Kit_GraphRootLevel(p->pGraphBest))) ) + { + p->GainBest = GainCur; + if ( p->pGraphBest ) + Kit_GraphFree( p->pGraphBest ); + p->pGraphBest = pGraphCur; + Vec_PtrCopy( p->vLeavesBest, vCut ); + } + else + Kit_GraphFree( pGraphCur ); + } + else + Kit_GraphFree( pGraphCur ); + } + // try negative phase + Kit_TruthNot( pTruth, pTruth, Vec_PtrSize(vCut) ); + RetValue = Kit_TruthIsop( pTruth, Vec_PtrSize(vCut), p->vMemory, 0 ); + if ( RetValue > -1 ) + { + pGraphCur = Kit_SopFactor( p->vMemory, 1, Vec_PtrSize(vCut), p->vMemory ); + nNodesAdded = Dar_RefactTryGraph( p->pAig, pObj, vCut, pGraphCur, nNodesSaved - !p->pPars->fUseZeros, Required ); + if ( nNodesAdded > -1 ) + { + GainCur = nNodesSaved - nNodesAdded; + if ( p->GainBest < GainCur || (p->GainBest == GainCur && + (Kit_GraphIsConst(pGraphCur) || Kit_GraphRootLevel(pGraphCur) < Kit_GraphRootLevel(p->pGraphBest))) ) + { + p->GainBest = GainCur; + if ( p->pGraphBest ) + Kit_GraphFree( p->pGraphBest ); + p->pGraphBest = pGraphCur; + Vec_PtrCopy( p->vLeavesBest, vCut ); + } + else + Kit_GraphFree( pGraphCur ); + } + else + Kit_GraphFree( pGraphCur ); + } + } + return p->GainBest; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if a non-PI node has nLevelMin or below.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dar_ObjCutLevelAchieved( Vec_Ptr_t * vCut, int nLevelMin ) +{ + Aig_Obj_t * pObj; + int i; + Vec_PtrForEachEntry( vCut, pObj, i ) + if ( !Aig_ObjIsPi(pObj) && (int)pObj->Level <= nLevelMin ) + return 1; + return 0; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars ) +{ + ProgressBar * pProgress; + Ref_Man_t * p; + Vec_Ptr_t * vCut, * vCut2; + Aig_Obj_t * pObj, * pObjNew; + int nNodesOld, nNodeBefore, nNodeAfter, nNodesSaved, nNodesSaved2; + int i, Required, nLevelMin, clkStart, clk; + + // start the manager + p = Dar_ManRefStart( 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 ); + + // resynthesize each node once + clkStart = clock(); + vCut = Vec_VecEntry( p->vCuts, 0 ); + vCut2 = Vec_VecEntry( p->vCuts, 1 ); + p->nNodesInit = Aig_ManNodeNum(pAig); + nNodesOld = Vec_PtrSize( pAig->vObjs ); + pProgress = Extra_ProgressBarStart( stdout, nNodesOld ); + Aig_ManForEachObj( pAig, pObj, i ) + { + Extra_ProgressBarUpdate( pProgress, i, NULL ); + if ( !Aig_ObjIsNode(pObj) ) + continue; + if ( i > nNodesOld ) + break; + Vec_VecClear( p->vCuts ); + + if ( pObj->Id == 738 ) + { + int x = 0; + } + +//printf( "\nConsidering node %d.\n", pObj->Id ); + // get the bounded MFFC size +clk = clock(); + nLevelMin = AIG_MAX( 0, Aig_ObjLevel(pObj) - 10 ); + nNodesSaved = Aig_NodeMffsSupp( pAig, pObj, nLevelMin, vCut ); + if ( nNodesSaved < p->pPars->nMffcMin ) // too small to consider + { +p->timeCuts += clock() - clk; + continue; + } + p->nNodesTried++; + if ( Vec_PtrSize(vCut) > p->pPars->nLeafMax ) // get one reconv-driven cut + { + Aig_ManFindCut( pObj, vCut, p->vCutNodes, p->pPars->nLeafMax, 50 ); + nNodesSaved = Aig_NodeMffsLabelCut( p->pAig, pObj, vCut ); + } + else if ( Vec_PtrSize(vCut) < p->pPars->nLeafMax - 2 && p->pPars->fExtend ) + { + if ( !Dar_ObjCutLevelAchieved(vCut, nLevelMin) ) + { + if ( Aig_NodeMffsExtendCut( pAig, pObj, vCut, vCut2 ) ) + { + nNodesSaved2 = Aig_NodeMffsLabelCut( p->pAig, pObj, vCut ); + assert( nNodesSaved2 == nNodesSaved ); + } + if ( Vec_PtrSize(vCut2) > p->pPars->nLeafMax ) + Vec_PtrClear(vCut2); + if ( Vec_PtrSize(vCut2) > 0 ) + { + p->nNodesExten++; +// printf( "%d(%d) ", Vec_PtrSize(vCut), Vec_PtrSize(vCut2) ); + } + } + else + p->nNodesBelow++; + } +p->timeCuts += clock() - clk; + + // try the cuts +clk = clock(); + Required = pAig->vLevelR? Aig_ObjRequiredLevel(pAig, pObj) : AIG_INFINITY; + Dar_ManRefactorTryCuts( p, pObj, nNodesSaved, Required ); +p->timeEval += clock() - clk; + + // check the best gain + if ( !(p->GainBest > 0 || (p->GainBest == 0 && p->pPars->fUseZeros)) ) + { + if ( p->pGraphBest ) + Kit_GraphFree( p->pGraphBest ); + continue; + } +//printf( "\n" ); + + // if we end up here, a rewriting step is accepted + nNodeBefore = Aig_ManNodeNum( pAig ); + pObjNew = Dar_RefactBuildGraph( pAig, p->vLeavesBest, p->pGraphBest ); + assert( (int)Aig_Regular(pObjNew)->Level <= Required ); + // replace the node + Aig_ObjReplace( pAig, pObj, pObjNew, 1, p->pPars->fUpdateLevel ); + // compare the gains + nNodeAfter = Aig_ManNodeNum( pAig ); + assert( p->GainBest <= nNodeBefore - nNodeAfter ); + Kit_GraphFree( p->pGraphBest ); + p->nCutsUsed++; +// break; + } +p->timeTotal = clock() - clkStart; +p->timeOther = p->timeTotal - p->timeCuts - p->timeEval; + + Extra_ProgressBarStop( pProgress ); + // put the nodes into the DFS order and reassign their IDs +// Aig_NtkReassignIds( p ); + // fix the levels + Aig_ManDeleteFanout( pAig ); + if ( p->pPars->fUpdateLevel ) + Aig_ManStopReverseLevels( pAig ); + + // stop the rewriting manager + Dar_ManRefStop( p ); + if ( !Aig_ManCheck( pAig ) ) + { + printf( "Dar_ManRefactor: The network check has failed.\n" ); + return 0; + } + return 1; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/aig/dar/darScript.c b/src/aig/dar/darScript.c index c98a263e..8423a4e6 100644 --- a/src/aig/dar/darScript.c +++ b/src/aig/dar/darScript.c @@ -30,15 +30,215 @@ /**Function************************************************************* - Synopsis [] + Synopsis [Reproduces script "compress2".] Description [] - SideEffects [] + SideEffects [This procedure does not tighten level during restructuring.] SeeAlso [] ***********************************************************************/ +Aig_Man_t * Dar_ManCompress2_old( Aig_Man_t * pAig, int fVerbose ) +//alias compress2 "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l" +{ + Aig_Man_t * pTemp; + int fBalance = 0; + + Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr; + Dar_RefPar_t ParsRef, * pParsRef = &ParsRef; + + Dar_ManDefaultRwrParams( pParsRwr ); + Dar_ManDefaultRefParams( pParsRef ); + + pParsRwr->fVerbose = fVerbose; + pParsRef->fVerbose = fVerbose; + + // balance + pAig = Dar_ManBalance( pTemp = pAig, fBalance ); + Aig_ManStop( pTemp ); + + // rewrite + Dar_ManRewrite( pAig, pParsRwr ); + pAig = Aig_ManDup( pTemp = pAig, 0 ); + Aig_ManStop( pTemp ); + + // refactor + Dar_ManRefactor( pAig, pParsRef ); + pAig = Aig_ManDup( pTemp = pAig, 0 ); + Aig_ManStop( pTemp ); + + // balance + pAig = Dar_ManBalance( pTemp = pAig, fBalance ); + Aig_ManStop( pTemp ); + + // rewrite + Dar_ManRewrite( pAig, pParsRwr ); + pAig = Aig_ManDup( pTemp = pAig, 0 ); + Aig_ManStop( pTemp ); + + pParsRwr->fUseZeros = 1; + pParsRef->fUseZeros = 1; + + // rewrite + Dar_ManRewrite( pAig, pParsRwr ); + pAig = Aig_ManDup( pTemp = pAig, 0 ); + Aig_ManStop( pTemp ); + + // balance + pAig = Dar_ManBalance( pTemp = pAig, fBalance ); + Aig_ManStop( pTemp ); + + // refactor + Dar_ManRefactor( pAig, pParsRef ); + pAig = Aig_ManDup( pTemp = pAig, 0 ); + Aig_ManStop( pTemp ); + + // rewrite + Dar_ManRewrite( pAig, pParsRwr ); + pAig = Aig_ManDup( pTemp = pAig, 0 ); + Aig_ManStop( pTemp ); + + // balance + pAig = Dar_ManBalance( pTemp = pAig, fBalance ); + Aig_ManStop( pTemp ); + return pAig; +} + +/**Function************************************************************* + + Synopsis [Reproduces script "compress2".] + + Description [] + + SideEffects [This procedure does not tighten level during restructuring.] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Dar_ManCompress2_no_z( Aig_Man_t * pAig, int fVerbose ) +//alias compress2 "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l" +{ + Aig_Man_t * pTemp; + int fBalance = 0; + + Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr; + Dar_RefPar_t ParsRef, * pParsRef = &ParsRef; + + Dar_ManDefaultRwrParams( pParsRwr ); + Dar_ManDefaultRefParams( pParsRef ); + + pParsRwr->fVerbose = fVerbose; + pParsRef->fVerbose = fVerbose; + + // rewrite + Dar_ManRewrite( pAig, pParsRwr ); + pAig = Aig_ManDup( pTemp = pAig, 0 ); + Aig_ManStop( pTemp ); + + // refactor + Dar_ManRefactor( pAig, pParsRef ); + pAig = Aig_ManDup( pTemp = pAig, 0 ); + Aig_ManStop( pTemp ); + + // balance + pAig = Dar_ManBalance( pTemp = pAig, fBalance ); + Aig_ManStop( pTemp ); + + // rewrite + Dar_ManRewrite( pAig, pParsRwr ); + pAig = Aig_ManDup( pTemp = pAig, 0 ); + Aig_ManStop( pTemp ); + + // refactor + Dar_ManRefactor( pAig, pParsRef ); + pAig = Aig_ManDup( pTemp = pAig, 0 ); + Aig_ManStop( pTemp ); + + // balance + pAig = Dar_ManBalance( pTemp = pAig, fBalance ); + Aig_ManStop( pTemp ); + + // rewrite + Dar_ManRewrite( pAig, pParsRwr ); + pAig = Aig_ManDup( pTemp = pAig, 0 ); + Aig_ManStop( pTemp ); + + // refactor + Dar_ManRefactor( pAig, pParsRef ); + pAig = Aig_ManDup( pTemp = pAig, 0 ); + Aig_ManStop( pTemp ); + return pAig; +} + +/**Function************************************************************* + + Synopsis [Reproduces script "compress2".] + + Description [] + + SideEffects [This procedure does not tighten level during restructuring.] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fVerbose ) +//alias compress2 "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l" +{ + Aig_Man_t * pTemp; + int fBalance = 0; + + Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr; + Dar_RefPar_t ParsRef, * pParsRef = &ParsRef; + + Dar_ManDefaultRwrParams( pParsRwr ); + Dar_ManDefaultRefParams( pParsRef ); + + pParsRwr->fVerbose = fVerbose; + pParsRef->fVerbose = fVerbose; + + // rewrite + Dar_ManRewrite( pAig, pParsRwr ); + pAig = Aig_ManDup( pTemp = pAig, 0 ); + Aig_ManStop( pTemp ); + + // refactor + Dar_ManRefactor( pAig, pParsRef ); + pAig = Aig_ManDup( pTemp = pAig, 0 ); + Aig_ManStop( pTemp ); +/* + // balance + pAig = Dar_ManBalance( pTemp = pAig, fBalance ); + Aig_ManStop( pTemp ); +*/ + // rewrite + Dar_ManRewrite( pAig, pParsRwr ); + pAig = Aig_ManDup( pTemp = pAig, 0 ); + Aig_ManStop( pTemp ); + + pParsRwr->fUseZeros = 1; + pParsRef->fUseZeros = 1; + + // rewrite + Dar_ManRewrite( pAig, pParsRwr ); + pAig = Aig_ManDup( pTemp = pAig, 0 ); + Aig_ManStop( pTemp ); + + // balance + pAig = Dar_ManBalance( pTemp = pAig, fBalance ); + Aig_ManStop( pTemp ); + + // refactor + Dar_ManRefactor( pAig, pParsRef ); + pAig = Aig_ManDup( pTemp = pAig, 0 ); + Aig_ManStop( pTemp ); + + // rewrite + Dar_ManRewrite( pAig, pParsRwr ); + pAig = Aig_ManDup( pTemp = pAig, 0 ); + Aig_ManStop( pTemp ); + return pAig; +} //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/kit/kit.h b/src/aig/kit/kit.h index e9a389e0..2f7bbef4 100644 --- a/src/aig/kit/kit.h +++ b/src/aig/kit/kit.h @@ -217,6 +217,7 @@ static inline Kit_Node_t * Kit_GraphVar( Kit_Graph_t * pGraph ) static inline int Kit_GraphVarInt( Kit_Graph_t * pGraph ) { assert( Kit_GraphIsVar( pGraph ) ); return Kit_GraphNodeInt( pGraph, Kit_GraphVar(pGraph) ); } static inline Kit_Node_t * Kit_GraphNodeFanin0( Kit_Graph_t * pGraph, Kit_Node_t * pNode ){ return Kit_GraphNodeIsVar(pGraph, pNode)? NULL : Kit_GraphNode(pGraph, pNode->eEdge0.Node); } static inline Kit_Node_t * Kit_GraphNodeFanin1( Kit_Graph_t * pGraph, Kit_Node_t * pNode ){ return Kit_GraphNodeIsVar(pGraph, pNode)? NULL : Kit_GraphNode(pGraph, pNode->eEdge1.Node); } +static inline int Kit_GraphRootLevel( Kit_Graph_t * pGraph ) { return Kit_GraphNode(pGraph, pGraph->eRoot.Node)->Level; } static inline int Kit_Float2Int( float Val ) { return *((int *)&Val); } static inline float Kit_Int2Float( int Num ) { return *((float *)&Num); } |