Adding switch %blast -d to dump dual-output miter after blasting.

8 files changed, 100 insertions, 43 deletions

diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index 229a6bfb..19f4b906 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -324,7 +324,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 );
+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 );
 /*=== wlcCom.c ========================================================*/
 extern void           Wlc_SetNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk );
 /*=== wlcNtk.c ========================================================*/
diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c
index c56d1262..e3370e25 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 );
+    Gia_Man_t * pGiaChoice = Wlc_NtkBitBlast( pChoice, NULL, -1, 0, 0, 0, 0, 0, 0 );
     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 );
+    Gia_Man_t * pGiaChoice = Wlc_NtkBitBlast( pChoice, NULL, -1, 0, 0, 0, 0, 0, 0 );
     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 );
+    Gia_Man_t * pGiaOrig = Wlc_NtkBitBlast( pOrig, NULL, -1, 0, 0, 0, 0, 0, 0 );
     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 );
+    pWla->pGia = Wlc_NtkBitBlast( pAbs, NULL, -1, 0, 0, 0, 0, 0, 0 );
 
     // if the abstraction has flops with DC-init state,
     // new PIs were introduced by bit-blasting at the end of the PI list
@@ -1828,7 +1828,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 );
+        pGia = Wlc_NtkBitBlast( pAbs, NULL, -1, 0, 0, 0, 0, 0, 0 );
 
         // 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 ff0092e6..4b2e6740 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 );
+        pGia = Wlc_NtkBitBlast( pAbs, NULL, -1, 0, 0, 0, 0, 0, 0 );
 
         // 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 02cb2b1c..794efbc4 100644
--- a/src/base/wlc/wlcBlast.c
+++ b/src/base/wlc/wlcBlast.c
@@ -868,14 +868,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 )
+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 fVerbose = 0;
     int fUseOldMultiplierBlasting = 0;
     int fSkipBitRange = 0;
     Tim_Man_t * pManTime = NULL;
     Gia_Man_t * pTemp, * pNew, * pExtra = NULL;
-    Wlc_Obj_t * pObj;
+    Wlc_Obj_t * pObj, * pObj2;
     Vec_Int_t * vBits = &p->vBits, * vTemp0, * vTemp1, * vTemp2, * vRes, * vAddOutputs = NULL, * vAddObjs = NULL;
     int nBits = Wlc_NtkPrepareBits( p );
     int nRange, nRange0, nRange1, nRange2;
@@ -1363,38 +1363,91 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in
     Vec_IntFree( vTemp2 );
     Vec_IntFree( vRes );
     // create COs
-    Wlc_NtkForEachCo( p, pObj, i )
+    if ( fCreateMiter )
     {
-        // skip all outputs except the given ones
-        if ( iOutput >= 0 && (i < iOutput || i >= iOutput + nOutputRange) )
-            continue;
-        // create additional PO literals
-        if ( vAddOutputs && pObj->fIsFi )
-        {
-            Vec_IntForEachEntry( vAddOutputs, iLit, k )
-                Gia_ManAppendCo( pNew, iLit );
-            printf( "Created %d additional POs for %d interesting internal word-level variables.\n", Vec_IntSize(vAddOutputs), Vec_IntSize(vAddObjs) );
-            Vec_IntFreeP( &vAddOutputs );
-        }
-        nRange = Wlc_ObjRange( pObj );
-        pFans0 = Vec_IntEntryP( vBits, Wlc_ObjCopy(p, Wlc_ObjId(p, pObj)) );
-        if ( fVerbose )
-            printf( "%s(%d) ", Wlc_ObjName(p, Wlc_ObjId(p, pObj)), Gia_ManCoNum(pNew) );
-        if ( Wlc_ObjRangeIsReversed(pObj) )
+        int nPairs = 0, nBits = 0;
+        assert( Wlc_NtkPoNum(p) % 2 == 0 );
+        Wlc_NtkForEachCo( p, pObj, i )
         {
-            for ( k = 0; k < nRange; k++ )
-                Gia_ManAppendCo( pNew, pFans0[nRange-1-k] );
+            if ( pObj->fIsFi )
+            {
+                nRange = Wlc_ObjRange( pObj );
+                pFans0 = Vec_IntEntryP( vBits, Wlc_ObjCopy(p, Wlc_ObjId(p, pObj)) );
+                if ( Wlc_ObjRangeIsReversed(pObj) )
+                {
+                    for ( k = 0; k < nRange; k++ )
+                        Gia_ManAppendCo( pNew, pFans0[nRange-1-k] );
+                }
+                else
+                {
+                    for ( k = 0; k < nRange; k++ )
+                        Gia_ManAppendCo( pNew, pFans0[k] );
+                }
+                nFFins += nRange;
+                continue;
+            }
+            pObj2   = Wlc_NtkCo( p, ++i );
+            nRange1 = Wlc_ObjRange( pObj );
+            nRange2 = Wlc_ObjRange( pObj2 );
+            assert( nRange1 == nRange2 );
+            pFans1  = Vec_IntEntryP( vBits, Wlc_ObjCopy(p, Wlc_ObjId(p, pObj)) );
+            pFans2  = Vec_IntEntryP( vBits, Wlc_ObjCopy(p, Wlc_ObjId(p, pObj2)) );
+            if ( Wlc_ObjRangeIsReversed(pObj) )
+            {
+                for ( k = 0; k < nRange1; k++ )
+                {
+                    Gia_ManAppendCo( pNew, pFans1[nRange1-1-k] );
+                    Gia_ManAppendCo( pNew, pFans2[nRange2-1-k] );
+                }
+            }
+            else
+            {
+                for ( k = 0; k < nRange1; k++ )
+                {
+                    Gia_ManAppendCo( pNew, pFans1[k] );
+                    Gia_ManAppendCo( pNew, pFans2[k] );
+                }
+            }
+            nPairs++;
+            nBits += nRange1;
         }
-        else
+        printf( "Derived a dual-output miter with %d pairs of bits belonging to %d pairs of word-level outputs.\n", nBits, nPairs );
+    }
+    else
+    {
+        Wlc_NtkForEachCo( p, pObj, i )
         {
-            for ( k = 0; k < nRange; k++ )
-                Gia_ManAppendCo( pNew, pFans0[k] );
+            // skip all outputs except the given ones
+            if ( iOutput >= 0 && (i < iOutput || i >= iOutput + nOutputRange) )
+                continue;
+            // create additional PO literals
+            if ( vAddOutputs && pObj->fIsFi )
+            {
+                Vec_IntForEachEntry( vAddOutputs, iLit, k )
+                    Gia_ManAppendCo( pNew, iLit );
+                printf( "Created %d additional POs for %d interesting internal word-level variables.\n", Vec_IntSize(vAddOutputs), Vec_IntSize(vAddObjs) );
+                Vec_IntFreeP( &vAddOutputs );
+            }
+            nRange = Wlc_ObjRange( pObj );
+            pFans0 = Vec_IntEntryP( vBits, Wlc_ObjCopy(p, Wlc_ObjId(p, pObj)) );
+            if ( fVerbose )
+                printf( "%s(%d) ", Wlc_ObjName(p, Wlc_ObjId(p, pObj)), Gia_ManCoNum(pNew) );
+            if ( Wlc_ObjRangeIsReversed(pObj) )
+            {
+                for ( k = 0; k < nRange; k++ )
+                    Gia_ManAppendCo( pNew, pFans0[nRange-1-k] );
+            }
+            else
+            {
+                for ( k = 0; k < nRange; k++ )
+                    Gia_ManAppendCo( pNew, pFans0[k] );
+            }
+            if ( pObj->fIsFi )
+                nFFins += nRange;
         }
-        if ( pObj->fIsFi )
-            nFFins += nRange;
+        if ( fVerbose )
+            printf( "\n" );
     }
-    if ( fVerbose )
-        printf( "\n" );
     //Vec_IntErase( vBits );
     //Vec_IntErase( &p->vCopies );
     // set the number of registers
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index 4e6fbd18..54fb8186 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -881,9 +881,9 @@ 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, fVerbose  = 0;
+    int c, iOutput = -1, nOutputRange = 2, fGiaSimple = 0, fAddOutputs = 0, fMulti = 0, fBooth = 0, fCreateMiter = 0, fVerbose  = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "ORcombvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "ORcombdvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -921,6 +921,9 @@ int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'b':
             fBooth ^= 1;
             break;
+        case 'd':
+            fCreateMiter ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -947,7 +950,7 @@ int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 0;
     }
     // transform
-    pNew = Wlc_NtkBitBlast( pNtk, vBoxIds, iOutput, nOutputRange, fGiaSimple, fAddOutputs, fBooth, 0 );
+    pNew = Wlc_NtkBitBlast( pNtk, vBoxIds, iOutput, nOutputRange, fGiaSimple, fAddOutputs, fBooth, 0, fCreateMiter );
     Vec_IntFreeP( &vBoxIds );
     if ( pNew == NULL )
     {
@@ -957,7 +960,7 @@ 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] [-combvh]\n" );
+    Abc_Print( -2, "usage: %%blast [-OR num] [-combdvh]\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 );
@@ -965,6 +968,7 @@ usage:
     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-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/wlcGraft.c b/src/base/wlc/wlcGraft.c
index 33de00c5..f1f55eb3 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 );
+    Gia_Man_t * pGia = Wlc_NtkBitBlast( p, NULL, -1, 0, 0, 0, 0, 1, 0 );
     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 );
+    Gia_Man_t * p = Wlc_NtkBitBlast( pNtk, NULL, -1, 0, 0, 0, 0, 1, 0 );
     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 63a6926b..a829e0fd 100644
--- a/src/base/wlc/wlcReadVer.c
+++ b/src/base/wlc/wlcReadVer.c
@@ -1292,7 +1292,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 );
+    pNew = Wlc_NtkBitBlast( pNtk, NULL, -1, 0, 0, 0, 0, 0, 0 );
     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 2ae3c86e..31a8a4a0 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 );
+    Gia_Man_t * pGia = Wlc_NtkBitBlast( p, NULL, -1, 0, 0, 0, 0, 0, 0 );
     Wlc_Obj_t * pWlcObj;
     int f, i, k, w, nBits, Counter = 0;
     // allocate simulation info for one timeframe