New profiling features for word-level optimizations.

src/base/abci/abc.c

@@ -2626,13 +2626,18 @@ usage:
 ***********************************************************************/
 int Abc_CommandPrintStatus( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    int c, fShort = 1;
+    extern void Abc_NtkPrintPoEquivs( Abc_Ntk_t * pNtk );
+    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
+    int c, fOutStatus = 0, fShort = 1;
     // set defaults
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "sh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "osh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'o':
+            fOutStatus ^= 1;
+            break;
         case 's':
             fShort ^= 1;
             break;
@@ -2642,6 +2647,16 @@ int Abc_CommandPrintStatus( Abc_Frame_t * pAbc, int argc, char ** argv )
             goto usage;
         }
     }
+    if ( fOutStatus )
+    {
+        if ( pNtk == NULL )
+        {
+            Abc_Print( -1, "Empty network.\n" );
+            return 1;
+        }
+        Abc_NtkPrintPoEquivs( pNtk );
+        return 0;
+    }
     Abc_Print( 1,"Status = %d  Frames = %d   ", pAbc->Status, pAbc->nFrames );
     if ( pAbc->pCex == NULL && pAbc->vCexVec == NULL )
         Abc_Print( 1,"Cex is not defined.\n" );
@@ -2691,8 +2706,9 @@ int Abc_CommandPrintStatus( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: print_status [-sh]\n" );
+    Abc_Print( -2, "usage: print_status [-osh]\n" );
     Abc_Print( -2, "\t        prints verification status\n" );
+    Abc_Print( -2, "\t-o    : toggle printing output status [default = %s]\n", fOutStatus? "yes": "no" );
     Abc_Print( -2, "\t-s    : toggle using short print-out [default = %s]\n", fShort? "yes": "no" );
     Abc_Print( -2, "\t-h    : print the command usage\n");
     return 1;

src/base/abci/abcPrint.c

@@ -1695,6 +1695,46 @@ void Abc_NtkPrintMiter( Abc_Ntk_t * pNtk )
         printf( "The first satisfiable output is number %d (%s).\n", iOut, Abc_ObjName( Abc_NtkPo(pNtk, iOut) ) );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Checks the status of the miter.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkPrintPoEquivs( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj, * pDriver, * pRepr;  int i, iRepr;
+    Vec_Int_t * vMap = Vec_IntStartFull( Abc_NtkObjNumMax(pNtk) );
+    Abc_NtkForEachPo( pNtk, pObj, i )
+    {
+        pDriver = Abc_ObjFanin0(pObj);
+        if ( Abc_NtkIsStrash(pNtk) && pDriver == Abc_AigConst1(pNtk) )
+        {
+            printf( "%s = Const%d\n", Abc_ObjName(pObj), !Abc_ObjFaninC0(pObj) );
+            continue;
+        }
+        else if ( !Abc_NtkIsStrash(pNtk) && Abc_NodeIsConst(pDriver) )
+        {
+            printf( "%s = Const%d\n", Abc_ObjName(pObj), Abc_NodeIsConst1(pDriver) );
+            continue;
+        }
+        iRepr = Vec_IntEntry( vMap, Abc_ObjId(pDriver) );
+        if ( iRepr == -1 )
+        {
+            Vec_IntWriteEntry( vMap, Abc_ObjId(pDriver), i );
+            continue;
+        }
+        pRepr = Abc_NtkCo(pNtk, iRepr);
+        printf( "%s = %s%s\n", Abc_ObjName(pObj), Abc_ObjFaninC0(pRepr) == Abc_ObjFaninC0(pObj) ? "" : "!", Abc_ObjName(pRepr) );
+    }
+    Vec_IntFree( vMap );
+}
+
 
 
 

src/base/wlc/wlc.h

@@ -257,7 +257,7 @@ extern Vec_Int_t *    Wlc_NtkFindUifableMultiplierPairs( Wlc_Ntk_t * p );
 extern Wlc_Ntk_t *    Wlc_NtkAbstractNodes( Wlc_Ntk_t * pNtk, Vec_Int_t * vNodes );
 extern Wlc_Ntk_t *    Wlc_NtkUifNodePairs( Wlc_Ntk_t * pNtk, Vec_Int_t * vPairs );
 /*=== wlcBlast.c ========================================================*/
-extern Gia_Man_t *    Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int fGiaSimple );
+extern Gia_Man_t *    Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int fGiaSimple, int fAddOutputs );
 /*=== wlcCom.c ========================================================*/
 extern void           Wlc_SetNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk );
 /*=== wlcNtk.c ========================================================*/

src/base/wlc/wlcBlast.c

@@ -716,14 +716,14 @@ void Wlc_BlastSquare( Gia_Man_t * pNew, int * pNum, int nNum, Vec_Int_t * vTmp,
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int fGiaSimple )
+Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int fGiaSimple, int fAddOutputs )
 {
     int fVerbose = 0;
     int fUseOldMultiplierBlasting = 0;
     Tim_Man_t * pManTime = NULL;
     Gia_Man_t * pTemp, * pNew, * pExtra = NULL;
     Wlc_Obj_t * pObj;
-    Vec_Int_t * vBits = &p->vBits, * vTemp0, * vTemp1, * vTemp2, * vRes;
+    Vec_Int_t * vBits = &p->vBits, * vTemp0, * vTemp1, * vTemp2, * vRes, * vAddOutputs = NULL, * vAddObjs = NULL;
     int nBits = Wlc_NtkPrepareBits( p );
     int nRange, nRange0, nRange1, nRange2;
     int i, k, b, iFanin, iLit, nAndPrev, * pFans0, * pFans1, * pFans2;
@@ -743,6 +743,10 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int fGiaSimple
     pNew->fGiaSimple = fGiaSimple;
     if ( !fGiaSimple )
         Gia_ManHashAlloc( pNew );
+    if ( fAddOutputs )
+        vAddOutputs = Vec_IntAlloc( 100 );
+    if ( fAddOutputs )
+        vAddObjs = Vec_IntAlloc( 100 );
     // prepare for AIG with boxes
     if ( vBoxIds )
     {
@@ -1183,6 +1187,17 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int fGiaSimple
         else assert( 0 );
         assert( Vec_IntSize(vBits) == Wlc_ObjCopy(p, i) );
         Vec_IntAppend( vBits, vRes );
+        if ( vAddOutputs && !Wlc_ObjIsCo(pObj) && 
+            (
+             (pObj->Type >= WLC_OBJ_MUX      && pObj->Type <= WLC_OBJ_ROTATE_L)     || 
+             (pObj->Type >= WLC_OBJ_COMP_EQU && pObj->Type <= WLC_OBJ_COMP_MOREEQU) || 
+             (pObj->Type >= WLC_OBJ_ARI_ADD  && pObj->Type <= WLC_OBJ_ARI_SQUARE)
+            )
+           )
+        {
+            Vec_IntAppend( vAddOutputs, vRes );
+            Vec_IntPush( vAddObjs, Wlc_ObjId(p, pObj) );
+        }
         p->nAnds[pObj->Type] += Gia_ManAndNum(pNew) - nAndPrev;
     }
     p->nAnds[0] = Gia_ManAndNum(pNew);
@@ -1194,6 +1209,14 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int fGiaSimple
     // create COs
     Wlc_NtkForEachCo( p, pObj, i )
     {
+        // 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 )
@@ -1307,42 +1330,62 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int fGiaSimple
         Vec_PtrPush( pNew->vNamesIn, Abc_UtilStrsav("abc_reset_flop") );
     assert( Vec_PtrSize(pNew->vNamesIn) == Gia_ManCiNum(pNew) );
     // create output names
-/*
-    pNew->vNamesOut = Vec_PtrAlloc( Gia_ManCoNum(pNew) );
-    Wlc_NtkForEachCo( p, pObj, i )
-    if ( Wlc_ObjIsPo(pObj) )
+    if ( vAddObjs )
     {
-        char * pName = Wlc_ObjName(p, Wlc_ObjId(p, pObj));
-        nRange = Wlc_ObjRange( pObj );
-        if ( 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 ( 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 ( 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) );
-            }
+        // add real primary outputs
+        pNew->vNamesOut = Vec_PtrAlloc( Gia_ManCoNum(pNew) );
+        Wlc_NtkForEachCo( p, pObj, i )
+        if ( Wlc_ObjIsPo(pObj) )
+        {
+            char * pName = Wlc_ObjName(p, Wlc_ObjId(p, pObj));
+            nRange = Wlc_ObjRange( pObj );
+            if ( 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) );
+                }
+        }
+        // add internal primary outputs
+        Wlc_NtkForEachObjVec( vAddObjs, p, pObj, i )
+        {
+            char * pName = Wlc_ObjName(p, Wlc_ObjId(p, pObj));
+            nRange = Wlc_ObjRange( pObj );
+            if ( 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) );
+                }
+        }
+        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 ( 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) );
     }
-    assert( Vec_PtrSize(pNew->vNamesOut) == Gia_ManCoNum(pNew) );
-*/
+
     pNew->pSpec = Abc_UtilStrsav( p->pSpec ? p->pSpec : p->pName );
     // dump the miter parts
     if ( 0 )

src/base/wlc/wlcCom.c

@@ -338,15 +338,18 @@ 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, fGiaSimple = 0, fMulti = 0, fVerbose  = 0;
+    int c, fGiaSimple = 0, fAddOutputs = 0, fMulti = 0, fVerbose  = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "cmvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "comvh" ) ) != EOF )
     {
         switch ( c )
         {
         case 'c':
             fGiaSimple ^= 1;
             break;
+        case 'o':
+            fAddOutputs ^= 1;
+            break;
         case 'm':
             fMulti ^= 1;
             break;
@@ -371,7 +374,7 @@ int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
             Abc_Print( 1, "Warning:  There is no multipliers in the design.\n" );
     }
     // transform
-    pNew = Wlc_NtkBitBlast( pNtk, vBoxIds, fGiaSimple );
+    pNew = Wlc_NtkBitBlast( pNtk, vBoxIds, fGiaSimple, fAddOutputs );
     Vec_IntFreeP( &vBoxIds );
     if ( pNew == NULL )
     {
@@ -381,9 +384,10 @@ int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_FrameUpdateGia( pAbc, pNew );
     return 0;
 usage:
-    Abc_Print( -2, "usage: %%blast [-cmvh]\n" );
+    Abc_Print( -2, "usage: %%blast [-comvh]\n" );
     Abc_Print( -2, "\t         performs bit-blasting of the word-level design\n" );
     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-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");

src/base/wlc/wlcReadVer.c

@@ -1291,7 +1291,7 @@ void Io_ReadWordTest( char * pFileName )
         return;
     Wlc_WriteVer( pNtk, "test.v", 0, 0 );
 
-    pNew = Wlc_NtkBitBlast( pNtk, NULL, 0 );
+    pNew = Wlc_NtkBitBlast( pNtk, NULL, 0, 0 );
     Gia_AigerWrite( pNew, "test.aig", 0, 0 );
     Gia_ManStop( pNew );
 

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, 0 );
+    Gia_Man_t * pGia = Wlc_NtkBitBlast( p, NULL, 0, 0 );
     Wlc_Obj_t * pWlcObj;
     int f, i, k, w, nBits, Counter = 0;
     // allocate simulation info for one timeframe