summaryrefslogtreecommitdiffstats
path: root/src/opt
diff options
context:
space:
mode:
Diffstat (limited to 'src/opt')
-rw-r--r--src/opt/sfm/sfm.h2
-rw-r--r--src/opt/sfm/sfmCore.c9
-rw-r--r--src/opt/sfm/sfmNtk.c3
-rw-r--r--src/opt/sfm/sfmSat.c6
-rw-r--r--src/opt/sfm/sfmWin.c36
5 files changed, 42 insertions, 14 deletions
diff --git a/src/opt/sfm/sfm.h b/src/opt/sfm/sfm.h
index c8a30030..1d97cd8b 100644
--- a/src/opt/sfm/sfm.h
+++ b/src/opt/sfm/sfm.h
@@ -77,7 +77,7 @@ extern word * Sfm_NodeReadTruth( Sfm_Ntk_t * p, int i );
extern int Sfm_NodeReadFixed( Sfm_Ntk_t * p, int i );
extern int Sfm_NodeReadUsed( Sfm_Ntk_t * p, int i );
/*=== sfmWin.c ==========================================================*/
-extern Vec_Int_t * Sfm_NtkDfs( Sfm_Ntk_t * p );
+extern Vec_Int_t * Sfm_NtkDfs( Sfm_Ntk_t * p, Vec_Wec_t * vGroups, Vec_Int_t * vGroupMap, Vec_Int_t * vBoxesLeft );
ABC_NAMESPACE_HEADER_END
diff --git a/src/opt/sfm/sfmCore.c b/src/opt/sfm/sfmCore.c
index 9936fa9f..11ace2d0 100644
--- a/src/opt/sfm/sfmCore.c
+++ b/src/opt/sfm/sfmCore.c
@@ -258,8 +258,13 @@ int Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars )
{
int i, k, Counter = 0;
p->timeTotal = Abc_Clock();
- if ( pPars->fVerbose && Vec_StrSum(p->vFixed) > 0 )
- printf( "Performing MFS with %d fixed objects.\n", Vec_StrSum(p->vFixed) );
+ if ( pPars->fVerbose )
+ {
+ int nFixed = p->vFixed ? Vec_StrSum(p->vFixed) : 0;
+ int nEmpty = p->vEmpty ? Vec_StrSum(p->vEmpty) : 0;
+ printf( "Performing MFS with %d PIs, %d POs, %d nodes (%d flexible, %d fixed, %d empty).\n",
+ p->nPis, p->nPos, p->nNodes, p->nNodes-nFixed, nFixed, nEmpty );
+ }
p->pPars = pPars;
Sfm_NtkPrepare( p );
// Sfm_ComputeInterpolantCheck( p );
diff --git a/src/opt/sfm/sfmNtk.c b/src/opt/sfm/sfmNtk.c
index fd04e432..1ded0ede 100644
--- a/src/opt/sfm/sfmNtk.c
+++ b/src/opt/sfm/sfmNtk.c
@@ -54,7 +54,8 @@ void Sfm_CheckConsistency( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t *
assert( Vec_IntSize(vArray) == 0 && Vec_StrEntry(vFixed, i) == (char)0 );
// nodes are in a topo order; POs cannot be fanins
Vec_IntForEachEntry( vArray, Fanin, k )
- assert( Fanin < i && Fanin + nPos < Vec_WecSize(vFanins) );
+// assert( Fanin < i && Fanin + nPos < Vec_WecSize(vFanins) );
+ assert( Fanin + nPos < Vec_WecSize(vFanins) );
// POs have one fanout
if ( i + nPos >= Vec_WecSize(vFanins) )
assert( Vec_IntSize(vArray) == 1 && Vec_StrEntry(vFixed, i) == (char)0 );
diff --git a/src/opt/sfm/sfmSat.c b/src/opt/sfm/sfmSat.c
index f61ee798..0d5bbca2 100644
--- a/src/opt/sfm/sfmSat.c
+++ b/src/opt/sfm/sfmSat.c
@@ -91,7 +91,8 @@ int Sfm_NtkWindowToSolver( Sfm_Ntk_t * p )
if ( Vec_IntSize(vClause) == 0 )
break;
RetValue = sat_solver_addclause( p->pSat, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause) );
- assert( RetValue );
+ if ( RetValue == 0 )
+ return 0;
}
}
if ( Vec_IntSize(p->vTfo) > 0 )
@@ -126,7 +127,8 @@ int Sfm_NtkWindowToSolver( Sfm_Ntk_t * p )
if ( Vec_IntSize(vClause) == 0 )
break;
RetValue = sat_solver_addclause( p->pSat, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause) );
- assert( RetValue );
+ if ( RetValue == 0 )
+ return 0;
}
}
// create XOR clauses for the roots
diff --git a/src/opt/sfm/sfmWin.c b/src/opt/sfm/sfmWin.c
index 9f91c936..6eab478e 100644
--- a/src/opt/sfm/sfmWin.c
+++ b/src/opt/sfm/sfmWin.c
@@ -125,33 +125,53 @@ static inline int Sfm_ObjIsTravIdCurrent2( Sfm_Ntk_t * p, int Id ) { return
Synopsis [Collects used internal nodes in a topological order.]
- Description []
+ Description [Additionally considers objects in groups as a single object
+ and collects them in a topological order together as single entity.]
SideEffects []
SeeAlso []
***********************************************************************/
-void Sfm_NtkDfs_rec( Sfm_Ntk_t * p, int iNode, Vec_Int_t * vNodes )
+void Sfm_NtkDfs_rec( Sfm_Ntk_t * p, int iNode, Vec_Int_t * vNodes, Vec_Wec_t * vGroups, Vec_Int_t * vGroupMap, Vec_Int_t * vBoxesLeft )
{
int i, iFanin;
if ( Sfm_ObjIsPi(p, iNode) )
return;
if ( Sfm_ObjIsTravIdCurrent(p, iNode) )
return;
- Sfm_ObjSetTravIdCurrent(p, iNode);
- Sfm_ObjForEachFanin( p, iNode, iFanin, i )
- Sfm_NtkDfs_rec( p, iFanin, vNodes );
- Vec_IntPush( vNodes, iNode );
+ if ( Vec_IntEntry(vGroupMap, iNode) >= 0 )
+ {
+ int k, iGroup = Abc_Lit2Var( Vec_IntEntry(vGroupMap, iNode) );
+ Vec_Int_t * vGroup = Vec_WecEntry( vGroups, iGroup );
+ Vec_IntForEachEntry( vGroup, iNode, i )
+ assert( Sfm_ObjIsNode(p, iNode) );
+ Vec_IntForEachEntry( vGroup, iNode, i )
+ Sfm_ObjSetTravIdCurrent( p, iNode );
+ Vec_IntForEachEntry( vGroup, iNode, i )
+ Sfm_ObjForEachFanin( p, iNode, iFanin, k )
+ Sfm_NtkDfs_rec( p, iFanin, vNodes, vGroups, vGroupMap, vBoxesLeft );
+ Vec_IntForEachEntry( vGroup, iNode, i )
+ Vec_IntPush( vNodes, iNode );
+ Vec_IntPush( vBoxesLeft, iGroup );
+ }
+ else
+ {
+ Sfm_ObjSetTravIdCurrent(p, iNode);
+ Sfm_ObjForEachFanin( p, iNode, iFanin, i )
+ Sfm_NtkDfs_rec( p, iFanin, vNodes, vGroups, vGroupMap, vBoxesLeft );
+ Vec_IntPush( vNodes, iNode );
+ }
}
-Vec_Int_t * Sfm_NtkDfs( Sfm_Ntk_t * p )
+Vec_Int_t * Sfm_NtkDfs( Sfm_Ntk_t * p, Vec_Wec_t * vGroups, Vec_Int_t * vGroupMap, Vec_Int_t * vBoxesLeft )
{
Vec_Int_t * vNodes;
int i;
+ Vec_IntClear( vBoxesLeft );
vNodes = Vec_IntAlloc( p->nObjs );
Sfm_NtkIncrementTravId( p );
Sfm_NtkForEachPo( p, i )
- Sfm_NtkDfs_rec( p, Sfm_ObjFanin(p, i, 0), vNodes );
+ Sfm_NtkDfs_rec( p, Sfm_ObjFanin(p, i, 0), vNodes, vGroups, vGroupMap, vBoxesLeft );
return vNodes;
}
generated by cgit v1.2.3 (git 2.25.1) at 2025-07-22 23:22:47 +0000