Adding support for black boxes in extended AIG.

5 files changed, 95 insertions, 36 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 51c373c8..41e38588 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1384,6 +1384,7 @@ extern Vec_Flt_t *         Gia_ManPrintOutputProb( Gia_Man_t * p );
 extern int                 Gia_ManBoxNum( Gia_Man_t * p );
 extern int                 Gia_ManRegBoxNum( Gia_Man_t * p );
 extern int                 Gia_ManNonRegBoxNum( Gia_Man_t * p );
+extern int                 Gia_ManBlackBoxNum( Gia_Man_t * p );
 extern int                 Gia_ManBoxCiNum( Gia_Man_t * p );
 extern int                 Gia_ManBoxCoNum( Gia_Man_t * p );
 extern int                 Gia_ManClockDomainNum( Gia_Man_t * p );
diff --git a/src/aig/gia/giaFadds.c b/src/aig/gia/giaFadds.c
index 4a3a07ea..4b757d35 100644
--- a/src/aig/gia/giaFadds.c
+++ b/src/aig/gia/giaFadds.c
@@ -538,7 +538,7 @@ Tim_Man_t * Gia_ManGenerateTim( int nPis, int nPos, int nBoxes, int nIns, int nO
     curPo = 0;
     for ( i = 0; i < nBoxes; i++ )
     {
-        Tim_ManCreateBox( pMan, curPo, nIns, curPi, nOuts, 0 );
+        Tim_ManCreateBox( pMan, curPo, nIns, curPi, nOuts, 0, 0 );
         curPi += nOuts;
         curPo += nIns;
     }
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index 78c9e42f..bae40c9a 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -447,6 +447,8 @@ void Gia_ManPrintStats( Gia_Man_t * p, Gps_Par_t * pPars )
         Abc_Print( 1, "  ch =%5d", Gia_ManChoiceNum(p) );
     if ( p->pManTime )
         Abc_Print( 1, "  box = %d", Gia_ManNonRegBoxNum(p) );
+    if ( p->pManTime )
+        Abc_Print( 1, "  bb = %d", Gia_ManBlackBoxNum(p) );
     if ( Gia_ManBufNum(p) )
         Abc_Print( 1, "  buf = %d", Gia_ManBufNum(p) );
     if ( pPars && pPars->fMuxXor )
diff --git a/src/aig/gia/giaMfs.c b/src/aig/gia/giaMfs.c
index ca5d4038..e5dfb788 100644
--- a/src/aig/gia/giaMfs.c
+++ b/src/aig/gia/giaMfs.c
@@ -65,10 +65,13 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p )
     int nRealPis = nBoxes ? Tim_ManPiNum(pManTime) : Gia_ManPiNum(p);
     int nRealPos = nBoxes ? Tim_ManPoNum(pManTime) : Gia_ManPoNum(p);
     int i, j, k, curCi, curCo, nBoxIns, nBoxOuts;
-    int Id, iFan, nMfsVars, Counter = 0;
+    int Id, iFan, nMfsVars, nBbIns = 0, nBbOuts = 0, Counter = 0;
     assert( !p->pAigExtra || Gia_ManPiNum(p->pAigExtra) <= 6 );
+    Tim_ManBlackBoxIoNum( pManTime, &nBbIns, &nBbOuts );
+    // skip PIs due to box outputs
+    Counter += nBbOuts;
     // prepare storage
-    nMfsVars = Gia_ManCiNum(p) + 1 + Gia_ManLutNum(p) + Gia_ManCoNum(p);
+    nMfsVars = Gia_ManCiNum(p) + 1 + Gia_ManLutNum(p) + Gia_ManCoNum(p) + nBbIns + nBbOuts;
     vFanins  = Vec_WecStart( nMfsVars );
     vFixed   = Vec_StrStart( nMfsVars );
     vEmpty   = Vec_StrStart( nMfsVars );
@@ -118,16 +121,18 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p )
         }
         Gia_ObjSetCopyArray( p, Gia_ObjId(p, pObj), Counter++ );
     }
+    // skip POs due to box inputs
+    Counter += nBbIns;
     assert( Counter == nMfsVars );
     // add functions of the boxes
     if ( p->pAigExtra )
     {
+        int iBbIn = 0, iBbOut = 0;
         Gia_ObjComputeTruthTableStart( p->pAigExtra, 6 );
         curCi = nRealPis;
         curCo = 0;
         for ( k = 0; k < nBoxes; k++ )
         {
-            assert( !Tim_ManBoxIsBlack(pManTime, k) );
             nBoxIns = Tim_ManBoxInputNum( pManTime, k );
             nBoxOuts = Tim_ManBoxOutputNum( pManTime, k );
             // collect truth table leaves
@@ -135,34 +140,62 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p )
             for ( i = 0; i < nBoxIns; i++ )
                 Vec_IntPush( vLeaves, Gia_ObjId(p->pAigExtra, Gia_ManCi(p->pAigExtra, i)) );
             // iterate through box outputs
-            //printf( "Box %d:\n", k );
-            for ( j = 0; j < nBoxOuts; j++ )
+            if ( !Tim_ManBoxIsBlack(pManTime, k) )
             {
-                // CI corresponding to the box outputs
-                pObj = Gia_ManCi( p, curCi + j );
-                Counter = Gia_ObjCopyArray( p, Gia_ObjId(p, pObj) );
-                // box output in the extra manager
-                pObjExtra = Gia_ManCo( p->pAigExtra, curCi - nRealPis + j );
-                // compute truth table
-                if ( Gia_ObjFaninId0p(p->pAigExtra, pObjExtra) == 0 )
-                    uTruth = 0;
-                else if ( Gia_ObjIsCi(Gia_ObjFanin0(pObjExtra)) )
-                    uTruth = uTruths6[Gia_ObjCioId(Gia_ObjFanin0(pObjExtra))];
-                else
-                    uTruth = *Gia_ObjComputeTruthTableCut( p->pAigExtra, Gia_ObjFanin0(pObjExtra), vLeaves );
-                uTruth = Gia_ObjFaninC0(pObjExtra) ? ~uTruth : uTruth;
-                Vec_WrdWriteEntry( vTruths, Counter, uTruth );
-                //Dau_DsdPrintFromTruth( &uTruth, Vec_IntSize(vLeaves) );
-                // add box inputs (POs of the AIG) as fanins
-                vArray = Vec_WecEntry( vFanins, Counter );
-                Vec_IntGrow( vArray, nBoxIns );
+                for ( j = 0; j < nBoxOuts; j++ )
+                {
+                    // CI corresponding to the box outputs
+                    pObj = Gia_ManCi( p, curCi + j );
+                    Counter = Gia_ObjCopyArray( p, Gia_ObjId(p, pObj) );
+                    // box output in the extra manager
+                    pObjExtra = Gia_ManCo( p->pAigExtra, curCi - nRealPis + j );
+                    // compute truth table
+                    if ( Gia_ObjFaninId0p(p->pAigExtra, pObjExtra) == 0 )
+                        uTruth = 0;
+                    else if ( Gia_ObjIsCi(Gia_ObjFanin0(pObjExtra)) )
+                        uTruth = uTruths6[Gia_ObjCioId(Gia_ObjFanin0(pObjExtra))];
+                    else
+                        uTruth = *Gia_ObjComputeTruthTableCut( p->pAigExtra, Gia_ObjFanin0(pObjExtra), vLeaves );
+                    uTruth = Gia_ObjFaninC0(pObjExtra) ? ~uTruth : uTruth;
+                    Vec_WrdWriteEntry( vTruths, Counter, uTruth );
+                    //Dau_DsdPrintFromTruth( &uTruth, Vec_IntSize(vLeaves) );
+                    // add box inputs (POs of the AIG) as fanins
+                    vArray = Vec_WecEntry( vFanins, Counter );
+                    Vec_IntGrow( vArray, nBoxIns );
+                    for ( i = 0; i < nBoxIns; i++ )
+                    {
+                        iFan = Gia_ObjId( p, Gia_ManCo(p, curCo + i) );
+                        assert( Gia_ObjCopyArray(p, iFan) >= 0 );
+                        Vec_IntPush( vArray, Gia_ObjCopyArray(p, iFan) );
+                    }
+                    Vec_StrWriteEntry( vFixed, Counter, (char)1 );
+                }
+            }
+            else // create buffers for black box inputs and outputs
+            {
+                for ( j = 0; j < nBoxOuts; j++ )
+                {
+                    // CI corresponding to the box outputs
+                    pObj = Gia_ManCi( p, curCi + j );
+                    Counter = Gia_ObjCopyArray( p, Gia_ObjId(p, pObj) );
+                    // connect it with the special primary input (iBbOut)
+                    vArray = Vec_WecEntry( vFanins, Counter );
+                    assert( Vec_IntSize(vArray) == 0 );
+                    Vec_IntFill( vArray, 1, iBbOut++ );
+                    Vec_StrWriteEntry( vFixed, Counter, (char)1 );
+                    Vec_StrWriteEntry( vEmpty, Counter, (char)1 );
+                    Vec_WrdWriteEntry( vTruths, Counter, uTruths6[0] );
+                }
                 for ( i = 0; i < nBoxIns; i++ )
                 {
-                    iFan = Gia_ObjId( p, Gia_ManCo(p, curCo + i) );
-                    assert( Gia_ObjCopyArray(p, iFan) >= 0 );
-                    Vec_IntPush( vArray, Gia_ObjCopyArray(p, iFan) );
+                    // CO corresponding to the box inputs
+                    pObj = Gia_ManCo( p, curCo + i );
+                    Counter = Gia_ObjCopyArray( p, Gia_ObjId(p, pObj) );
+                    // connect it with the special primary output (iBbIn)
+                    vArray = Vec_WecEntry( vFanins, nMfsVars - nBbIns + iBbIn++ );
+                    assert( Vec_IntSize(vArray) == 0 );
+                    Vec_IntFill( vArray, 1, Counter );
                 }
-                Vec_StrWriteEntry( vFixed, Counter, (char)1 );
             }
             // set internal POs pointing directly to internal PIs as no-delay
             for ( i = 0; i < nBoxIns; i++ )
@@ -182,10 +215,12 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p )
         assert( curCi == Gia_ManCiNum(p) );
         assert( curCo == Gia_ManCoNum(p) );
         assert( curCi - nRealPis == Gia_ManCoNum(p->pAigExtra) );
+        assert( iBbIn  == nBbIns );
+        assert( iBbOut == nBbOuts );
     }
     // finalize 
     Vec_IntFree( vLeaves );
-    return Sfm_NtkConstruct( vFanins, nRealPis, nRealPos, vFixed, vEmpty, vTruths );
+    return Sfm_NtkConstruct( vFanins, nBbOuts + nRealPis, nRealPos + nBbIns, vFixed, vEmpty, vTruths );
 }
 
 /**Function*************************************************************
@@ -208,14 +243,19 @@ Gia_Man_t * Gia_ManInsertMfs( Gia_Man_t * p, Sfm_Ntk_t * pNtk )
     int nRealPis = nBoxes ? Tim_ManPiNum(pManTime) : Gia_ManPiNum(p);
     int nRealPos = nBoxes ? Tim_ManPoNum(pManTime) : Gia_ManPoNum(p);
     int i, k, Id, curCi, curCo, nBoxIns, nBoxOuts, iLitNew, iMfsId, iGroup, Fanin;
-    int nMfsNodes = 1 + Gia_ManCiNum(p) + Gia_ManLutNum(p) + Gia_ManCoNum(p);
+    int nMfsNodes;
     word * pTruth, uTruthVar = ABC_CONST(0xAAAAAAAAAAAAAAAA);
     Vec_Wec_t * vGroups = Vec_WecStart( nBoxes );
-    Vec_Int_t * vMfs2Gia = Vec_IntStartFull( nMfsNodes );
-    Vec_Int_t * vGroupMap = Vec_IntStartFull( nMfsNodes );
+    Vec_Int_t * vMfs2Gia;
+    Vec_Int_t * vGroupMap;
     Vec_Int_t * vMfsTopo, * vCover, * vBoxesLeft;
     Vec_Int_t * vArray, * vLeaves;
     Vec_Int_t * vMapping, * vMapping2;
+    int nBbIns = 0, nBbOuts = 0;
+    Tim_ManBlackBoxIoNum( pManTime, &nBbIns, &nBbOuts );
+    nMfsNodes = 1 + Gia_ManCiNum(p) + Gia_ManLutNum(p) + Gia_ManCoNum(p) + nBbIns + nBbOuts;
+    vMfs2Gia  = Vec_IntStartFull( nMfsNodes );
+    vGroupMap = Vec_IntStartFull( nMfsNodes );
     // collect nodes
     curCi = nRealPis;
     curCo = 0;
@@ -280,6 +320,14 @@ Gia_Man_t * Gia_ManInsertMfs( Gia_Man_t * p, Sfm_Ntk_t * pNtk )
         pTruth = Sfm_NodeReadTruth( pNtk, iMfsId );
         iGroup = Vec_IntEntry( vGroupMap, iMfsId );
         vArray = Sfm_NodeReadFanins( pNtk, iMfsId ); // belongs to pNtk
+        if ( Vec_IntSize(vArray) == 1 && Vec_IntEntry(vArray,0) < nBbOuts ) // skip unreal inputs
+        {
+            // create CI for the output of black box
+            assert( Abc_LitIsCompl(iGroup) );
+            iLitNew = Gia_ManAppendCi( pNew );
+            Vec_IntWriteEntry( vMfs2Gia, iMfsId, iLitNew );
+            continue;
+        }
         Vec_IntClear( vLeaves );
         Vec_IntForEachEntry( vArray, Fanin, k )
         {
diff --git a/src/aig/gia/giaTim.c b/src/aig/gia/giaTim.c
index d48f2637..98f0ee44 100644
--- a/src/aig/gia/giaTim.c
+++ b/src/aig/gia/giaTim.c
@@ -58,6 +58,10 @@ int Gia_ManNonRegBoxNum( Gia_Man_t * p )
 {
     return Gia_ManBoxNum(p) - Gia_ManRegBoxNum(p);
 }
+int Gia_ManBlackBoxNum( Gia_Man_t * p )
+{
+    return Tim_ManBlackBoxNum((Tim_Man_t *)p->pManTime);
+}
 int Gia_ManBoxCiNum( Gia_Man_t * p )
 {
     return p->pManTime ? Gia_ManCiNum(p) - Tim_ManPiNum((Tim_Man_t *)p->pManTime) : 0;
@@ -751,7 +755,7 @@ Gia_Man_t * Gia_ManDupCollapse( Gia_Man_t * p, Gia_Man_t * pBoxes, Vec_Int_t * v
     Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime;
     Gia_Man_t * pNew, * pTemp;
     Gia_Obj_t * pObj, * pObjBox;
-    int i, k, curCi, curCo;
+    int i, k, curCi, curCo, nBBins = 0, nBBouts = 0;
     assert( !fSeq || p->vRegClasses );
     //assert( Gia_ManRegNum(p) == 0 );
     assert( Gia_ManCiNum(p) == Tim_ManPiNum(pManTime) + Gia_ManCoNum(pBoxes) );
@@ -782,6 +786,7 @@ Gia_Man_t * Gia_ManDupCollapse( Gia_Man_t * p, Gia_Man_t * pBoxes, Vec_Int_t * v
         Gia_ObjSetTravIdCurrent( pBoxes, Gia_ManConst0(pBoxes) );
         Gia_ManConst0(pBoxes)->Value = 0;
         // add internal nodes
+        //printf( "%d ", Tim_ManBoxIsBlack(pManTime, i) );
         if ( Tim_ManBoxIsBlack(pManTime, i) )
         {
             int fSkip = (vBoxPres != NULL && !Vec_IntEntry(vBoxPres, i));
@@ -790,12 +795,14 @@ Gia_Man_t * Gia_ManDupCollapse( Gia_Man_t * p, Gia_Man_t * pBoxes, Vec_Int_t * v
                 pObj = Gia_ManCo( p, curCo + k );
                 Gia_ManDupCollapse_rec( p, Gia_ObjFanin0(pObj), pNew );
                 pObj->Value = fSkip ? -1 : Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+                nBBouts++;
             }
             for ( k = 0; k < Tim_ManBoxOutputNum(pManTime, i); k++ )
             {
                 pObj = Gia_ManCi( p, curCi + k );
                 pObj->Value = fSkip ? 0 : Gia_ManAppendCi(pNew);
                 Gia_ObjSetTravIdCurrent( p, pObj );
+                nBBins++;
             }
         }
         else
@@ -824,6 +831,7 @@ Gia_Man_t * Gia_ManDupCollapse( Gia_Man_t * p, Gia_Man_t * pBoxes, Vec_Int_t * v
         curCo += Tim_ManBoxInputNum(pManTime, i);
         curCi += Tim_ManBoxOutputNum(pManTime, i);
     }
+    //printf( "\n" );
     // add remaining nodes
     for ( i = Tim_ManCoNum(pManTime) - Tim_ManPoNum(pManTime); i < Tim_ManCoNum(pManTime); i++ )
     {
@@ -840,10 +848,10 @@ Gia_Man_t * Gia_ManDupCollapse( Gia_Man_t * p, Gia_Man_t * pBoxes, Vec_Int_t * v
     pNew = Gia_ManCleanup( pTemp = pNew );
     Gia_ManCleanupRemap( p, pTemp );
     Gia_ManStop( pTemp );
-    assert( Tim_ManPoNum(pManTime) == Gia_ManCoNum(pNew) );
-    assert( Tim_ManPiNum(pManTime) == Gia_ManCiNum(pNew) );
+    assert( Tim_ManPoNum(pManTime) == Gia_ManCoNum(pNew) - nBBouts );
+    assert( Tim_ManPiNum(pManTime) == Gia_ManCiNum(pNew) - nBBins );
     // implement initial state if given
-    if ( p->vRegInits && Vec_IntSum(p->vRegInits) )
+    if ( fSeq && p->vRegInits && Vec_IntSum(p->vRegInits) )
     {
         char * pInit = ABC_ALLOC( char, Vec_IntSize(p->vRegInits) + 1 );
         Gia_Obj_t * pObj;