luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

&mfs: Fix issues with traversal when re-importing network 

The former implementation of `Sfm_NtkDfs` was trying to serialize the
network while ordering all box inputs ahead of the box outputs. This is
sometimes impossible, leaving the result unordered, which led to crashes
in the `&mfs` code when it was reintegrating the result into the GIA
structure:

  ABC: Assertion failed: iLitNew >= 0 (src/aig/gia/giaMfs.c: Gia_ManInsertMfs: 388)

With a small change to `Gia_ManInsertMfs` which does the reintegration
we don't really need the ordering to see through boxes, ordering on the
paths between boxes is sufficient. Relaxing the ordering requirement, we
make `Sfm_NtkDfs` robust.
This commit is contained in:
Martin Povišer 2024-03-22 22:01:08 +01:00
parent b83985c25b
commit fda490235e
2 changed files with 49 additions and 24 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
src/aig/gia/giaMfs.c
View File

@ -381,6 +381,15 @@ Gia_Man_t * Gia_ManInsertMfs( Gia_Man_t * p, Sfm_Ntk_t * pNtk, int fAllBoxes )
continue;
}
Vec_IntClear( vLeaves );
// handle internal CIs first, before we go looking for vLeaves
if ( iGroup != -1 && Abc_LitIsCompl(iGroup) )
{
//Dau_DsdPrintFromTruth( pTruth, Vec_IntSize(vLeaves) );
iLitNew = Gia_ManAppendCi( pNew );
goto done;
}
Vec_IntForEachEntry( vArray, Fanin, k )
{
iLitNew = Vec_IntEntry( vMfs2Gia, Fanin ); assert( iLitNew >= 0 );
@ -405,17 +414,13 @@ Gia_Man_t * Gia_ManInsertMfs( Gia_Man_t * p, Sfm_Ntk_t * pNtk, int fAllBoxes )
else
iLitNew = Gia_ManFromIfLogicCreateLut( pNew, pTruth, vLeaves, vCover, vMapping, vMapping2 );
}
else if ( Abc_LitIsCompl(iGroup) ) // internal CI
{
//Dau_DsdPrintFromTruth( pTruth, Vec_IntSize(vLeaves) );
iLitNew = Gia_ManAppendCi( pNew );
}
else // internal CO
{
assert( pTruth[0] == uTruthVar || pTruth[0] == ~uTruthVar );
iLitNew = Gia_ManAppendCo( pNew, Abc_LitNotCond(Vec_IntEntry(vLeaves, 0), pTruth[0] == ~uTruthVar) );
//printf("Group = %d. po = %d\n", iGroup>>1, iMfsId );
}
done:
Vec_IntWriteEntry( vMfs2Gia, iMfsId, iLitNew );
}
Vec_IntFree( vCover );

58
src/opt/sfm/sfmWin.c
View File

@ -142,18 +142,19 @@ void Sfm_NtkDfs_rec( Sfm_Ntk_t * p, int iNode, Vec_Int_t * vNodes, Vec_Wec_t * v
return;
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 );
int iGroup = Abc_Lit2Var(Vec_IntEntry(vGroupMap, iNode));
Vec_Int_t * vGroup = Vec_WecEntry(vGroups, iGroup);
assert(Abc_LitIsCompl(Vec_IntEntry(vGroupMap, iNode)));
Vec_IntPush(vBoxesLeft, iGroup);
Vec_IntForEachEntry(vGroup, iNode, i)
{
// ignore inputs
if ( !Abc_LitIsCompl(Vec_IntEntry(vGroupMap, iNode)))
continue;
assert(Sfm_ObjIsNode(p, iNode));
Sfm_ObjSetTravIdCurrent(p, iNode);
Vec_IntPush(vNodes, iNode);
}
}
else
{
@ -170,14 +171,33 @@ Vec_Int_t * Sfm_NtkDfs( Sfm_Ntk_t * p, Vec_Wec_t * vGroups, Vec_Int_t * vGroupMa
Vec_IntClear( vBoxesLeft );
vNodes = Vec_IntAlloc( p->nObjs );
Sfm_NtkIncrementTravId( p );
if ( fAllBoxes )
{
Vec_Int_t * vGroup;
Vec_WecForEachLevel( vGroups, vGroup, i )
Sfm_NtkDfs_rec( p, Vec_IntEntry(vGroup, 0), vNodes, vGroups, vGroupMap, vBoxesLeft );
assert(!fAllBoxes); // TODO
Sfm_NtkForEachPo( p, i ) {
int iFanin = Sfm_ObjFanin(p, i, 0);
// detect fake PO modeling blackbox input
if (Vec_IntEntry(vGroupMap, iFanin) >= 0 && !Abc_LitIsCompl(Vec_IntEntry(vGroupMap, iFanin)))
continue;
Sfm_NtkDfs_rec( p, iFanin, vNodes, vGroups, vGroupMap, vBoxesLeft );
}
Sfm_NtkForEachPo( p, i )
Sfm_NtkDfs_rec( p, Sfm_ObjFanin(p, i, 0), vNodes, vGroups, vGroupMap, vBoxesLeft );
for (i = 0; i < Vec_IntSize( vBoxesLeft ); i++)
{
int k, j, iNode, iFanin;
int iGroup = Vec_IntEntry( vBoxesLeft, i );
Vec_Int_t * vGroup = Vec_WecEntry( vGroups, iGroup );
Vec_IntForEachEntry( vGroup, iNode, k )
{
// ignore outputs
if ( Abc_LitIsCompl( Vec_IntEntry(vGroupMap, iNode)) )
continue;
Sfm_ObjForEachFanin( p, iNode, iFanin, j )
Sfm_NtkDfs_rec( p, iFanin, vNodes, vGroups, vGroupMap, vBoxesLeft );
Vec_IntPush( vNodes, iNode );
}
}
return vNodes;
}