Enabling AIGs with boxes for word-level and sequential designs.

6 files changed, 164 insertions, 24 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 7d457187..051c1aae 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -26474,11 +26474,7 @@ int Abc_CommandAbc9Strash( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     else if ( fCollapse && pAbc->pGia->pAigExtra )
     {
-        Gia_Man_t * pNew = Gia_ManDupUnnormalize( pAbc->pGia );
-        pNew->pManTime = pAbc->pGia->pManTime;
-        pTemp = Gia_ManDupCollapse( pNew, pAbc->pGia->pAigExtra, NULL );
-        pNew->pManTime = NULL;
-        Gia_ManStop( pNew );
+        pTemp = Gia_ManDupCollapse( pAbc->pGia, pAbc->pGia->pAigExtra, NULL );
         if ( !Abc_FrameReadFlag("silentmode") )
             printf( "Collapsed AIG with boxes and logic of the boxes.\n" );
     }
@@ -26494,7 +26490,8 @@ int Abc_CommandAbc9Strash( Abc_Frame_t * pAbc, int argc, char ** argv )
         if ( !Abc_FrameReadFlag("silentmode") )
             printf( "Rehashed the current AIG.\n" );
     }
-    Gia_ManTransferTiming( pTemp, pAbc->pGia );
+    if ( !(fCollapse && pAbc->pGia->pAigExtra) )
+        Gia_ManTransferTiming( pTemp, pAbc->pGia );
     Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 
@@ -30662,6 +30659,7 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9Verify( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
+    char * pFileSpec = NULL;
     Cec_ParCec_t ParsCec, * pPars = &ParsCec;
     int c;
     Cec_ManCecSetDefaultParams( pPars );
@@ -30701,16 +30699,23 @@ int Abc_CommandAbc9Verify( Abc_Frame_t * pAbc, int argc, char ** argv )
             goto usage;
         }
     }
-    Gia_ManVerifyWithBoxes( pAbc->pGia, pPars );
+    if ( argc == globalUtilOptind + 1 )
+    {
+        pFileSpec = argv[globalUtilOptind];
+        Extra_FileNameCorrectPath( pFileSpec );
+        printf( "Taking spec from file \"%s\".\n", pFileSpec );
+    }
+    Gia_ManVerifyWithBoxes( pAbc->pGia, pPars, pFileSpec );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &verify [-CT num] [-vh]\n" );
+    Abc_Print( -2, "usage: &verify [-CT num] [-vh] <file>\n" );
     Abc_Print( -2, "\t         performs verification of combinational design\n" );
     Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
     Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->TimeLimit );
     Abc_Print( -2, "\t-v     : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes":"no");
     Abc_Print( -2, "\t-h     : print the command usage\n");
+    Abc_Print( -2, "\t<file> : optional file name with the spec [default = not used\n" );
     return 1;
 }
 
diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index a485873c..26e1c3d5 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -204,6 +204,8 @@ static inline Wlc_Obj_t *  Wlc_ObjFoToFi( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )
 
 #define Wlc_NtkForEachObj( p, pObj, i )                                             \
     for ( i = 1; (i < Wlc_NtkObjNumMax(p)) && (((pObj) = Wlc_NtkObj(p, i)), 1); i++ )
+#define Wlc_NtkForEachObjVec( vVec, p, pObj, i )                                    \
+    for ( i = 0; (i < Vec_IntSize(vVec)) && (((pObj) = Wlc_NtkObj(p, Vec_IntEntry(vVec, i))), 1); i++ )
 #define Wlc_NtkForEachPi( p, pPi, i )                                               \
     for ( i = 0; (i < Wlc_NtkPiNum(p)) && (((pPi) = Wlc_NtkPi(p, i)), 1); i++ )
 #define Wlc_NtkForEachPo( p, pPo, i )                                               \
@@ -226,7 +228,7 @@ static inline Wlc_Obj_t *  Wlc_ObjFoToFi( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )
 ////////////////////////////////////////////////////////////////////////
 
 /*=== wlcBlast.c ========================================================*/
-extern Gia_Man_t *    Wlc_NtkBitBlast( Wlc_Ntk_t * p );
+extern Gia_Man_t *    Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds );
 /*=== wlcNtk.c ========================================================*/
 extern Wlc_Ntk_t *    Wlc_NtkAlloc( char * pName, int nObjsAlloc );
 extern int            Wlc_ObjAlloc( Wlc_Ntk_t * p, int Type, int Signed, int End, int Beg );
@@ -240,6 +242,7 @@ extern void           Wlc_NtkPrintNodes( Wlc_Ntk_t * p, int Type );
 extern void           Wlc_NtkPrintStats( Wlc_Ntk_t * p, int fDistrib, int fVerbose );
 extern Wlc_Ntk_t *    Wlc_NtkDupDfs( Wlc_Ntk_t * p );
 extern void           Wlc_NtkTransferNames( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p );
+extern Vec_Int_t *    Wlc_NtkCollectMultipliers( Wlc_Ntk_t * p );
 /*=== wlcReadWord.c ========================================================*/
 extern Wlc_Ntk_t *    Wlc_ReadVer( char * pFileName );
 /*=== wlcWriteWord.c ========================================================*/
diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c
index 94d04760..bf9ff8a3 100644
--- a/src/base/wlc/wlcBlast.c
+++ b/src/base/wlc/wlcBlast.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "wlc.h"
+#include "misc/tim/tim.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -377,32 +378,64 @@ void Wlc_BlastTable( Gia_Man_t * pNew, word * pTable, int * pFans, int nFans, in
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p )
+Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds )
 {
     int fVerbose = 0;
-    Gia_Man_t * pTemp, * pNew;
+    Tim_Man_t * pManTime = NULL;
+    Gia_Man_t * pTemp, * pNew, * pExtra = NULL;
     Wlc_Obj_t * pObj, * pPrev = NULL;
     Vec_Int_t * vBits, * vTemp0, * vTemp1, * vTemp2, * vRes;
     int nBits = Wlc_NtkPrepareBits( p );
     int nRange, nRange0, nRange1, nRange2;
-    int i, k, b, iFanin, iLit, * pFans0, * pFans1, * pFans2;
-    int nFFins = 0, nFFouts = 0;
+    int i, k, b, iFanin, iLit, nAndPrev, * pFans0, * pFans1, * pFans2;
+    int nFFins = 0, nFFouts = 0, curPi = 0, curPo = 0;
+    int nBitCis = 0, nBitCos = 0;
     vBits  = Vec_IntAlloc( nBits );
     vTemp0 = Vec_IntAlloc( 1000 );
     vTemp1 = Vec_IntAlloc( 1000 );
     vTemp2 = Vec_IntAlloc( 1000 );
     vRes   = Vec_IntAlloc( 1000 );
+    // clean AND-gate counters
+    memset( p->nAnds, 0, sizeof(int) * WLC_OBJ_NUMBER );
     // create AIG manager
     pNew = Gia_ManStart( 5 * Wlc_NtkObjNum(p) + 1000 );
     pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManHashAlloc( pNew );
-    // clean AND-gate counters
-    memset( p->nAnds, 0, sizeof(int) * WLC_OBJ_NUMBER );
-    // create primary inputs
+    // prepare for AIG with boxes
+    if ( vBoxIds )
+    {
+        int nNewCis = 0, nNewCos = 0;
+        Wlc_NtkForEachObj( p, pObj, i )
+            pObj->Mark = 0;
+        // count bit-width of regular CIs/COs
+        Wlc_NtkForEachCi( p, pObj, i )
+            nBitCis += Wlc_ObjRange( pObj );
+        Wlc_NtkForEachCo( p, pObj, i )
+            nBitCos += Wlc_ObjRange( pObj );
+        // count bit-width of additional CIs/COs due to selected multipliers
+        assert( Vec_IntSize(vBoxIds) > 0 );
+        Wlc_NtkForEachObjVec( vBoxIds, p, pObj, i )
+        {
+            // currently works only for multipliers
+            assert( pObj->Type == WLC_OBJ_ARI_MULTI );
+            nNewCis += Wlc_ObjRange( pObj );
+            nNewCos += Wlc_ObjRange( Wlc_ObjFanin0(p, pObj) );
+            nNewCos += Wlc_ObjRange( Wlc_ObjFanin1(p, pObj) );
+            pObj->Mark = 1;
+        }
+        // create hierarchy manager
+        pManTime = Tim_ManStart( nBitCis + nNewCis, nBitCos + nNewCos );
+        curPi = nBitCis;
+        curPo = 0;
+        // create AIG manager for logic of the boxes
+        pExtra = Gia_ManStart( Wlc_NtkObjNum(p) );
+        Gia_ManHashAlloc( pExtra );
+    }
+    // blast in the topological order
     Wlc_NtkForEachObj( p, pObj, i )
     {
 //        char * pName = Wlc_ObjName(p, i);
-        int nAndPrev = Gia_ManAndNum(pNew);
+        nAndPrev = Gia_ManAndNum(pNew);
         nRange  = Wlc_ObjRange( pObj );
         nRange0 = Wlc_ObjFaninNum(pObj) > 0 ? Wlc_ObjRange( Wlc_ObjFanin0(p, pObj) ) : -1;
         nRange1 = Wlc_ObjFaninNum(pObj) > 1 ? Wlc_ObjRange( Wlc_ObjFanin1(p, pObj) ) : -1;
@@ -412,7 +445,52 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p )
         pFans2  = Wlc_ObjFaninNum(pObj) > 2 ? Vec_IntEntryP( vBits, Wlc_ObjCopy(p, Wlc_ObjFaninId2(pObj)) ) : NULL;
         Vec_IntClear( vRes );
         assert( nRange > 0 );
-        if ( Wlc_ObjIsCi(pObj) )
+        if ( vBoxIds && pObj->Mark )
+        {
+            pObj->Mark = 0;
+
+            // create new box
+            Tim_ManCreateBox( pManTime, curPo, nRange0 + nRange1, curPi, nRange, -1 );
+            curPi += nRange;
+            curPo += nRange0 + nRange1;
+
+            // create combinational outputs in the normal manager
+            for ( k = 0; k < nRange0; k++ )
+                Gia_ManAppendCo( pNew, pFans0[k] );
+            for ( k = 0; k < nRange1; k++ )
+                Gia_ManAppendCo( pNew, pFans1[k] );
+
+            // make sure there is enough primary inputs in the manager
+            for ( k = Gia_ManPiNum(pExtra); k < nRange0 + nRange1; k++ )
+                Gia_ManAppendCi( pExtra );
+            // create combinational inputs
+            Vec_IntClear( vTemp0 );
+            for ( k = 0; k < nRange0; k++ )
+                Vec_IntPush( vTemp0, Gia_Obj2Lit(pExtra, Gia_ManPi(pExtra, k)) );
+            Vec_IntClear( vTemp1 );
+            for ( k = 0; k < nRange1; k++ )
+                Vec_IntPush( vTemp1, Gia_Obj2Lit(pExtra, Gia_ManPi(pExtra, nRange0+k)) );
+            // get new fanin arrays
+            pFans0 = Vec_IntArray( vTemp0 );
+            pFans1 = Vec_IntArray( vTemp1 );
+            // bit-blast the multiplier in the external manager
+            {
+                int nRangeMax = Abc_MaxInt( nRange, Abc_MaxInt(nRange0, nRange1) );
+                int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, Wlc_ObjFanin0(p, pObj)->Signed && Wlc_ObjFanin1(p, pObj)->Signed );
+                int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRangeMax, Wlc_ObjFanin0(p, pObj)->Signed && Wlc_ObjFanin1(p, pObj)->Signed );
+                Wlc_BlastMultiplier( pExtra, pArg0, pArg1, nRange, vTemp2, vRes );
+                Vec_IntShrink( vRes, nRange );
+            }
+            // create outputs in the external manager
+            for ( k = 0; k < nRange; k++ )
+                Gia_ManAppendCo( pExtra, Vec_IntEntry(vRes, k) );
+
+            // create combinational inputs in the normal manager
+            Vec_IntClear( vRes );
+            for ( k = 0; k < nRange; k++ )
+                Vec_IntPush( vRes, Gia_ManAppendCi(pNew) );
+        }
+        else if ( Wlc_ObjIsCi(pObj) )
         {
             for ( k = 0; k < nRange; k++ )
                 Vec_IntPush( vRes, Gia_ManAppendCi(pNew) );
@@ -664,9 +742,27 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p )
     // set the number of registers
     assert( nFFins == nFFouts );
     Gia_ManSetRegNum( pNew, nFFins );
-    // finalize and cleanup
+    // finalize AIG
     pNew = Gia_ManCleanup( pTemp = pNew );
     Gia_ManStop( pTemp );
+    // finalize AIG with boxes
+    if ( vBoxIds )
+    {
+        curPo += nBitCos;
+        assert( curPi == Tim_ManCiNum(pManTime) );
+        assert( curPo == Tim_ManCoNum(pManTime) );
+        // normalize AIG
+        pNew = Gia_ManDupNormalize( pTemp = pNew );
+        Gia_ManStop( pTemp );
+        // finalize the extra AIG
+        pExtra = Gia_ManCleanup( pTemp = pExtra );
+        Gia_ManStop( pTemp );
+        assert( Gia_ManPoNum(pExtra) == Gia_ManPiNum(pNew) - nBitCis );
+        // attach
+        pNew->pAigExtra = pExtra;
+        pNew->pManTime = pManTime;
+        //Tim_ManPrint( pManTime );
+    }
     return pNew;
 }
 
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index 0a8b90e0..5c786838 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -269,13 +269,17 @@ usage:
 int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+    Vec_Int_t * vBoxIds = NULL;
     Gia_Man_t * pNew = NULL;
-    int c, fVerbose  = 0;
+    int c, fMulti = 0, fVerbose  = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "mvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'm':
+            fMulti ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -290,8 +294,15 @@ int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( 1, "Abc_CommandBlast(): There is no current design.\n" );
         return 0;
     }
+    if ( fMulti )
+    {
+        vBoxIds = Wlc_NtkCollectMultipliers( pNtk );
+        if ( vBoxIds == NULL )
+            Abc_Print( 1, "Warning:  There is no multipliers in the design.\n" );
+    }
     // transform
-    pNew = Wlc_NtkBitBlast( pNtk );
+    pNew = Wlc_NtkBitBlast( pNtk, vBoxIds );
+    Vec_IntFreeP( &vBoxIds );
     if ( pNew == NULL )
     {
         Abc_Print( 1, "Abc_CommandBlast(): Bit-blasting has failed.\n" );
@@ -300,8 +311,9 @@ int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_FrameUpdateGia( pAbc, pNew );
     return 0;
 usage:
-    Abc_Print( -2, "usage: %%blast [-vh]\n" );
+    Abc_Print( -2, "usage: %%blast [-mvh]\n" );
     Abc_Print( -2, "\t         performs bit-blasting of the word-level design\n" );
+    Abc_Print( -2, "\t-m     : toggle creating boxes for all multipliers in the design [default = %s]\n", fMulti? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c
index 55448c11..9f779a2e 100644
--- a/src/base/wlc/wlcNtk.c
+++ b/src/base/wlc/wlcNtk.c
@@ -473,6 +473,30 @@ void Wlc_NtkTransferNames( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p )
     pNew->vTables = p->vTables;      p->vTables = NULL;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Collect IDs of the multipliers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Wlc_NtkCollectMultipliers( Wlc_Ntk_t * p )
+{
+    Wlc_Obj_t * pObj;  int i;
+    Vec_Int_t * vBoxIds = Vec_IntAlloc( 100 );
+    Wlc_NtkForEachObj( p, pObj, i )
+        if ( pObj->Type == WLC_OBJ_ARI_MULTI )
+            Vec_IntPush( vBoxIds, i );
+    if ( Vec_IntSize( vBoxIds ) > 0 )
+        return vBoxIds;
+    Vec_IntFree( vBoxIds );
+    return NULL;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/wlc/wlcReadVer.c b/src/base/wlc/wlcReadVer.c
index ac3cfaee..6000549f 100644
--- a/src/base/wlc/wlcReadVer.c
+++ b/src/base/wlc/wlcReadVer.c
@@ -1118,7 +1118,7 @@ void Io_ReadWordTest( char * pFileName )
         return;
     Wlc_WriteVer( pNtk, "test.v" );
 
-    pNew = Wlc_NtkBitBlast( pNtk );
+    pNew = Wlc_NtkBitBlast( pNtk, NULL );
     Gia_AigerWrite( pNew, "test.aig", 0, 0 );
     Gia_ManStop( pNew );