Fixing a bug in &mfs when black boxes are present.

This commit is contained in:
Alan Mishchenko
2025-11-26 17:57:16 -08:00
parent ee899284b8
commit 7691e2ed3c
3 changed files with 92 additions and 37 deletions

View File

@@ -300,6 +300,9 @@ Gia_Man_t * Gia_ManInsertMfs( Gia_Man_t * p, Sfm_Ntk_t * pNtk, int fAllBoxes )
Vec_Int_t * vArray, * vLeaves;
Vec_Int_t * vMapping, * vMapping2;
Vec_Int_t * vCoDrivers;
Vec_Int_t * vPiBoxes = NULL;
Vec_Int_t * vBbCiMap = NULL;
Vec_Int_t * vBbOutLit = NULL;
int nBbIns = 0, nBbOuts = 0;
if ( pManTime ) Tim_ManBlackBoxIoNum( pManTime, &nBbIns, &nBbOuts );
nMfsNodes = 1 + Gia_ManCiNum(p) + Gia_ManLutNum(p) + Gia_ManCoNum(p) + nBbIns + nBbOuts;
@@ -341,8 +344,36 @@ Gia_Man_t * Gia_ManInsertMfs( Gia_Man_t * p, Sfm_Ntk_t * pNtk, int fAllBoxes )
assert( curCo == Gia_ManCoNum(p) );
// collect nodes in the given order
if ( nBbOuts > 0 )
{
int iBbOut = 0;
vPiBoxes = Vec_IntStartFull( nBbOuts + nRealPis );
vBbCiMap = Vec_IntStartFull( Gia_ManCiNum(p) );
vBbOutLit = Vec_IntStartFull( nBbOuts );
curCi = nRealPis;
curCo = 0;
for ( i = 0; i < nBoxes; i++ )
{
nBoxIns = Tim_ManBoxInputNum( pManTime, i );
nBoxOuts = Tim_ManBoxOutputNum( pManTime, i );
if ( Tim_ManBoxIsBlack(pManTime, i) )
for ( k = 0; k < nBoxOuts; k++ )
{
assert( iBbOut < nBbOuts );
Vec_IntWriteEntry( vPiBoxes, iBbOut, i );
Vec_IntWriteEntry( vBbCiMap, curCi + k, iBbOut );
iBbOut++;
}
curCo += nBoxIns;
curCi += nBoxOuts;
}
curCo += nRealPos;
assert( curCi == Gia_ManCiNum(p) );
assert( curCo == Gia_ManCoNum(p) );
assert( iBbOut == nBbOuts );
}
vBoxesLeft = Vec_IntAlloc( nBoxes );
vMfsTopo = Sfm_NtkDfs( pNtk, vGroups, vGroupMap, vBoxesLeft, fAllBoxes );
vMfsTopo = Sfm_NtkDfs( pNtk, vGroups, vGroupMap, vBoxesLeft, fAllBoxes, vPiBoxes );
Vec_IntUniqify( vBoxesLeft ); // reduce to sorted unique indices expected by the timing manager
vBoxKeep = Vec_IntStart( nBoxes );
Vec_IntForEachEntry( vBoxesLeft, iBox, i )
@@ -370,12 +401,18 @@ Gia_Man_t * Gia_ManInsertMfs( Gia_Man_t * p, Sfm_Ntk_t * pNtk, int fAllBoxes )
{
int iCiId = Gia_ObjId( p, pObj );
int iBox = pManTime ? Tim_ManBoxForCi( pManTime, Gia_ObjCioId(pObj) ) : -1;
int iBbOut = vBbCiMap ? Vec_IntEntry(vBbCiMap, i) : -1;
if ( iBox >= 0 && !Vec_IntEntry(vBoxKeep, iBox) )
{
Vec_IntWriteEntry( vMfs2Gia, Gia_ObjCopyArray(p, iCiId), -1 );
if ( iBbOut >= 0 && vBbOutLit )
Vec_IntWriteEntry( vBbOutLit, iBbOut, -1 );
continue;
}
Vec_IntWriteEntry( vMfs2Gia, Gia_ObjCopyArray(p, iCiId), Gia_ManAppendCi(pNew) );
iLitNew = Gia_ManAppendCi(pNew);
Vec_IntWriteEntry( vMfs2Gia, Gia_ObjCopyArray(p, iCiId), iLitNew );
if ( iBbOut >= 0 && vBbOutLit )
Vec_IntWriteEntry( vBbOutLit, iBbOut, iLitNew );
}
// map internal nodes
vLeaves = Vec_IntAlloc( 6 );
@@ -389,18 +426,20 @@ Gia_Man_t * Gia_ManInsertMfs( Gia_Man_t * p, Sfm_Ntk_t * pNtk, int fAllBoxes )
if ( Vec_IntSize(vArray) == 1 && Vec_IntEntry(vArray,0) < nBbOuts ) // skip unreal inputs
{
assert( Abc_LitIsCompl(iGroup) );
iLitNew = Vec_IntEntry( vMfs2Gia, iMfsId );
if ( iLitNew == -1 )
{
iLitNew = Gia_ManAppendCi( pNew );
Vec_IntWriteEntry( vMfs2Gia, iMfsId, iLitNew );
}
assert( vBbOutLit != NULL );
iLitNew = Vec_IntEntry( vBbOutLit, Vec_IntEntry(vArray,0) );
assert( iLitNew >= 0 );
Vec_IntWriteEntry( vMfs2Gia, iMfsId, iLitNew );
continue;
}
Vec_IntClear( vLeaves );
Vec_IntForEachEntry( vArray, Fanin, k )
{
iLitNew = Vec_IntEntry( vMfs2Gia, Fanin ); assert( iLitNew >= 0 );
if ( Fanin < nBbOuts )
iLitNew = Vec_IntEntry( vBbOutLit, Fanin );
else
iLitNew = Vec_IntEntry( vMfs2Gia, Fanin );
assert( iLitNew >= 0 );
Vec_IntPush( vLeaves, iLitNew );
}
if ( iGroup == -1 ) // internal node
@@ -502,6 +541,9 @@ Gia_Man_t * Gia_ManInsertMfs( Gia_Man_t * p, Sfm_Ntk_t * pNtk, int fAllBoxes )
Vec_IntFree( vBoxesLeft );
Vec_IntFree( vBoxKeep );
Vec_IntFree( vCoDrivers );
Vec_IntFreeP( &vPiBoxes );
Vec_IntFreeP( &vBbCiMap );
Vec_IntFreeP( &vBbOutLit );
return pNew;
}

View File

@@ -95,7 +95,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, Vec_Wec_t * vGroups, Vec_Int_t * vGroupMap, Vec_Int_t * vBoxesLeft, int fAllBoxes );
extern Vec_Int_t * Sfm_NtkDfs( Sfm_Ntk_t * p, Vec_Wec_t * vGroups, Vec_Int_t * vGroupMap, Vec_Int_t * vBoxesLeft, int fAllBoxes, Vec_Int_t * vPiBoxes );
ABC_NAMESPACE_HEADER_END
@@ -105,4 +105,3 @@ ABC_NAMESPACE_HEADER_END
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

View File

@@ -133,37 +133,52 @@ static inline int Sfm_ObjIsTravIdCurrent2( Sfm_Ntk_t * p, int Id ) { return
SeeAlso []
***********************************************************************/
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 )
static 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, Vec_Int_t * vPiBoxes );
static void Sfm_NtkDfsVisitGroup( Sfm_Ntk_t * p, int iGroup, Vec_Int_t * vNodes, Vec_Wec_t * vGroups, Vec_Int_t * vGroupMap, Vec_Int_t * vBoxesLeft, Vec_Int_t * vPiBoxes )
{
int i, iFanin;
if ( Sfm_ObjIsPi(p, iNode) )
return;
int i, iFanin, k, Obj;
Vec_Int_t * vGroup = Vec_WecEntry( vGroups, iGroup );
Vec_IntForEachEntry( vGroup, Obj, i )
assert( Sfm_ObjIsNode(p, Obj) );
Vec_IntForEachEntry( vGroup, Obj, i )
Sfm_ObjSetTravIdCurrent( p, Obj );
Vec_IntForEachEntry( vGroup, Obj, i )
Sfm_ObjForEachFanin( p, Obj, iFanin, k )
Sfm_NtkDfs_rec( p, iFanin, vNodes, vGroups, vGroupMap, vBoxesLeft, vPiBoxes );
Vec_IntForEachEntry( vGroup, Obj, i )
Vec_IntPush( vNodes, Obj );
Vec_IntPush( vBoxesLeft, iGroup );
}
static 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, Vec_Int_t * vPiBoxes )
{
int i, iFanin, iGroup;
if ( Sfm_ObjIsTravIdCurrent(p, iNode) )
return;
if ( Vec_IntEntry(vGroupMap, iNode) >= 0 )
iGroup = Vec_IntEntry(vGroupMap, iNode);
if ( iGroup >= 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 );
Sfm_NtkDfsVisitGroup( p, Abc_Lit2Var(iGroup), vNodes, vGroups, vGroupMap, vBoxesLeft, vPiBoxes );
return;
}
else
if ( Sfm_ObjIsPi(p, iNode) )
{
Sfm_ObjSetTravIdCurrent(p, iNode);
Sfm_ObjForEachFanin( p, iNode, iFanin, i )
Sfm_NtkDfs_rec( p, iFanin, vNodes, vGroups, vGroupMap, vBoxesLeft );
Vec_IntPush( vNodes, iNode );
if ( vPiBoxes && iNode < Vec_IntSize(vPiBoxes) )
{
int iBox = Vec_IntEntry( vPiBoxes, iNode );
if ( iBox >= 0 )
{
Sfm_ObjSetTravIdCurrent( p, iNode );
Sfm_NtkDfsVisitGroup( p, iBox, vNodes, vGroups, vGroupMap, vBoxesLeft, vPiBoxes );
}
}
return;
}
Sfm_ObjSetTravIdCurrent(p, iNode);
Sfm_ObjForEachFanin( p, iNode, iFanin, i )
Sfm_NtkDfs_rec( p, iFanin, vNodes, vGroups, vGroupMap, vBoxesLeft, vPiBoxes );
Vec_IntPush( vNodes, iNode );
}
Vec_Int_t * Sfm_NtkDfs( Sfm_Ntk_t * p, Vec_Wec_t * vGroups, Vec_Int_t * vGroupMap, Vec_Int_t * vBoxesLeft, int fAllBoxes )
Vec_Int_t * Sfm_NtkDfs( Sfm_Ntk_t * p, Vec_Wec_t * vGroups, Vec_Int_t * vGroupMap, Vec_Int_t * vBoxesLeft, int fAllBoxes, Vec_Int_t * vPiBoxes )
{
Vec_Int_t * vNodes;
int i;
@@ -174,10 +189,10 @@ Vec_Int_t * Sfm_NtkDfs( Sfm_Ntk_t * p, Vec_Wec_t * vGroups, Vec_Int_t * vGroupMa
{
Vec_Int_t * vGroup;
Vec_WecForEachLevel( vGroups, vGroup, i )
Sfm_NtkDfs_rec( p, Vec_IntEntry(vGroup, 0), vNodes, vGroups, vGroupMap, vBoxesLeft );
Sfm_NtkDfs_rec( p, Vec_IntEntry(vGroup, 0), vNodes, vGroups, vGroupMap, vBoxesLeft, vPiBoxes );
}
Sfm_NtkForEachPo( p, i )
Sfm_NtkDfs_rec( p, Sfm_ObjFanin(p, i, 0), vNodes, vGroups, vGroupMap, vBoxesLeft );
Sfm_NtkDfs_rec( p, Sfm_ObjFanin(p, i, 0), vNodes, vGroups, vGroupMap, vBoxesLeft, vPiBoxes );
return vNodes;
}
@@ -478,4 +493,3 @@ void Sfm_NtkWindowTest( Sfm_Ntk_t * p, int iNode )
ABC_NAMESPACE_IMPL_END