Experiments with word-level data structures.

4 files changed, 440 insertions, 33 deletions

diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index a40673a7..ec733b85 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -539,7 +539,7 @@ void Gia_ManPrintStats( Gia_Man_t * p, Gps_Par_t * pPars )
     Abc_Print( 1, "  %s =%8d", p->pMuxes? "nod" : "and", Gia_ManAndNum(p) );
     SetConsoleTextAttribute( hConsole, 13 ); // magenta
     Abc_Print( 1, "  lev =%5d", Gia_ManLevelNum(p) ); 
-    Abc_Print( 1, " (%.2f)", Gia_ManLevelAve(p) ); 
+    Abc_Print( 1, " (%7.2f)", Gia_ManLevelAve(p) ); 
     SetConsoleTextAttribute( hConsole, 7 ); // normal
     }
 #else
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index d8b8247a..2ea17169 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -2130,18 +2130,22 @@ int Abc_CommandSolve( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern void Rtl_LibOrderWires( Rtl_Lib_t * pLib );
     extern void Rtl_LibOrderCells( Rtl_Lib_t * pLib );
     extern void Rtl_LibBlast( Rtl_Lib_t * pLib );
+    extern void Rtl_LibBlast2( Rtl_Lib_t * pLib );
     extern void Rtl_LibReorderModules( Rtl_Lib_t * pLib );
     extern void Rtl_LibSolve( Rtl_Lib_t * pLib );
     extern void Rtl_LibPreprocess( Rtl_Lib_t * pLib );
 
     Gia_Man_t * pGia = NULL;
     Rtl_Lib_t * pLib = Wlc_AbcGetRtl(pAbc);
-    int c, fPrepro = 0, fVerbose  = 0;
+    int c, fOldBlast = 0, fPrepro = 0, fVerbose  = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "pvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "opvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'o':
+            fOldBlast ^= 1;
+            break;
         case 'p':
             fPrepro ^= 1;
             break;
@@ -2157,9 +2161,14 @@ int Abc_CommandSolve( Abc_Frame_t * pAbc, int argc, char ** argv )
     Rtl_LibPrintStats( pLib );
     //Rtl_LibPrint( NULL, pLib );
     Rtl_LibOrderWires( pLib );
-    Rtl_LibOrderCells( pLib );
 
-    Rtl_LibBlast( pLib );
+    if ( fOldBlast )
+    {
+        Rtl_LibOrderCells( pLib );
+        Rtl_LibBlast( pLib );
+    }
+    else
+        Rtl_LibBlast2( pLib );
     //Rtl_LibReorderModules( pLib );
     //Rtl_LibPrintStats( pLib );
 
@@ -2172,8 +2181,9 @@ int Abc_CommandSolve( Abc_Frame_t * pAbc, int argc, char ** argv )
     Gia_ManStopP( &pGia );
     return 0;
 usage:
-    Abc_Print( -2, "usage: %%solve [-pvh]\n" );
+    Abc_Print( -2, "usage: %%solve [-opvh]\n" );
     Abc_Print( -2, "\t         experiments with word-level networks\n" );
+    Abc_Print( -2, "\t-o     : toggle using old bit-blasting procedure [default = %s]\n", fOldBlast? "yes": "no" );
     Abc_Print( -2, "\t-p     : toggle preprocessing for verification [default = %s]\n", fPrepro? "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");
diff --git a/src/base/wln/wlnRead.c b/src/base/wln/wlnRead.c
index 71b1b98c..b58c2516 100644
--- a/src/base/wln/wlnRead.c
+++ b/src/base/wln/wlnRead.c
@@ -27,12 +27,13 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-#define MAX_LINE 10000
+#define MAX_LINE 1000000
 
-#define MAX_MAP     32
-#define CELL_NUM     8
-#define WIRE_NUM     5
-#define TEMP_NUM     5
+#define MAX_MAP       32
+#define CELL_NUM       8
+#define WIRE_NUM       5
+#define TEMP_NUM       5
+#define CONST_SHIFT   99
 
 //typedef struct Rtl_Lib_t_  Rtl_Lib_t;
 struct Rtl_Lib_t_ 
@@ -58,14 +59,16 @@ struct Rtl_Ntk_t_
     int                   nInputs;   // word-level inputs
     int                   nOutputs;  // word-level outputs
     Vec_Int_t             vWires;    // wires (name{upto,signed,in,out}+width+offset+number)
-    Vec_Int_t             vCells;    // instances ([0]type+[1]name+[2]mod+[3]ins+[4]nattr+[5]nparams+[6]nconns+[6]mark+(attr+params+conns))
+    Vec_Int_t             vCells;    // instances ([0]type+[1]name+[2]mod+[3]ins+[4]nattr+[5]nparams+[6]nconns+[7]mark+(attr+params+conns))
     Vec_Int_t             vConns;    // connection pairs
     Vec_Int_t             vStore;    // storage for cells
     Vec_Int_t             vAttrs;    // attributes
     Rtl_Lib_t *           pLib;      // parent
     Vec_Int_t             vOrder;    // topological order
     Vec_Int_t             vLits;     // bit-level view
+    Vec_Int_t             vDrivers;  // bit-level view
     Vec_Int_t             vBitTemp;  // storage for bits
+    Vec_Int_t             vBitTemp2; // storage for bits
     Gia_Man_t *           pGia;      // derived by bit-blasting
     int                   Slice0;    // first slice
     int                   Slice1;    // last slice
@@ -187,7 +190,9 @@ void Rtl_NtkFree( Rtl_Ntk_t * p )
     ABC_FREE( p->vAttrs.pArray );
     ABC_FREE( p->vOrder.pArray );
     ABC_FREE( p->vLits.pArray );
+    ABC_FREE( p->vDrivers.pArray );
     ABC_FREE( p->vBitTemp.pArray );
+    ABC_FREE( p->vBitTemp2.pArray );
     ABC_FREE( p );
 }
 void Rtl_NtkCountPio( Rtl_Ntk_t * p, int Counts[4] )
@@ -229,8 +234,8 @@ void Rtl_NtkPrintStats( Rtl_Ntk_t * p, int nNameSymbs )
 {
     int Counts[4] = {0};     Rtl_NtkCountPio( p, Counts );
     printf( "%*s : ",        nNameSymbs, Rtl_NtkName(p) );
-    printf( "PI = %3d (%3d)  ", Counts[0], Counts[1] );
-    printf( "PO = %3d (%3d)  ", Counts[2], Counts[3] );
+    printf( "PI = %5d (%5d)  ", Counts[0], Counts[1] );
+    printf( "PO = %5d (%5d)  ", Counts[2], Counts[3] );
     printf( "Wire = %6d   ", Rtl_NtkWireNum(p) );
     printf( "Cell = %6d   ", Rtl_NtkCellNum(p) );
     printf( "Con = %6d",     Rtl_NtkConNum(p) );
@@ -897,22 +902,23 @@ void Rtl_TokenRespace( char * p )
 Vec_Int_t * Rtl_NtkReadFile( char * pFileName, Abc_Nam_t * p )
 {
     Vec_Int_t * vTokens;
-    char * pTemp, Buffer[MAX_LINE]; 
+    char * pTemp, * pBuffer; 
     FILE * pFile = fopen( pFileName, "rb" );
     if ( pFile == NULL )
     {
         printf( "Cannot open file \"%s\" for reading.\n", pFileName );
         return NULL;
     }
+    pBuffer = ABC_ALLOC( char, MAX_LINE );
     Abc_NamStrFindOrAdd( p, "module", NULL );
     assert( Abc_NamObjNumMax(p) == 2 );
     vTokens = Vec_IntAlloc( 1000 );
-    while ( fgets( Buffer, MAX_LINE, pFile ) != NULL )
+    while ( fgets( pBuffer, MAX_LINE, pFile ) != NULL )
     {
-        if ( Buffer[0] == '#' )
+        if ( pBuffer[0] == '#' )
             continue;
-        Rtl_TokenUnspace( Buffer );
-        pTemp = strtok( Buffer, " \t\r\n" );
+        Rtl_TokenUnspace( pBuffer );
+        pTemp = strtok( pBuffer, " \t\r\n" );
         if ( pTemp == NULL )
             continue;
         while ( pTemp )
@@ -923,6 +929,7 @@ Vec_Int_t * Rtl_NtkReadFile( char * pFileName, Abc_Nam_t * p )
         }
         Vec_IntPush( vTokens, -1 );
     }
+    ABC_FREE( pBuffer );
     fclose( pFile );
     return vTokens;
 }
@@ -1406,6 +1413,117 @@ Rtl_Lib_t * Rtl_LibReadFile( char * pFileName, char * pFileSpec )
   SeeAlso     []
 
 ***********************************************************************/
+extern int Rtl_NtkMapSignalRange( Rtl_Ntk_t * p, int Sig, int iCell, int iBit );
+
+int Rtl_NtkMapWireRange( Rtl_Ntk_t * p, int NameId, int Left, int Right, int iCell, int iBit )
+{
+    //char * pName = Rtl_NtkStr( p, NameId );
+    int Wire  = Rtl_WireMapNameToId( p, NameId );
+    int First = Rtl_WireBitStart( p, Wire );
+    int Width = Rtl_WireWidth( p, Wire ), i, k = 0;
+    Left  = Left  == -1 ? Width-1 :  Left;
+    Right = Right == -1 ? 0       : Right;
+    assert ( Right >= 0 && Right <= Left );
+    for ( i = Right; i <= Left; i++ )
+    {
+        assert( Vec_IntEntry(&p->vDrivers, 2*(First+i)) == -4 );
+        Vec_IntWriteEntry(&p->vDrivers, 2*(First+i)+0, iCell );
+        Vec_IntWriteEntry(&p->vDrivers, 2*(First+i)+1, iBit + (i - Right) );
+    }
+    return Left - Right + 1;
+}
+int Rtl_NtkMapSliceRange( Rtl_Ntk_t * p, int * pSlice, int iCell, int iBit )
+{
+    return Rtl_NtkMapWireRange( p, pSlice[0], pSlice[1], pSlice[2], iCell, iBit );
+}
+int Rtl_NtkMapConcatRange( Rtl_Ntk_t * p, int * pConcat, int iCell, int iBit )
+{
+    int i, k = 0;
+    for ( i = 1; i <= pConcat[0]; i++ )
+        k += Rtl_NtkMapSignalRange( p, pConcat[i], iCell, iBit+k );
+    return k;
+}
+int Rtl_NtkMapSignalRange( Rtl_Ntk_t * p, int Sig, int iCell, int iBit )
+{
+    int nBits = ABC_INFINITY;
+    if ( Rtl_SigIsNone(Sig) )
+        nBits = Rtl_NtkMapWireRange( p, Sig >> 2, -1, -1, iCell, iBit );
+    if ( Rtl_SigIsSlice(Sig) )
+        nBits = Rtl_NtkMapSliceRange( p, Vec_IntEntryP(&p->pLib->vSlices, Sig >> 2), iCell, iBit );
+    if ( Rtl_SigIsConcat(Sig) )
+        nBits = Rtl_NtkMapConcatRange( p, Vec_IntEntryP(&p->pLib->vConcats, Sig >> 2), iCell, iBit );
+    if ( Rtl_SigIsConst(Sig) )
+        assert( 0 );
+    return nBits;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+extern void Rtl_NtkCollectSignalInfo( Rtl_Ntk_t * p, int Sig );
+
+void Rtl_NtkCollectWireInfo( Rtl_Ntk_t * p, int NameId, int Left, int Right )
+{
+    int Wire  = Rtl_WireMapNameToId( p, NameId );
+    int First = Rtl_WireBitStart( p, Wire );
+    int Width = Rtl_WireWidth( p, Wire ), i;
+    Left  = Left  == -1 ? Width-1 :  Left;
+    Right = Right == -1 ? 0       : Right;
+    assert ( Right >= 0 && Right <= Left );
+    for ( i = Right; i <= Left; i++ )
+        Vec_IntPush( &p->vBitTemp, First+i );
+}
+void Rtl_NtkCollectConstInfo( Rtl_Ntk_t * p, int * pConst )
+{
+    int i, nLimit = pConst[0];
+    if ( nLimit == -1 )
+        nLimit = 32;
+    for ( i = 0; i < nLimit; i++ )
+        Vec_IntPush( &p->vBitTemp, Abc_InfoHasBit((unsigned *)pConst+1,i)-CONST_SHIFT );
+}
+void Rtl_NtkCollectSliceInfo( Rtl_Ntk_t * p, int * pSlice )
+{
+    Rtl_NtkCollectWireInfo( p, pSlice[0], pSlice[1], pSlice[2] );
+}
+void Rtl_NtkCollectConcatInfo( Rtl_Ntk_t * p, int * pConcat )
+{
+    int i;
+    for ( i = pConcat[0]; i >= 1; i-- )
+        Rtl_NtkCollectSignalInfo( p, pConcat[i] );
+}
+void Rtl_NtkCollectSignalInfo( Rtl_Ntk_t * p, int Sig )
+{
+    if ( Rtl_SigIsNone(Sig) )
+        Rtl_NtkCollectWireInfo( p, Sig >> 2, -1, -1 );
+    else if ( Rtl_SigIsConst(Sig) )
+        Rtl_NtkCollectConstInfo( p, Vec_IntEntryP(&p->pLib->vConsts, Sig >> 2) );
+    else if ( Rtl_SigIsSlice(Sig) )
+        Rtl_NtkCollectSliceInfo( p, Vec_IntEntryP(&p->pLib->vSlices, Sig >> 2) );
+    else if ( Rtl_SigIsConcat(Sig) )
+        Rtl_NtkCollectConcatInfo( p, Vec_IntEntryP(&p->pLib->vConcats, Sig >> 2) );
+    else assert( 0 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 extern void Rtl_NtkCollectSignalRange( Rtl_Ntk_t * p, int Sig );
 
 void Rtl_NtkCollectWireRange( Rtl_Ntk_t * p, int NameId, int Left, int Right )
@@ -1427,7 +1545,6 @@ void Rtl_NtkCollectConstRange( Rtl_Ntk_t * p, int * pConst )
     int i, nLimit = pConst[0];
     if ( nLimit == -1 )
         nLimit = 32;
-    //assert( pConst[0] > 0 );
     for ( i = 0; i < nLimit; i++ )
         Vec_IntPush( &p->vBitTemp, Abc_InfoHasBit((unsigned *)pConst+1,i) );
 }
@@ -1609,6 +1726,20 @@ void Rtl_NtkBlastOperator( Gia_Man_t * pNew, Rtl_Ntk_t * p, int * pCell )
     assert( nBits == Vec_IntSize(vRes) );
     //printf( "Finished blasting cell %s (Value = %d).\n", Rtl_CellNameStr(p, pCell), Vec_IntEntry(vRes, 0) );
 }
+char * Rtl_ShortenName( char * pName, int nSize )
+{
+    static char Buffer[1000];
+    if ( (int)strlen(pName) <= nSize )
+        return pName;
+    Buffer[0] = 0;
+    strcat( Buffer, pName );
+    Buffer[nSize-4] = ' ';
+    Buffer[nSize-3] = '.';
+    Buffer[nSize-2] = '.';
+    Buffer[nSize-1] = '.';
+    Buffer[nSize-0] = 0;
+    return Buffer;
+}
 Gia_Man_t * Rtl_NtkBlast( Rtl_Ntk_t * p )
 {
     Gia_Man_t * pTemp, * pNew = Gia_ManStart( 1000 );
@@ -1642,10 +1773,9 @@ Gia_Man_t * Rtl_NtkBlast( Rtl_Ntk_t * p )
     pNew = Gia_ManCleanup( pTemp = pNew );
     Gia_ManStop( pTemp );
 
-sprintf( Buffer, "temp%d.aig", counter++ );
-//sprintf( Buffer, "temp%d.aig", counter );
+sprintf( Buffer, "old%02d.aig", counter++ );
 Gia_AigerWrite( pNew, Buffer, 0, 0, 0 );
-printf( "Dumpted blasted AIG into file \"%s\" for module \"%s\".\n", Buffer, Rtl_NtkName(p) );
+printf( "Dumped \"%s\" with AIG for module %-20s : ", Buffer, Rtl_ShortenName(Rtl_NtkName(p), 20) );
 Gia_ManPrintStats( pNew, NULL );
     return pNew;
 }
@@ -1668,6 +1798,234 @@ void Rtl_LibBlast( Rtl_Lib_t * pLib )
   SeeAlso     []
 
 ***********************************************************************/
+// -4 unassigned
+// -3 other bit
+// -2 constant
+// -1 primary input
+// 0+ cell
+int Rtl_NtkBlastCons( Rtl_Ntk_t * p )
+{
+    int c, i, iBit0, iBit1, * pCon, * pDri0, * pDri1, nChanges = 0;
+    Rtl_NtkForEachCon( p, pCon, c )
+    {
+        Vec_IntClear( &p->vBitTemp );
+        Rtl_NtkCollectSignalInfo( p, pCon[1] );
+        Vec_IntClearAppend( &p->vBitTemp2, &p->vBitTemp );
+
+        Vec_IntClear( &p->vBitTemp );
+        Rtl_NtkCollectSignalInfo( p, pCon[0] );
+        assert( Vec_IntSize(&p->vBitTemp2) == Vec_IntSize(&p->vBitTemp) );
+
+        Vec_IntForEachEntryTwo( &p->vBitTemp, &p->vBitTemp2, iBit0, iBit1, i )
+        {
+            pDri0 = iBit0 >= 0 ? Vec_IntEntryP(&p->vDrivers, 2*iBit0) : NULL;
+            pDri1 = iBit1 >= 0 ? Vec_IntEntryP(&p->vDrivers, 2*iBit1) : NULL;
+            assert( iBit0 >= 0 || iBit1 >= 0 );
+            if ( iBit0 < 0 )
+            {
+                if ( pDri1[0] == -4 )
+                {
+                    assert( pDri1[1] == -4 );
+                    pDri1[0] = -2;
+                    pDri1[1] = iBit0+CONST_SHIFT;
+                    nChanges++;
+                }
+                continue;
+            }
+            if ( iBit1 < 0 )
+            {
+                if ( pDri0[0] == -4 )
+                {
+                    assert( pDri0[1] == -4 );
+                    pDri0[0] = -2;
+                    pDri0[1] = iBit1+CONST_SHIFT;
+                    nChanges++;
+                }
+                continue;
+            }
+            if ( pDri0[0] == -4 && pDri1[0] != -4 )
+            {
+                assert( pDri0[1] == -4 );
+                pDri0[0] = -3;
+                pDri0[1] = iBit1;
+                nChanges++;
+                continue;
+            }
+            if ( pDri1[0] == -4 && pDri0[0] != -4 )
+            {
+                assert( pDri1[1] == -4 );
+                pDri1[0] = -3;
+                pDri1[1] = iBit0;
+                nChanges++;
+                continue;
+            }
+        }
+    }
+    //printf( "Changes %d\n", nChanges );
+    return nChanges;
+}
+void Rtl_NtkBlastMap( Rtl_Ntk_t * p, int nBits )
+{
+    int i, k, Par, Val, * pCell, iBit = 0, fChange = 1;
+    Vec_IntFill( &p->vDrivers, 2*nBits, -4 );
+    for ( i = 0; i < p->nInputs; i++ )
+    {
+        int First = Rtl_WireBitStart( p, i );
+        int Width = Rtl_WireWidth( p, i );
+        for ( k = 0; k < Width; k++ )
+        {
+            assert( Vec_IntEntry(&p->vDrivers, 2*(First+k)) == -4 );
+            Vec_IntWriteEntry(&p->vDrivers, 2*(First+k)+0, -1 );
+            Vec_IntWriteEntry(&p->vDrivers, 2*(First+k)+1, iBit++ );
+        }
+    }
+    Rtl_NtkForEachCell( p, pCell, i )
+    {
+        int iBit = 0;
+        Rtl_CellForEachOutput( p, pCell, Par, Val, k )
+            iBit += Rtl_NtkMapSignalRange( p, Val, i, iBit );
+    }
+    for ( i = 0; i < 100; i++ )
+        if ( !Rtl_NtkBlastCons(p) )
+            break;
+    if ( i == 100 )
+        printf( "Mapping connections did not succeed after %d iterations.\n", i );
+//    else
+//        printf( "Mapping connections converged after %d iterations.\n", i );
+}
+int Rtl_NtkCollectOrComputeBit( Rtl_Ntk_t * p, int iBit )
+{
+    extern void Rtl_NtkBlast2_rec( Rtl_Ntk_t * p, int iBit, int * pDriver );
+    if ( Vec_IntEntry(&p->vLits, iBit) == -1 )
+    {
+        int * pDriver = Vec_IntEntryP(&p->vDrivers, 2*iBit);
+        assert( pDriver[0] != -4 );
+        Rtl_NtkBlast2_rec( p, iBit, pDriver );
+    }
+    assert( Vec_IntEntry(&p->vLits, iBit) >= 0 );
+    return Vec_IntEntry(&p->vLits, iBit);
+}
+int Rtl_NtkBlast2Spec( Rtl_Ntk_t * p, int * pCell, int iInput )
+{
+    int i, Par, Val, pLits[3] = {-1, -1, -1}, iBit;
+    Rtl_CellForEachInput( p, pCell, Par, Val, i )
+    {
+        Vec_Int_t * vTemp;
+        Vec_IntClear( &p->vBitTemp );
+        Rtl_NtkCollectSignalInfo( p, Val );
+        vTemp = Vec_IntDup( &p->vBitTemp );
+        iBit = Vec_IntEntry( vTemp, i==2 ? 0 : iInput );
+        if ( iBit >= 0 )
+            pLits[i] = Rtl_NtkCollectOrComputeBit( p, iBit );
+        else
+            pLits[i] = iBit+CONST_SHIFT;
+        assert( pLits[i] >= 0 );
+        Vec_IntFree( vTemp );
+    }
+    return Gia_ManHashMux(p->pGia, pLits[2], pLits[1], pLits[0]);
+}
+void Rtl_NtkBlastPrepareInputs( Rtl_Ntk_t * p, int * pCell )
+{
+    int i, k, Par, Val, iBit;
+    Rtl_CellForEachInput( p, pCell, Par, Val, i )
+    {
+        Vec_Int_t * vTemp;
+        Vec_IntClear( &p->vBitTemp );
+        Rtl_NtkCollectSignalInfo( p, Val );
+        vTemp = Vec_IntDup( &p->vBitTemp );
+        Vec_IntForEachEntry( vTemp, iBit, k )
+            if ( iBit >= 0 )
+                Rtl_NtkCollectOrComputeBit( p, iBit );
+        Vec_IntFree( vTemp );
+    }
+}
+void Rtl_NtkBlast2_rec( Rtl_Ntk_t * p, int iBit, int * pDriver )
+{
+    assert( pDriver[0] != -1 );
+    if ( pDriver[0] == -3 )
+    {
+        int * pDriver1 = Vec_IntEntryP( &p->vDrivers, 2*pDriver[1] );
+        if ( Vec_IntEntry(&p->vLits, pDriver[1]) == -1 )
+            Rtl_NtkBlast2_rec( p, pDriver[1], pDriver1 );
+        assert( Vec_IntEntry(&p->vLits, pDriver[1]) >= 0 );
+        Vec_IntWriteEntry( &p->vLits, iBit, Vec_IntEntry(&p->vLits, pDriver[1]) );
+        return;
+    }
+    if ( pDriver[0] == -2 )
+    {
+        Vec_IntWriteEntry( &p->vLits, iBit, pDriver[1] );
+        return;
+    }
+    else
+    {
+        int * pCell = Rtl_NtkCell(p, pDriver[0]);
+        assert( pDriver[0] >= 0 );
+        if ( Rtl_CellModule(pCell) == ABC_OPER_SEL_NMUX ) // special case
+        {
+            int iLit = Rtl_NtkBlast2Spec( p, pCell, pDriver[1] );
+            Vec_IntWriteEntry( &p->vLits, iBit, iLit );
+            return;
+        }
+        Rtl_NtkBlastPrepareInputs( p, pCell );
+        if ( Rtl_CellModule(pCell) >= ABC_INFINITY )
+            Rtl_NtkBlastHierarchy( p->pGia, p, pCell );
+        else if ( Rtl_CellModule(pCell) < ABC_OPER_LAST )
+            Rtl_NtkBlastOperator( p->pGia, p, pCell );
+        else
+            printf( "Cannot blast black box %s in module %s.\n", Rtl_NtkStr(p, Rtl_CellType(pCell)), Rtl_NtkName(p) );
+    }
+}
+Gia_Man_t * Rtl_NtkBlast2( Rtl_Ntk_t * p )
+{
+    Gia_Man_t * pTemp;
+    int i, b, nBits = Rtl_NtkRangeWires( p );
+    char Buffer[100]; static int counter = 0;
+    Vec_IntFill( &p->vLits, nBits, -1 );
+    Rtl_NtkMapWires( p, 0 );
+    Rtl_NtkBlastMap( p, nBits );
+    assert( p->pGia == NULL );
+    p->pGia = Gia_ManStart( 1000 );
+    Rtl_NtkBlastInputs( p->pGia, p );
+    Gia_ManHashAlloc( p->pGia );
+    for ( i = 0; i < p->nOutputs; i++ )
+    {
+        int First = Rtl_WireBitStart( p, p->nInputs + i );
+        int Width = Rtl_WireWidth( p, p->nInputs + i );
+        for ( b = 0; b < Width; b++ )
+            Rtl_NtkCollectOrComputeBit( p, First+b );
+    }
+    Gia_ManHashStop( p->pGia );
+    Rtl_NtkBlastOutputs( p->pGia, p );
+    Rtl_NtkMapWires( p, 1 );
+    p->pGia = Gia_ManCleanup( pTemp = p->pGia );
+    Gia_ManStop( pTemp );
+
+sprintf( Buffer, "new%02d.aig", counter++ );
+Gia_AigerWrite( p->pGia, Buffer, 0, 0, 0 );
+printf( "Dumped \"%s\" with AIG for module %-20s : ", Buffer, Rtl_ShortenName(Rtl_NtkName(p), 20) );
+Gia_ManPrintStats( p->pGia, NULL );
+    return p->pGia;
+}
+void Rtl_LibBlast2( Rtl_Lib_t * pLib )
+{
+    Rtl_Ntk_t * p; int i;
+    Vec_PtrForEachEntry( Rtl_Ntk_t *, pLib->vNtks, p, i )
+        if ( p->pGia == NULL )
+            p->pGia = Rtl_NtkBlast2( p );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Rtl_LibPreprocess( Rtl_Lib_t * pLib )
 {
     abctime clk = Abc_Clock(); 
@@ -1705,21 +2063,31 @@ finish:
     Vec_PtrForEachEntry( Rtl_Ntk_t *, pLib->vNtks, p, i )
         if ( p != p1 && p != p2 )
             Gia_ManStopP( &p->pGia );
-    Rtl_LibBlast( pLib );
+    //Rtl_LibBlast( pLib );
+    Rtl_LibBlast2( pLib );
 }
 void Rtl_LibSolve( Rtl_Lib_t * pLib )
 {
+    extern Gia_Man_t * Cec4_ManSimulateTest3( Gia_Man_t * p, int nBTLimit, int fVerbose );
     abctime clk = Abc_Clock(); int Status;
     Rtl_Ntk_t * pTop = Rtl_LibTop( pLib );
-    Gia_Man_t * pCopy = Gia_ManDup( pTop->pGia );
-    Gia_ManInvertPos( pCopy );
-    Gia_ManAppendCo( pCopy, 0 );
-    Status = Cec_ManVerifySimple( pCopy );
-    Gia_ManStop( pCopy );
-    if ( Status == 1 )
-        printf( "Verification problem solved!  " );
+    Gia_Man_t * pSwp = Cec4_ManSimulateTest3( pTop->pGia, 1000000, 0 );
+    int RetValue = Gia_ManAndNum(pSwp) == 0;
+    Gia_ManStop( pSwp );
+    if ( RetValue )
+        printf( "Verification problem solved after SAT sweeping!  " );
     else
-        printf( "Verification problem is NOT solved!  " );
+    {
+        Gia_Man_t * pCopy = Gia_ManDup( pTop->pGia );
+        Gia_ManInvertPos( pCopy );
+        Gia_ManAppendCo( pCopy, 0 );
+        Status = Cec_ManVerifySimple( pCopy );
+        Gia_ManStop( pCopy );
+        if ( Status == 1 )
+            printf( "Verification problem solved after CEC!  " );
+        else
+            printf( "Verification problem is NOT solved!  " );
+    }
     Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
 }
 
diff --git a/src/base/wln/wlnRtl.c b/src/base/wln/wlnRtl.c
index 89680bbd..df53ebe0 100644
--- a/src/base/wln/wlnRtl.c
+++ b/src/base/wln/wlnRtl.c
@@ -49,6 +49,34 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
+#define MAX_LINE 1000000
+
+void Rtl_NtkCleanFile( char * pFileName )
+{
+    char * pBuffer, * pFileName2 = "_temp__.rtlil"; 
+    FILE * pFile = fopen( pFileName, "rb" );
+    FILE * pFile2;
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open file \"%s\" for reading.\n", pFileName );
+        return;
+    }
+    pFile2 = fopen( pFileName2, "wb" );
+    if ( pFile2 == NULL )
+    {
+        fclose( pFile );
+        printf( "Cannot open file \"%s\" for writing.\n", pFileName2 );
+        return;
+    }
+    pBuffer = ABC_ALLOC( char, MAX_LINE );
+    while ( fgets( pBuffer, MAX_LINE, pFile ) != NULL )
+        if ( !strstr(pBuffer, "attribute \\src") )
+            fputs( pBuffer, pFile2 );
+    ABC_FREE( pBuffer );
+    fclose( pFile );
+    fclose( pFile2 );
+}
+
 char * Wln_GetYosysName()
 {
     char * pYosysName = NULL;
@@ -105,7 +133,8 @@ Rtl_Lib_t * Wln_ReadSystemVerilog( char * pFileName, char * pTopModule, int fCol
         printf( "Dumped the design into file \"%s\".\n", pFileTemp );
         return NULL;
     }
-    //unlink( pFileTemp );
+    Rtl_NtkCleanFile( pFileTemp );
+    unlink( pFileTemp );
     return pNtk;
 }
 Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pTopModule, int fSkipStrash, int fInvert, int fTechMap, int fVerbose )