Adding parameters and improvements to %blast.

9 files changed, 296 insertions, 98 deletions

diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index 55e85330..c00cd4d0 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -190,6 +190,40 @@ struct Wlc_Par_t_
     int                    (*pFuncStop)(int);  // callback to terminate
 };
 
+typedef struct Wlc_BstPar_t_ Wlc_BstPar_t;
+struct Wlc_BstPar_t_
+{
+    int                    iOutput;
+    int                    nOutputRange;
+    int                    nAdderLimit;
+    int                    nMultLimit;
+    int                    fGiaSimple;
+    int                    fAddOutputs;
+    int                    fMulti;
+    int                    fBooth;
+    int                    fNoCleanup;
+    int                    fCreateMiter;
+    int                    fDecMuxes;
+    int                    fVerbose;
+    Vec_Int_t *            vBoxIds;
+};
+
+static inline void Wlc_BstParDefault( Wlc_BstPar_t * pPar )
+{
+    memset( pPar, 0, sizeof(Wlc_BstPar_t) );
+    pPar->iOutput      = -1;
+    pPar->nOutputRange =  0;
+    pPar->nAdderLimit  =  0;
+    pPar->nMultLimit   =  0;
+    pPar->fGiaSimple   =  0;
+    pPar->fAddOutputs  =  0;
+    pPar->fMulti       =  0;
+    pPar->fBooth       =  0;
+    pPar->fCreateMiter =  0;
+    pPar->fDecMuxes    =  0;
+    pPar->fVerbose     =  0;
+}
+
 typedef struct Wla_Man_t_ Wla_Man_t;
 struct Wla_Man_t_
 {
@@ -325,7 +359,7 @@ extern int            Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars );
 /*=== wlcAbs2.c ========================================================*/
 extern int            Wlc_NtkAbsCore2( Wlc_Ntk_t * p, Wlc_Par_t * pPars );
 /*=== wlcBlast.c ========================================================*/
-extern Gia_Man_t *    Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, int nRange, int fGiaSimple, int fAddOutputs, int fBooth, int fNoCleanup, int fCreateMiter, int fDecMuxes );
+extern Gia_Man_t *    Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pPars );
 /*=== wlcCom.c ========================================================*/
 extern void           Wlc_SetNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk );
 /*=== wlcNdr.c ========================================================*/
@@ -376,6 +410,7 @@ extern int            Wlc_StdinProcessSmt( Abc_Frame_t * pAbc, char * pCmd );
 /*=== wlcReadVer.c ========================================================*/
 extern Wlc_Ntk_t *    Wlc_ReadVer( char * pFileName, char * pStr );
 /*=== wlcUif.c ========================================================*/
+extern Vec_Int_t *    Wlc_NtkCollectAddMult( Wlc_Ntk_t * p, Wlc_BstPar_t * pPar, int * pCountA, int * CountM );
 extern int            Wlc_NtkPairIsUifable( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Wlc_Obj_t * pObj2 );
 extern Vec_Int_t *    Wlc_NtkCollectMultipliers( Wlc_Ntk_t * p );
 extern Vec_Int_t *    Wlc_NtkFindUifableMultiplierPairs( Wlc_Ntk_t * p );
diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c
index 9e829182..2eb665bb 100644
--- a/src/base/wlc/wlcAbs.c
+++ b/src/base/wlc/wlcAbs.c
@@ -320,7 +320,7 @@ static Vec_Int_t * Wlc_NtkGetCoreSels( Gia_Man_t * pFrames, int nFrames, int fir
 
 static Gia_Man_t * Wlc_NtkUnrollWoCex(Wlc_Ntk_t * pChoice, int nFrames, int first_sel_pi, int num_sel_pis)
 {
-    Gia_Man_t * pGiaChoice = Wlc_NtkBitBlast( pChoice, NULL, -1, 0, 0, 0, 0, 0, 0, 0 );
+    Gia_Man_t * pGiaChoice = Wlc_NtkBitBlast( pChoice, NULL );
     Gia_Man_t * pFrames = NULL, * pGia;
     Gia_Obj_t * pObj, * pObjRi;
     int f, i;
@@ -366,7 +366,7 @@ static Gia_Man_t * Wlc_NtkUnrollWoCex(Wlc_Ntk_t * pChoice, int nFrames, int firs
 
 static Gia_Man_t * Wlc_NtkUnrollWithCex(Wlc_Ntk_t * pChoice, Abc_Cex_t * pCex, int nbits_old_pis, int num_sel_pis, int * p_num_ppis, int sel_pi_first, int fUsePPI) 
 {
-    Gia_Man_t * pGiaChoice = Wlc_NtkBitBlast( pChoice, NULL, -1, 0, 0, 0, 0, 0, 0, 0 );
+    Gia_Man_t * pGiaChoice = Wlc_NtkBitBlast( pChoice, NULL );
     int nbits_new_pis = Wlc_NtkNumPiBits( pChoice );
     int num_ppis = nbits_new_pis - nbits_old_pis - num_sel_pis;
     int num_undc_pis = Gia_ManPiNum(pGiaChoice) - nbits_new_pis;
@@ -560,7 +560,7 @@ Wlc_Ntk_t * Wlc_NtkIntroduceChoices( Wlc_Ntk_t * pNtk, Vec_Int_t * vBlacks, Vec_
 
 static Abc_Cex_t * Wlc_NtkCexIsReal( Wlc_Ntk_t * pOrig, Abc_Cex_t * pCex ) 
 {
-    Gia_Man_t * pGiaOrig = Wlc_NtkBitBlast( pOrig, NULL, -1, 0, 0, 0, 0, 0, 0, 0 );
+    Gia_Man_t * pGiaOrig = Wlc_NtkBitBlast( pOrig, NULL );
     int f, i;
     Gia_Obj_t * pObj, * pObjRi;
     Abc_Cex_t * pCexReal = Abc_CexAlloc( Gia_ManRegNum(pGiaOrig), Gia_ManPiNum(pGiaOrig), pCex->iFrame + 1 );
@@ -1401,7 +1401,7 @@ Aig_Man_t * Wla_ManBitBlast( Wla_Man_t * pWla, Wlc_Ntk_t * pAbs )
     Gia_Man_t * pTemp;
     Aig_Man_t * pAig;
 
-    pWla->pGia = Wlc_NtkBitBlast( pAbs, NULL, -1, 0, 0, 0, 0, 0, 0, 0 );
+    pWla->pGia = Wlc_NtkBitBlast( pAbs, NULL );
 
     // if the abstraction has flops with DC-init state,
     // new PIs were introduced by bit-blasting at the end of the PI list
@@ -1829,7 +1829,7 @@ int Wlc_NtkAbsCore( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
 
             pAbs = Wlc_NtkAbs( p, pPars, vUnmark, &vPisNew, NULL, pPars->fVerbose );
         }
-        pGia = Wlc_NtkBitBlast( pAbs, NULL, -1, 0, 0, 0, 0, 0, 0, 0 );
+        pGia = Wlc_NtkBitBlast( pAbs, NULL );
 
         // if the abstraction has flops with DC-init state,
         // new PIs were introduced by bit-blasting at the end of the PI list
diff --git a/src/base/wlc/wlcAbs2.c b/src/base/wlc/wlcAbs2.c
index f51d5dd5..1bb76398 100644
--- a/src/base/wlc/wlcAbs2.c
+++ b/src/base/wlc/wlcAbs2.c
@@ -328,7 +328,7 @@ int Wlc_NtkAbsCore2( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
 
         // get abstracted GIA and the set of pseudo-PIs (vPisNew)
         pAbs = Wlc_NtkAbs( p, pPars, vUnmark, &vPisNew, pPars->fVerbose );
-        pGia = Wlc_NtkBitBlast( pAbs, NULL, -1, 0, 0, 0, 0, 0, 0, 0 );
+        pGia = Wlc_NtkBitBlast( pAbs, NULL );
 
         // if the abstraction has flops with DC-init state,
         // new PIs were introduced by bit-blasting at the end of the PI list
diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c
index 37ea3186..dcdf99bc 100644
--- a/src/base/wlc/wlcBlast.c
+++ b/src/base/wlc/wlcBlast.c
@@ -878,7 +878,6 @@ void Wlc_BlastBooth( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int
     Vec_IntFree( vArgB );
 }
 
-
 /**Function*************************************************************
 
   Synopsis    []
@@ -890,12 +889,14 @@ void Wlc_BlastBooth( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, int nOutputRange, int fGiaSimple, int fAddOutputs, int fBooth, int fNoCleanup, int fCreateMiter, int fDecMuxes )
+Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn )
 {
     int fVerbose = 0;
     int fUseOldMultiplierBlasting = 0;
     int fSkipBitRange = 0;
     Tim_Man_t * pManTime = NULL;
+    If_LibBox_t * pBoxLib = NULL;
+    Vec_Ptr_t * vTables = NULL;
     Gia_Man_t * pTemp, * pNew, * pExtra = NULL;
     Wlc_Obj_t * pObj, * pObj2;
     Vec_Int_t * vBits = &p->vBits, * vTemp0, * vTemp1, * vTemp2, * vRes, * vAddOutputs = NULL, * vAddObjs = NULL;
@@ -904,6 +905,9 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in
     int i, k, b, iFanin, iLit, nAndPrev, * pFans0, * pFans1, * pFans2;
     int nFFins = 0, nFFouts = 0, curPi = 0, curPo = 0;
     int nBitCis = 0, nBitCos = 0, fAdded = 0;
+    Wlc_BstPar_t Par, * pPar = &Par;
+    Wlc_BstParDefault( pPar );
+    pPar = pParIn ? pParIn : pPar;
     Vec_IntClear( vBits );
     Vec_IntGrow( vBits, nBits );
     vTemp0 = Vec_IntAlloc( 1000 );
@@ -915,15 +919,15 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in
     // create AIG manager
     pNew = Gia_ManStart( 5 * Wlc_NtkObjNum(p) + 1000 );
     pNew->pName = Abc_UtilStrsav( p->pName );
-    pNew->fGiaSimple = fGiaSimple;
-    if ( !fGiaSimple )
+    pNew->fGiaSimple = pPar->fGiaSimple;
+    if ( !pPar->fGiaSimple )
         Gia_ManHashAlloc( pNew );
-    if ( fAddOutputs )
+    if ( pPar->fAddOutputs )
         vAddOutputs = Vec_IntAlloc( 100 );
-    if ( fAddOutputs )
+    if ( pPar->fAddOutputs )
         vAddObjs = Vec_IntAlloc( 100 );
     // prepare for AIG with boxes
-    if ( vBoxIds )
+    if ( pPar->vBoxIds )
     {
         int nNewCis = 0, nNewCos = 0;
         Wlc_NtkForEachObj( p, pObj, i )
@@ -934,14 +938,16 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in
         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 )
+        assert( Vec_IntSize(pPar->vBoxIds) > 0 );
+        Wlc_NtkForEachObjVec( pPar->vBoxIds, p, pObj, i )
         {
             // currently works only for multipliers
-            assert( pObj->Type == WLC_OBJ_ARI_MULTI );
+            assert( pObj->Type == WLC_OBJ_ARI_MULTI || pObj->Type == WLC_OBJ_ARI_ADD );
             nNewCis += Wlc_ObjRange( pObj );
             nNewCos += Wlc_ObjRange( Wlc_ObjFanin0(p, pObj) );
             nNewCos += Wlc_ObjRange( Wlc_ObjFanin1(p, pObj) );
+            if ( Wlc_ObjFaninNum(pObj) > 2 )
+            nNewCos += Wlc_ObjRange( Wlc_ObjFanin2(p, pObj) );
             pObj->Mark = 1;
         }
         // create hierarchy manager
@@ -951,7 +957,9 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in
         // create AIG manager for logic of the boxes
         pExtra = Gia_ManStart( Wlc_NtkObjNum(p) );
         Gia_ManHashAlloc( pExtra );
-        assert( !fGiaSimple );
+        assert( !pPar->fGiaSimple );
+        // create box library
+        pBoxLib = If_LibBoxStart();
     }
     // blast in the topological order
     Wlc_NtkForEachObj( p, pObj, i )
@@ -969,23 +977,48 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in
         pFans2  = Wlc_ObjFaninNum(pObj) > 2 ? Vec_IntEntryP( vBits, Wlc_ObjCopy(p, Wlc_ObjFaninId2(pObj)) ) : NULL;
         Vec_IntClear( vRes );
         assert( nRange > 0 );
-        if ( vBoxIds && pObj->Mark )
+        if ( pPar->vBoxIds && pObj->Mark )
         {
+            If_Box_t * pBox;
+            char Buffer[100];
+            float * pTable;
+            int CarryIn = 0;
+
             pObj->Mark = 0;
+            assert( pObj->Type == WLC_OBJ_ARI_MULTI || pObj->Type == WLC_OBJ_ARI_ADD || pObj->Type == WLC_OBJ_ARI_SUB );
+
+            // account for carry-in
+            if ( Wlc_ObjFaninNum(pObj) == 3 )
+                assert( nRange2 == 1 );
+            else
+                nRange2 = 0;
 
             // create new box
-            Tim_ManCreateBox( pManTime, curPo, nRange0 + nRange1, curPi, nRange, -1, 0 );
+            if ( vTables == NULL )
+                Tim_ManSetDelayTables( pManTime, (vTables = Vec_PtrAlloc(100)) );
+            Tim_ManCreateBox( pManTime, curPo, nRange0 + nRange1 + nRange2, curPi, nRange, Vec_PtrSize(vTables), 0 );
             curPi += nRange;
-            curPo += nRange0 + nRange1;
+            curPo += nRange0 + nRange1 + nRange2;
+
+            // create delay table
+            pTable = ABC_ALLOC( float, 3 + nRange * (nRange0 + nRange1 + nRange2) );
+            pTable[0] = Vec_PtrSize(vTables);
+            pTable[1] = nRange0 + nRange1 + nRange2;
+            pTable[2] = nRange;
+            for ( k = 0; k < nRange * (nRange0 + nRange1 + nRange2); k++ )
+                pTable[3 + k] = 1.0;
+            Vec_PtrPush( vTables, pTable );
 
             // 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] );
+            for ( k = 0; k < nRange2; 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++ )
+            for ( k = Gia_ManPiNum(pExtra); k < nRange0 + nRange1 + nRange2; k++ )
                 Gia_ManAppendCi( pExtra );
             // create combinational inputs
             Vec_IntClear( vTemp0 );
@@ -994,11 +1027,26 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in
             Vec_IntClear( vTemp1 );
             for ( k = 0; k < nRange1; k++ )
                 Vec_IntPush( vTemp1, Gia_Obj2Lit(pExtra, Gia_ManPi(pExtra, nRange0+k)) );
+            if ( nRange2 == 1 )
+                CarryIn = Gia_Obj2Lit(pExtra, Gia_ManPi(pExtra, nRange0+nRange1));
+
             // get new fanin arrays
             pFans0 = Vec_IntArray( vTemp0 );
             pFans1 = Vec_IntArray( vTemp1 );
-            // bit-blast the multiplier in the external manager
-            if ( fUseOldMultiplierBlasting )
+
+            // bit-blast in the external manager
+            if ( pObj->Type == WLC_OBJ_ARI_ADD || pObj->Type == WLC_OBJ_ARI_SUB ) 
+            {
+                int nRangeMax = Abc_MaxInt( nRange, Abc_MaxInt(nRange0, nRange1) );
+                int * pArg0 = Wlc_VecLoadFanins( vRes,   pFans0, nRange0, nRangeMax, Wlc_ObjIsSignedFanin01(p, pObj) );
+                int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRangeMax, Wlc_ObjIsSignedFanin01(p, pObj) );
+                if ( pObj->Type == WLC_OBJ_ARI_ADD )
+                    Wlc_BlastAdder( pExtra, pArg0, pArg1, nRange, CarryIn ); // result is in pFan0 (vRes)
+                else 
+                    Wlc_BlastSubtract( pExtra, pArg0, pArg1, nRange ); // result is in pFan0 (vRes)
+                Vec_IntShrink( vRes, nRange );
+            }
+            else if ( fUseOldMultiplierBlasting )
             {                
                 int nRangeMax = Abc_MaxInt( nRange, Abc_MaxInt(nRange0, nRange1) );
                 int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, Wlc_ObjIsSignedFanin01(p, pObj) );
@@ -1012,7 +1060,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in
                 int nRangeMax = Abc_MaxInt(nRange0, nRange1);
                 int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, fSigned );
                 int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRangeMax, fSigned );
-                Wlc_BlastMultiplier( pNew, pArg0, pArg1, nRangeMax, nRangeMax, vTemp2, vRes, fSigned );
+                Wlc_BlastMultiplier( pExtra, pArg0, pArg1, nRangeMax, nRangeMax, vTemp2, vRes, fSigned );
                 if ( nRange > nRangeMax + nRangeMax )
                     Vec_IntFillExtra( vRes, nRange, fSigned ? Vec_IntEntryLast(vRes) : 0 );
                 else
@@ -1027,6 +1075,14 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in
             Vec_IntClear( vRes );
             for ( k = 0; k < nRange; k++ )
                 Vec_IntPush( vRes, Gia_ManAppendCi(pNew) );
+
+            // add box to the library
+            sprintf( Buffer, "%s%03d", pObj->Type == WLC_OBJ_ARI_ADD ? "add":"mul", 1+If_LibBoxNum(pBoxLib) );
+            pBox = If_BoxStart( Abc_UtilStrsav(Buffer), 1+If_LibBoxNum(pBoxLib), nRange, nRange0 + nRange1 + nRange2, 0, 0, 0 ); 
+            If_LibBoxAdd( pBoxLib, pBox );
+            for ( k = 0; k < pBox->nPis * pBox->nPos; k++ )
+                pBox->pDelays[k] = 1;
+            printf( "adding box %s\n", Buffer);
         }
         else if ( Wlc_ObjIsCi(pObj) )
         {
@@ -1084,7 +1140,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in
                 if ( k > 0 )
                     fSigned &= Wlc_NtkObj(p, iFanin)->Signed;
             Vec_IntClear( vTemp1 );
-            if ( fDecMuxes )
+            if ( pPar->fDecMuxes )
             {
                 for ( k = 0; k < (1 << nRange0); k++ )
                 {
@@ -1107,7 +1163,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in
                         else // Statement 2
                             Vec_IntPush( vTemp0, b < nRange1 ? pFans1[b] : (Wlc_NtkObj(p, iFanin)->Signed? pFans1[nRange1-1] : 0) );
                     }
-                if ( fDecMuxes )
+                if ( pPar->fDecMuxes )
                     Vec_IntPush( vRes, Wlc_NtkMuxTree2(pNew, pFans0, nRange0, vTemp0, vTemp1, vTemp2) );
                 else
                     Vec_IntPush( vRes, Wlc_NtkMuxTree_rec(pNew, pFans0, nRange0, vTemp0, 0) );
@@ -1340,7 +1396,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in
                 int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRangeMax, fSigned );
                 if ( Wlc_NtkCountConstBits(pArg0, nRangeMax) < Wlc_NtkCountConstBits(pArg1, nRangeMax) )
                     ABC_SWAP( int *, pArg0, pArg1 );
-                if ( fBooth )
+                if ( pPar->fBooth )
                     Wlc_BlastBooth( pNew, pArg0, pArg1, nRange0, nRange1, vRes, fSigned );
                 else
                     Wlc_BlastMultiplier( pNew, pArg0, pArg1, nRangeMax, nRangeMax, vTemp2, vRes, fSigned );
@@ -1425,7 +1481,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in
     Vec_IntFree( vTemp2 );
     Vec_IntFree( vRes );
     // create COs
-    if ( fCreateMiter )
+    if ( pPar->fCreateMiter )
     {
         int nPairs = 0, nBits = 0;
         assert( Wlc_NtkPoNum(p) % 2 == 0 );
@@ -1480,7 +1536,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in
         Wlc_NtkForEachCo( p, pObj, i )
         {
             // skip all outputs except the given ones
-            if ( iOutput >= 0 && (i < iOutput || i >= iOutput + nOutputRange) )
+            if ( pPar->iOutput >= 0 && (i < pPar->iOutput || i >= pPar->iOutput + pPar->nOutputRange) )
                 continue;
             // create additional PO literals
             if ( vAddOutputs && pObj->fIsFi )
@@ -1516,7 +1572,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in
     assert( nFFins == nFFouts );
     Gia_ManSetRegNum( pNew, nFFins );
     // finalize AIG
-    if ( !fGiaSimple && !fNoCleanup )
+    if ( !pPar->fGiaSimple && !pPar->fNoCleanup )
     {
         pNew = Gia_ManCleanup( pTemp = pNew );
         Gia_ManDupRemapLiterals( vBits, pTemp );
@@ -1533,13 +1589,13 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in
         }
         else
         {
-            pNew = Gia_ManDupZeroUndc( pTemp = pNew, p->pInits, fGiaSimple, 0 );
+            pNew = Gia_ManDupZeroUndc( pTemp = pNew, p->pInits, pPar->fGiaSimple, 0 );
             Gia_ManDupRemapLiterals( vBits, pTemp );
             Gia_ManStop( pTemp );
         }
     }
     // finalize AIG with boxes
-    if ( vBoxIds )
+    if ( pPar->vBoxIds )
     {
         curPo += nBitCos;
         assert( curPi == Tim_ManCiNum(pManTime) );
@@ -1603,27 +1659,61 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in
     }
     if ( p->pInits && fAdded )
         Vec_PtrPush( pNew->vNamesIn, Abc_UtilStrsav("abc_reset_flop") );
-    assert( Vec_PtrSize(pNew->vNamesIn) == Gia_ManCiNum(pNew) );
-    // create output names
-    if ( vAddObjs )
+    if ( pPar->vBoxIds )
     {
-        // add real primary outputs
-        pNew->vNamesOut = Vec_PtrAlloc( Gia_ManCoNum(pNew) );
-        Wlc_NtkForEachCo( p, pObj, i )
-        if ( Wlc_ObjIsPo(pObj) )
+        Wlc_NtkForEachObjVec( pPar->vBoxIds, p, pObj, i )
         {
             char * pName = Wlc_ObjName(p, Wlc_ObjId(p, pObj));
             nRange = Wlc_ObjRange( pObj );
-            if ( fSkipBitRange && nRange == 1 )
-                Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav(pName) );
-            else
+            assert( nRange > 1 );
+            for ( k = 0; k < nRange; k++ )
+            {
+                char Buffer[1000];
+                sprintf( Buffer, "%s[%d]", pName, k );
+                Vec_PtrPush( pNew->vNamesIn, Abc_UtilStrsav(Buffer) );
+            }
+        }
+    }
+    assert( Vec_PtrSize(pNew->vNamesIn) == Gia_ManCiNum(pNew) );
+    // create output names
+    pNew->vNamesOut = Vec_PtrAlloc( Gia_ManCoNum(pNew) );
+    if ( pPar->vBoxIds )
+    {
+        Wlc_NtkForEachObjVec( pPar->vBoxIds, p, pObj, i )
+        {
+            int iFanin, f;
+            Wlc_ObjForEachFanin( pObj, iFanin, f )
+            {
+                char * pName = Wlc_ObjName(p, iFanin);
+                nRange = Wlc_ObjRange( Wlc_NtkObj(p, iFanin) );
+                assert( nRange >= 1 );
                 for ( k = 0; k < nRange; k++ )
                 {
                     char Buffer[1000];
                     sprintf( Buffer, "%s[%d]", pName, k );
                     Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav(Buffer) );
                 }
+            }
         }
+    }
+    // add real primary outputs
+    Wlc_NtkForEachCo( p, pObj, i )
+    if ( Wlc_ObjIsPo(pObj) )
+    {
+        char * pName = Wlc_ObjName(p, Wlc_ObjId(p, pObj));
+        nRange = Wlc_ObjRange( pObj );
+        if ( fSkipBitRange && nRange == 1 )
+            Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav(pName) );
+        else
+            for ( k = 0; k < nRange; k++ )
+            {
+                char Buffer[1000];
+                sprintf( Buffer, "%s[%d]", pName, k );
+                Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav(Buffer) );
+            }
+    }
+    if ( vAddObjs )
+    {
         // add internal primary outputs
         Wlc_NtkForEachObjVec( vAddObjs, p, pObj, i )
         {
@@ -1640,25 +1730,32 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in
                 }
         }
         Vec_IntFreeP( &vAddObjs );
-        // add flop outputs
-        if ( fAdded )
-            Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav("abc_reset_flop_in") );
-        Wlc_NtkForEachCo( p, pObj, i )
-        if ( !Wlc_ObjIsPo(pObj) )
-        {
-            char * pName = Wlc_ObjName(p, Wlc_ObjId(p, pObj));
-            nRange = Wlc_ObjRange( pObj );
-            if ( fSkipBitRange && nRange == 1 )
-                Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav(pName) );
-            else
-                for ( k = 0; k < nRange; k++ )
-                {
-                    char Buffer[1000];
-                    sprintf( Buffer, "%s[%d]", pName, k );
-                    Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav(Buffer) );
-                }
-        }
-        assert( Vec_PtrSize(pNew->vNamesOut) == Gia_ManCoNum(pNew) );
+    }
+    // add flop outputs
+    if ( fAdded )
+        Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav("abc_reset_flop_in") );
+    Wlc_NtkForEachCo( p, pObj, i )
+    if ( !Wlc_ObjIsPo(pObj) )
+    {
+        char * pName = Wlc_ObjName(p, Wlc_ObjId(p, pObj));
+        nRange = Wlc_ObjRange( pObj );
+        if ( fSkipBitRange && nRange == 1 )
+            Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav(pName) );
+        else
+            for ( k = 0; k < nRange; k++ )
+            {
+                char Buffer[1000];
+                sprintf( Buffer, "%s[%d]", pName, k );
+                Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav(Buffer) );
+            }
+    }
+    assert( Vec_PtrSize(pNew->vNamesOut) == Gia_ManCoNum(pNew) );
+
+    // replace the current library
+    if ( pBoxLib )
+    {
+        If_LibBoxFree( (If_LibBox_t *)Abc_FrameReadLibBox() );
+        Abc_FrameSetLibBox( pBoxLib );
     }
 
     //pNew->pSpec = Abc_UtilStrsav( p->pSpec ? p->pSpec : p->pName );
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index bef1ccb4..2b453cbc 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -888,11 +888,12 @@ 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, iOutput = -1, nOutputRange = 2, fGiaSimple = 0, fAddOutputs = 0, fMulti = 0, fBooth = 0, fCreateMiter = 0, fDecMuxes = 0, fVerbose  = 0;
+    Gia_Man_t * pNew = NULL; int c;
+    Wlc_BstPar_t Par, * pPar = &Par;
+    Wlc_BstParDefault( pPar );
+    pPar->nOutputRange = 2;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "ORcombdsvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "ORAMcombdsvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -902,9 +903,9 @@ int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
                 Abc_Print( -1, "Command line switch \"-O\" should be followed by an integer.\n" );
                 goto usage;
             }
-            iOutput = atoi(argv[globalUtilOptind]);
+            pPar->iOutput = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( iOutput < 0 )
+            if ( pPar->iOutput < 0 )
                 goto usage;
             break;
         case 'R':
@@ -913,31 +914,53 @@ int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
                 Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" );
                 goto usage;
             }
-            nOutputRange = atoi(argv[globalUtilOptind]);
+            pPar->nOutputRange = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPar->nOutputRange < 0 )
+                goto usage;
+            break;
+        case 'A':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-A\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPar->nAdderLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPar->nAdderLimit < 0 )
+                goto usage;
+            break;
+        case 'M':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPar->nMultLimit = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( nOutputRange < 0 )
+            if ( pPar->nMultLimit < 0 )
                 goto usage;
             break;
         case 'c':
-            fGiaSimple ^= 1;
+            pPar->fGiaSimple ^= 1;
             break;
         case 'o':
-            fAddOutputs ^= 1;
+            pPar->fAddOutputs ^= 1;
             break;
         case 'm':
-            fMulti ^= 1;
+            pPar->fMulti ^= 1;
             break;
         case 'b':
-            fBooth ^= 1;
+            pPar->fBooth ^= 1;
             break;
         case 'd':
-            fCreateMiter ^= 1;
+            pPar->fCreateMiter ^= 1;
             break;
         case 's':
-            fDecMuxes ^= 1;
+            pPar->fDecMuxes ^= 1;
             break;
         case 'v':
-            fVerbose ^= 1;
+            pPar->fVerbose ^= 1;
             break;
         case 'h':
             goto usage;
@@ -950,20 +973,29 @@ 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 )
+    if ( pPar->fMulti )
     {
-        vBoxIds = Wlc_NtkCollectMultipliers( pNtk );
-        if ( vBoxIds == NULL )
+        pPar->vBoxIds = Wlc_NtkCollectMultipliers( pNtk );
+        if ( pPar->vBoxIds == NULL )
             Abc_Print( 1, "Warning:  There is no multipliers in the design.\n" );
     }
-    if ( iOutput >= 0 && iOutput + nOutputRange > Wlc_NtkPoNum(pNtk) )
+    else if ( pPar->nAdderLimit || pPar->nMultLimit )
     {
-        Abc_Print( 1, "Abc_CommandBlast(): The output range [%d:%d] is incorrect.\n", iOutput, iOutput + nOutputRange - 1 );
+        int CountA, CountM;
+        pPar->vBoxIds = Wlc_NtkCollectAddMult( pNtk, pPar, &CountA, &CountM );
+        if ( pPar->vBoxIds == NULL )
+            Abc_Print( 1, "Warning:  There is no adders and multipliers that will not be blasted.\n" );
+        else 
+            Abc_Print( 1, "Warning:  %d adders and %d multipliers will not be blasted.\n", CountA, CountM );
+    }
+    if ( pPar->iOutput >= 0 && pPar->iOutput + pPar->nOutputRange > Wlc_NtkPoNum(pNtk) )
+    {
+        Abc_Print( 1, "Abc_CommandBlast(): The output range [%d:%d] is incorrect.\n", pPar->iOutput, pPar->iOutput + pPar->nOutputRange - 1 );
         return 0;
     }
     // transform
-    pNew = Wlc_NtkBitBlast( pNtk, vBoxIds, iOutput, nOutputRange, fGiaSimple, fAddOutputs, fBooth, 0, fCreateMiter, fDecMuxes );
-    Vec_IntFreeP( &vBoxIds );
+    pNew = Wlc_NtkBitBlast( pNtk, pPar );
+    Vec_IntFreeP( &pPar->vBoxIds );
     if ( pNew == NULL )
     {
         Abc_Print( 1, "Abc_CommandBlast(): Bit-blasting has failed.\n" );
@@ -972,17 +1004,19 @@ int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_FrameUpdateGia( pAbc, pNew );
     return 0;
 usage:
-    Abc_Print( -2, "usage: %%blast [-OR num] [-combdsvh]\n" );
+    Abc_Print( -2, "usage: %%blast [-ORAM num] [-combdsvh]\n" );
     Abc_Print( -2, "\t         performs bit-blasting of the word-level design\n" );
-    Abc_Print( -2, "\t-O num : zero-based index of the first word-level PO to bit-blast [default = %d]\n", iOutput );
-    Abc_Print( -2, "\t-R num : the total number of word-level POs to bit-blast [default = %d]\n", nOutputRange );
-    Abc_Print( -2, "\t-c     : toggle using AIG w/o const propagation and strashing [default = %s]\n", fGiaSimple? "yes": "no" );
-    Abc_Print( -2, "\t-o     : toggle using additional POs on the word-level boundaries [default = %s]\n", fAddOutputs? "yes": "no" );
-    Abc_Print( -2, "\t-m     : toggle creating boxes for all multipliers in the design [default = %s]\n", fMulti? "yes": "no" );
-    Abc_Print( -2, "\t-b     : toggle generating radix-4 Booth multipliers [default = %s]\n", fBooth? "yes": "no" );
-    Abc_Print( -2, "\t-d     : toggle creating dual-output miter [default = %s]\n", fCreateMiter? "yes": "no" );
-    Abc_Print( -2, "\t-s     : toggle creating decoded MUXes [default = %s]\n", fDecMuxes? "yes": "no" );
-    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-O num : zero-based index of the first word-level PO to bit-blast [default = %d]\n", pPar->iOutput );
+    Abc_Print( -2, "\t-R num : the total number of word-level POs to bit-blast [default = %d]\n",          pPar->nOutputRange );
+    Abc_Print( -2, "\t-A num : blast adders smaller than this (0 = unused) [default = %d]\n",              pPar->nAdderLimit );
+    Abc_Print( -2, "\t-M num : blast multipliers smaller than this (0 = unused) [default = %d]\n",         pPar->nMultLimit );
+    Abc_Print( -2, "\t-c     : toggle using AIG w/o const propagation and strashing [default = %s]\n",     pPar->fGiaSimple? "yes": "no" );
+    Abc_Print( -2, "\t-o     : toggle using additional POs on the word-level boundaries [default = %s]\n", pPar->fAddOutputs? "yes": "no" );
+    Abc_Print( -2, "\t-m     : toggle creating boxes for all multipliers in the design [default = %s]\n",  pPar->fMulti? "yes": "no" );
+    Abc_Print( -2, "\t-b     : toggle generating radix-4 Booth multipliers [default = %s]\n",              pPar->fBooth? "yes": "no" );
+    Abc_Print( -2, "\t-d     : toggle creating dual-output miter [default = %s]\n",                        pPar->fCreateMiter? "yes": "no" );
+    Abc_Print( -2, "\t-s     : toggle creating decoded MUXes [default = %s]\n",                            pPar->fDecMuxes? "yes": "no" );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n",                      pPar->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
 }
diff --git a/src/base/wlc/wlcGraft.c b/src/base/wlc/wlcGraft.c
index 03cfac4d..8e1ed20f 100644
--- a/src/base/wlc/wlcGraft.c
+++ b/src/base/wlc/wlcGraft.c
@@ -210,7 +210,7 @@ Wlc_Ntk_t * Wlc_NtkGraftMulti( Wlc_Ntk_t * p, int fVerbose )
     Gia_Obj_t * pObj;
     Vec_Int_t * vObjsLHS = Wlc_NtkCollectObjs( p, 0, &nMultiLHS );
     Vec_Int_t * vObjsRHS = Wlc_NtkCollectObjs( p, 1, &nMultiRHS );
-    Gia_Man_t * pGia = Wlc_NtkBitBlast( p, NULL, -1, 0, 0, 0, 0, 1, 0, 0 );
+    Gia_Man_t * pGia = Wlc_NtkBitBlast( p, NULL ); //, -1, 0, 0, 0, 0, 1, 0, 0 ); // <= no cleanup
     Vec_Mem_t * vTtMem = Vec_MemAlloc( nWords, 10 );
     Vec_MemHashAlloc( vTtMem, 10000 );
 
@@ -540,7 +540,7 @@ int Sbc_ManWlcNodes( Wlc_Ntk_t * pNtk, Gia_Man_t * p, Vec_Int_t * vGia2Out, int
 void Sbc_ManDetectMultTest( Wlc_Ntk_t * pNtk, int fVerbose )
 {
     extern Vec_Int_t * Sdb_StoComputeCutsDetect( Gia_Man_t * pGia );
-    Gia_Man_t * p = Wlc_NtkBitBlast( pNtk, NULL, -1, 0, 0, 0, 0, 1, 0, 0 );
+    Gia_Man_t * p = Wlc_NtkBitBlast( pNtk, NULL );//, -1, 0, 0, 0, 0, 1, 0, 0 ); // <= no cleanup
     Vec_Int_t * vIns, * vGia2Out;
     int iObjFound = -1;
 //    Gia_Obj_t * pObj; int i;
diff --git a/src/base/wlc/wlcReadVer.c b/src/base/wlc/wlcReadVer.c
index f2d482f7..bc82fa3c 100644
--- a/src/base/wlc/wlcReadVer.c
+++ b/src/base/wlc/wlcReadVer.c
@@ -1298,7 +1298,7 @@ void Io_ReadWordTest( char * pFileName )
         return;
     Wlc_WriteVer( pNtk, "test.v", 0, 0 );
 
-    pNew = Wlc_NtkBitBlast( pNtk, NULL, -1, 0, 0, 0, 0, 0, 0, 0 );
+    pNew = Wlc_NtkBitBlast( pNtk, NULL );
     Gia_AigerWrite( pNew, "test.aig", 0, 0 );
     Gia_ManStop( pNew );
 
diff --git a/src/base/wlc/wlcSim.c b/src/base/wlc/wlcSim.c
index 3d664527..4286bd23 100644
--- a/src/base/wlc/wlcSim.c
+++ b/src/base/wlc/wlcSim.c
@@ -129,7 +129,7 @@ Vec_Ptr_t * Wlc_NtkSimulate( Wlc_Ntk_t * p, Vec_Int_t * vNodes, int nWords, int
 {
     Gia_Obj_t * pObj; 
     Vec_Ptr_t * vOne, * vRes;
-    Gia_Man_t * pGia = Wlc_NtkBitBlast( p, NULL, -1, 0, 0, 0, 0, 0, 0, 0 );
+    Gia_Man_t * pGia = Wlc_NtkBitBlast( p, NULL );
     Wlc_Obj_t * pWlcObj;
     int f, i, k, w, nBits, Counter = 0;
     // allocate simulation info for one timeframe
diff --git a/src/base/wlc/wlcUif.c b/src/base/wlc/wlcUif.c
index 78451c17..3c7a08ac 100644
--- a/src/base/wlc/wlcUif.c
+++ b/src/base/wlc/wlcUif.c
@@ -32,6 +32,38 @@ ABC_NAMESPACE_IMPL_START
 
 /**Function*************************************************************
 
+  Synopsis    [Collect adds and mults.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Wlc_NtkCollectAddMult( Wlc_Ntk_t * p, Wlc_BstPar_t * pPar, int * pCountA, int * pCountM )
+{
+    Vec_Int_t * vBoxIds;
+    Wlc_Obj_t * pObj;  int i;
+    *pCountA = *pCountM = 0;
+    if ( pPar->nAdderLimit == 0 && pPar->nMultLimit == 0 )
+        return NULL;
+    vBoxIds = Vec_IntAlloc( 100 );
+    Wlc_NtkForEachObj( p, pObj, i )
+    {
+        if ( pObj->Type == WLC_OBJ_ARI_ADD && pPar->nAdderLimit && Wlc_ObjRange(pObj) >= pPar->nAdderLimit )
+            Vec_IntPush( vBoxIds, i ), (*pCountA)++;
+        else if ( pObj->Type == WLC_OBJ_ARI_MULTI && pPar->nMultLimit && Wlc_ObjRange(pObj) >= pPar->nMultLimit )
+            Vec_IntPush( vBoxIds, i ), (*pCountM)++;
+    }
+    if ( Vec_IntSize( vBoxIds ) > 0 )
+        return vBoxIds;
+    Vec_IntFree( vBoxIds );
+    return NULL;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Check if two objects have the same input/output signatures.]
 
   Description []