summaryrefslogtreecommitdiffstats
path: root/src/opt/sfm
diff options
context:
space:
mode:
Diffstat (limited to 'src/opt/sfm')
-rw-r--r--src/opt/sfm/sfm.h3
-rw-r--r--src/opt/sfm/sfmCore.c26
-rw-r--r--src/opt/sfm/sfmInt.h3
-rw-r--r--src/opt/sfm/sfmSat.c31
-rw-r--r--src/opt/sfm/sfmWin.c84
5 files changed, 64 insertions, 83 deletions
diff --git a/src/opt/sfm/sfm.h b/src/opt/sfm/sfm.h
index f6380e65..c34ae859 100644
--- a/src/opt/sfm/sfm.h
+++ b/src/opt/sfm/sfm.h
@@ -45,10 +45,11 @@ struct Sfm_Par_t_
int nTfoLevMax; // the maximum fanout levels
int nFanoutMax; // the maximum number of fanouts
int nDepthMax; // the maximum depth to try
- int nDivNumMax; // the maximum number of divisors
int nWinSizeMax; // the maximum window size
+ int nDivNumMax; // the maximum number of divisors
int nBTLimit; // the maximum number of conflicts in one SAT run
int fFixLevel; // does not allow level to increase
+ int fRrOnly; // perform redundance removal
int fArea; // performs optimization for area
int fMoreEffort; // performs high-affort minimization
int fVerbose; // enable basic stats
diff --git a/src/opt/sfm/sfmCore.c b/src/opt/sfm/sfmCore.c
index e9721ec7..9d96a1ac 100644
--- a/src/opt/sfm/sfmCore.c
+++ b/src/opt/sfm/sfmCore.c
@@ -47,11 +47,12 @@ void Sfm_ParSetDefault( Sfm_Par_t * pPars )
memset( pPars, 0, sizeof(Sfm_Par_t) );
pPars->nTfoLevMax = 2; // the maximum fanout levels
pPars->nFanoutMax = 10; // the maximum number of fanouts
- pPars->nDepthMax = 0; // the maximum depth to try
- pPars->nDivNumMax = 300; // the maximum number of divisors
+ pPars->nDepthMax = 20; // the maximum depth to try
pPars->nWinSizeMax = 300; // the maximum window size
+ pPars->nDivNumMax = 300; // the maximum number of divisors
pPars->nBTLimit = 0; // the maximum number of conflicts in one SAT run
pPars->fFixLevel = 1; // does not allow level to increase
+ pPars->fRrOnly = 0; // perform redundancy removal
pPars->fArea = 0; // performs optimization for area
pPars->fMoreEffort = 0; // performs high-affort minimization
pPars->fVerbose = 0; // enable basic stats
@@ -76,13 +77,13 @@ void Sfm_NtkPrintStats( Sfm_Ntk_t * p )
Sfm_NtkNodeNum(p), p->nNodesTried, p->nRemoves + p->nResubs, p->nTotalDivs, p->nSatCalls, p->nTimeOuts );
printf( "Attempts : " );
- printf( "Remove %6d -> %6d (%6.2f %%) ", p->nTryRemoves, p->nRemoves, 100.0*p->nRemoves/Abc_MaxInt(1, p->nTryRemoves) );
- printf( "Resub %6d -> %6d (%6.2f %%) ", p->nTryResubs, p->nResubs, 100.0*p->nResubs /Abc_MaxInt(1, p->nTryResubs) );
+ printf( "Remove %6d out of %6d (%6.2f %%) ", p->nRemoves, p->nTryRemoves, p->nRemoves, 100.0*p->nRemoves/Abc_MaxInt(1, p->nTryRemoves) );
+ printf( "Resub %6d out of %6d (%6.2f %%) ", p->nResubs, p->nTryResubs, p->nResubs, 100.0*p->nResubs /Abc_MaxInt(1, p->nTryResubs) );
printf( "\n" );
printf( "Reduction: " );
- printf( "Nodes %6d -> %6d (%6.2f %%) ", p->nTotalNodesBeg, p->nTotalNodesEnd, 100.0*(p->nTotalNodesBeg-p->nTotalNodesEnd)/Abc_MaxInt(1, p->nTotalNodesBeg) );
- printf( "Edges %6d -> %6d (%6.2f %%) ", p->nTotalEdgesBeg, p->nTotalEdgesEnd, 100.0*(p->nTotalEdgesBeg-p->nTotalEdgesEnd)/Abc_MaxInt(1, p->nTotalEdgesBeg) );
+ printf( "Nodes %6d out of %6d (%6.2f %%) ", p->nTotalNodesBeg-p->nTotalNodesEnd, p->nTotalNodesEnd, 100.0*(p->nTotalNodesBeg-p->nTotalNodesEnd)/Abc_MaxInt(1, p->nTotalNodesBeg) );
+ printf( "Edges %6d out of %6d (%6.2f %%) ", p->nTotalEdgesBeg-p->nTotalEdgesEnd, p->nTotalEdgesEnd, 100.0*(p->nTotalEdgesBeg-p->nTotalEdgesEnd)/Abc_MaxInt(1, p->nTotalEdgesBeg) );
printf( "\n" );
ABC_PRTP( "Win", p->timeWin , p->timeTotal );
@@ -117,10 +118,7 @@ int Sfm_NodeResubSolve( Sfm_Ntk_t * p, int iNode, int f, int fRemoveOnly )
{
int i = 0;
}
- if ( fRemoveOnly )
- p->nTryRemoves++;
- else
- p->nTryResubs++;
+ p->nTryRemoves++;
// report init stats
if ( p->pPars->fVeryVerbose )
printf( "%5d : Lev =%3d. Leaf =%3d. Node =%3d. Div=%3d. Fanin = %d/%d. MFFC = %d\n",
@@ -145,10 +143,10 @@ p->timeSat += clock() - clk;
}
if ( uTruth != SFM_SAT_SAT )
goto finish;
- if ( fRemoveOnly || Vec_IntSize(p->vDivs) == 0 )
+ if ( fRemoveOnly || p->pPars->fRrOnly || Vec_IntSize(p->vDivs) == 0 )
return 0;
-// return 0;
+ p->nTryResubs++;
if ( fVeryVerbose )
{
for ( i = 0; i < 9; i++ )
@@ -197,7 +195,8 @@ finish:
if ( iVar == -1 )
printf( "Node %d: Fanin %d (%d) can be removed. ", iNode, f, Sfm_ObjFanin(p, iNode, f) );
else
- printf( "Node %d: Fanin %d (%d) can be replaced by divisor %d. ", iNode, f, Sfm_ObjFanin(p, iNode, f), iVar );
+ printf( "Node %d: Fanin %d (%d) can be replaced by divisor %d (%d). ",
+ iNode, f, Sfm_ObjFanin(p, iNode, f), iVar, Vec_IntEntry(p->vDivs, iVar) );
Kit_DsdPrintFromTruth( (unsigned *)&uTruth, Vec_IntSize(p->vDivIds) ); printf( "\n" );
}
if ( iVar == -1 )
@@ -218,7 +217,6 @@ int Sfm_NodeResub( Sfm_Ntk_t * p, int iNode )
if ( !Sfm_NtkCreateWindow( p, iNode, p->pPars->fVeryVerbose ) )
return 0;
Sfm_NtkWindowToSolver( p );
- Sfm_NtkPrepareDivisors( p, iNode );
// try replacing area critical fanins
Sfm_ObjForEachFanin( p, iNode, iFanin, i )
if ( Sfm_ObjIsNode(p, iFanin) && Sfm_ObjFanoutNum(p, iFanin) == 1 )
diff --git a/src/opt/sfm/sfmInt.h b/src/opt/sfm/sfmInt.h
index 5c41e9f0..bdb1c600 100644
--- a/src/opt/sfm/sfmInt.h
+++ b/src/opt/sfm/sfmInt.h
@@ -152,6 +152,7 @@ static inline void Sfm_ObjSetLevel( Sfm_Ntk_t * p, int iObj, int Lev ) { Vec_In
static inline int Sfm_ObjUpdateFaninCount( Sfm_Ntk_t * p, int iObj ) { return Vec_IntAddToEntry(&p->vCounts, iObj, -1); }
static inline void Sfm_ObjResetFaninCount( Sfm_Ntk_t * p, int iObj ) { Vec_IntWriteEntry(&p->vCounts, iObj, Sfm_ObjFaninNum(p, iObj)-1); }
+extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars );
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
@@ -181,8 +182,6 @@ extern word Sfm_ComputeInterpolant( Sfm_Ntk_t * p );
/*=== sfmWin.c ==========================================================*/
extern int Sfm_ObjMffcSize( Sfm_Ntk_t * p, int iObj );
extern int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose );
-extern void Sfm_NtkPrepareDivisors( Sfm_Ntk_t * p, int iNode );
-
ABC_NAMESPACE_HEADER_END
diff --git a/src/opt/sfm/sfmSat.c b/src/opt/sfm/sfmSat.c
index 4a06dde6..228a5fd8 100644
--- a/src/opt/sfm/sfmSat.c
+++ b/src/opt/sfm/sfmSat.c
@@ -42,28 +42,6 @@ static word s_Truths6[6] = {
/**Function*************************************************************
- Synopsis [Creates order of objects in the SAT solver.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Sfm_NtkOrderObjects( Sfm_Ntk_t * p )
-{
- int i, iNode;
- assert( Vec_IntEntryLast(p->vNodes) == Vec_IntEntry(p->vDivs, Vec_IntSize(p->vLeaves) + Vec_IntSize(p->vNodes) - 1) );
- Vec_IntClear( p->vOrder );
- Vec_IntForEachEntryReverse( p->vNodes, iNode, i )
- Vec_IntPush( p->vOrder, iNode );
- Vec_IntForEachEntryStart( p->vDivs, iNode, i, Vec_IntSize(p->vLeaves) + Vec_IntSize(p->vNodes) )
- Vec_IntPush( p->vOrder, iNode );
-}
-
-/**Function*************************************************************
-
Synopsis [Converts a window into a SAT solver.]
Description []
@@ -85,14 +63,17 @@ void Sfm_NtkWindowToSolver( Sfm_Ntk_t * p )
// create SAT variables
Sfm_NtkCleanVars( p );
p->nSatVars = 1;
- Sfm_NtkOrderObjects( p );
Vec_IntForEachEntry( p->vOrder, iNode, i )
Sfm_ObjSetSatVar( p, iNode, p->nSatVars++ );
- Vec_IntForEachEntry( p->vLeaves, iNode, i )
- Sfm_ObjSetSatVar( p, iNode, p->nSatVars++ );
+ // create divisor variables
+ Vec_IntClear( p->vDivVars );
+ Vec_IntForEachEntry( p->vDivs, iNode, i )
+ Vec_IntPush( p->vDivVars, Sfm_ObjSatVar(p, iNode) );
// add CNF clauses for the TFI
Vec_IntForEachEntry( p->vOrder, iNode, i )
{
+ if ( Sfm_ObjIsPi(p, iNode) )
+ continue;
// collect fanin variables
Vec_IntClear( p->vFaninMap );
Sfm_ObjForEachFanin( p, iNode, iFanin, k )
diff --git a/src/opt/sfm/sfmWin.c b/src/opt/sfm/sfmWin.c
index 887bf0f7..f96221c0 100644
--- a/src/opt/sfm/sfmWin.c
+++ b/src/opt/sfm/sfmWin.c
@@ -265,14 +265,51 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
else
Vec_IntPush( p->vRoots, iNode );
p->timeWin += clock() - clk;
- // collect divisors of the TFI nodes
clk = clock();
- Vec_IntAppend( p->vDivs, p->vLeaves );
- Vec_IntAppend( p->vDivs, p->vNodes );
+ // create ordering of the nodes
+ Vec_IntClear( p->vOrder );
+ Vec_IntForEachEntryReverse( p->vNodes, iNode, i )
+ Vec_IntPush( p->vOrder, iNode );
+ Vec_IntForEachEntry( p->vLeaves, iNode, i )
+ Vec_IntPush( p->vOrder, iNode );
+ // mark fanins
Sfm_NtkIncrementTravId2( p );
- Vec_IntForEachEntry( p->vDivs, iTemp, i )
- if ( iTemp != iNode && Vec_IntSize(p->vDivs) < p->pPars->nDivNumMax )
- Sfm_NtkAddDivisors( p, iTemp, Sfm_ObjLevel(p, iNode) );
+ Sfm_ObjSetTravIdCurrent2( p, iNode );
+ Sfm_ObjForEachFanin( p, iNode, iTemp, i )
+ Sfm_ObjSetTravIdCurrent2( p, iTemp );
+ // compact divisors
+ Vec_IntClear( p->vDivs );
+ Vec_IntForEachEntry( p->vLeaves, iTemp, i )
+ if ( !Sfm_ObjIsTravIdCurrent2( p, iTemp ) )
+ Vec_IntPush( p->vDivs, iTemp );
+ Vec_IntForEachEntry( p->vNodes, iTemp, i )
+ if ( !Sfm_ObjIsTravIdCurrent2( p, iTemp ) )
+ Vec_IntPush( p->vDivs, iTemp );
+ // if we exceed the limit, remove the first few
+ if ( Vec_IntSize(p->vDivs) > p->pPars->nDivNumMax )
+ {
+ int k = 0;
+ Vec_IntForEachEntryStart( p->vDivs, iTemp, i, Vec_IntSize(p->vDivs) - p->pPars->nDivNumMax )
+ Vec_IntWriteEntry( p->vDivs, k++, iTemp );
+ Vec_IntShrink( p->vDivs, k );
+ assert( Vec_IntSize(p->vDivs) == p->pPars->nDivNumMax );
+ }
+ // collect additional divisors of the TFI nodes
+ if ( Vec_IntSize(p->vDivs) < p->pPars->nDivNumMax )
+ {
+ int nStartNew = Vec_IntSize(p->vDivs);
+ Sfm_NtkIncrementTravId2( p );
+ Vec_IntForEachEntry( p->vDivs, iTemp, i )
+ if ( Vec_IntSize(p->vDivs) < p->pPars->nDivNumMax )
+ Sfm_NtkAddDivisors( p, iTemp, Sfm_ObjLevel(p, iNode) );
+ if ( Vec_IntSize(p->vDivs) > p->pPars->nDivNumMax )
+ Vec_IntShrink( p->vDivs, p->pPars->nDivNumMax );
+ // add new divisor variable to the order
+ Vec_IntForEachEntryStart( p->vDivs, iTemp, i, nStartNew )
+ Vec_IntPush( p->vOrder, iTemp );
+ }
+ assert( Vec_IntSize(p->vDivs) <= p->pPars->nDivNumMax );
+ // statistics
p->nTotalDivs += Vec_IntSize(p->vDivs);
p->timeDiv += clock() - clk;
if ( !fVerbose )
@@ -294,41 +331,6 @@ void Sfm_NtkWindowTest( Sfm_Ntk_t * p, int iNode )
Sfm_NtkCreateWindow( p, i, 1 );
}
-/**Function*************************************************************
-
- Synopsis [Removes node and its fanins from the array of divisors.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Sfm_NtkPrepareDivisors( Sfm_Ntk_t * p, int iNode )
-{
- int i, iFanin, k = 0;
- // mark fanins
- Sfm_NtkIncrementTravId( p );
- Sfm_ObjSetTravIdCurrent( p, iNode );
- Sfm_ObjForEachFanin( p, iNode, iFanin, i )
- Sfm_ObjSetTravIdCurrent( p, iFanin );
- // compact divisors
- Vec_IntClear( p->vDivVars );
- Vec_IntForEachEntry( p->vDivs, iFanin, i )
- if ( !Sfm_ObjIsTravIdCurrent( p, iFanin ) )
- {
- Vec_IntPush( p->vDivVars, Sfm_ObjSatVar(p, iFanin) );
- Vec_IntWriteEntry( p->vDivs, k++, iFanin );
- }
- assert( Vec_IntSize(p->vDivs) == k + Sfm_ObjFaninNum(p, iNode) + 1 );
- Vec_IntShrink( p->vDivs, k );
- // collect fanins
-// Vec_IntClear( p->vFans );
-// Sfm_ObjForEachFanin( p, iNode, iFanin, i )
-// Vec_IntPush( p->vFans, iFanin );
-}
-
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 06:09:19 +0000