Word-level abstraction.

src/base/wlc/wlc.h

@@ -304,7 +304,8 @@ extern void           Wlc_NtkPrintNodes( Wlc_Ntk_t * p, int Type );
 extern void           Wlc_NtkPrintStats( Wlc_Ntk_t * p, int fDistrib, int fTwoSides, int fVerbose );
 extern void           Wlc_NtkTransferNames( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p );
 extern char *         Wlc_NtkNewName( Wlc_Ntk_t * p, int iCoId, int fSeq );
-extern Wlc_Ntk_t *    Wlc_NtkDupDfs( Wlc_Ntk_t * p, int fMarked, int fSeq, Vec_Int_t * vPisNew );
+extern Wlc_Ntk_t *    Wlc_NtkDupDfs( Wlc_Ntk_t * p, int fMarked, int fSeq );
+extern Wlc_Ntk_t *    Wlc_NtkDupDfsAbs( Wlc_Ntk_t * p, Vec_Int_t * vPisOld, Vec_Int_t * vPisNew, Vec_Int_t * vFlops );
 extern void           Wlc_NtkCleanMarks( Wlc_Ntk_t * p );
 extern void           Wlc_NtkMarkCone( Wlc_Ntk_t * p, int iCoId, int Range, int fSeq, int fAllPis );
 extern void           Wlc_NtkProfileCones( Wlc_Ntk_t * p );

src/base/wlc/wlcAbs.c

@@ -173,7 +173,7 @@ Wlc_Ntk_t * Wlc_NtkAbstractNodes( Wlc_Ntk_t * p, Vec_Int_t * vNodesInit )
     if ( vNodes != vNodesInit )
         Vec_IntFree( vNodes );
     // reconstruct topological order
-    pNew = Wlc_NtkDupDfs( p, 0, 1, NULL );
+    pNew = Wlc_NtkDupDfs( p, 0, 1 );
     return pNew;
 }
 
@@ -277,7 +277,7 @@ Wlc_Ntk_t * Wlc_NtkUifNodePairs( Wlc_Ntk_t * p, Vec_Int_t * vPairsInit )
     if ( vPairs != vPairsInit )
         Vec_IntFree( vPairs );
     // reconstruct topological order
-    pNew = Wlc_NtkDupDfs( p, 0, 1, NULL );
+    pNew = Wlc_NtkDupDfs( p, 0, 1 );
     return pNew;
 }
 

src/base/wlc/wlcAbs2.c

@@ -52,10 +52,10 @@ struct Wabs_Par_t_
 void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars )
 {
     memset( pPars, 0, sizeof(Wlc_Par_t) );
-    pPars->nBitsAdd       =      16;  // adder bit-width
-    pPars->nBitsMul       =       8;  // multiplier bit-widht 
-    pPars->nBitsMux       =      32;  // MUX bit-width
-    pPars->nBitsFlop      =      32;  // flop bit-width
+    pPars->nBitsAdd    = ABC_INFINITY;   // adder bit-width
+    pPars->nBitsMul    = ABC_INFINITY;   // multiplier bit-widht 
+    pPars->nBitsMux    = ABC_INFINITY;   // MUX bit-width
+    pPars->nBitsFlop   = ABC_INFINITY;   // flop bit-width
     pPars->fVerbose    =             0;  // verbose output`
 }
 
@@ -73,40 +73,41 @@ void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars )
 Vec_Bit_t * Wlc_NtkAbsMarkOpers( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
 {
     Vec_Bit_t * vLeaves = Vec_BitStart( Wlc_NtkObjNumMax(p) );
-    Wlc_Obj_t * pObj; int i;
+    Wlc_Obj_t * pObj; int i, Count[4] = {0};
     Wlc_NtkForEachObj( p, pObj, i )
     {
         if ( pObj->Type == WLC_OBJ_ARI_ADD || pObj->Type == WLC_OBJ_ARI_SUB || pObj->Type == WLC_OBJ_ARI_MINUS )
         {
             if ( Wlc_ObjRange(pObj) >= pPars->nBitsAdd )
-                Vec_BitWriteEntry( vLeaves, Wlc_ObjId(p, pObj), 1 );
+                Vec_BitWriteEntry( vLeaves, Wlc_ObjId(p, pObj), 1 ), Count[0]++;
             continue;
         }
         if ( pObj->Type == WLC_OBJ_ARI_MULTI || pObj->Type == WLC_OBJ_ARI_DIVIDE || pObj->Type == WLC_OBJ_ARI_REM || pObj->Type == WLC_OBJ_ARI_MODULUS )
         {
             if ( Wlc_ObjRange(pObj) >= pPars->nBitsMul )
-                Vec_BitWriteEntry( vLeaves, Wlc_ObjId(p, pObj), 1 );
+                Vec_BitWriteEntry( vLeaves, Wlc_ObjId(p, pObj), 1 ), Count[1]++;
             continue;
         }
         if ( pObj->Type == WLC_OBJ_MUX )
         {
             if ( Wlc_ObjRange(pObj) >= pPars->nBitsMux )
-                Vec_BitWriteEntry( vLeaves, Wlc_ObjId(p, pObj), 1 );
+                Vec_BitWriteEntry( vLeaves, Wlc_ObjId(p, pObj), 1 ), Count[2]++;
             continue;
         }
         if ( Wlc_ObjIsCi(pObj) && !Wlc_ObjIsPi(pObj) )
         {
             if ( Wlc_ObjRange(pObj) >= pPars->nBitsFlop )
-                Vec_BitWriteEntry( vLeaves, Wlc_ObjId(p, pObj), 1 );
+                Vec_BitWriteEntry( vLeaves, Wlc_ObjId(p, pObj), 1 ), Count[3]++;
             continue;
         }
     }
+    printf( "Abstraction engine marked %d adds/subs, %d muls/divs, %d muxes, and %d flops to be abstracted away.\n", Count[0], Count[1], Count[2], Count[3] );
     return vLeaves;
 }
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Marks nodes to be included in the abstracted network.]
 
   Description []
                
@@ -115,7 +116,7 @@ Vec_Bit_t * Wlc_NtkAbsMarkOpers( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
   SeeAlso     []
 
 ***********************************************************************/
-void Wlc_NtkAbsMarkNodes_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Bit_t * vLeaves, Vec_Int_t * vFlops, Vec_Int_t * vPisNew )
+void Wlc_NtkAbsMarkNodes_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Bit_t * vLeaves, Vec_Int_t * vPisOld, Vec_Int_t * vPisNew, Vec_Int_t * vFlops )
 {
     int i, iFanin;
     if ( pObj->Mark )
@@ -123,42 +124,45 @@ void Wlc_NtkAbsMarkNodes_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Bit_t * vLeav
     pObj->Mark = 1;
     if ( Vec_BitEntry(vLeaves, Wlc_ObjId(p, pObj)) )
     {
+        assert( !Wlc_ObjIsPi(pObj) );
         Vec_IntPush( vPisNew, Wlc_ObjId(p, pObj) );
         return;
     }
     if ( Wlc_ObjIsCi(pObj) )
     {
-        if ( !Wlc_ObjIsPi(pObj) )
-            Vec_IntPush( vFlops, Wlc_ObjCiId(pObj) );
+        if ( Wlc_ObjIsPi(pObj) )
+            Vec_IntPush( vPisOld, Wlc_ObjId(p, pObj) );
+        else
+            Vec_IntPush( vFlops, Wlc_ObjId(p, pObj) );
         return;
     }
     Wlc_ObjForEachFanin( pObj, iFanin, i )
-        Wlc_NtkAbsMarkNodes_rec( p, Wlc_NtkObj(p, iFanin), vLeaves, vFlops, vPisNew );
+        Wlc_NtkAbsMarkNodes_rec( p, Wlc_NtkObj(p, iFanin), vLeaves, vPisOld, vPisNew, vFlops );
 }
 
-Vec_Int_t * Wlc_NtkAbsMarkNodes( Wlc_Ntk_t * p, Vec_Bit_t * vLeaves )
+void Wlc_NtkAbsMarkNodes( Wlc_Ntk_t * p, Vec_Bit_t * vLeaves, Vec_Int_t * vPisOld, Vec_Int_t * vPisNew, Vec_Int_t * vFlops )
 {
-    Vec_Int_t * vFlops;
-    Vec_Int_t * vPisNew;
     Wlc_Obj_t * pObj;
-    int i, CiId, CoId;
+    int i, Count = 0;
     Wlc_NtkCleanMarks( p );
-    vFlops = Vec_IntAlloc( 100 );
-    vPisNew = Vec_IntAlloc( 100 );
     Wlc_NtkForEachCo( p, pObj, i )
-        Wlc_NtkAbsMarkNodes_rec( p, pObj, vLeaves, vFlops, vPisNew );
-    Vec_IntForEachEntry( vFlops, CiId, i )
-    {
-        CoId = Wlc_NtkPoNum(p) + CiId - Wlc_NtkPiNum(p);
-        Wlc_NtkAbsMarkNodes_rec( p, Wlc_NtkCo(p, CoId), vLeaves, vFlops, vPisNew );
-    }
-    Vec_IntFree( vFlops );
-    return vPisNew;
+        Wlc_NtkAbsMarkNodes_rec( p, pObj, vLeaves, vPisOld, vPisNew, vFlops );
+    Wlc_NtkForEachObjVec( vFlops, p, pObj, i )
+        Wlc_NtkAbsMarkNodes_rec( p, Wlc_ObjFo2Fi(p, pObj), vLeaves, vPisOld, vPisNew, vFlops );
+    Wlc_NtkForEachObj( p, pObj, i )
+        Count += pObj->Mark;
+//    printf( "Collected %d old PIs, %d new PIs, %d flops, and %d other objects.\n", 
+//        Vec_IntSize(vPisOld), Vec_IntSize(vPisNew), Vec_IntSize(vFlops), 
+//        Count - Vec_IntSize(vPisOld) - Vec_IntSize(vPisNew) - Vec_IntSize(vFlops) );
+    Vec_IntSort( vPisOld, 0 );
+    Vec_IntSort( vPisNew, 0 );
+    Vec_IntSort( vFlops, 0 );
+    Wlc_NtkCleanMarks( p );
 }
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Derive abstraction based on the parameter values.]
 
   Description []
                
@@ -169,11 +173,17 @@ Vec_Int_t * Wlc_NtkAbsMarkNodes( Wlc_Ntk_t * p, Vec_Bit_t * vLeaves )
 ***********************************************************************/
 Wlc_Ntk_t * Wlc_NtkAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
 {
+    Wlc_Ntk_t * pNtkNew = NULL;
+    Vec_Int_t * vPisOld = Vec_IntAlloc( 100 );
+    Vec_Int_t * vPisNew = Vec_IntAlloc( 100 );
+    Vec_Int_t * vFlops  = Vec_IntAlloc( 100 );
     Vec_Bit_t * vLeaves = Wlc_NtkAbsMarkOpers( p, pPars );
-    Vec_Int_t * vPisNew = Wlc_NtkAbsMarkNodes( p, vLeaves );
-    Wlc_Ntk_t * pNtkNew = Wlc_NtkDupDfs( p, 1, 1, vPisNew );
-    Vec_IntFree( vPisNew );
+    Wlc_NtkAbsMarkNodes( p, vLeaves, vPisOld, vPisNew, vFlops );
     Vec_BitFree( vLeaves );
+    pNtkNew = Wlc_NtkDupDfsAbs( p, vPisOld, vPisNew, vFlops );
+    Vec_IntFree( vPisOld );
+    Vec_IntFree( vPisNew );
+    Vec_IntFree( vFlops );
     return pNtkNew;
 }
 

src/base/wlc/wlcCom.c

@@ -423,7 +423,7 @@ int Abc_CommandCone( Abc_Frame_t * pAbc, int argc, char ** argv )
     printf( "Extracting output %d as a %s word-level network.\n", iOutput, fSeq ? "sequential" : "combinational" );
     pName = Wlc_NtkNewName( pNtk, iOutput, fSeq );
     Wlc_NtkMarkCone( pNtk, iOutput, Range, fSeq, fAllPis );
-    pNtk = Wlc_NtkDupDfs( pNtk, 1, fSeq, NULL );
+    pNtk = Wlc_NtkDupDfs( pNtk, 1, fSeq );
     ABC_FREE( pNtk->pName );
     pNtk->pName = Abc_UtilStrsav( pName );
     Wlc_AbcUpdateNtk( pAbc, pNtk );
@@ -941,6 +941,7 @@ usage:
 ******************************************************************************/
 int Abc_CommandInvCheck( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
+    abctime clk = Abc_Clock();
     extern int Pdr_InvCheck( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose );
     int c, nFailed, fVerbose  = 0;
     Extra_UtilGetoptReset();
@@ -974,9 +975,10 @@ int Abc_CommandInvCheck( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     nFailed = Pdr_InvCheck( pAbc->pGia, Wlc_AbcGetInv(pAbc), fVerbose );
     if ( nFailed )
-        printf( "Invariant verification failed for %d clauses (out of %d).\n", nFailed, Vec_IntEntry(Wlc_AbcGetInv(pAbc),0) );
+        printf( "Invariant verification failed for %d clauses (out of %d). ", nFailed, Vec_IntEntry(Wlc_AbcGetInv(pAbc),0) );
     else
-        printf( "Invariant verification succeeded.\n" );
+        printf( "Invariant verification succeeded.    " );
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
     return 0;
 usage:
     Abc_Print( -2, "usage: inv_check [-vh]\n" );

src/base/wlc/wlcNtk.c

@@ -648,7 +648,7 @@ void Wlc_NtkPrintStats( Wlc_Ntk_t * p, int fDistrib, int fTwoSides, int fVerbose
     printf( "PI = %4d  ",      Wlc_NtkCountRealPis(p) ); //Wlc_NtkPiNum(p) );
     printf( "PO = %4d  ",      Wlc_NtkPoNum(p) );
     printf( "FF = %4d  ",      Wlc_NtkFfNum(p) );
-    printf( "Obj = %6d  ",     Wlc_NtkObjNum(p) );
+    printf( "Obj = %6d  ",     Wlc_NtkObjNum(p) - Wlc_NtkPiNum(p) - Wlc_NtkPoNum(p) - Wlc_NtkFfNum(p) );
     printf( "Mem = %.3f MB",   1.0*Wlc_NtkMemUsage(p)/(1<<20) );
     printf( "\n" );
     if ( fDistrib )
@@ -723,7 +723,7 @@ Vec_Int_t * Wlc_ReduceMarkedInitVec( Wlc_Ntk_t * p, Vec_Int_t * vInit )
     assert( Vec_IntSize(vInit) == Wlc_NtkCiNum(p) - Wlc_NtkPiNum(p) );
     Wlc_NtkForEachCi( p, pObj, i )
         if ( !Wlc_ObjIsPi(pObj) && pObj->Mark )
-            Vec_IntWriteEntry( vInitNew, k++, Vec_IntEntry(vInit, i) );
+            Vec_IntWriteEntry( vInitNew, k++, Vec_IntEntry(vInit, i - Wlc_NtkPiNum(p)) );
     Vec_IntShrink( vInitNew, k );
     return vInitNew;
 }
@@ -803,7 +803,7 @@ void Wlc_NtkDupDfs_rec( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, int iObj, Vec_Int_t * v
         Wlc_NtkDupDfs_rec( pNew, p, iFanin, vFanins );
     Wlc_ObjDup( pNew, p, iObj, vFanins );
 }
-Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p, int fMarked, int fSeq, Vec_Int_t * vPisNew )
+Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p, int fMarked, int fSeq )
 {
     Wlc_Ntk_t * pNew;
     Wlc_Obj_t * pObj;
@@ -813,24 +813,6 @@ Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p, int fMarked, int fSeq, Vec_Int_t * vPi
     Wlc_NtkCleanCopy( p );
     pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc );
     pNew->fSmtLib = p->fSmtLib;
-    if ( vPisNew )
-    {
-        // duplicate marked PIs
-        Wlc_NtkForEachPi( p, pObj, i )
-            if ( pObj->Mark )
-                Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
-        // duplicated additional PIs
-        Wlc_NtkForEachObjVec( vPisNew, p, pObj, i )
-        {
-            unsigned Type = pObj->Type;
-            assert( !Wlc_ObjIsPi(pObj) );
-            pObj->Type = WLC_OBJ_PI;
-            Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
-            pObj->Type = Type;
-        }
-    }
-    else
-    {
     Wlc_NtkForEachCi( p, pObj, i )
         if ( !fMarked || pObj->Mark )
         {
@@ -839,7 +821,6 @@ Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p, int fMarked, int fSeq, Vec_Int_t * vPi
             Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
             pObj->Type = Type;
         }
-    }
     Wlc_NtkForEachCo( p, pObj, i )
         if ( !fMarked || pObj->Mark )
             Wlc_NtkDupDfs_rec( pNew, p, Wlc_ObjId(p, pObj), vFanins );
@@ -869,6 +850,71 @@ Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p, int fMarked, int fSeq, Vec_Int_t * vPi
     Wlc_NtkTransferNames( pNew, p );
     return pNew;
 }
+Wlc_Ntk_t * Wlc_NtkDupDfsAbs( Wlc_Ntk_t * p, Vec_Int_t * vPisOld, Vec_Int_t * vPisNew, Vec_Int_t * vFlops )
+{
+    Wlc_Ntk_t * pNew;
+    Wlc_Obj_t * pObj;
+    Vec_Int_t * vFanins;
+    int i;
+    Wlc_NtkCleanCopy( p );
+    pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc );
+    pNew->fSmtLib = p->fSmtLib;
+
+    // duplicate marked PIs
+    vFanins = Vec_IntAlloc( 100 );
+    Wlc_NtkForEachObjVec( vPisOld, p, pObj, i )
+    {
+        assert( Wlc_ObjIsPi(pObj) );
+        Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
+    }
+    // duplicate additional PIs
+    Wlc_NtkForEachObjVec( vPisNew, p, pObj, i )
+    {
+        unsigned Type = pObj->Type;
+        int nFanins = Wlc_ObjFaninNum(pObj);
+        assert( !Wlc_ObjIsPi(pObj) );
+        pObj->Type = WLC_OBJ_PI;
+        pObj->nFanins = 0;
+        Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
+        pObj->Type = Type;
+        pObj->nFanins = (unsigned)nFanins;
+    }
+    // duplicate flop outputs
+    Wlc_NtkForEachObjVec( vFlops, p, pObj, i )
+    {
+        assert( !Wlc_ObjIsPi(pObj) && Wlc_ObjIsCi(pObj) );
+        Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
+    }
+
+    // duplicate logic cones of primary outputs
+    Wlc_NtkForEachPo( p, pObj, i )
+        Wlc_NtkDupDfs_rec( pNew, p, Wlc_ObjId(p, pObj), vFanins );
+    // duplidate logic cone of flop inputs
+    Wlc_NtkForEachObjVec( vFlops, p, pObj, i )
+        Wlc_NtkDupDfs_rec( pNew, p, Wlc_ObjId(p, Wlc_ObjFo2Fi(p, pObj)), vFanins );
+
+    // duplicate POs
+    Wlc_NtkForEachPo( p, pObj, i )
+        Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), 0 );
+    // duplicate flop inputs 
+    Wlc_NtkForEachObjVec( vFlops, p, pObj, i )
+        Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, Wlc_ObjFo2Fi(p, pObj)), 1 );
+    Vec_IntFree( vFanins );
+
+    // mark flop outputs
+    Wlc_NtkForEachObjVec( vFlops, p, pObj, i )
+        pObj->Mark = 1;
+    if ( p->vInits )
+        pNew->vInits = Wlc_ReduceMarkedInitVec( p, p->vInits );
+    if ( p->pInits )
+        pNew->pInits = Wlc_ReduceMarkedInitStr( p, p->pInits );
+    Wlc_NtkCleanMarks( p );
+
+    if ( p->pSpec )
+        pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Wlc_NtkTransferNames( pNew, p );
+    return pNew;
+}
 
 /**Function*************************************************************
 

src/base/wlc/wlcReadVer.c

@@ -1265,7 +1265,7 @@ Wlc_Ntk_t * Wlc_ReadVer( char * pFileName, char * pStr )
     if ( !Wlc_PrsDerive( p ) )
         goto finish;
     // derive topological order
-    pNtk = Wlc_NtkDupDfs( p->pNtk, 0, 1, NULL );
+    pNtk = Wlc_NtkDupDfs( p->pNtk, 0, 1 );
     pNtk->pSpec = Abc_UtilStrsav( pFileName );
 finish:
     Wlc_PrsPrintErrorMessage( p );