summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2008-04-02 08:01:00 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2008-04-02 08:01:00 -0700
commit0080244a89eaaccd64c64af8f394486ab5d3e5b5 (patch)
tree0a0badb1e94215e0689edf36faeed7d7e9f2b88a
parent2c7f6e39b84d29db096388459db7583c01b79b01 (diff)
downloadabc-0080244a89eaaccd64c64af8f394486ab5d3e5b5.tar.gz
abc-0080244a89eaaccd64c64af8f394486ab5d3e5b5.tar.bz2
abc-0080244a89eaaccd64c64af8f394486ab5d3e5b5.zip
Version abc80402
-rw-r--r--abc.dsp4
-rw-r--r--src/aig/aig/aig.h1
-rw-r--r--src/aig/aig/aigDfs.c74
-rw-r--r--src/aig/aig/aigFrames.c1
-rw-r--r--src/aig/aig/aigHaig.c1
-rw-r--r--src/aig/aig/aigMan.c8
-rw-r--r--src/aig/aig/aigMem.c41
-rw-r--r--src/aig/aig/aigObj.c1
-rw-r--r--src/aig/aig/aigPart.c44
-rw-r--r--src/aig/aig/aigRepr.c1
-rw-r--r--src/aig/aig/aigRet.c1
-rw-r--r--src/aig/aig/aigScl.c1
-rw-r--r--src/aig/dar/dar.h2
-rw-r--r--src/aig/dar/darBalance.c33
-rw-r--r--src/aig/dar/darScript.c37
-rw-r--r--src/aig/fra/fraBmc.c1
-rw-r--r--src/aig/fra/fraClass.c1
-rw-r--r--src/aig/fra/fraInd.c1
-rw-r--r--src/aig/fra/fraMan.c1
-rw-r--r--src/aig/kit/kitDsd.c4
-rw-r--r--src/aig/mem/mem.c2
-rw-r--r--src/aig/mfx/mfxCore.c64
-rw-r--r--src/aig/mfx/mfxDiv.c14
-rw-r--r--src/aig/mfx/mfxInt.h2
-rw-r--r--src/aig/mfx/mfxMan.c4
-rw-r--r--src/aig/mfx/mfxResub.c7
-rw-r--r--src/aig/nwk/nwk.h20
-rw-r--r--src/aig/nwk/nwkDfs.c126
-rw-r--r--src/aig/nwk/nwkMan.c5
-rw-r--r--src/aig/nwk/nwkMap.c57
-rw-r--r--src/aig/nwk/nwkObj.c1
-rw-r--r--src/aig/nwk/nwkStrash.c6
-rw-r--r--src/aig/nwk/nwkTiming.c350
-rw-r--r--src/aig/nwk/nwkUtil.c32
-rw-r--r--src/aig/tim/tim.c53
-rw-r--r--src/aig/tim/tim.h2
-rw-r--r--src/base/abc/abcCheck.c5
-rw-r--r--src/base/abc/abcNtk.c4
-rw-r--r--src/base/abci/abc.c14
-rw-r--r--src/base/abci/abcAbc8.c9
-rw-r--r--src/map/if/if.h2
-rw-r--r--src/map/if/ifMan.c2
-rw-r--r--src/misc/extra/extraUtilMemory.c20
-rw-r--r--src/sat/bsat/satMem.c34
44 files changed, 798 insertions, 295 deletions
diff --git a/abc.dsp b/abc.dsp
index 7bd1abfd..009d7847 100644
--- a/abc.dsp
+++ b/abc.dsp
@@ -42,7 +42,7 @@ RSC=rc.exe
# PROP Ignore_Export_Lib 0
# PROP Target_Dir ""
# ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c
-# ADD CPP /nologo /W3 /GX /O2 /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /c
+# ADD CPP /nologo /W3 /GX /O2 /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /c
# ADD BASE RSC /l 0x409 /d "NDEBUG"
# ADD RSC /l 0x409 /d "NDEBUG"
BSC32=bscmake.exe
@@ -66,7 +66,7 @@ LINK32=link.exe
# PROP Ignore_Export_Lib 0
# PROP Target_Dir ""
# ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /GZ /c
-# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /GZ /c
+# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /GZ /c
# SUBTRACT CPP /X
# ADD BASE RSC /l 0x409 /d "_DEBUG"
# ADD RSC /l 0x409 /d "_DEBUG"
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 0b3abce7..38fd5190 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -444,6 +444,7 @@ extern void Aig_ManCheckPhase( Aig_Man_t * p );
extern Aig_ManCut_t * Aig_ComputeCuts( Aig_Man_t * pAig, int nCutsMax, int nLeafMax, int fTruth, int fVerbose );
extern void Aig_ManCutStop( Aig_ManCut_t * p );
/*=== aigDfs.c ==========================================================*/
+extern int Aig_ManVerifyTopoOrder( Aig_Man_t * p );
extern Vec_Ptr_t * Aig_ManDfs( Aig_Man_t * p );
extern Vec_Vec_t * Aig_ManLevelize( Aig_Man_t * p );
extern Vec_Ptr_t * Aig_ManDfsPio( Aig_Man_t * p );
diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c
index aebe6c95..95ed1c3a 100644
--- a/src/aig/aig/aigDfs.c
+++ b/src/aig/aig/aigDfs.c
@@ -19,6 +19,7 @@
***********************************************************************/
#include "aig.h"
+#include "tim.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -30,6 +31,79 @@
/**Function*************************************************************
+ Synopsis [Verifies that the objects are in a topo order.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Aig_ManVerifyTopoOrder( Aig_Man_t * p )
+{
+ Aig_Obj_t * pObj, * pNext;
+ int i, iBox, iTerm1, nTerms;
+ Aig_ManSetPioNumbers( p );
+ Aig_ManIncrementTravId( p );
+ Aig_ManForEachObj( p, pObj, i )
+ {
+ if ( Aig_ObjIsNode(pObj) )
+ {
+ pNext = Aig_ObjFanin0(pObj);
+ if ( !Aig_ObjIsTravIdCurrent(p,pNext) )
+ {
+ printf( "Node %d has fanin %d that is not in a topological order.\n", pObj->Id, pNext->Id );
+ return 0;
+ }
+ pNext = Aig_ObjFanin1(pObj);
+ if ( !Aig_ObjIsTravIdCurrent(p,pNext) )
+ {
+ printf( "Node %d has fanin %d that is not in a topological order.\n", pObj->Id, pNext->Id );
+ return 0;
+ }
+ }
+ else if ( Aig_ObjIsPo(pObj) )
+ {
+ pNext = Aig_ObjFanin0(pObj);
+ if ( !Aig_ObjIsTravIdCurrent(p,pNext) )
+ {
+ printf( "Node %d has fanin %d that is not in a topological order.\n", pObj->Id, pNext->Id );
+ return 0;
+ }
+ }
+ else if ( Aig_ObjIsPi(pObj) )
+ {
+ if ( p->pManTime )
+ {
+ iBox = Tim_ManBoxForCi( p->pManTime, Aig_ObjPioNum(pObj) );
+ if ( iBox >= 0 ) // this is not a true PI
+ {
+ iTerm1 = Tim_ManBoxInputFirst( p->pManTime, iBox );
+ nTerms = Tim_ManBoxInputNum( p->pManTime, iBox );
+ for ( i = 0; i < nTerms; i++ )
+ {
+ pNext = Aig_ManPo( p, iTerm1 + i );
+ assert( Tim_ManBoxForCo( p->pManTime, Aig_ObjPioNum(pNext) ) == iBox );
+ if ( !Aig_ObjIsTravIdCurrent(p,pNext) )
+ {
+ printf( "Box %d has input %d that is not in a topological order.\n", iBox, pNext->Id );
+ return 0;
+ }
+ }
+ }
+ }
+ }
+ else
+ assert( 0 );
+ Aig_ObjSetTravIdCurrent( p, pObj );
+ }
+ Aig_ManCleanPioNumbers( p );
+ return 1;
+}
+
+/**Function*************************************************************
+
Synopsis [Collects internal nodes in the DFS order.]
Description []
diff --git a/src/aig/aig/aigFrames.c b/src/aig/aig/aigFrames.c
index 4a3b0c7c..f8bc4bda 100644
--- a/src/aig/aig/aigFrames.c
+++ b/src/aig/aig/aigFrames.c
@@ -59,6 +59,7 @@ Aig_Man_t * Aig_ManFrames( Aig_Man_t * pAig, int nFs, int fInit, int fOuts, int
// start the fraig package
pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * nFs );
pFrames->pName = Aig_UtilStrsav( pAig->pName );
+ pFrames->pSpec = Aig_UtilStrsav( pAig->pSpec );
// map constant nodes
for ( f = 0; f < nFs; f++ )
Aig_ObjSetFrames( pObjMap, nFs, Aig_ManConst1(pAig), f, Aig_ManConst1(pFrames) );
diff --git a/src/aig/aig/aigHaig.c b/src/aig/aig/aigHaig.c
index eaf9fd05..dc083465 100644
--- a/src/aig/aig/aigHaig.c
+++ b/src/aig/aig/aigHaig.c
@@ -101,6 +101,7 @@ Aig_Man_t * Aig_ManHaigFrames( Aig_Man_t * pHaig, int nFrames )
// start the frames
pFrames = Aig_ManStart( Aig_ManObjNumMax(pHaig) * nFrames );
pFrames->pName = Aig_UtilStrsav( pHaig->pName );
+ pFrames->pSpec = Aig_UtilStrsav( pHaig->pSpec );
pFrames->nRegs = pHaig->nRegs;
// create PI nodes for the frames
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index 741ecc8d..3dddc687 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -90,6 +90,7 @@ Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p )
// create the new manager
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pSpec = Aig_UtilStrsav( p->pSpec );
// create the PIs
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
Aig_ManForEachPi( p, pObj, i )
@@ -122,6 +123,7 @@ Aig_Man_t * Aig_ManDupExor( Aig_Man_t * p )
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->fCatchExor = 1;
pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pSpec = Aig_UtilStrsav( p->pSpec );
pNew->nRegs = p->nRegs;
pNew->nAsserts = p->nAsserts;
if ( p->vFlopNums )
@@ -213,6 +215,7 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
// create the new manager
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pSpec = Aig_UtilStrsav( p->pSpec );
pNew->nRegs = p->nRegs;
pNew->nAsserts = p->nAsserts;
if ( p->vFlopNums )
@@ -254,7 +257,6 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
else
{
/*
-
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
Aig_ManForEachObj( p, pObj, i )
@@ -276,6 +278,7 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
}
}
*/
+
Vec_Vec_t * vLevels;
int k;
@@ -399,6 +402,7 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
// create the new manager
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pSpec = Aig_UtilStrsav( p->pSpec );
pNew->nRegs = p->nRegs;
pNew->nAsserts = p->nAsserts;
if ( p->vFlopNums )
@@ -481,6 +485,7 @@ Aig_Man_t * Aig_ManDupWithoutPos( Aig_Man_t * p )
// create the new manager
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pSpec = Aig_UtilStrsav( p->pSpec );
// create the PIs
Aig_ManCleanData( p );
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
@@ -515,6 +520,7 @@ Aig_Man_t * Aig_ManExtractMiter( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t *
// create the new manager
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pSpec = Aig_UtilStrsav( p->pSpec );
// create the PIs
Aig_ManCleanData( p );
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
diff --git a/src/aig/aig/aigMem.c b/src/aig/aig/aigMem.c
index dab90777..80a5ceb5 100644
--- a/src/aig/aig/aigMem.c
+++ b/src/aig/aig/aigMem.c
@@ -64,10 +64,14 @@ struct Aig_MmFlex_t_
struct Aig_MmStep_t_
{
- int nMems; // the number of fixed memory managers employed
+ int nMems; // the number of fixed memory managers employed
Aig_MmFixed_t ** pMems; // memory managers: 2^1 words, 2^2 words, etc
- int nMapSize; // the size of the memory array
+ int nMapSize; // the size of the memory array
Aig_MmFixed_t ** pMap; // maps the number of bytes into its memory manager
+ // additional memory chunks
+ int nChunksAlloc; // the maximum number of memory chunks
+ int nChunks; // the current number of memory chunks
+ char ** pChunks; // the allocated memory
};
#define ALLOC(type, num) ((type *) malloc(sizeof(type) * (num)))
@@ -486,6 +490,9 @@ Aig_MmStep_t * Aig_MmStepStart( int nSteps )
p->pMap[k] = p->pMems[i];
//for ( i = 1; i < 100; i ++ )
//printf( "%10d: size = %10d\n", i, p->pMap[i]->nEntrySize );
+ p->nChunksAlloc = 64;
+ p->nChunks = 0;
+ p->pChunks = ALLOC( char *, p->nChunksAlloc );
return p;
}
@@ -505,12 +512,12 @@ void Aig_MmStepStop( Aig_MmStep_t * p, int fVerbose )
int i;
for ( i = 0; i < p->nMems; i++ )
Aig_MmFixedStop( p->pMems[i], fVerbose );
-// if ( p->pLargeChunks )
-// {
-// for ( i = 0; i < p->nLargeChunks; i++ )
-// free( p->pLargeChunks[i] );
-// free( p->pLargeChunks );
-// }
+ if ( p->nChunksAlloc )
+ {
+ for ( i = 0; i < p->nChunks; i++ )
+ free( p->pChunks[i] );
+ free( p->pChunks );
+ }
free( p->pMems );
free( p->pMap );
free( p );
@@ -533,19 +540,13 @@ char * Aig_MmStepEntryFetch( Aig_MmStep_t * p, int nBytes )
return NULL;
if ( nBytes > p->nMapSize )
{
-// printf( "Allocating %d bytes.\n", nBytes );
-/*
- if ( p->nLargeChunks == p->nLargeChunksAlloc )
+ if ( p->nChunks == p->nChunksAlloc )
{
- if ( p->nLargeChunksAlloc == 0 )
- p->nLargeChunksAlloc = 5;
- p->nLargeChunksAlloc *= 2;
- p->pLargeChunks = REALLOC( char *, p->pLargeChunks, p->nLargeChunksAlloc );
+ p->nChunksAlloc *= 2;
+ p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc );
}
- p->pLargeChunks[ p->nLargeChunks++ ] = ALLOC( char, nBytes );
- return p->pLargeChunks[ p->nLargeChunks - 1 ];
-*/
- return ALLOC( char, nBytes );
+ p->pChunks[ p->nChunks++ ] = ALLOC( char, nBytes );
+ return p->pChunks[p->nChunks-1];
}
return Aig_MmFixedEntryFetch( p->pMap[nBytes] );
}
@@ -568,7 +569,7 @@ void Aig_MmStepEntryRecycle( Aig_MmStep_t * p, char * pEntry, int nBytes )
return;
if ( nBytes > p->nMapSize )
{
- free( pEntry );
+// free( pEntry );
return;
}
Aig_MmFixedEntryRecycle( p->pMap[nBytes], pEntry );
diff --git a/src/aig/aig/aigObj.c b/src/aig/aig/aigObj.c
index 2f92f720..d02e3228 100644
--- a/src/aig/aig/aigObj.c
+++ b/src/aig/aig/aigObj.c
@@ -142,6 +142,7 @@ void Aig_ObjConnect( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFan0, Aig_Obj
// add the node to the dynamically updated topological order
// if ( p->pOrderData && Aig_ObjIsNode(pObj) )
// Aig_ObjOrderInsert( p, pObj->Id );
+ assert( !Aig_ObjIsNode(pObj) || pObj->Level > 0 );
}
/**Function*************************************************************
diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c
index 2a9800cf..4ce36245 100644
--- a/src/aig/aig/aigPart.c
+++ b/src/aig/aig/aigPart.c
@@ -1494,7 +1494,7 @@ void Aig_ManChoiceLevel_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj )
LevelMax++;
// get the level of the nodes in the choice node
- if ( pNew->pEquivs && (pNext = pNew->pEquivs[pObj->iData]) )
+ if ( pNew->pEquivs && (pNext = pNew->pEquivs[pObj->Id]) )
{
Aig_ManChoiceLevel_rec( pNew, pNext );
if ( LevelMax < Aig_ObjLevel(pNext) )
@@ -1504,6 +1504,7 @@ void Aig_ManChoiceLevel_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj )
else
assert( 0 );
Aig_ObjSetLevel( pObj, LevelMax );
+ assert( !Aig_ObjIsNode(pObj) || LevelMax > 0 );
}
/**Function*************************************************************
@@ -1546,6 +1547,46 @@ int Aig_ManChoiceLevel( Aig_Man_t * pNew )
SeeAlso []
***********************************************************************/
+void Aig_ManChoiceEval( Aig_Man_t * p )
+{
+ Vec_Ptr_t * vSupp;
+ Aig_Obj_t * pNode, * pTemp;
+ int i, Counter;
+
+ vSupp = Vec_PtrAlloc( 100 );
+ Aig_ManForEachNode( p, pNode, i )
+ {
+ if ( !Aig_ObjIsChoice(p, pNode) )
+ continue;
+ if ( pNode->Id == 4225 )
+ {
+ int x = 0;
+ }
+ Counter = 0;
+ for ( pTemp = pNode; pTemp; pTemp = p->pEquivs[pTemp->Id] )
+ Counter++;
+ printf( "Choice node = %5d. Level = %2d. Choices = %d. { ", pNode->Id, pNode->Level, Counter );
+ for ( pTemp = pNode; pTemp; pTemp = p->pEquivs[pTemp->Id] )
+ {
+ Counter = Aig_NodeMffsSupp( p, pTemp, 0, vSupp );
+ printf( "S=%d N=%d L=%d ", Vec_PtrSize(vSupp), Counter, pTemp->Level );
+ }
+ printf( "}\n" );
+ }
+ Vec_PtrFree( vSupp );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Constructively accumulates choices.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
Aig_Man_t * Aig_ManChoiceConstructive( Vec_Ptr_t * vAigs, int fVerbose )
{
Aig_Man_t * pNew, * pThis, * pPrev;
@@ -1573,6 +1614,7 @@ Aig_Man_t * Aig_ManChoiceConstructive( Vec_Ptr_t * vAigs, int fVerbose )
//Aig_ManPrintStats( pNew );
// reset levels
Aig_ManChoiceLevel( pNew );
+// Aig_ManChoiceEval( pNew );
return pNew;
}
diff --git a/src/aig/aig/aigRepr.c b/src/aig/aig/aigRepr.c
index eb4325f4..eff31fff 100644
--- a/src/aig/aig/aigRepr.c
+++ b/src/aig/aig/aigRepr.c
@@ -269,6 +269,7 @@ Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p, int fOrdered )
// start the HOP package
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pSpec = Aig_UtilStrsav( p->pSpec );
pNew->nRegs = p->nRegs;
if ( p->vFlopNums )
pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
diff --git a/src/aig/aig/aigRet.c b/src/aig/aig/aigRet.c
index d1784b1b..e20b1d4f 100644
--- a/src/aig/aig/aigRet.c
+++ b/src/aig/aig/aigRet.c
@@ -950,6 +950,7 @@ clk = clock();
// get the new manager
pNew = Rtm_ManToAig( pRtm );
pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pSpec = Aig_UtilStrsav( p->pSpec );
Rtm_ManFree( pRtm );
// group the registers
clk = clock();
diff --git a/src/aig/aig/aigScl.c b/src/aig/aig/aigScl.c
index d8ffda9a..92bfcd28 100644
--- a/src/aig/aig/aigScl.c
+++ b/src/aig/aig/aigScl.c
@@ -48,6 +48,7 @@ Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap )
// create the new manager
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pSpec = Aig_UtilStrsav( p->pSpec );
pNew->nRegs = p->nRegs;
pNew->nAsserts = p->nAsserts;
if ( p->vFlopNums )
diff --git a/src/aig/dar/dar.h b/src/aig/dar/dar.h
index 1cc239b1..99c0276d 100644
--- a/src/aig/dar/dar.h
+++ b/src/aig/dar/dar.h
@@ -80,6 +80,7 @@ extern void Dar_LibStart();
extern void Dar_LibStop();
/*=== darBalance.c ========================================================*/
extern Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel );
+extern Aig_Man_t * Dar_ManBalanceXor( Aig_Man_t * pAig, int fExor, int fUpdateLevel, int fVerbose );
extern void Dar_BalancePrintStats( Aig_Man_t * p );
/*=== darCore.c ========================================================*/
extern void Dar_ManDefaultRwrParams( Dar_RwrPar_t * pPars );
@@ -94,7 +95,6 @@ extern Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbos
extern Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose );
extern Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fFanout, int fVerbose );
extern Aig_Man_t * Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose );
-extern Aig_Man_t * Dar_ManBalanceXor( Aig_Man_t * pAig, int fExor, int fUpdateLevel, int fVerbose );
#ifdef __cplusplus
}
diff --git a/src/aig/dar/darBalance.c b/src/aig/dar/darBalance.c
index 63f6f232..6e78041a 100644
--- a/src/aig/dar/darBalance.c
+++ b/src/aig/dar/darBalance.c
@@ -333,7 +333,7 @@ Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjOld, Vec_Vec_t *
if ( vSuper->nSize == 0 )
return pObjOld->pData = Aig_ManConst0(pNew);
if ( Vec_PtrSize(vSuper) < 2 )
- printf( "BUG!\n" );
+ printf( "Dar_Balance_rec: Internal error!\n" );
// for each old node, derive the new well-balanced node
for ( i = 0; i < Vec_PtrSize(vSuper); i++ )
{
@@ -366,9 +366,11 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
Aig_Obj_t * pObj, * pDriver, * pObjNew;
Vec_Vec_t * vStore;
int i;
+ assert( Aig_ManVerifyTopoOrder(p) );
// create the new manager
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pSpec = Aig_UtilStrsav( p->pSpec );
pNew->nRegs = p->nRegs;
pNew->nAsserts = p->nAsserts;
if ( p->vFlopNums )
@@ -439,6 +441,35 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
/**Function*************************************************************
+ Synopsis [Reproduces script "compress2".]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Dar_ManBalanceXor( Aig_Man_t * pAig, int fExor, int fUpdateLevel, int fVerbose )
+{
+ Aig_Man_t * pAigXor, * pRes;
+ if ( fExor )
+ {
+ pAigXor = Aig_ManDupExor( pAig );
+ if ( fVerbose )
+ Dar_BalancePrintStats( pAigXor );
+ pRes = Dar_ManBalance( pAigXor, fUpdateLevel );
+ Aig_ManStop( pAigXor );
+ }
+ else
+ {
+ pRes = Dar_ManBalance( pAig, fUpdateLevel );
+ }
+ return pRes;
+}
+
+/**Function*************************************************************
+
Synopsis [Inserts a new node in the order by levels.]
Description []
diff --git a/src/aig/dar/darScript.c b/src/aig/dar/darScript.c
index 2a0aa7d5..7d78bf40 100644
--- a/src/aig/dar/darScript.c
+++ b/src/aig/dar/darScript.c
@@ -341,11 +341,19 @@ Vec_Ptr_t * Dar_ManChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateL
//Aig_ManPrintStats( pAig );
Aig_ManForEachObj( pAig, pObj, i )
+ {
+ pObj->pNext = pObj->pHaig;
pObj->pHaig = pObj;
+ }
pAig = Dar_ManCompress2(pAig, fBalance, fUpdateLevel, 1, fVerbose);
Vec_PtrPush( vAigs, pAig );
//Aig_ManPrintStats( pAig );
+
+ pAig = Vec_PtrEntry( vAigs, 1 );
+ Aig_ManForEachObj( pAig, pObj, i )
+ pObj->pHaig = pObj->pNext;
+
return vAigs;
}
@@ -399,35 +407,6 @@ PRT( "Choicing time ", clock() - clk );
// return NULL;
}
-/**Function*************************************************************
-
- Synopsis [Reproduces script "compress2".]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Man_t * Dar_ManBalanceXor( Aig_Man_t * pAig, int fExor, int fUpdateLevel, int fVerbose )
-{
- Aig_Man_t * pAigXor, * pRes;
- if ( fExor )
- {
- pAigXor = Aig_ManDupExor( pAig );
- if ( fVerbose )
- Dar_BalancePrintStats( pAigXor );
- pRes = Dar_ManBalance( pAigXor, fUpdateLevel );
- Aig_ManStop( pAigXor );
- }
- else
- {
- pRes = Dar_ManBalance( pAig, fUpdateLevel );
- }
- return pRes;
-}
-
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/fra/fraBmc.c b/src/aig/fra/fraBmc.c
index cf026fac..9b975b82 100644
--- a/src/aig/fra/fraBmc.c
+++ b/src/aig/fra/fraBmc.c
@@ -241,6 +241,7 @@ Aig_Man_t * Fra_BmcFrames( Fra_Bmc_t * p, int fKeepPos )
// start the fraig package
pAigFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFramesAll );
pAigFrames->pName = Aig_UtilStrsav( p->pAig->pName );
+ pAigFrames->pSpec = Aig_UtilStrsav( p->pAig->pSpec );
// create PI nodes for the frames
for ( f = 0; f < p->nFramesAll; f++ )
Bmc_ObjSetFrames( Aig_ManConst1(p->pAig), f, Aig_ManConst1(pAigFrames) );
diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c
index baae7c3f..498ea758 100644
--- a/src/aig/fra/fraClass.c
+++ b/src/aig/fra/fraClass.c
@@ -801,6 +801,7 @@ Aig_Man_t * Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK )
// start the fraig package
pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * nFramesAll );
pManFraig->pName = Aig_UtilStrsav( p->pAig->pName );
+ pManFraig->pSpec = Aig_UtilStrsav( p->pAig->pSpec );
// allocate place for the node mapping
ppEquivs = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) );
Fra_ObjSetEqu( ppEquivs, Aig_ManConst1(p->pAig), Aig_ManConst1(pManFraig) );
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index 1ac2adab..8b9e863e 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -134,6 +134,7 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
// start the fraig package
pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pManAig) * p->nFramesAll );
pManFraig->pName = Aig_UtilStrsav( p->pManAig->pName );
+ pManFraig->pSpec = Aig_UtilStrsav( p->pManAig->pSpec );
pManFraig->nRegs = p->pManAig->nRegs;
// create PI nodes for the frames
for ( f = 0; f < p->nFramesAll; f++ )
diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c
index b06f98d4..720260a5 100644
--- a/src/aig/fra/fraMan.c
+++ b/src/aig/fra/fraMan.c
@@ -178,6 +178,7 @@ Aig_Man_t * Fra_ManPrepareComb( Fra_Man_t * p )
// start the fraig package
pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pManAig) );
pManFraig->pName = Aig_UtilStrsav( p->pManAig->pName );
+ pManFraig->pSpec = Aig_UtilStrsav( p->pManAig->pSpec );
pManFraig->nRegs = p->pManAig->nRegs;
pManFraig->nAsserts = p->pManAig->nAsserts;
// set the pointers to the available fraig nodes
diff --git a/src/aig/kit/kitDsd.c b/src/aig/kit/kitDsd.c
index e24a9964..a397d452 100644
--- a/src/aig/kit/kitDsd.c
+++ b/src/aig/kit/kitDsd.c
@@ -2111,8 +2111,8 @@ void Kit_DsdTest( unsigned * pTruth, int nVars )
// if ( Kit_DsdNtkRoot(pNtk)->nFans == (unsigned)nVars && nVars == 6 )
- printf( "\n" );
- Kit_DsdPrint( stdout, pNtk );
+// printf( "\n" );
+// Kit_DsdPrint( stdout, pNtk );
pNtk = Kit_DsdExpand( pTemp = pNtk );
Kit_DsdNtkFree( pTemp );
diff --git a/src/aig/mem/mem.c b/src/aig/mem/mem.c
index f5bfbfd8..911ceffb 100644
--- a/src/aig/mem/mem.c
+++ b/src/aig/mem/mem.c
@@ -574,7 +574,7 @@ void Mem_StepEntryRecycle( Mem_Step_t * p, char * pEntry, int nBytes )
return;
if ( nBytes > p->nMapSize )
{
- free( pEntry );
+// free( pEntry );
return;
}
Mem_FixedEntryRecycle( p->pMap[nBytes], pEntry );
diff --git a/src/aig/mfx/mfxCore.c b/src/aig/mfx/mfxCore.c
index 4c8988cc..6e47c986 100644
--- a/src/aig/mfx/mfxCore.c
+++ b/src/aig/mfx/mfxCore.c
@@ -19,6 +19,7 @@
***********************************************************************/
#include "mfxInt.h"
+#include "bar.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -83,8 +84,8 @@ p->timeWin += clock() - clk;
return 1;
// compute the divisors of the window
clk = clock();
-// p->vDivs = Mfx_ComputeDivisors( p, pNode, Nwk_ObjRequired(pNode) - If_LutLibSlowestPinDelay(pNode->pMan->pLutLib) );
- p->vDivs = Mfx_ComputeDivisors( p, pNode, AIG_INFINITY );
+ p->vDivs = Mfx_ComputeDivisors( p, pNode, Nwk_ObjRequired(pNode) - If_LutLibSlowestPinDelay(pNode->pMan->pLutLib) );
+// p->vDivs = Mfx_ComputeDivisors( p, pNode, AIG_INFINITY );
p->nTotalDivs += Vec_PtrSize(p->vDivs);
p->timeDiv += clock() - clk;
// construct AIG for the window
@@ -192,10 +193,10 @@ p->timeSat += clock() - clk;
SeeAlso []
***********************************************************************/
-int Mfx_Perform( Nwk_Man_t * pNtk, Mfx_Par_t * pPars )
+int Mfx_Perform( Nwk_Man_t * pNtk, Mfx_Par_t * pPars, If_Lib_t * pLutLib )
{
Bdc_Par_t Pars = {0}, * pDecPars = &Pars;
-// ProgressBar * pProgress;
+ Bar_Progress_t * pProgress;
Mfx_Man_t * p;
Tim_Man_t * pManTimeOld = NULL;
Nwk_Obj_t * pObj;
@@ -223,23 +224,19 @@ int Mfx_Perform( Nwk_Man_t * pNtk, Mfx_Par_t * pPars )
nFaninMax = MFX_FANIN_MAX;
}
}
-
-/*
- // prepare timing information
- if ( pNtk->pManTime )
+ if ( pLutLib && pLutLib->LutMax < nFaninMax )
{
- // compute levels
- Nwk_ManLevel( pNtk );
- // compute delay trace with white-boxes
- Nwk_ManDelayTraceLut( pNtk, pNtk->pLutLib );
- // save the general timing manager
- pManTimeOld = pNtk->pManTime;
- // derive an approximate timing manager without white-boxes
- pNtk->pManTime = Tim_ManDupApprox( pNtk->pManTime );
+ printf( "The selected LUT library with max LUT size (%d) cannot be used to compute timing for network with %d-input nodes. Using unit-delay model.\n", pLutLib->LutMax, nFaninMax );
+ pLutLib = NULL;
}
- // compute delay trace with the given timing manager
- Nwk_ManDelayTraceLut( pNtk, pNtk->pLutLib );
-*/
+ pNtk->pLutLib = pLutLib;
+
+ // compute levels
+ Nwk_ManLevel( pNtk );
+ assert( Nwk_ManVerifyLevel( pNtk ) );
+ // compute delay trace with white-boxes
+ Nwk_ManDelayTraceLut( pNtk );
+ assert( Nwk_ManVerifyTiming( pNtk ) );
// start the manager
p = Mfx_ManAlloc( pPars );
@@ -259,27 +256,27 @@ int Mfx_Perform( Nwk_Man_t * pNtk, Mfx_Par_t * pPars )
p->nTotalEdgesBeg = nTotalEdgesBeg;
if ( pPars->fResub )
{
-// pProgress = Extra_ProgressBarStart( stdout, Nwk_ObjNumMax(pNtk) );
+ pProgress = Bar_ProgressStart( stdout, Nwk_ManObjNumMax(pNtk) );
Nwk_ManForEachNode( pNtk, pObj, i )
{
if ( p->pPars->nDepthMax && pObj->Level > p->pPars->nDepthMax )
continue;
if ( Nwk_ObjFaninNum(pObj) < 2 || Nwk_ObjFaninNum(pObj) > nFaninMax )
continue;
-// if ( !p->pPars->fVeryVerbose )
-// Extra_ProgressBarUpdate( pProgress, i, NULL );
+ if ( !p->pPars->fVeryVerbose )
+ Bar_ProgressUpdate( pProgress, i, NULL );
Mfx_Resub( p, pObj );
}
-// Extra_ProgressBarStop( pProgress );
+ Bar_ProgressStop( pProgress );
}
else
{
-// pProgress = Extra_ProgressBarStart( stdout, Nwk_NodeNum(pNtk) );
+ pProgress = Bar_ProgressStart( stdout, Nwk_ManNodeNum(pNtk) );
vLevels = Nwk_ManLevelize( pNtk );
Vec_VecForEachLevelStart( vLevels, vNodes, k, 1 )
{
-// if ( !p->pPars->fVeryVerbose )
-// Extra_ProgressBarUpdate( pProgress, nNodes, NULL );
+ if ( !p->pPars->fVeryVerbose )
+ Bar_ProgressUpdate( pProgress, nNodes, NULL );
p->nNodesGainedLevel = 0;
p->nTotConfLevel = 0;
p->nTimeOutsLevel = 0;
@@ -303,20 +300,15 @@ int Mfx_Perform( Nwk_Man_t * pNtk, Mfx_Par_t * pPars )
PRT( "Time", clock() - clk2 );
}
}
-// Extra_ProgressBarStop( pProgress );
+ Bar_ProgressStop( pProgress );
Vec_VecFree( vLevels );
}
p->nTotalNodesEnd = Nwk_ManNodeNum(pNtk);
p->nTotalEdgesEnd = Nwk_ManGetTotalFanins(pNtk);
-/*
- // reset the timing manager
- if ( pNtk->pManTime )
- {
- Tim_ManStop( pNtk->pManTime );
- pNtk->pManTime = pManTimeOld;
- }
- Nwk_ManVerifyLevel( pNtk );
-*/
+
+ assert( Nwk_ManVerifyLevel( pNtk ) );
+ assert( Nwk_ManVerifyTiming( pNtk ) );
+
// free the manager
p->timeTotal = clock() - clk;
Mfx_ManStop( p );
diff --git a/src/aig/mfx/mfxDiv.c b/src/aig/mfx/mfxDiv.c
index b7b76031..33f55ecb 100644
--- a/src/aig/mfx/mfxDiv.c
+++ b/src/aig/mfx/mfxDiv.c
@@ -88,17 +88,17 @@ Vec_Ptr_t * Abc_MfxWinMarkTfi( Nwk_Obj_t * pNode )
SeeAlso []
***********************************************************************/
-void Abc_MfxWinSweepLeafTfo_rec( Nwk_Obj_t * pObj, int nLevelLimit )
+void Abc_MfxWinSweepLeafTfo_rec( Nwk_Obj_t * pObj, float tArrivalMax )
{
Nwk_Obj_t * pFanout;
int i;
- if ( Nwk_ObjIsCo(pObj) || (int)pObj->Level > nLevelLimit )
+ if ( Nwk_ObjIsCo(pObj) || Nwk_ObjArrival(pObj) > tArrivalMax )
return;
if ( Nwk_ObjIsTravIdCurrent(pObj) )
return;
Nwk_ObjSetTravIdCurrent( pObj );
Nwk_ObjForEachFanout( pObj, pFanout, i )
- Abc_MfxWinSweepLeafTfo_rec( pFanout, nLevelLimit );
+ Abc_MfxWinSweepLeafTfo_rec( pFanout, tArrivalMax );
}
/**Function*************************************************************
@@ -187,7 +187,7 @@ int Abc_MfxWinVisitMffc( Nwk_Obj_t * pNode )
SeeAlso []
***********************************************************************/
-Vec_Ptr_t * Mfx_ComputeDivisors( Mfx_Man_t * p, Nwk_Obj_t * pNode, int nLevDivMax )
+Vec_Ptr_t * Mfx_ComputeDivisors( Mfx_Man_t * p, Nwk_Obj_t * pNode, float tArrivalMax )
{
Vec_Ptr_t * vCone, * vDivs;
Nwk_Obj_t * pObj, * pFanout, * pFanin;
@@ -210,7 +210,7 @@ Vec_Ptr_t * Mfx_ComputeDivisors( Mfx_Man_t * p, Nwk_Obj_t * pNode, int nLevDivMa
// (2) the MFFC of the node
// (3) the node's fanins (these are treated as a special case)
Nwk_ManIncrementTravId( pNode->pMan );
- Abc_MfxWinSweepLeafTfo_rec( pNode, nLevDivMax );
+ Abc_MfxWinSweepLeafTfo_rec( pNode, tArrivalMax );
Abc_MfxWinVisitMffc( pNode );
Nwk_ObjForEachFanin( pNode, pObj, k )
Nwk_ObjSetTravIdCurrent( pObj );
@@ -225,7 +225,7 @@ Vec_Ptr_t * Mfx_ComputeDivisors( Mfx_Man_t * p, Nwk_Obj_t * pNode, int nLevDivMa
{
if ( !Nwk_ObjIsTravIdPrevious(pObj) )
continue;
- if ( (int)pObj->Level > nLevDivMax )
+ if ( Nwk_ObjArrival(pObj) > tArrivalMax )
continue;
Vec_PtrPush( vDivs, pObj );
if ( Vec_PtrSize(vDivs) >= p->pPars->nDivMax )
@@ -253,7 +253,7 @@ Vec_Ptr_t * Mfx_ComputeDivisors( Mfx_Man_t * p, Nwk_Obj_t * pNode, int nLevDivMa
if ( !Nwk_ObjIsNode(pFanout) )
continue;
// skip nodes with large level
- if ( (int)pFanout->Level > nLevDivMax )
+ if ( Nwk_ObjArrival(pFanout) > tArrivalMax )
continue;
// skip nodes whose fanins are not divisors
Nwk_ObjForEachFanin( pFanout, pFanin, m )
diff --git a/src/aig/mfx/mfxInt.h b/src/aig/mfx/mfxInt.h
index 88792bf2..0693200d 100644
--- a/src/aig/mfx/mfxInt.h
+++ b/src/aig/mfx/mfxInt.h
@@ -125,7 +125,7 @@ struct Mfx_Man_t_
////////////////////////////////////////////////////////////////////////
/*=== mfxDiv.c ==========================================================*/
-extern Vec_Ptr_t * Mfx_ComputeDivisors( Mfx_Man_t * p, Nwk_Obj_t * pNode, int nLevDivMax );
+extern Vec_Ptr_t * Mfx_ComputeDivisors( Mfx_Man_t * p, Nwk_Obj_t * pNode, float tArrivalMax );
/*=== mfxInter.c ==========================================================*/
extern sat_solver * Mfx_CreateSolverResub( Mfx_Man_t * p, int * pCands, int nCands, int fInvert );
extern Hop_Obj_t * Mfx_Interplate( Mfx_Man_t * p, int * pCands, int nCands );
diff --git a/src/aig/mfx/mfxMan.c b/src/aig/mfx/mfxMan.c
index 1b536f8c..63531770 100644
--- a/src/aig/mfx/mfxMan.c
+++ b/src/aig/mfx/mfxMan.c
@@ -120,8 +120,8 @@ void Mfx_ManPrint( Mfx_Man_t * p )
if ( p->pPars->fSwapEdge )
printf( "Swappable edges = %d. Total edges = %d. Ratio = %5.2f.\n",
p->nNodesResub, Nwk_ManGetTotalFanins(p->pNtk), 1.00 * p->nNodesResub / Nwk_ManGetTotalFanins(p->pNtk) );
- else
- Mfx_PrintResubStats( p );
+// else
+// Mfx_PrintResubStats( p );
// printf( "Average ratio of DCs in the resubed nodes = %.2f.\n", 1.0*p->nDcMints/(64 * p->nNodesResub) );
}
else
diff --git a/src/aig/mfx/mfxResub.c b/src/aig/mfx/mfxResub.c
index 2eafc559..7179173b 100644
--- a/src/aig/mfx/mfxResub.c
+++ b/src/aig/mfx/mfxResub.c
@@ -45,17 +45,10 @@ void Mfx_UpdateNetwork( Mfx_Man_t * p, Nwk_Obj_t * pObj, Vec_Ptr_t * vFanins, Ho
int k;
// create the new node
pObjNew = Nwk_ManCreateNode( pObj->pMan, Vec_PtrSize(vFanins), Nwk_ObjFanoutNum(pObj) );
-if ( pObjNew->Id == 19969 )
-{
- int x = 0;
-}
pObjNew->pFunc = pFunc;
Vec_PtrForEachEntry( vFanins, pFanin, k )
Nwk_ObjAddFanin( pObjNew, pFanin );
// replace the old node by the new node
-//printf( "Replacing node " ); Nwk_ObjPrint( stdout, pObj );
-//printf( "Inserting node " ); Nwk_ObjPrint( stdout, pObjNew );
- // update the level of the node
Nwk_ManUpdate( pObj, pObjNew, p->vLevels );
}
diff --git a/src/aig/nwk/nwk.h b/src/aig/nwk/nwk.h
index 295b3a9e..191ca3e5 100644
--- a/src/aig/nwk/nwk.h
+++ b/src/aig/nwk/nwk.h
@@ -131,6 +131,7 @@ static inline Nwk_Obj_t * Nwk_ObjFanout0( Nwk_Obj_t * p ) { return p->pF
static inline Nwk_Obj_t * Nwk_ObjFanin( Nwk_Obj_t * p, int i ) { return p->pFanio[i]; }
static inline Nwk_Obj_t * Nwk_ObjFanout( Nwk_Obj_t * p, int i ) { return p->pFanio[p->nFanins+1]; }
+static inline int Nwk_ObjIsNone( Nwk_Obj_t * p ) { return p->Type == NWK_OBJ_NONE; }
static inline int Nwk_ObjIsCi( Nwk_Obj_t * p ) { return p->Type == NWK_OBJ_CI; }
static inline int Nwk_ObjIsCo( Nwk_Obj_t * p ) { return p->Type == NWK_OBJ_CO; }
static inline int Nwk_ObjIsNode( Nwk_Obj_t * p ) { return p->Type == NWK_OBJ_NODE; }
@@ -154,6 +155,10 @@ static inline void Nwk_ObjSetTravIdPrevious( Nwk_Obj_t * pObj ) { p
static inline int Nwk_ObjIsTravIdCurrent( Nwk_Obj_t * pObj ) { return pObj->TravId == pObj->pMan->nTravIds; }
static inline int Nwk_ObjIsTravIdPrevious( Nwk_Obj_t * pObj ) { return pObj->TravId == pObj->pMan->nTravIds - 1; }
+static inline int Nwk_ManTimeEqual( float f1, float f2, float Eps ) { return (f1 < f2 + Eps) && (f2 < f1 + Eps); }
+static inline int Nwk_ManTimeLess( float f1, float f2, float Eps ) { return (f1 < f2 + Eps); }
+static inline int Nwk_ManTimeMore( float f1, float f2, float Eps ) { return (f1 + Eps > f2); }
+
////////////////////////////////////////////////////////////////////////
/// ITERATORS ///
////////////////////////////////////////////////////////////////////////
@@ -191,8 +196,10 @@ static inline int Nwk_ObjIsTravIdPrevious( Nwk_Obj_t * pObj ) { r
extern void Nwk_ManBidecResyn( Nwk_Man_t * pNtk, int fVerbose );
extern Hop_Obj_t * Nwk_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, unsigned * puCare );
/*=== nwkDfs.c ==========================================================*/
+extern int Nwk_ManVerifyTopoOrder( Nwk_Man_t * pNtk );
+extern int Nwk_ManLevelBackup( Nwk_Man_t * pNtk );
extern int Nwk_ManLevel( Nwk_Man_t * pNtk );
-extern int Nwk_ManLevel2( Nwk_Man_t * pNtk );
+extern int Nwk_ManLevelMax( Nwk_Man_t * pNtk );
extern Vec_Vec_t * Nwk_ManLevelize( Nwk_Man_t * pNtk );
extern Vec_Ptr_t * Nwk_ManDfs( Nwk_Man_t * pNtk );
extern Vec_Ptr_t * Nwk_ManDfsNodes( Nwk_Man_t * pNtk, Nwk_Obj_t ** ppNodes, int nNodes );
@@ -203,9 +210,12 @@ extern int Nwk_ObjMffcLabel( Nwk_Obj_t * pNode );
/*=== nwkFanio.c ==========================================================*/
extern void Nwk_ObjCollectFanins( Nwk_Obj_t * pNode, Vec_Ptr_t * vNodes );
extern void Nwk_ObjCollectFanouts( Nwk_Obj_t * pNode, Vec_Ptr_t * vNodes );
+extern int Nwk_ObjFindFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin );
+extern int Nwk_ObjFindFanout( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanout );
extern void Nwk_ObjAddFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin );
extern void Nwk_ObjDeleteFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin );
extern void Nwk_ObjPatchFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFaninOld, Nwk_Obj_t * pFaninNew );
+extern void Nwk_ObjTransferFanout( Nwk_Obj_t * pNodeFrom, Nwk_Obj_t * pNodeTo );
extern void Nwk_ObjReplace( Nwk_Obj_t * pNodeOld, Nwk_Obj_t * pNodeNew );
/*=== nwkMan.c ============================================================*/
extern Nwk_Man_t * Nwk_ManAlloc();
@@ -222,10 +232,11 @@ extern Nwk_Obj_t * Nwk_ManCreateLatch( Nwk_Man_t * pMan );
extern void Nwk_ManDeleteNode( Nwk_Obj_t * pObj );
extern void Nwk_ManDeleteNode_rec( Nwk_Obj_t * pObj );
/*=== nwkTiming.c ============================================================*/
-extern float Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk, If_Lib_t * pLutLib );
-extern void Nwk_ManDelayTracePrint( Nwk_Man_t * pNtk, If_Lib_t * pLutLib );
+extern int Nwk_ManVerifyTiming( Nwk_Man_t * pNtk );
+extern float Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk );
+extern void Nwk_ManDelayTracePrint( Nwk_Man_t * pNtk );
extern void Nwk_ManUpdate( Nwk_Obj_t * pObj, Nwk_Obj_t * pObjNew, Vec_Vec_t * vLevels );
-extern void Nwk_ManVerifyLevel( Nwk_Man_t * pNtk );
+extern int Nwk_ManVerifyLevel( Nwk_Man_t * pNtk );
/*=== nwkUtil.c ============================================================*/
extern void Nwk_ManIncrementTravId( Nwk_Man_t * pNtk );
extern int Nwk_ManGetFaninMax( Nwk_Man_t * pNtk );
@@ -235,6 +246,7 @@ extern int Nwk_ManPoNum( Nwk_Man_t * pNtk );
extern int Nwk_ManGetAigNodeNum( Nwk_Man_t * pNtk );
extern int Nwk_NodeCompareLevelsIncrease( Nwk_Obj_t ** pp1, Nwk_Obj_t ** pp2 );
extern int Nwk_NodeCompareLevelsDecrease( Nwk_Obj_t ** pp1, Nwk_Obj_t ** pp2 );
+extern void Nwk_ObjPrint( Nwk_Obj_t * pObj );
#ifdef __cplusplus
}
diff --git a/src/aig/nwk/nwkDfs.c b/src/aig/nwk/nwkDfs.c
index a5f5a660..bf669086 100644
--- a/src/aig/nwk/nwkDfs.c
+++ b/src/aig/nwk/nwkDfs.c
@@ -30,6 +30,63 @@
/**Function*************************************************************
+ Synopsis [Verifies that the objects are in a topo order.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Nwk_ManVerifyTopoOrder( Nwk_Man_t * pNtk )
+{
+ Nwk_Obj_t * pObj, * pNext;
+ int i, k, iBox, iTerm1, nTerms;
+ Nwk_ManIncrementTravId( pNtk );
+ Nwk_ManForEachObj( pNtk, pObj, i )
+ {
+ if ( Nwk_ObjIsNode(pObj) || Nwk_ObjIsCo(pObj) )
+ {
+ Nwk_ObjForEachFanin( pObj, pNext, k )
+ {
+ if ( !Nwk_ObjIsTravIdCurrent(pNext) )
+ {
+ printf( "Node %d has fanin %d that is not in a topological order.\n", pObj->Id, pNext->Id );
+ return 0;
+ }
+ }
+ }
+ else if ( Nwk_ObjIsCi(pObj) )
+ {
+ if ( pNtk->pManTime )
+ {
+ iBox = Tim_ManBoxForCi( pNtk->pManTime, pObj->PioId );
+ if ( iBox >= 0 ) // this is not a true PI
+ {
+ iTerm1 = Tim_ManBoxInputFirst( pNtk->pManTime, iBox );
+ nTerms = Tim_ManBoxInputNum( pNtk->pManTime, iBox );
+ for ( i = 0; i < nTerms; i++ )
+ {
+ pNext = Nwk_ManCo( pNtk, iTerm1 + i );
+ if ( !Nwk_ObjIsTravIdCurrent(pNext) )
+ {
+ printf( "Box %d has input %d that is not in a topological order.\n", iBox, pNext->Id );
+ return 0;
+ }
+ }
+ }
+ }
+ }
+ else
+ assert( 0 );
+ Nwk_ObjSetTravIdCurrent( pObj );
+ }
+ return 1;
+}
+
+/**Function*************************************************************
+
Synopsis [Computes the number of logic levels not counting PIs/POs.]
Description [Assumes that white boxes have unit level.]
@@ -39,11 +96,12 @@
SeeAlso []
***********************************************************************/
-int Nwk_ManLevel( Nwk_Man_t * pNtk )
+int Nwk_ManLevelBackup( Nwk_Man_t * pNtk )
{
Tim_Man_t * pManTimeUnit;
Nwk_Obj_t * pObj, * pFanin;
int i, k, LevelMax, Level;
+ assert( Nwk_ManVerifyTopoOrder(pNtk) );
// clean the levels
Nwk_ManForEachObj( pNtk, pObj, i )
Nwk_ObjSetLevel( pObj, 0 );
@@ -85,11 +143,9 @@ int Nwk_ManLevel( Nwk_Man_t * pNtk )
return LevelMax;
}
-
-
/**Function*************************************************************
- Synopsis [Performs DFS for one node.]
+ Synopsis [Computes the number of logic levels not counting PIs/POs.]
Description []
@@ -98,8 +154,9 @@ int Nwk_ManLevel( Nwk_Man_t * pNtk )
SeeAlso []
***********************************************************************/
-void Nwk_ManLevel2_rec( Nwk_Obj_t * pObj )
+void Nwk_ManLevel_rec( Nwk_Obj_t * pObj )
{
+ Tim_Man_t * pManTime = pObj->pMan->pManTime;
Nwk_Obj_t * pNext;
int i, iBox, iTerm1, nTerms, LevelMax = 0;
if ( Nwk_ObjIsTravIdCurrent( pObj ) )
@@ -107,30 +164,33 @@ void Nwk_ManLevel2_rec( Nwk_Obj_t * pObj )
Nwk_ObjSetTravIdCurrent( pObj );
if ( Nwk_ObjIsCi(pObj) )
{
- iBox = Tim_ManBoxForCi( pObj->pMan->pManTime, pObj->PioId );
- if ( iBox >= 0 ) // this is not a true PI
+ if ( pManTime )
{
- iTerm1 = Tim_ManBoxInputFirst( pObj->pMan->pManTime, iBox );
- nTerms = Tim_ManBoxInputNum( pObj->pMan->pManTime, iBox );
- for ( i = 0; i < nTerms; i++ )
+ iBox = Tim_ManBoxForCi( pManTime, pObj->PioId );
+ if ( iBox >= 0 ) // this is not a true PI
{
- pNext = Nwk_ManCo(pObj->pMan, iTerm1 + i);
- Nwk_ManLevel2_rec( pNext );
- if ( LevelMax < Nwk_ObjLevel(pNext) )
- LevelMax = Nwk_ObjLevel(pNext);
+ iTerm1 = Tim_ManBoxInputFirst( pManTime, iBox );
+ nTerms = Tim_ManBoxInputNum( pManTime, iBox );
+ for ( i = 0; i < nTerms; i++ )
+ {
+ pNext = Nwk_ManCo(pObj->pMan, iTerm1 + i);
+ Nwk_ManLevel_rec( pNext );
+ if ( LevelMax < Nwk_ObjLevel(pNext) )
+ LevelMax = Nwk_ObjLevel(pNext);
+ }
+ LevelMax++;
}
- LevelMax++;
}
}
else if ( Nwk_ObjIsNode(pObj) || Nwk_ObjIsCo(pObj) )
{
Nwk_ObjForEachFanin( pObj, pNext, i )
{
- Nwk_ManLevel2_rec( pNext );
+ Nwk_ManLevel_rec( pNext );
if ( LevelMax < Nwk_ObjLevel(pNext) )
LevelMax = Nwk_ObjLevel(pNext);
}
- if ( Nwk_ObjIsNode(pObj) )
+ if ( Nwk_ObjIsNode(pObj) && Nwk_ObjFaninNum(pObj) > 0 )
LevelMax++;
}
else
@@ -140,16 +200,16 @@ void Nwk_ManLevel2_rec( Nwk_Obj_t * pObj )
/**Function*************************************************************
- Synopsis [Returns the DFS ordered array of all objects except latches.]
+ Synopsis [Computes the number of logic levels not counting PIs/POs.]
- Description []
+ Description [Does not assume that the objects are in a topo order.]
SideEffects []
SeeAlso []
***********************************************************************/
-int Nwk_ManLevel2( Nwk_Man_t * pNtk )
+int Nwk_ManLevel( Nwk_Man_t * pNtk )
{
Nwk_Obj_t * pObj;
int i, LevelMax = 0;
@@ -158,7 +218,7 @@ int Nwk_ManLevel2( Nwk_Man_t * pNtk )
Nwk_ManIncrementTravId( pNtk );
Nwk_ManForEachPo( pNtk, pObj, i )
{
- Nwk_ManLevel2_rec( pObj );
+ Nwk_ManLevel_rec( pObj );
if ( LevelMax < Nwk_ObjLevel(pObj) )
LevelMax = Nwk_ObjLevel(pObj);
}
@@ -169,6 +229,27 @@ int Nwk_ManLevel2( Nwk_Man_t * pNtk )
Synopsis [Computes the number of logic levels not counting PIs/POs.]
+ Description [Does not assume that the objects are in a topo order.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Nwk_ManLevelMax( Nwk_Man_t * pNtk )
+{
+ Nwk_Obj_t * pObj;
+ int i, LevelMax = 0;
+ Nwk_ManForEachPo( pNtk, pObj, i )
+ if ( LevelMax < Nwk_ObjLevel(pObj) )
+ LevelMax = Nwk_ObjLevel(pObj);
+ return LevelMax;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the array of objects in the AIG manager ordered by level.]
+
Description []
SideEffects []
@@ -181,7 +262,8 @@ Vec_Vec_t * Nwk_ManLevelize( Nwk_Man_t * pNtk )
Nwk_Obj_t * pObj;
Vec_Vec_t * vLevels;
int nLevels, i;
- nLevels = Nwk_ManLevel( pNtk );
+ assert( Nwk_ManVerifyLevel(pNtk) );
+ nLevels = Nwk_ManLevelMax( pNtk );
vLevels = Vec_VecStart( nLevels + 1 );
Nwk_ManForEachNode( pNtk, pObj, i )
{
diff --git a/src/aig/nwk/nwkMan.c b/src/aig/nwk/nwkMan.c
index d05543e6..2d0254f2 100644
--- a/src/aig/nwk/nwkMan.c
+++ b/src/aig/nwk/nwkMan.c
@@ -93,6 +93,7 @@ void Nwk_ManFree( Nwk_Man_t * p )
***********************************************************************/
void Nwk_ManPrintStats( Nwk_Man_t * p, If_Lib_t * pLutLib )
{
+ p->pLutLib = pLutLib;
printf( "%-15s : ", p->pName );
printf( "pi = %5d ", Nwk_ManPiNum(p) );
printf( "po = %5d ", Nwk_ManPoNum(p) );
@@ -102,8 +103,8 @@ void Nwk_ManPrintStats( Nwk_Man_t * p, If_Lib_t * pLutLib )
printf( "node = %5d ", Nwk_ManNodeNum(p) );
printf( "aig = %6d ", Nwk_ManGetAigNodeNum(p) );
printf( "lev = %3d ", Nwk_ManLevel(p) );
-// printf( "lev2 = %3d ", Nwk_ManLevel2(p) );
- printf( "delay = %5.2f", Nwk_ManDelayTraceLut(p, pLutLib) );
+// printf( "lev2 = %3d ", Nwk_ManLevelBackup(p) );
+ printf( "delay = %5.2f", Nwk_ManDelayTraceLut(p) );
printf( "\n" );
// Nwk_ManDelayTracePrint( p, pLutLib );
fflush( stdout );
diff --git a/src/aig/nwk/nwkMap.c b/src/aig/nwk/nwkMap.c
index ed67966e..eae3bd24 100644
--- a/src/aig/nwk/nwkMap.c
+++ b/src/aig/nwk/nwkMap.c
@@ -96,50 +96,45 @@ void Nwk_ManSetIfParsDefault( If_Par_t * pPars )
SeeAlso []
***********************************************************************/
-If_Man_t * Nwk_ManToIf( Aig_Man_t * p, If_Par_t * pPars )
+If_Man_t * Nwk_ManToIf( Aig_Man_t * p, If_Par_t * pPars, Vec_Ptr_t * vAigToIf )
{
If_Man_t * pIfMan;
- Aig_Obj_t * pNode;//, * pFanin, * pPrev;
+ If_Obj_t * pIfObj;
+ Aig_Obj_t * pNode, * pFanin, * pPrev;
int i;
// start the mapping manager and set its parameters
pIfMan = If_ManStart( pPars );
- // print warning about excessive memory usage
-// if ( 1.0 * Aig_ManObjNum(p) * pIfMan->nObjBytes / (1<<30) > 1.0 )
-// printf( "Warning: The mapper will allocate %.1f Gb for to represent the subject graph with %d AIG nodes.\n",
-// 1.0 * Aig_ManObjNum(p) * pIfMan->nObjBytes / (1<<30), Aig_ManObjNum(p) );
// load the AIG into the mapper
Aig_ManForEachObj( p, pNode, i )
{
if ( Aig_ObjIsAnd(pNode) )
- pNode->pData = (Aig_Obj_t *)If_ManCreateAnd( pIfMan,
- If_NotCond( (If_Obj_t *)Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ),
- If_NotCond( (If_Obj_t *)Aig_ObjFanin1(pNode)->pData, Aig_ObjFaninC1(pNode) ) );
+ pIfObj = If_ManCreateAnd( pIfMan,
+ If_NotCond( Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ),
+ If_NotCond( Aig_ObjFanin1(pNode)->pData, Aig_ObjFaninC1(pNode) ) );
else if ( Aig_ObjIsPi(pNode) )
{
- pNode->pData = If_ManCreateCi( pIfMan );
- ((If_Obj_t *)pNode->pData)->Level = pNode->Level;
- if ( pIfMan->nLevelMax < (int)pNode->Level )
- pIfMan->nLevelMax = (int)pNode->Level;
+ pIfObj = If_ManCreateCi( pIfMan );
+ If_ObjSetLevel( pIfObj, Aig_ObjLevel(pNode) );
}
else if ( Aig_ObjIsPo(pNode) )
- pNode->pData = If_ManCreateCo( pIfMan, If_NotCond( Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ) );
+ pIfObj = If_ManCreateCo( pIfMan, If_NotCond( Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ) );
else if ( Aig_ObjIsConst1(pNode) )
- Aig_ManConst1(p)->pData = If_ManConst1( pIfMan );
+ pIfObj = If_ManConst1( pIfMan );
else // add the node to the mapper
assert( 0 );
+ // save the result
+ assert( Vec_PtrEntry(vAigToIf, i) == NULL );
+ Vec_PtrWriteEntry( vAigToIf, i, pIfObj );
+ pNode->pData = pIfObj;
// set up the choice node
-// if ( Aig_AigNodeIsChoice( pNode ) )
-// {
-// pIfMan->nChoices++;
-// for ( pPrev = pNode, pFanin = pNode->pData; pFanin; pPrev = pFanin, pFanin = pFanin->pData )
-// If_ObjSetChoice( (If_Obj_t *)pPrev->pData, (If_Obj_t *)pFanin->pData );
-// If_ManCreateChoice( pIfMan, (If_Obj_t *)pNode->pData );
-// }
+ if ( Aig_ObjIsChoice( p, pNode ) )
{
- If_Obj_t * pIfObj = pNode->pData;
- assert( !If_IsComplement(pIfObj) );
- assert( pIfObj->Id == pNode->Id );
+ pIfMan->nChoices++;
+ for ( pPrev = pNode, pFanin = pNode->pData; pFanin; pPrev = pFanin, pFanin = pFanin->pData )
+ If_ObjSetChoice( pPrev->pData, pFanin->pData );
+ If_ManCreateChoice( pIfMan, pNode->pData );
}
+ assert( If_ObjLevel(pIfObj) == Aig_ObjLevel(pNode) );
}
return pIfMan;
}
@@ -243,7 +238,7 @@ Hop_Obj_t * Nwk_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t *
SeeAlso []
***********************************************************************/
-Nwk_Man_t * Nwk_ManFromIf( If_Man_t * pIfMan, Aig_Man_t * p )
+Nwk_Man_t * Nwk_ManFromIf( If_Man_t * pIfMan, Aig_Man_t * p, Vec_Ptr_t * vAigToIf )
{
Nwk_Man_t * pNtk;
Nwk_Obj_t * pObjNew;
@@ -261,7 +256,7 @@ Nwk_Man_t * Nwk_ManFromIf( If_Man_t * pIfMan, Aig_Man_t * p )
pNtk->pSpec = Aig_UtilStrsav( p->pSpec );
Aig_ManForEachObj( p, pObj, i )
{
- pIfObj = If_ManObj( pIfMan, i );
+ pIfObj = Vec_PtrEntry( vAigToIf, i );
if ( pIfObj->nRefs == 0 && !If_ObjIsTerm(pIfObj) )
continue;
if ( Aig_ObjIsNode(pObj) )
@@ -312,12 +307,13 @@ Nwk_Man_t * Nwk_MappingIf( Aig_Man_t * p, Tim_Man_t * pManTime, If_Par_t * pPars
{
Nwk_Man_t * pNtk;
If_Man_t * pIfMan;
- // perform FPGA mapping
+ Vec_Ptr_t * vAigToIf;
// set the arrival times
pPars->pTimesArr = ALLOC( float, Aig_ManPiNum(p) );
memset( pPars->pTimesArr, 0, sizeof(float) * Aig_ManPiNum(p) );
// translate into the mapper
- pIfMan = Nwk_ManToIf( p, pPars );
+ vAigToIf = Vec_PtrStart( Aig_ManObjNumMax(p) );
+ pIfMan = Nwk_ManToIf( p, pPars, vAigToIf );
if ( pIfMan == NULL )
return NULL;
pIfMan->pManTim = Tim_ManDup( pManTime, 0 );
@@ -327,8 +323,9 @@ Nwk_Man_t * Nwk_MappingIf( Aig_Man_t * p, Tim_Man_t * pManTime, If_Par_t * pPars
return NULL;
}
// transform the result of mapping into the new network
- pNtk = Nwk_ManFromIf( pIfMan, p );
+ pNtk = Nwk_ManFromIf( pIfMan, p, vAigToIf );
If_ManStop( pIfMan );
+ Vec_PtrFree( vAigToIf );
return pNtk;
}
diff --git a/src/aig/nwk/nwkObj.c b/src/aig/nwk/nwkObj.c
index 0806eecf..6d1f0428 100644
--- a/src/aig/nwk/nwkObj.c
+++ b/src/aig/nwk/nwkObj.c
@@ -194,7 +194,6 @@ void Nwk_ManDeleteNode_rec( Nwk_Obj_t * pObj )
Vec_PtrFree( vNodes );
}
-
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/nwk/nwkStrash.c b/src/aig/nwk/nwkStrash.c
index 668889a6..627bfa67 100644
--- a/src/aig/nwk/nwkStrash.c
+++ b/src/aig/nwk/nwkStrash.c
@@ -95,11 +95,13 @@ Aig_Obj_t * Nwk_ManStrashNode( Aig_Man_t * p, Nwk_Obj_t * pObj )
***********************************************************************/
Aig_Man_t * Nwk_ManStrash( Nwk_Man_t * pNtk )
{
- Aig_Man_t * pMan;
+ Aig_Man_t * pMan;//, * pTemp;
Aig_Obj_t * pObjNew;
Nwk_Obj_t * pObj;
int i, Level;
pMan = Aig_ManStart( Nwk_ManGetAigNodeNum(pNtk) );
+ pMan->pName = Aig_UtilStrsav( pNtk->pName );
+ pMan->pSpec = Aig_UtilStrsav( pNtk->pSpec );
pMan->pManTime = Tim_ManDup( pNtk->pManTime, 1 );
Tim_ManIncrementTravId( pMan->pManTime );
Nwk_ManForEachObj( pNtk, pObj, i )
@@ -125,6 +127,8 @@ Aig_Man_t * Nwk_ManStrash( Nwk_Man_t * pNtk )
pObj->pCopy = pObjNew;
}
Aig_ManCleanup( pMan );
+// pMan = Aig_ManDup( pTemp = pMan, 1 );
+// Aig_ManStop( pTemp );
return pMan;
}
diff --git a/src/aig/nwk/nwkTiming.c b/src/aig/nwk/nwkTiming.c
index 0cbcb7f8..5e4967da 100644
--- a/src/aig/nwk/nwkTiming.c
+++ b/src/aig/nwk/nwkTiming.c
@@ -24,10 +24,6 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-static inline int Nwk_ManTimeEqual( float f1, float f2, float Eps ) { return (f1 < f2 + Eps) && (f2 < f1 + Eps); }
-static inline int Nwk_ManTimeLess( float f1, float f2, float Eps ) { return (f1 < f2 + Eps); }
-static inline int Nwk_ManTimeMore( float f1, float f2, float Eps ) { return (f1 + Eps > f2); }
-
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -100,7 +96,7 @@ void Nwk_ManDelayTraceSortPins( Nwk_Obj_t * pNode, int * pPinPerm, float * pPinD
/**Function*************************************************************
- Synopsis [Computes the arrival times for the given node.]
+ Synopsis [Sorts the pins in the decreasing order of delays.]
Description []
@@ -109,14 +105,39 @@ void Nwk_ManDelayTraceSortPins( Nwk_Obj_t * pNode, int * pPinPerm, float * pPinD
SeeAlso []
***********************************************************************/
-float Nwk_NodeComputeArrival( Nwk_Obj_t * pObj, If_Lib_t * pLutLib, int fUseSorting )
+int Nwk_ManWhereIsPin( Nwk_Obj_t * pFanout, Nwk_Obj_t * pFanin, int * pPinPerm )
{
+ int i;
+ for ( i = 0; i < Nwk_ObjFaninNum(pFanout); i++ )
+ if ( Nwk_ObjFanin(pFanout, pPinPerm[i]) == pFanin )
+ return i;
+ return -1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes the arrival times for the given object.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+float Nwk_NodeComputeArrival( Nwk_Obj_t * pObj, int fUseSorting )
+{
+ If_Lib_t * pLutLib = pObj->pMan->pLutLib;
int pPinPerm[32];
float pPinDelays[32];
Nwk_Obj_t * pFanin;
float tArrival, * pDelays;
int k;
- assert( Nwk_ObjIsNode(pObj) );
+ assert( Nwk_ObjIsNode(pObj) || Nwk_ObjIsCi(pObj) || Nwk_ObjIsCo(pObj) );
+ if ( Nwk_ObjIsCi(pObj) )
+ return Nwk_ObjArrival(pObj);
+ if ( Nwk_ObjIsCo(pObj) )
+ return Nwk_ObjArrival( Nwk_ObjFanin0(pObj) );
tArrival = -AIG_INFINITY;
if ( pLutLib == NULL )
{
@@ -164,28 +185,35 @@ float Nwk_NodeComputeArrival( Nwk_Obj_t * pObj, If_Lib_t * pLutLib, int fUseSort
SeeAlso []
***********************************************************************/
-float Nwk_NodeComputeRequired( Nwk_Obj_t * pObj, If_Lib_t * pLutLib, int fUseSorting )
+float Nwk_NodeComputeRequired( Nwk_Obj_t * pObj, int fUseSorting )
{
+ If_Lib_t * pLutLib = pObj->pMan->pLutLib;
int pPinPerm[32];
float pPinDelays[32];
Nwk_Obj_t * pFanout;
- float tRequired, * pDelays;
- int k;
- assert( Nwk_ObjIsNode(pObj) || Nwk_ObjIsCi(pObj) );
+ float tRequired, tDelay, * pDelays;
+ int k, iFanin;
+ assert( Nwk_ObjIsNode(pObj) || Nwk_ObjIsCi(pObj) || Nwk_ObjIsCo(pObj) );
+ if ( Nwk_ObjIsCo(pObj) )
+ return Nwk_ObjRequired(pObj);
tRequired = AIG_INFINITY;
if ( pLutLib == NULL )
{
Nwk_ObjForEachFanout( pObj, pFanout, k )
- if ( tRequired > Nwk_ObjRequired(pFanout) - 1.0 )
- tRequired = Nwk_ObjRequired(pFanout) - 1.0;
+ {
+ tDelay = Nwk_ObjIsCo(pFanout)? 0.0 : 1.0;
+ if ( tRequired > Nwk_ObjRequired(pFanout) - tDelay )
+ tRequired = Nwk_ObjRequired(pFanout) - tDelay;
+ }
}
else if ( !pLutLib->fVarPinDelays )
{
Nwk_ObjForEachFanout( pObj, pFanout, k )
{
pDelays = pLutLib->pLutDelays[Nwk_ObjFaninNum(pFanout)];
- if ( tRequired > Nwk_ObjRequired(pFanout) - pDelays[0] )
- tRequired = Nwk_ObjRequired(pFanout) - pDelays[0];
+ tDelay = Nwk_ObjIsCo(pFanout)? 0.0 : pDelays[0];
+ if ( tRequired > Nwk_ObjRequired(pFanout) - tDelay )
+ tRequired = Nwk_ObjRequired(pFanout) - tDelay;
}
}
else
@@ -196,8 +224,11 @@ float Nwk_NodeComputeRequired( Nwk_Obj_t * pObj, If_Lib_t * pLutLib, int fUseSor
{
pDelays = pLutLib->pLutDelays[Nwk_ObjFaninNum(pFanout)];
Nwk_ManDelayTraceSortPins( pFanout, pPinPerm, pPinDelays );
- if ( tRequired > Nwk_ObjRequired(Nwk_ObjFanout(pObj,pPinPerm[k])) - pDelays[k] )
- tRequired = Nwk_ObjRequired(Nwk_ObjFanout(pObj,pPinPerm[k])) - pDelays[k];
+ iFanin = Nwk_ManWhereIsPin( pFanout, pObj, pPinPerm );
+ assert( Nwk_ObjFanin(pFanout,pPinPerm[iFanin]) == pObj );
+ tDelay = Nwk_ObjIsCo(pFanout)? 0.0 : pDelays[iFanin];
+ if ( tRequired > Nwk_ObjRequired(pFanout) - tDelay )
+ tRequired = Nwk_ObjRequired(pFanout) - tDelay;
}
}
else
@@ -205,8 +236,11 @@ float Nwk_NodeComputeRequired( Nwk_Obj_t * pObj, If_Lib_t * pLutLib, int fUseSor
Nwk_ObjForEachFanout( pObj, pFanout, k )
{
pDelays = pLutLib->pLutDelays[Nwk_ObjFaninNum(pFanout)];
- if ( tRequired > Nwk_ObjRequired(pFanout) - pDelays[k] )
- tRequired = Nwk_ObjRequired(pFanout) - pDelays[k];
+ iFanin = Nwk_ObjFindFanin( pFanout, pObj );
+ assert( Nwk_ObjFanin(pFanout,iFanin) == pObj );
+ tDelay = Nwk_ObjIsCo(pFanout)? 0.0 : pDelays[iFanin];
+ if ( tRequired > Nwk_ObjRequired(pFanout) - tDelay )
+ tRequired = Nwk_ObjRequired(pFanout) - tDelay;
}
}
}
@@ -224,8 +258,9 @@ float Nwk_NodeComputeRequired( Nwk_Obj_t * pObj, If_Lib_t * pLutLib, int fUseSor
SeeAlso []
***********************************************************************/
-float Nwk_NodePropagateRequired( Nwk_Obj_t * pObj, If_Lib_t * pLutLib, int fUseSorting )
+float Nwk_NodePropagateRequired( Nwk_Obj_t * pObj, int fUseSorting )
{
+ If_Lib_t * pLutLib = pObj->pMan->pLutLib;
int pPinPerm[32];
float pPinDelays[32];
Nwk_Obj_t * pFanin;
@@ -284,9 +319,10 @@ float Nwk_NodePropagateRequired( Nwk_Obj_t * pObj, If_Lib_t * pLutLib, int fUseS
SeeAlso []
***********************************************************************/
-float Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk, If_Lib_t * pLutLib )
+float Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk )
{
int fUseSorting = 1;
+ If_Lib_t * pLutLib = pNtk->pLutLib;
Vec_Ptr_t * vNodes;
Nwk_Obj_t * pObj;
float tArrival, tRequired, tSlack;
@@ -311,22 +347,11 @@ float Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk, If_Lib_t * pLutLib )
Tim_ManIncrementTravId( pNtk->pManTime );
Nwk_ManForEachObj( pNtk, pObj, i )
{
- if ( Nwk_ObjIsNode(pObj) )
- {
- tArrival = Nwk_NodeComputeArrival( pObj, pLutLib, fUseSorting );
- }
- else if ( Nwk_ObjIsCi(pObj) )
- {
- tArrival = pNtk->pManTime? Tim_ManGetPiArrival( pNtk->pManTime, pObj->PioId ) : (float)0.0;
- }
- else if ( Nwk_ObjIsCo(pObj) )
- {
- tArrival = Nwk_ObjArrival( Nwk_ObjFanin0(pObj) );
- if ( pNtk->pManTime )
- Tim_ManSetPoArrival( pNtk->pManTime, pObj->PioId, tArrival );
- }
- else
- assert( 0 );
+ tArrival = Nwk_NodeComputeArrival( pObj, fUseSorting );
+ if ( Nwk_ObjIsCo(pObj) && pNtk->pManTime )
+ Tim_ManSetPoArrival( pNtk->pManTime, pObj->PioId, tArrival );
+ if ( Nwk_ObjIsCi(pObj) && pNtk->pManTime )
+ tArrival = Tim_ManGetPiArrival( pNtk->pManTime, pObj->PioId );
Nwk_ObjSetArrival( pObj, tArrival );
}
@@ -343,15 +368,17 @@ float Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk, If_Lib_t * pLutLib )
Tim_ManSetPoRequiredAll( pNtk->pManTime, tArrival );
}
else
- Nwk_ManForEachPo( pNtk, pObj, i )
+ {
+ Nwk_ManForEachCo( pNtk, pObj, i )
Nwk_ObjSetRequired( pObj, tArrival );
+ }
// propagate the required times
Vec_PtrForEachEntry( vNodes, pObj, i )
{
if ( Nwk_ObjIsNode(pObj) )
{
- Nwk_NodePropagateRequired( pObj, pLutLib, fUseSorting );
+ Nwk_NodePropagateRequired( pObj, fUseSorting );
}
else if ( Nwk_ObjIsCi(pObj) )
{
@@ -370,7 +397,7 @@ float Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk, If_Lib_t * pLutLib )
// set slack for this object
tSlack = Nwk_ObjRequired(pObj) - Nwk_ObjArrival(pObj);
- assert( tSlack + 0.001 > 0.0 );
+ assert( tSlack + 0.01 > 0.0 );
Nwk_ObjSetSlack( pObj, tSlack < 0.0 ? 0.0 : tSlack );
}
Vec_PtrFree( vNodes );
@@ -379,6 +406,38 @@ float Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk, If_Lib_t * pLutLib )
/**Function*************************************************************
+ Synopsis [Computes the arrival times for the given node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Nwk_ManVerifyTiming( Nwk_Man_t * pNtk )
+{
+ Nwk_Obj_t * pObj;
+ float tArrival, tRequired;
+ int i;
+ Nwk_ManForEachObj( pNtk, pObj, i )
+ {
+ tArrival = Nwk_NodeComputeArrival( pObj, 1 );
+ tRequired = Nwk_NodeComputeRequired( pObj, 1 );
+ if ( Nwk_ObjIsCi(pObj) && pNtk->pManTime )
+ tArrival = Tim_ManGetPiArrival( pNtk->pManTime, pObj->PioId );
+ if ( Nwk_ObjIsCo(pObj) && pNtk->pManTime )
+ tArrival = Tim_ManGetPoRequired( pNtk->pManTime, pObj->PioId );
+ if ( !Nwk_ManTimeEqual( tArrival, Nwk_ObjArrival(pObj), (float)0.01 ) )
+ printf( "Nwk_ManVerifyTiming(): Arrival time of object %d is incorrect.\n", pObj->Id );
+ if ( !Nwk_ManTimeEqual( tRequired, Nwk_ObjRequired(pObj), (float)0.01 ) )
+ printf( "Nwk_ManVerifyTiming(): Required time of object %d is incorrect.\n", pObj->Id );
+ }
+ return 1;
+}
+
+/**Function*************************************************************
+
Synopsis [Prints the delay trace for the given network.]
Description []
@@ -388,8 +447,9 @@ float Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk, If_Lib_t * pLutLib )
SeeAlso []
***********************************************************************/
-void Nwk_ManDelayTracePrint( Nwk_Man_t * pNtk, If_Lib_t * pLutLib )
+void Nwk_ManDelayTracePrint( Nwk_Man_t * pNtk )
{
+ If_Lib_t * pLutLib = pNtk->pLutLib;
Nwk_Obj_t * pNode;
int i, Nodes, * pCounters;
float tArrival, tDelta, nSteps, Num;
@@ -401,11 +461,11 @@ void Nwk_ManDelayTracePrint( Nwk_Man_t * pNtk, If_Lib_t * pLutLib )
return;
}
// decide how many steps
- nSteps = pLutLib ? 20 : Nwk_ManLevel(pNtk);
+ nSteps = pLutLib ? 20 : Nwk_ManLevelMax(pNtk);
pCounters = ALLOC( int, nSteps + 1 );
memset( pCounters, 0, sizeof(int)*(nSteps + 1) );
// perform delay trace
- tArrival = Nwk_ManDelayTraceLut( pNtk, pLutLib );
+ tArrival = Nwk_ManDelayTraceLut( pNtk );
tDelta = tArrival / nSteps;
// count how many nodes have slack in the corresponding intervals
Nwk_ManForEachNode( pNtk, pNode, i )
@@ -491,39 +551,66 @@ void Nwk_NodeUpdateAddToQueue( Vec_Ptr_t * vQueue, Nwk_Obj_t * pObj, int iCurren
SeeAlso []
***********************************************************************/
-void Nwk_NodeUpdateArrival( Nwk_Obj_t * pObj, If_Lib_t * pLutLib )
+void Nwk_NodeUpdateArrival( Nwk_Obj_t * pObj )
{
+ If_Lib_t * pLutLib = pObj->pMan->pLutLib;
Tim_Man_t * pManTime = pObj->pMan->pManTime;
Vec_Ptr_t * vQueue = pObj->pMan->vTemp;
Nwk_Obj_t * pTemp, * pNext;
float tArrival;
- int i, k;
+ int i, k, iBox, iTerm1, nTerms;
assert( Nwk_ObjIsNode(pObj) );
+ // verify the arrival time
+ tArrival = Nwk_NodeComputeArrival( pObj, 1 );
+ assert( Nwk_ManTimeLess( tArrival, Nwk_ObjRequired(pObj), (float)0.01 ) );
// initialize the queue with the node
Vec_PtrClear( vQueue );
Vec_PtrPush( vQueue, pObj );
pObj->MarkA = 1;
// process objects
- Tim_ManTravIdDisable( pManTime );
+ if ( pManTime )
+ Tim_ManIncrementTravId( pManTime );
Vec_PtrForEachEntry( vQueue, pTemp, i )
{
pTemp->MarkA = 0;
- tArrival = Nwk_NodeComputeArrival( pTemp, pLutLib, 1 );
- if ( Nwk_ManTimeEqual( tArrival, Nwk_ObjArrival(pTemp), (float)0.001 ) )
+ tArrival = Nwk_NodeComputeArrival( pTemp, 1 );
+ if ( Nwk_ObjIsCi(pTemp) && pManTime )
+ tArrival = Tim_ManGetPiArrival( pManTime, pTemp->PioId );
+ if ( Nwk_ManTimeEqual( tArrival, Nwk_ObjArrival(pTemp), (float)0.01 ) )
continue;
Nwk_ObjSetArrival( pTemp, tArrival );
// add the fanouts to the queue
- Nwk_ObjForEachFanout( pTemp, pNext, k )
+ if ( Nwk_ObjIsCo(pTemp) )
+ {
+ if ( pManTime )
+ {
+ Tim_ManSetPoArrival( pManTime, pTemp->PioId, tArrival );
+ iBox = Tim_ManBoxForCo( pManTime, pNext->PioId );
+ Tim_ManSetCurrentTravIdBoxInputs( pManTime, iBox );
+ if ( iBox >= 0 ) // this is not a true PO
+ {
+ iTerm1 = Tim_ManBoxOutputFirst( pManTime, iBox );
+ nTerms = Tim_ManBoxOutputNum( pManTime, iBox );
+ for ( i = 0; i < nTerms; i++ )
+ {
+ pNext = Nwk_ManCi(pNext->pMan, iTerm1 + i);
+ if ( pNext->MarkA )
+ continue;
+ Nwk_NodeUpdateAddToQueue( vQueue, pNext, i, 1 );
+ pNext->MarkA = 1;
+ }
+ }
+ }
+ }
+ else
{
- if ( Nwk_ObjIsCo(pNext) )
+ Nwk_ObjForEachFanout( pTemp, pNext, k )
{
- Nwk_ObjSetArrival( pNext, tArrival );
- continue;
+ if ( pNext->MarkA )
+ continue;
+ Nwk_NodeUpdateAddToQueue( vQueue, pNext, i, 1 );
+ pNext->MarkA = 1;
}
- if ( pNext->MarkA )
- continue;
- Nwk_NodeUpdateAddToQueue( vQueue, pNext, i, 1 );
- pNext->MarkA = 1;
}
}
}
@@ -539,18 +626,27 @@ void Nwk_NodeUpdateArrival( Nwk_Obj_t * pObj, If_Lib_t * pLutLib )
SeeAlso []
***********************************************************************/
-void Nwk_NodeUpdateRequired( Nwk_Obj_t * pObj, If_Lib_t * pLutLib )
+void Nwk_NodeUpdateRequired( Nwk_Obj_t * pObj )
{
+ If_Lib_t * pLutLib = pObj->pMan->pLutLib;
Tim_Man_t * pManTime = pObj->pMan->pManTime;
Vec_Ptr_t * vQueue = pObj->pMan->vTemp;
Nwk_Obj_t * pTemp, * pNext;
float tRequired;
- int i, k;
+ int i, k, iBox, iTerm1, nTerms;
assert( Nwk_ObjIsNode(pObj) );
+
+if ( pObj->Id == 1384 )
+{
+ int x = 0;
+// Nwk_ObjPrint( Nwk_ManObj(pObj->pMan, 1384) );
+// Nwk_ObjPrint( Nwk_ManObj(pObj->pMan, 422) );
+}
+
// make sure the node's required time remained the same
- tRequired = Nwk_NodeComputeRequired( pObj, pLutLib, 1 );
- assert( Nwk_ManTimeEqual( tRequired, Nwk_ObjRequired(pObj), (float)0.001 ) );
- // initialize the queue with the node's fanins
+ tRequired = Nwk_NodeComputeRequired( pObj, 1 );
+ assert( Nwk_ManTimeEqual( tRequired, Nwk_ObjRequired(pObj), (float)0.01 ) );
+ // initialize the queue with the node's faninsa and the old node's fanins
Vec_PtrClear( vQueue );
Nwk_ObjForEachFanin( pObj, pNext, k )
{
@@ -560,21 +656,49 @@ void Nwk_NodeUpdateRequired( Nwk_Obj_t * pObj, If_Lib_t * pLutLib )
pNext->MarkA = 1;
}
// process objects
- Tim_ManTravIdDisable( pManTime );
+ if ( pManTime )
+ Tim_ManIncrementTravId( pManTime );
Vec_PtrForEachEntry( vQueue, pTemp, i )
{
pTemp->MarkA = 0;
- tRequired = Nwk_NodeComputeRequired( pTemp, pLutLib, 1 );
- if ( Nwk_ManTimeEqual( tRequired, Nwk_ObjRequired(pTemp), (float)0.001 ) )
+ tRequired = Nwk_NodeComputeRequired( pTemp, 1 );
+ if ( Nwk_ObjIsCo(pTemp) && pManTime )
+ tRequired = Tim_ManGetPoRequired( pManTime, pTemp->PioId );
+ if ( Nwk_ManTimeEqual( tRequired, Nwk_ObjRequired(pTemp), (float)0.01 ) )
continue;
Nwk_ObjSetRequired( pTemp, tRequired );
- // schedule fanins of the node
- Nwk_ObjForEachFanin( pTemp, pNext, k )
+ // add the fanouts to the queue
+ if ( Nwk_ObjIsCi(pTemp) )
{
- if ( pNext->MarkA )
- continue;
- Nwk_NodeUpdateAddToQueue( vQueue, pNext, i, 0 );
- pNext->MarkA = 1;
+ if ( pManTime )
+ {
+ Tim_ManSetPiRequired( pManTime, pTemp->PioId, tRequired );
+ iBox = Tim_ManBoxForCi( pManTime, pNext->PioId );
+ Tim_ManSetCurrentTravIdBoxOutputs( pManTime, iBox );
+ if ( iBox >= 0 ) // this is not a true PO
+ {
+ iTerm1 = Tim_ManBoxInputFirst( pManTime, iBox );
+ nTerms = Tim_ManBoxInputNum( pManTime, iBox );
+ for ( i = 0; i < nTerms; i++ )
+ {
+ pNext = Nwk_ManCo(pNext->pMan, iTerm1 + i);
+ if ( pNext->MarkA )
+ continue;
+ Nwk_NodeUpdateAddToQueue( vQueue, pNext, i, 0 );
+ pNext->MarkA = 1;
+ }
+ }
+ }
+ }
+ else
+ {
+ Nwk_ObjForEachFanin( pTemp, pNext, k )
+ {
+ if ( pNext->MarkA )
+ continue;
+ Nwk_NodeUpdateAddToQueue( vQueue, pNext, i, 0 );
+ pNext->MarkA = 1;
+ }
}
}
}
@@ -592,10 +716,28 @@ void Nwk_NodeUpdateRequired( Nwk_Obj_t * pObj, If_Lib_t * pLutLib )
***********************************************************************/
int Nwk_ObjLevelNew( Nwk_Obj_t * pObj )
{
+ Tim_Man_t * pManTime = pObj->pMan->pManTime;
Nwk_Obj_t * pFanin;
- int i, Level = 0;
+ int i, iBox, iTerm1, nTerms, Level = 0;
if ( Nwk_ObjIsCi(pObj) || Nwk_ObjIsLatch(pObj) )
- return 0;
+ {
+ if ( pManTime )
+ {
+ iBox = Tim_ManBoxForCi( pManTime, pObj->PioId );
+ if ( iBox >= 0 ) // this is not a true PI
+ {
+ iTerm1 = Tim_ManBoxInputFirst( pManTime, iBox );
+ nTerms = Tim_ManBoxInputNum( pManTime, iBox );
+ for ( i = 0; i < nTerms; i++ )
+ {
+ pFanin = Nwk_ManCo(pObj->pMan, iTerm1 + i);
+ Level = AIG_MAX( Level, Nwk_ObjLevel(pFanin) );
+ }
+ Level++;
+ }
+ }
+ return Level;
+ }
assert( Nwk_ObjIsNode(pObj) || Nwk_ObjIsCo(pObj) );
Nwk_ObjForEachFanin( pObj, pFanin, i )
Level = AIG_MAX( Level, Nwk_ObjLevel(pFanin) );
@@ -615,9 +757,10 @@ int Nwk_ObjLevelNew( Nwk_Obj_t * pObj )
***********************************************************************/
void Nwk_ManUpdateLevel( Nwk_Obj_t * pObj )
{
+ Tim_Man_t * pManTime = pObj->pMan->pManTime;
Vec_Ptr_t * vQueue = pObj->pMan->vTemp;
Nwk_Obj_t * pTemp, * pNext;
- int LevelNew, i, k;
+ int LevelNew, i, k, iBox, iTerm1, nTerms;
assert( Nwk_ObjIsNode(pObj) );
// initialize the queue with the node
Vec_PtrClear( vQueue );
@@ -632,17 +775,36 @@ void Nwk_ManUpdateLevel( Nwk_Obj_t * pObj )
continue;
Nwk_ObjSetLevel( pTemp, LevelNew );
// add the fanouts to the queue
- Nwk_ObjForEachFanout( pTemp, pNext, k )
+ if ( Nwk_ObjIsCo(pTemp) )
+ {
+ if ( pManTime )
+ {
+ iBox = Tim_ManBoxForCo( pManTime, pNext->PioId );
+ Tim_ManSetCurrentTravIdBoxInputs( pManTime, iBox );
+ if ( iBox >= 0 ) // this is not a true PO
+ {
+ iTerm1 = Tim_ManBoxOutputFirst( pManTime, iBox );
+ nTerms = Tim_ManBoxOutputNum( pManTime, iBox );
+ for ( i = 0; i < nTerms; i++ )
+ {
+ pNext = Nwk_ManCi(pNext->pMan, iTerm1 + i);
+ if ( pNext->MarkA )
+ continue;
+ Nwk_NodeUpdateAddToQueue( vQueue, pNext, i, 1 );
+ pNext->MarkA = 1;
+ }
+ }
+ }
+ }
+ else
{
- if ( Nwk_ObjIsCo(pNext) )
+ Nwk_ObjForEachFanout( pTemp, pNext, k )
{
- Nwk_ObjSetLevel( pNext, LevelNew );
- continue;
+ if ( pNext->MarkA )
+ continue;
+ Nwk_NodeUpdateAddToQueue( vQueue, pNext, i, 1 );
+ pNext->MarkA = 1;
}
- if ( pNext->MarkA )
- continue;
- Nwk_NodeUpdateAddToQueue( vQueue, pNext, i, 1 );
- pNext->MarkA = 1;
}
}
}
@@ -658,7 +820,7 @@ void Nwk_ManUpdateLevel( Nwk_Obj_t * pObj )
SeeAlso []
***********************************************************************/
-void Nwk_ManVerifyLevel( Nwk_Man_t * pNtk )
+int Nwk_ManVerifyLevel( Nwk_Man_t * pNtk )
{
Nwk_Obj_t * pObj;
int LevelNew, i;
@@ -672,6 +834,7 @@ void Nwk_ManVerifyLevel( Nwk_Man_t * pNtk )
i, Nwk_ObjLevel(pObj), LevelNew );
}
}
+ return 1;
}
/**Function*************************************************************
@@ -687,6 +850,14 @@ void Nwk_ManVerifyLevel( Nwk_Man_t * pNtk )
***********************************************************************/
void Nwk_ManUpdate( Nwk_Obj_t * pObj, Nwk_Obj_t * pObjNew, Vec_Vec_t * vLevels )
{
+// float Temp;
+ assert( pObj->pMan == pObjNew->pMan );
+ assert( pObj != pObjNew );
+ assert( Nwk_ObjFanoutNum(pObj) > 0 );
+ assert( Nwk_ObjIsNode(pObj) && !Nwk_ObjIsCo(pObjNew) );
+// Temp = Nwk_NodeComputeRequired( pObj, 1 );
+ // transfer fanouts to the old node
+ Nwk_ObjTransferFanout( pObj, pObjNew );
// transfer the timing information
// (this is needed because updating level happens if the level has changed;
// when we set the old level, it will be recomputed by the level updating
@@ -694,13 +865,16 @@ void Nwk_ManUpdate( Nwk_Obj_t * pObj, Nwk_Obj_t * pObjNew, Vec_Vec_t * vLevels )
pObjNew->Level = pObj->Level;
pObjNew->tArrival = pObj->tArrival;
pObjNew->tRequired = pObj->tRequired;
- // replace the old node by the new node
- Nwk_ObjReplace( pObj, pObjNew );
- // update the level of the node
+ // update required times of the old fanins
+ pObj->tRequired = AIG_INFINITY;
+ Nwk_NodeUpdateRequired( pObj );
+ // remove the old node
+ Nwk_ManDeleteNode_rec( pObj );
+ // update the information of the new node
Nwk_ManUpdateLevel( pObjNew );
-//Nwk_ManVerifyLevel( pObjNew->pMan );
-// Nwk_NodeUpdateArrival( pObjNew, pObj->pMan->pLutLib );
-// Nwk_NodeUpdateRequired( pObjNew, pObj->pMan->pLutLib );
+ Nwk_NodeUpdateArrival( pObjNew );
+ Nwk_NodeUpdateRequired( pObjNew );
+//Nwk_ManVerifyTiming( pObjNew->pMan );
}
diff --git a/src/aig/nwk/nwkUtil.c b/src/aig/nwk/nwkUtil.c
index 47e76844..b25fd68a 100644
--- a/src/aig/nwk/nwkUtil.c
+++ b/src/aig/nwk/nwkUtil.c
@@ -207,6 +207,38 @@ int Nwk_NodeCompareLevelsDecrease( Nwk_Obj_t ** pp1, Nwk_Obj_t ** pp2 )
return 0;
}
+/**Function*************************************************************
+
+ Synopsis [Deletes the node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Nwk_ObjPrint( Nwk_Obj_t * pObj )
+{
+ Nwk_Obj_t * pNext;
+ int i;
+ printf( "ObjId = %5d. ", pObj->Id );
+ if ( Nwk_ObjIsPi(pObj) )
+ printf( "PI" );
+ if ( Nwk_ObjIsPo(pObj) )
+ printf( "PO" );
+ if ( Nwk_ObjIsNode(pObj) )
+ printf( "Node" );
+ printf( " Fanins = " );
+ Nwk_ObjForEachFanin( pObj, pNext, i )
+ printf( "%d ", pNext->Id );
+ printf( " Fanouts = " );
+ Nwk_ObjForEachFanout( pObj, pNext, i )
+ printf( "%d ", pNext->Id );
+ printf( "\n" );
+}
+
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/tim/tim.c b/src/aig/tim/tim.c
index ea8a3df1..d66dbd35 100644
--- a/src/aig/tim/tim.c
+++ b/src/aig/tim/tim.c
@@ -78,6 +78,7 @@ struct Tim_Obj_t_
static inline Tim_Obj_t * Tim_ManPi( Tim_Man_t * p, int i ) { assert( i < p->nPis ); return p->pPis + i; }
static inline Tim_Obj_t * Tim_ManPo( Tim_Man_t * p, int i ) { assert( i < p->nPos ); return p->pPos + i; }
+static inline Tim_Box_t * Tim_ManBox( Tim_Man_t * p, int i ) { return Vec_PtrEntry(p->vBoxes, i); }
static inline Tim_Box_t * Tim_ManPiBox( Tim_Man_t * p, int i ) { return Tim_ManPi(p,i)->iObj2Box < 0 ? NULL : Vec_PtrEntry( p->vBoxes, Tim_ManPi(p,i)->iObj2Box ); }
static inline Tim_Box_t * Tim_ManPoBox( Tim_Man_t * p, int i ) { return Tim_ManPo(p,i)->iObj2Box < 0 ? NULL : Vec_PtrEntry( p->vBoxes, Tim_ManPo(p,i)->iObj2Box ); }
@@ -363,6 +364,48 @@ void Tim_ManTravIdEnable( Tim_Man_t * p )
/**Function*************************************************************
+ Synopsis [Label box inputs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Tim_ManSetCurrentTravIdBoxInputs( Tim_Man_t * p, int iBox )
+{
+ Tim_Box_t * pBox;
+ Tim_Obj_t * pObj;
+ int i;
+ pBox = Tim_ManBox( p, iBox );
+ Tim_ManBoxForEachInput( p, pBox, pObj, i )
+ pObj->TravId = p->nTravIds;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Label box outputs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Tim_ManSetCurrentTravIdBoxOutputs( Tim_Man_t * p, int iBox )
+{
+ Tim_Box_t * pBox;
+ Tim_Obj_t * pObj;
+ int i;
+ pBox = Tim_ManBox( p, iBox );
+ Tim_ManBoxForEachOutput( p, pBox, pObj, i )
+ pObj->TravId = p->nTravIds;
+}
+
+/**Function*************************************************************
+
Synopsis [Sets the vector of timing tables associated with the manager.]
Description []
@@ -469,6 +512,16 @@ void Tim_ManCreateBoxFirst( Tim_Man_t * p, int firstIn, int nIns, int firstOut,
***********************************************************************/
void Tim_ManIncrementTravId( Tim_Man_t * p )
{
+ int i;
+ if ( p->nTravIds >= (1<<30)-1 )
+ {
+ p->nTravIds = 0;
+ for ( i = 0; i < p->nPis; i++ )
+ p->pPis[i].TravId = 0;
+ for ( i = 0; i < p->nPos; i++ )
+ p->pPos[i].TravId = 0;
+ }
+ assert( p->nTravIds < (1<<30)-1 );
p->nTravIds++;
}
diff --git a/src/aig/tim/tim.h b/src/aig/tim/tim.h
index 6904984f..d092434e 100644
--- a/src/aig/tim/tim.h
+++ b/src/aig/tim/tim.h
@@ -65,6 +65,8 @@ extern void Tim_ManStop( Tim_Man_t * p );
extern void Tim_ManPrint( Tim_Man_t * p );
extern void Tim_ManTravIdDisable( Tim_Man_t * p );
extern void Tim_ManTravIdEnable( Tim_Man_t * p );
+extern void Tim_ManSetCurrentTravIdBoxInputs( Tim_Man_t * p, int iBox );
+extern void Tim_ManSetCurrentTravIdBoxOutputs( Tim_Man_t * p, int iBox );
extern void Tim_ManSetDelayTables( Tim_Man_t * p, Vec_Ptr_t * vDelayTables );
extern void Tim_ManCreateBox( Tim_Man_t * p, int * pIns, int nIns, int * pOuts, int nOuts, float * pDelayTable );
extern void Tim_ManCreateBoxFirst( Tim_Man_t * p, int firstIn, int nIns, int firstOut, int nOuts, float * pDelayTable );
diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c
index 79b76348..025d2001 100644
--- a/src/base/abc/abcCheck.c
+++ b/src/base/abc/abcCheck.c
@@ -154,10 +154,7 @@ bool Abc_NtkDoCheck( Abc_Ntk_t * pNtk )
if ( Abc_NtkIsNetlist(pNtk) )
{
if ( Abc_NtkNetNum(pNtk) == 0 )
- {
- fprintf( stdout, "NetworkCheck: Netlist has no nets.\n" );
- return 0;
- }
+ fprintf( stdout, "NetworkCheck: Warning! Netlist has no nets.\n" );
// check the nets
Abc_NtkForEachNet( pNtk, pNet, i )
if ( !Abc_NtkCheckNet( pNtk, pNet ) )
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index 1e88859c..6f34fa0b 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -953,8 +953,8 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
Abc_NtkForEachObj( pNtk, pObj, i )
{
// free large fanout arrays
- if ( pNtk->pMmObj && pObj->vFanouts.nCap * 4 > LargePiece )
- FREE( pObj->vFanouts.pArray );
+// if ( pNtk->pMmObj && pObj->vFanouts.nCap * 4 > LargePiece )
+// FREE( pObj->vFanouts.pArray );
// these flags should be always zero
// if this is not true, something is wrong somewhere
assert( pObj->fMarkA == 0 );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 2f52248e..f77c90e5 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -17,7 +17,7 @@
Revision [$Id: abc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
-
+
#include "abc.h"
#include "mainInt.h"
#include "fraig.h"
@@ -1781,8 +1781,8 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv )
pTruth = Hop_ManConvertAigToTruth( pNtk->pManFunc, Hop_Regular(pObj->pData), Abc_ObjFaninNum(pObj), vMemory, 0 );
if ( Hop_IsComplement(pObj->pData) )
Extra_TruthNot( pTruth, pTruth, Abc_ObjFaninNum(pObj) );
- Extra_PrintBinary( stdout, pTruth, 1 << Abc_ObjFaninNum(pObj) );
- printf( "\n" );
+// Extra_PrintBinary( stdout, pTruth, 1 << Abc_ObjFaninNum(pObj) );
+// printf( "\n" );
if ( fCofactor )
Kit_DsdPrintCofactors( pTruth, Abc_ObjFaninNum(pObj), nCofLevel, 1 );
else
@@ -7108,7 +7108,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
// extern void Abc_NtkDarTestBlif( char * pFileName );
// extern Abc_Ntk_t * Abc_NtkDarPartition( Abc_Ntk_t * pNtk );
// extern Abc_Ntk_t * Abc_NtkTestExor( Abc_Ntk_t * pNtk, int fVerbose );
- extern Abc_Ntk_t * Abc_NtkNtkTest( Abc_Ntk_t * pNtk );
+ extern Abc_Ntk_t * Abc_NtkNtkTest( Abc_Ntk_t * pNtk, If_Lib_t * pLutLib );
@@ -7295,7 +7295,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
// Abc_NtkDarPartition( pNtk );
- pNtkRes = Abc_NtkNtkTest( pNtk );
+ pNtkRes = Abc_NtkNtkTest( pNtk, Abc_FrameReadLibLut() );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Command has failed.\n" );
@@ -15343,7 +15343,7 @@ int Abc_CommandAbc8Mfs( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Mfx_Par_t Pars, * pPars = &Pars;
int c;
- extern int Mfx_Perform( void * pNtk, Mfx_Par_t * pPars );
+ extern int Mfx_Perform( void * pNtk, Mfx_Par_t * pPars, If_Lib_t * pLutLib );
// set defaults
Mfx_ParsDefault( pPars );
@@ -15449,7 +15449,7 @@ int Abc_CommandAbc8Mfs( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// modify the current network
- if ( !Mfx_Perform( pAbc->pAbc8Nwk, pPars ) )
+ if ( !Mfx_Perform( pAbc->pAbc8Nwk, pPars, pAbc->pAbc8Lib ) )
{
fprintf( stdout, "Abc_CommandAbc8Mfs(): Command has failed.\n" );
return 1;
diff --git a/src/base/abci/abcAbc8.c b/src/base/abci/abcAbc8.c
index 3c60bde0..e918417c 100644
--- a/src/base/abci/abcAbc8.c
+++ b/src/base/abci/abcAbc8.c
@@ -198,8 +198,9 @@ clk = clock();
PRT( "Time", clock() - clk );
pMan = Abc_NtkToNtkNew( pNtk );
+ pMan->pLutLib = Abc_FrameReadLibLut();
clk = clock();
- printf( "%6.2f\n", Nwk_ManDelayTraceLut( pMan, Abc_FrameReadLibLut() ) );
+ printf( "%6.2f\n", Nwk_ManDelayTraceLut( pMan ) );
PRT( "Time", clock() - clk );
pNtkNew = Abc_NtkFromNtkNew( pNtk, pMan );
@@ -218,9 +219,9 @@ PRT( "Time", clock() - clk );
SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Abc_NtkNtkTest( Abc_Ntk_t * pNtk )
+Abc_Ntk_t * Abc_NtkNtkTest( Abc_Ntk_t * pNtk, If_Lib_t * pLutLib )
{
- extern int Mfx_Perform( Nwk_Man_t * pNtk, Mfx_Par_t * pPars );
+ extern int Mfx_Perform( Nwk_Man_t * pNtk, Mfx_Par_t * pPars, If_Lib_t * pLutLib );
Mfx_Par_t Pars, * pPars = &Pars;
Abc_Ntk_t * pNtkNew;
@@ -228,7 +229,7 @@ Abc_Ntk_t * Abc_NtkNtkTest( Abc_Ntk_t * pNtk )
pMan = Abc_NtkToNtkNew( pNtk );
Mfx_ParsDefault( pPars );
- Mfx_Perform( pMan, pPars );
+ Mfx_Perform( pMan, pPars, pLutLib );
pNtkNew = Abc_NtkFromNtkNew( pNtk, pMan );
Nwk_ManFree( pMan );
diff --git a/src/map/if/if.h b/src/map/if/if.h
index 61f81622..e0b9584d 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -255,6 +255,8 @@ static inline If_Obj_t * If_ObjFanin1( If_Obj_t * pObj ) { r
static inline int If_ObjFaninC0( If_Obj_t * pObj ) { return pObj->fCompl0; }
static inline int If_ObjFaninC1( If_Obj_t * pObj ) { return pObj->fCompl1; }
static inline void * If_ObjCopy( If_Obj_t * pObj ) { return pObj->pCopy; }
+static inline int If_ObjLevel( If_Obj_t * pObj ) { return pObj->Level; }
+static inline void If_ObjSetLevel( If_Obj_t * pObj, int Level ) { pObj->Level = Level; }
static inline void If_ObjSetCopy( If_Obj_t * pObj, void * pCopy ) { pObj->pCopy = pCopy; }
static inline void If_ObjSetChoice( If_Obj_t * pObj, If_Obj_t * pEqu ) { pObj->pEquiv = pEqu; }
diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c
index 7bb7fcd1..d1a17b6a 100644
--- a/src/map/if/ifMan.c
+++ b/src/map/if/ifMan.c
@@ -191,6 +191,8 @@ If_Obj_t * If_ManCreateCo( If_Man_t * p, If_Obj_t * pDriver )
pObj->fCompl0 = If_IsComplement(pDriver); pDriver = If_Regular(pDriver);
pObj->pFanin0 = pDriver; pDriver->nRefs++;
pObj->Level = pDriver->Level;
+ if ( p->nLevelMax < (int)pObj->Level )
+ p->nLevelMax = (int)pObj->Level;
p->nObjs[IF_CO]++;
return pObj;
}
diff --git a/src/misc/extra/extraUtilMemory.c b/src/misc/extra/extraUtilMemory.c
index 6eccf015..376ed9b0 100644
--- a/src/misc/extra/extraUtilMemory.c
+++ b/src/misc/extra/extraUtilMemory.c
@@ -527,12 +527,12 @@ void Extra_MmStepStop( Extra_MmStep_t * p )
int i;
for ( i = 0; i < p->nMems; i++ )
Extra_MmFixedStop( p->pMems[i] );
-// if ( p->pLargeChunks )
-// {
-// for ( i = 0; i < p->nLargeChunks; i++ )
-// free( p->pLargeChunks[i] );
-// free( p->pLargeChunks );
-// }
+ if ( p->pLargeChunks )
+ {
+ for ( i = 0; i < p->nLargeChunks; i++ )
+ free( p->pLargeChunks[i] );
+ free( p->pLargeChunks );
+ }
free( p->pMems );
free( p->pMap );
free( p );
@@ -556,18 +556,16 @@ char * Extra_MmStepEntryFetch( Extra_MmStep_t * p, int nBytes )
if ( nBytes > p->nMapSize )
{
// printf( "Allocating %d bytes.\n", nBytes );
-/*
+// return ALLOC( char, nBytes );
if ( p->nLargeChunks == p->nLargeChunksAlloc )
{
if ( p->nLargeChunksAlloc == 0 )
- p->nLargeChunksAlloc = 5;
+ p->nLargeChunksAlloc = 32;
p->nLargeChunksAlloc *= 2;
p->pLargeChunks = REALLOC( char *, p->pLargeChunks, p->nLargeChunksAlloc );
}
p->pLargeChunks[ p->nLargeChunks++ ] = ALLOC( char, nBytes );
return p->pLargeChunks[ p->nLargeChunks - 1 ];
-*/
- return ALLOC( char, nBytes );
}
return Extra_MmFixedEntryFetch( p->pMap[nBytes] );
}
@@ -590,7 +588,7 @@ void Extra_MmStepEntryRecycle( Extra_MmStep_t * p, char * pEntry, int nBytes )
return;
if ( nBytes > p->nMapSize )
{
- free( pEntry );
+// free( pEntry );
return;
}
Extra_MmFixedEntryRecycle( p->pMap[nBytes], pEntry );
diff --git a/src/sat/bsat/satMem.c b/src/sat/bsat/satMem.c
index 7fa1a824..1dacb854 100644
--- a/src/sat/bsat/satMem.c
+++ b/src/sat/bsat/satMem.c
@@ -63,10 +63,14 @@ struct Sat_MmFlex_t_
struct Sat_MmStep_t_
{
- int nMems; // the number of fixed memory managers employed
- Sat_MmFixed_t ** pMems; // memory managers: 2^1 words, 2^2 words, etc
- int nMapSize; // the size of the memory array
- Sat_MmFixed_t ** pMap; // maps the number of bytes into its memory manager
+ int nMems; // the number of fixed memory managers employed
+ Sat_MmFixed_t ** pMems; // memory managers: 2^1 words, 2^2 words, etc
+ int nMapSize; // the size of the memory array
+ Sat_MmFixed_t ** pMap; // maps the number of bytes into its memory manager
+ // additional memory chunks
+ int nChunksAlloc; // the maximum number of memory chunks
+ int nChunks; // the current number of memory chunks
+ char ** pChunks; // the allocated memory
};
////////////////////////////////////////////////////////////////////////
@@ -291,7 +295,7 @@ Sat_MmFlex_t * Sat_MmFlexStart()
p->pCurrent = NULL;
p->pEnd = NULL;
- p->nChunkSize = (1 << 12);
+ p->nChunkSize = (1 << 16);
p->nChunksAlloc = 64;
p->nChunks = 0;
p->pChunks = ALLOC( char *, p->nChunksAlloc );
@@ -436,6 +440,9 @@ Sat_MmStep_t * Sat_MmStepStart( int nSteps )
p->pMap[k] = p->pMems[i];
//for ( i = 1; i < 100; i ++ )
//printf( "%10d: size = %10d\n", i, p->pMap[i]->nEntrySize );
+ p->nChunksAlloc = 64;
+ p->nChunks = 0;
+ p->pChunks = ALLOC( char *, p->nChunksAlloc );
return p;
}
@@ -453,6 +460,12 @@ Sat_MmStep_t * Sat_MmStepStart( int nSteps )
void Sat_MmStepStop( Sat_MmStep_t * p, int fVerbose )
{
int i;
+ if ( p->nChunksAlloc )
+ {
+ for ( i = 0; i < p->nChunks; i++ )
+ free( p->pChunks[i] );
+ free( p->pChunks );
+ }
for ( i = 0; i < p->nMems; i++ )
Sat_MmFixedStop( p->pMems[i], fVerbose );
free( p->pMems );
@@ -477,8 +490,13 @@ char * Sat_MmStepEntryFetch( Sat_MmStep_t * p, int nBytes )
return NULL;
if ( nBytes > p->nMapSize )
{
-// printf( "Allocating %d bytes.\n", nBytes );
- return ALLOC( char, nBytes );
+ if ( p->nChunks == p->nChunksAlloc )
+ {
+ p->nChunksAlloc *= 2;
+ p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc );
+ }
+ p->pChunks[ p->nChunks++ ] = ALLOC( char, nBytes );
+ return p->pChunks[p->nChunks-1];
}
return Sat_MmFixedEntryFetch( p->pMap[nBytes] );
}
@@ -501,7 +519,7 @@ void Sat_MmStepEntryRecycle( Sat_MmStep_t * p, char * pEntry, int nBytes )
return;
if ( nBytes > p->nMapSize )
{
- free( pEntry );
+// free( pEntry );
return;
}
Sat_MmFixedEntryRecycle( p->pMap[nBytes], pEntry );