summaryrefslogtreecommitdiffstats
path: root/src/opt
diff options
context:
space:
mode:
Diffstat (limited to 'src/opt')
-rw-r--r--src/opt/mfs/mfs.h1
-rw-r--r--src/opt/sfm/sfm.h1
-rw-r--r--src/opt/sfm/sfmCore.c1
-rw-r--r--src/opt/sfm/sfmInt.h8
-rw-r--r--src/opt/sfm/sfmNtk.c62
-rw-r--r--src/opt/sfm/sfmWin.c5
6 files changed, 65 insertions, 13 deletions
diff --git a/src/opt/mfs/mfs.h b/src/opt/mfs/mfs.h
index 4ca0df00..cf7e2f6e 100644
--- a/src/opt/mfs/mfs.h
+++ b/src/opt/mfs/mfs.h
@@ -46,7 +46,6 @@ struct Mfs_Par_t_
int nWinTfoLevs; // the maximum fanout levels
int nFanoutsMax; // the maximum number of fanouts
int nDepthMax; // the maximum number of logic levels
- int nDivMax; // the maximum number of divisors
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
diff --git a/src/opt/sfm/sfm.h b/src/opt/sfm/sfm.h
index 18960183..ef04da02 100644
--- a/src/opt/sfm/sfm.h
+++ b/src/opt/sfm/sfm.h
@@ -46,6 +46,7 @@ struct Sfm_Par_t_
int nFanoutMax; // the maximum number of fanouts
int nDepthMax; // the maximum depth to try
int nWinSizeMax; // the maximum window size
+ int nGrowthLevel; // the maximum allowed growth in level
int nBTLimit; // the maximum number of conflicts in one SAT run
int nFirstFixed; // the number of first nodes to be treated as fixed
int fFixLevel; // does not allow level to increase
diff --git a/src/opt/sfm/sfmCore.c b/src/opt/sfm/sfmCore.c
index af2cb836..9efb70e2 100644
--- a/src/opt/sfm/sfmCore.c
+++ b/src/opt/sfm/sfmCore.c
@@ -49,6 +49,7 @@ void Sfm_ParSetDefault( Sfm_Par_t * pPars )
pPars->nFanoutMax = 30; // the maximum number of fanouts
pPars->nDepthMax = 20; // the maximum depth to try
pPars->nWinSizeMax = 300; // the maximum window size
+ pPars->nGrowthLevel = 0; // the maximum allowed growth in level
pPars->nBTLimit = 5000; // the maximum number of conflicts in one SAT run
pPars->fFixLevel = 1; // does not allow level to increase
pPars->fRrOnly = 0; // perform redundancy removal
diff --git a/src/opt/sfm/sfmInt.h b/src/opt/sfm/sfmInt.h
index 60648b44..c9ccbc89 100644
--- a/src/opt/sfm/sfmInt.h
+++ b/src/opt/sfm/sfmInt.h
@@ -58,6 +58,7 @@ struct Sfm_Ntk_t_
int nPos; // PO count (POs should be last objects)
int nNodes; // internal nodes
int nObjs; // total objects
+ int nLevelMax; // maximum level
// user data
Vec_Str_t * vFixed; // persistent objects
Vec_Wrd_t * vTruths; // truth tables
@@ -65,6 +66,7 @@ struct Sfm_Ntk_t_
// attributes
Vec_Wec_t vFanouts; // fanouts
Vec_Int_t vLevels; // logic level
+ Vec_Int_t vLevelsR; // logic level
Vec_Int_t vCounts; // fanin counters
Vec_Int_t vId2Var; // ObjId -> SatVar
Vec_Int_t vVar2Id; // SatVar -> ObjId
@@ -148,6 +150,9 @@ static inline void Sfm_NtkCleanVars( Sfm_Ntk_t * p ) { int i;
static inline int Sfm_ObjLevel( Sfm_Ntk_t * p, int iObj ) { return Vec_IntEntry( &p->vLevels, iObj ); }
static inline void Sfm_ObjSetLevel( Sfm_Ntk_t * p, int iObj, int Lev ) { Vec_IntWriteEntry( &p->vLevels, iObj, Lev ); }
+static inline int Sfm_ObjLevelR( Sfm_Ntk_t * p, int iObj ) { return Vec_IntEntry( &p->vLevelsR, iObj ); }
+static inline void Sfm_ObjSetLevelR( Sfm_Ntk_t * p, int iObj, int Lev ) { Vec_IntWriteEntry( &p->vLevelsR, iObj, Lev ); }
+
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); }
@@ -157,7 +162,8 @@ extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars );
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
-#define Sfm_NtkForEachNode( p, i ) for ( i = p->nPis; i + p->nPos < p->nObjs; i++ )
+#define Sfm_NtkForEachNode( p, i ) for ( i = p->nPis; i + p->nPos < p->nObjs; i++ )
+#define Sfm_NtkForEachNodeReverse( p, i ) for ( i = p->nObjs - p->nPos - 1; i >= p->nPis; i-- )
#define Sfm_ObjForEachFanin( p, Node, Fan, i ) for ( i = 0; i < Sfm_ObjFaninNum(p, Node) && ((Fan = Sfm_ObjFanin(p, Node, i)), 1); i++ )
#define Sfm_ObjForEachFanout( p, Node, Fan, i ) for ( i = 0; i < Sfm_ObjFanoutNum(p, Node) && ((Fan = Sfm_ObjFanout(p, Node, i)), 1); i++ )
diff --git a/src/opt/sfm/sfmNtk.c b/src/opt/sfm/sfmNtk.c
index e66e6e8e..1e650454 100644
--- a/src/opt/sfm/sfmNtk.c
+++ b/src/opt/sfm/sfmNtk.c
@@ -107,21 +107,49 @@ void Sfm_CreateFanout( Vec_Wec_t * vFanins, Vec_Wec_t * vFanouts )
SeeAlso []
***********************************************************************/
-static inline int Sfm_ObjCreateLevel( Vec_Int_t * vArray, Vec_Int_t * vLevels )
+static inline int Sfm_ObjLevelNew( Vec_Int_t * vArray, Vec_Int_t * vLevels )
{
int k, Fanin, Level = 0;
Vec_IntForEachEntry( vArray, Fanin, k )
- Level = Abc_MaxInt( Level, Vec_IntEntry(vLevels, Fanin) + 1 );
- return Level;
+ Level = Abc_MaxInt( Level, Vec_IntEntry(vLevels, Fanin) );
+ return Level + 1;
}
void Sfm_CreateLevel( Vec_Wec_t * vFanins, Vec_Int_t * vLevels )
{
Vec_Int_t * vArray;
int i;
assert( Vec_IntSize(vLevels) == 0 );
- Vec_IntGrow( vLevels, Vec_WecSize(vFanins) );
+ Vec_IntFill( vLevels, Vec_WecSize(vFanins), 0 );
Vec_WecForEachLevel( vFanins, vArray, i )
- Vec_IntPush( vLevels, Sfm_ObjCreateLevel(vArray, vLevels) );
+ Vec_IntWriteEntry( vLevels, i, Sfm_ObjLevelNew(vArray, vLevels) );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Sfm_ObjLevelNewR( Vec_Int_t * vArray, Vec_Int_t * vLevelsR )
+{
+ int k, Fanout, LevelR = 0;
+ Vec_IntForEachEntry( vArray, Fanout, k )
+ LevelR = Abc_MaxInt( LevelR, Vec_IntEntry(vLevelsR, Fanout) );
+ return LevelR + 1;
+}
+void Sfm_CreateLevelR( Vec_Wec_t * vFanouts, Vec_Int_t * vLevelsR )
+{
+ Vec_Int_t * vArray;
+ int i;
+ assert( Vec_IntSize(vLevelsR) == 0 );
+ Vec_IntFill( vLevelsR, Vec_WecSize(vFanouts), 0 );
+ Vec_WecForEachLevelReverse( vFanouts, vArray, i )
+ Vec_IntWriteEntry( vLevelsR, i, Sfm_ObjLevelNewR(vArray, vLevelsR) );
}
/**Function*************************************************************
@@ -152,6 +180,7 @@ Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t
// attributes
Sfm_CreateFanout( &p->vFanins, &p->vFanouts );
Sfm_CreateLevel( &p->vFanins, &p->vLevels );
+ Sfm_CreateLevelR( &p->vFanouts, &p->vLevelsR );
Vec_IntFill( &p->vCounts, p->nObjs, 0 );
Vec_IntFill( &p->vTravIds, p->nObjs, 0 );
Vec_IntFill( &p->vTravIds2, p->nObjs, 0 );
@@ -163,6 +192,7 @@ Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t
}
void Sfm_NtkPrepare( Sfm_Ntk_t * p )
{
+ p->nLevelMax = Vec_IntFindMax(&p->vLevels) + p->pPars->nGrowthLevel;
p->vNodes = Vec_IntAlloc( 1000 );
p->vDivs = Vec_IntAlloc( 100 );
p->vRoots = Vec_IntAlloc( 1000 );
@@ -187,6 +217,7 @@ void Sfm_NtkFree( Sfm_Ntk_t * p )
// attributes
Vec_WecErase( &p->vFanouts );
ABC_FREE( p->vLevels.pArray );
+ ABC_FREE( p->vLevelsR.pArray );
ABC_FREE( p->vCounts.pArray );
ABC_FREE( p->vTravIds.pArray );
ABC_FREE( p->vTravIds2.pArray );
@@ -260,13 +291,22 @@ void Sfm_NtkDeleteObj_rec( Sfm_Ntk_t * p, int iNode )
void Sfm_NtkUpdateLevel_rec( Sfm_Ntk_t * p, int iNode )
{
int i, iFanout;
- int LevelNew = Sfm_ObjCreateLevel( Sfm_ObjFiArray(p, iNode), &p->vLevels );
+ int LevelNew = Sfm_ObjLevelNew( Sfm_ObjFiArray(p, iNode), &p->vLevels );
if ( LevelNew == Sfm_ObjLevel(p, iNode) )
return;
Sfm_ObjSetLevel( p, iNode, LevelNew );
- if ( Sfm_ObjIsNode(p, iNode) )
- Sfm_ObjForEachFanout( p, iNode, iFanout, i )
- Sfm_NtkUpdateLevel_rec( p, iFanout );
+ Sfm_ObjForEachFanout( p, iNode, iFanout, i )
+ Sfm_NtkUpdateLevel_rec( p, iFanout );
+}
+void Sfm_NtkUpdateLevelR_rec( Sfm_Ntk_t * p, int iNode )
+{
+ int i, iFanin;
+ int LevelNew = Sfm_ObjLevelNewR( Sfm_ObjFoArray(p, iNode), &p->vLevelsR );
+ if ( LevelNew == Sfm_ObjLevelR(p, iNode) )
+ return;
+ Sfm_ObjSetLevelR( p, iNode, LevelNew );
+ Sfm_ObjForEachFanin( p, iNode, iFanin, i )
+ Sfm_NtkUpdateLevelR_rec( p, iFanin );
}
void Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth )
{
@@ -292,6 +332,10 @@ void Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth
}
// update logic level
Sfm_NtkUpdateLevel_rec( p, iNode );
+ if ( iFaninNew != -1 )
+ Sfm_NtkUpdateLevelR_rec( p, iFaninNew );
+ if ( Sfm_ObjFanoutNum(p, iFanin) > 0 )
+ Sfm_NtkUpdateLevelR_rec( p, iFanin );
// update truth table
Vec_WrdWriteEntry( p->vTruths, iNode, uTruth );
Sfm_TruthToCnf( uTruth, Sfm_ObjFaninNum(p, iNode), p->vCover, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode) );
diff --git a/src/opt/sfm/sfmWin.c b/src/opt/sfm/sfmWin.c
index db6bd0ea..f12474c9 100644
--- a/src/opt/sfm/sfmWin.c
+++ b/src/opt/sfm/sfmWin.c
@@ -215,7 +215,7 @@ void Sfm_NtkAddDivisors( Sfm_Ntk_t * p, int iNode, int nLevelMax )
return;
// skip TFI nodes, PO nodes, or nodes with high logic level
if ( Sfm_ObjIsTravIdCurrent(p, iFanout) || Sfm_ObjIsPo(p, iFanout) ||
- (p->pPars->fFixLevel && Sfm_ObjLevel(p, iFanout) >= nLevelMax) )
+ (p->pPars->fFixLevel && Sfm_ObjLevel(p, iFanout) > nLevelMax) )
continue;
// handle single-input nodes
if ( Sfm_ObjFaninNum(p, iFanout) == 1 )
@@ -311,7 +311,8 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
Sfm_NtkIncrementTravId2( p );
Vec_IntForEachEntry( p->vDivs, iTemp, i )
if ( Vec_IntSize(p->vDivs) < p->pPars->nWinSizeMax + 0 )
- Sfm_NtkAddDivisors( p, iTemp, Sfm_ObjLevel(p, iNode) );
+// Sfm_NtkAddDivisors( p, iTemp, Sfm_ObjLevel(p, iNode) - 1 );
+ Sfm_NtkAddDivisors( p, iTemp, p->nLevelMax - Sfm_ObjLevelR(p, iNode) );
}
if ( Vec_IntSize(p->vDivs) > p->pPars->nWinSizeMax )
{
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 07:17:11 +0000