From fda490235eace499ccee78501d0fd1c268e64b52 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Martin=20Povi=C5=A1er?= <povik@cutebit.org>
Date: Fri, 22 Mar 2024 22:01:08 +0100
Subject: [PATCH] &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.
---
 src/aig/gia/giaMfs.c | 15 ++++++++----
 src/opt/sfm/sfmWin.c | 58 +++++++++++++++++++++++++++++---------------
 2 files changed, 49 insertions(+), 24 deletions(-)

diff --git a/src/aig/gia/giaMfs.c b/src/aig/gia/giaMfs.c
index b1e657f73..e5d7c37ee 100644
--- a/src/aig/gia/giaMfs.c
+++ b/src/aig/gia/giaMfs.c
@@ -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 );
diff --git a/src/opt/sfm/sfmWin.c b/src/opt/sfm/sfmWin.c
index 53f9a71ef..2e1681991 100644
--- a/src/opt/sfm/sfmWin.c
+++ b/src/opt/sfm/sfmWin.c
@@ -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;
 }