summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/base/abci/abc.c6
-rw-r--r--src/base/abci/abcMfs.c3
-rw-r--r--src/opt/mfs/mfs.h2
-rw-r--r--src/opt/mfs/mfsCore.c10
-rw-r--r--src/opt/mfs/mfsCore_.c1
-rw-r--r--src/opt/mfs/mfsDiv.c11
-rw-r--r--src/opt/mfs/mfsInt.h1
-rw-r--r--src/opt/mfs/mfsMan.c8
-rw-r--r--src/opt/mfs/mfsResub.c4
-rw-r--r--src/opt/sfm/sfmWin.c1
10 files changed, 26 insertions, 21 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 4493c361..d5bcb48f 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -4361,9 +4361,9 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
goto usage;
}
- pPars->nWinSizeMax = atoi(argv[globalUtilOptind]);
+ pPars->nWinMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
- if ( pPars->nWinSizeMax < 0 )
+ if ( pPars->nWinMax < 0 )
goto usage;
break;
case 'L':
@@ -4450,7 +4450,7 @@ usage:
Abc_Print( -2, "\t-W <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nWinTfoLevs );
Abc_Print( -2, "\t-F <num> : the max number of fanouts to skip (1 <= num) [default = %d]\n", pPars->nFanoutsMax );
Abc_Print( -2, "\t-D <num> : the max depth nodes to try (0 = no limit) [default = %d]\n", pPars->nDepthMax );
- Abc_Print( -2, "\t-M <num> : the max node count of windows to consider (0 = no limit) [default = %d]\n", pPars->nWinSizeMax );
+ Abc_Print( -2, "\t-M <num> : the max node count of windows to consider (0 = no limit) [default = %d]\n", pPars->nWinMax );
Abc_Print( -2, "\t-L <num> : the max increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel );
Abc_Print( -2, "\t-C <num> : the max number of conflicts in one SAT run (0 = no limit) [default = %d]\n", pPars->nBTLimit );
Abc_Print( -2, "\t-d : toggle performing redundancy removal [default = %s]\n", pPars->fRrOnly? "yes": "no" );
diff --git a/src/base/abci/abcMfs.c b/src/base/abci/abcMfs.c
index 76dfb162..dfd950dc 100644
--- a/src/base/abci/abcMfs.c
+++ b/src/base/abci/abcMfs.c
@@ -74,9 +74,10 @@ Vec_Ptr_t * Abc_NtkAssignIDs2( Abc_Ntk_t * pNtk )
vNodes = Vec_PtrAlloc( Abc_NtkNodeNum(pNtk) );
Abc_NtkForEachNode( pNtk, pObj, i )
{
+ pObj->iTemp = Abc_NtkCiNum(pNtk) + Vec_PtrSize(vNodes);
Vec_PtrPush( vNodes, pObj );
- pObj->iTemp = Abc_NtkCiNum(pNtk) + i;
}
+ assert( Vec_PtrSize(vNodes) == Abc_NtkNodeNum(pNtk) );
Abc_NtkForEachCo( pNtk, pObj, i )
pObj->iTemp = Abc_NtkCiNum(pNtk) + Vec_PtrSize(vNodes) + i;
return vNodes;
diff --git a/src/opt/mfs/mfs.h b/src/opt/mfs/mfs.h
index 8292e617..4ca0df00 100644
--- a/src/opt/mfs/mfs.h
+++ b/src/opt/mfs/mfs.h
@@ -47,7 +47,7 @@ struct Mfs_Par_t_
int nFanoutsMax; // the maximum number of fanouts
int nDepthMax; // the maximum number of logic levels
int nDivMax; // the maximum number of divisors
- int nWinSizeMax; // the maximum size of the window
+ int nWinMax; // the maximum size of the window
int nGrowthLevel; // the maximum allowed growth in level
int nBTLimit; // the maximum number of conflicts in one SAT run
int fRrOnly; // perform redundance removal
diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c
index d652d8cd..bb36b85c 100644
--- a/src/opt/mfs/mfsCore.c
+++ b/src/opt/mfs/mfsCore.c
@@ -50,8 +50,7 @@ void Abc_NtkMfsParsDefault( Mfs_Par_t * pPars )
pPars->nWinTfoLevs = 2;
pPars->nFanoutsMax = 30;
pPars->nDepthMax = 20;
- pPars->nDivMax = 250;
- pPars->nWinSizeMax = 300;
+ pPars->nWinMax = 300;
pPars->nGrowthLevel = 0;
pPars->nBTLimit = 5000;
pPars->fRrOnly = 0;
@@ -98,7 +97,7 @@ int Abc_WinNode(Mfs_Man_t * p, Abc_Obj_t *pNode)
p->vRoots = Abc_MfsComputeRoots( pNode, p->pPars->nWinTfoLevs, p->pPars->nFanoutsMax );
p->vSupp = Abc_NtkNodeSupport( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
p->vNodes = Abc_NtkDfsNodes( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
- if ( p->pPars->nWinSizeMax && Vec_PtrSize(p->vNodes) > p->pPars->nWinSizeMax )
+ if ( p->pPars->nWinMax && Vec_PtrSize(p->vNodes) > p->pPars->nWinMax )
return 1;
// compute the divisors of the window
p->vDivs = Abc_MfsComputeDivisors( p, pNode, Abc_ObjRequiredLevel(pNode) - 1 );
@@ -246,8 +245,11 @@ clk = clock();
p->vSupp = Abc_NtkNodeSupport( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
p->vNodes = Abc_NtkDfsNodes( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
p->timeWin += clock() - clk;
- if ( p->pPars->nWinSizeMax && Vec_PtrSize(p->vNodes) > p->pPars->nWinSizeMax )
+ if ( p->pPars->nWinMax && Vec_PtrSize(p->vNodes) > p->pPars->nWinMax )
+ {
+ p->nMaxDivs++;
return 1;
+ }
// compute the divisors of the window
clk = clock();
p->vDivs = Abc_MfsComputeDivisors( p, pNode, Abc_ObjRequiredLevel(pNode) - 1 );
diff --git a/src/opt/mfs/mfsCore_.c b/src/opt/mfs/mfsCore_.c
index 49105da6..38e407bc 100644
--- a/src/opt/mfs/mfsCore_.c
+++ b/src/opt/mfs/mfsCore_.c
@@ -48,7 +48,6 @@ void Abc_NtkMfsParsDefault( Mfs_Par_t * pPars )
pPars->nWinTfoLevs = 2;
pPars->nFanoutsMax = 10;
pPars->nDepthMax = 20;
- pPars->nDivMax = 250;
pPars->nWinSizeMax = 300;
pPars->nGrowthLevel = 0;
pPars->nBTLimit = 5000;
diff --git a/src/opt/mfs/mfsDiv.c b/src/opt/mfs/mfsDiv.c
index 0b29673e..ece8ec64 100644
--- a/src/opt/mfs/mfsDiv.c
+++ b/src/opt/mfs/mfsDiv.c
@@ -223,7 +223,7 @@ Vec_Ptr_t * Abc_MfsComputeDivisors( Mfs_Man_t * p, Abc_Obj_t * pNode, int nLevDi
// nodes to be avoided as divisors are marked with current trav ID
// start collecting the divisors
- vDivs = Vec_PtrAlloc( p->pPars->nDivMax );
+ vDivs = Vec_PtrAlloc( p->pPars->nWinMax );
Vec_PtrForEachEntry( Abc_Obj_t *, vCone, pObj, k )
{
if ( !Abc_NodeIsTravIdPrevious(pObj) )
@@ -231,13 +231,13 @@ Vec_Ptr_t * Abc_MfsComputeDivisors( Mfs_Man_t * p, Abc_Obj_t * pNode, int nLevDi
if ( (int)pObj->Level > nLevDivMax )
continue;
Vec_PtrPush( vDivs, pObj );
- if ( Vec_PtrSize(vDivs) >= p->pPars->nDivMax )
+ if ( Vec_PtrSize(vDivs) >= p->pPars->nWinMax )
break;
}
Vec_PtrFree( vCone );
// explore the fanouts of already collected divisors
- if ( Vec_PtrSize(vDivs) < p->pPars->nDivMax )
+ if ( Vec_PtrSize(vDivs) < p->pPars->nWinMax )
Vec_PtrForEachEntry( Abc_Obj_t *, vDivs, pObj, k )
{
// consider fanouts of this node
@@ -273,12 +273,13 @@ Vec_Ptr_t * Abc_MfsComputeDivisors( Mfs_Man_t * p, Abc_Obj_t * pNode, int nLevDi
Vec_PtrPushUnique( p->vNodes, pFanout );
Abc_NodeSetTravIdPrevious( pFanout );
nDivsPlus++;
- if ( Vec_PtrSize(vDivs) >= p->pPars->nDivMax )
+ if ( Vec_PtrSize(vDivs) >= p->pPars->nWinMax )
break;
}
- if ( Vec_PtrSize(vDivs) >= p->pPars->nDivMax )
+ if ( Vec_PtrSize(vDivs) >= p->pPars->nWinMax )
break;
}
+ p->nMaxDivs += (Vec_PtrSize(vDivs) >= p->pPars->nWinMax);
// sort the divisors by level in the increasing order
Vec_PtrSort( vDivs, (int (*)(void))Abc_NodeCompareLevelsIncrease );
diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h
index 23a59833..ddaa323d 100644
--- a/src/opt/mfs/mfsInt.h
+++ b/src/opt/mfs/mfsInt.h
@@ -114,6 +114,7 @@ struct Mfs_Man_t_
int nTimeOuts;
int nTimeOutsLevel;
int nDcMints;
+ int nMaxDivs;
double dTotalRatios;
// node/edge stats
int nTotalNodesBeg;
diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c
index 6042f15e..1132275f 100644
--- a/src/opt/mfs/mfsMan.c
+++ b/src/opt/mfs/mfsMan.c
@@ -52,8 +52,8 @@ Mfs_Man_t * Mfs_ManAlloc( Mfs_Par_t * pPars )
p->vProjVarsCnf = Vec_IntAlloc( 100 );
p->vProjVarsSat = Vec_IntAlloc( 100 );
p->vDivLits = Vec_IntAlloc( 100 );
- p->nDivWords = Abc_BitWordNum(p->pPars->nDivMax + MFS_FANIN_MAX);
- p->vDivCexes = Vec_PtrAllocSimInfo( p->pPars->nDivMax+MFS_FANIN_MAX+1, p->nDivWords );
+ p->nDivWords = Abc_BitWordNum(p->pPars->nWinMax + MFS_FANIN_MAX);
+ p->vDivCexes = Vec_PtrAllocSimInfo( p->pPars->nWinMax + MFS_FANIN_MAX + 1, p->nDivWords );
p->pMan = Int_ManAlloc();
p->vMem = Vec_IntAlloc( 0 );
p->vLevels = Vec_VecStart( 32 );
@@ -112,8 +112,8 @@ void Mfs_ManPrint( Mfs_Man_t * p )
{
if ( p->pPars->fResub )
{
- printf( "Nodes = %d. Try = %d. Resub = %d. Div = %d. SAT calls = %d. Timeouts = %d.\n",
- p->nTotalNodesBeg, p->nNodesTried, p->nNodesResub, p->nTotalDivs, p->nSatCalls, p->nTimeOuts );
+ printf( "Nodes = %d. Try = %d. Resub = %d. Div = %d. SAT calls = %d. Timeouts = %d. MaxDivs = %d.\n",
+ p->nTotalNodesBeg, p->nNodesTried, p->nNodesResub, p->nTotalDivs, p->nSatCalls, p->nTimeOuts, p->nMaxDivs );
printf( "Attempts : " );
printf( "Remove %6d out of %6d (%6.2f %%) ", p->nRemoves, p->nTryRemoves, 100.0*p->nRemoves/Abc_MaxInt(1, p->nTryRemoves) );
diff --git a/src/opt/mfs/mfsResub.c b/src/opt/mfs/mfsResub.c
index 85eb8140..694b366c 100644
--- a/src/opt/mfs/mfsResub.c
+++ b/src/opt/mfs/mfsResub.c
@@ -297,7 +297,7 @@ p->timeInt += clock() - clk;
p->nResubs++;
return 1;
}
- if ( p->nCexes >= p->pPars->nDivMax )
+ if ( p->nCexes >= p->pPars->nWinMax )
break;
}
if ( p->pPars->fVeryVerbose )
@@ -467,7 +467,7 @@ clk = clock();
p->timeInt += clock() - clk;
return 1;
}
- if ( p->nCexes >= p->pPars->nDivMax )
+ if ( p->nCexes >= p->pPars->nWinMax )
break;
}
return 0;
diff --git a/src/opt/sfm/sfmWin.c b/src/opt/sfm/sfmWin.c
index 3c30c480..9efe30d3 100644
--- a/src/opt/sfm/sfmWin.c
+++ b/src/opt/sfm/sfmWin.c
@@ -275,6 +275,7 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
Sfm_NtkIncrementTravId( p );
if ( Sfm_NtkCollectTfi_rec( p, iNode, p->pPars->nWinSizeMax ) )
{
+ p->nMaxDivs++;
p->timeWin += clock() - clk;
return 0;
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-02 23:59:34 +0000