summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2007-07-14 08:01:00 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2007-07-14 08:01:00 -0700
commit1647addf5e3ce4f82cc35cd4983bc5f7b9730290 (patch)
tree2811c3b08ad01dd1a63ea95f250c5d21483208d6 /src
parentc5277d3334e3dbca556fbf82bbe1c0cacdc85cb1 (diff)
downloadabc-1647addf5e3ce4f82cc35cd4983bc5f7b9730290.tar.gz
abc-1647addf5e3ce4f82cc35cd4983bc5f7b9730290.tar.bz2
abc-1647addf5e3ce4f82cc35cd4983bc5f7b9730290.zip
Version abc70714
Diffstat (limited to 'src')
-rw-r--r--src/aig/aig/aig.h45
-rw-r--r--src/aig/aig/aigDfs.c59
-rw-r--r--src/aig/aig/aigFanout.c189
-rw-r--r--src/aig/aig/aigMan.c68
-rw-r--r--src/aig/aig/aigMem.c3
-rw-r--r--src/aig/aig/aigObj.c130
-rw-r--r--src/aig/aig/aigSeq.c11
-rw-r--r--src/aig/aig/aigTable.c133
-rw-r--r--src/aig/aig/aigTiming.c275
-rw-r--r--src/aig/aig/module.make2
-rw-r--r--src/aig/dar/darBalance.c18
-rw-r--r--src/aig/dar/darCore.c47
-rw-r--r--src/aig/dar/darCut.c50
-rw-r--r--src/aig/dar/darInt.h16
-rw-r--r--src/aig/dar/darLib.c268
-rw-r--r--src/aig/dar/darMan.c21
-rw-r--r--src/aig/dar/darRefact.c48
-rw-r--r--src/aig/dar/darResub.c48
-rw-r--r--src/aig/dar/darScript.c48
-rw-r--r--src/aig/dar/dar_.c2
-rw-r--r--src/aig/dar/module.make3
-rw-r--r--src/aig/fra/fraCore.c2
-rw-r--r--src/base/abci/abc.c2
-rw-r--r--src/base/abci/abcDar.c12
-rw-r--r--src/base/abci/abcRewrite.c4
-rw-r--r--src/base/abci/abcTiming.c4
26 files changed, 1274 insertions, 234 deletions
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
@@ -119,6 +119,65 @@ Vec_Ptr_t * Aig_ManDfsNodes( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes )
/**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.]
Description []
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
@@ -96,6 +97,28 @@ Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p )
/**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.]
Description []
@@ -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,11 +245,15 @@ 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 );
@@ -253,18 +261,89 @@ void Aig_ObjPatchFanin0( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFaninNew
/**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,15 +55,58 @@ 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.]
Description []
@@ -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 &gt;= 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++ )
@@ -566,6 +578,28 @@ Dar_Cut_t * Dar_ObjPrepareCuts( Dar_Man_t * p, Aig_Obj_t * pObj )
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 []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
Dar_Cut_t * Dar_ObjComputeCuts( Dar_Man_t * p, Aig_Obj_t * pObj )
{
Aig_Obj_t * pFanin0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
@@ -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 );
@@ -163,6 +174,31 @@ void Dar_LibFree( Dar_Lib_t * 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.]
Description []
@@ -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,11 +383,11 @@ 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;
@@ -355,6 +395,133 @@ void Dar_LibSetup( Dar_Lib_t * p, Vec_Int_t * vOuts, Vec_Int_t * vPrios )
/**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.]
Description []
@@ -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