Experiments with word-level data structures.

5 files changed, 667 insertions, 10 deletions

diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 4f094b48..1164e16b 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -5221,6 +5221,144 @@ Gia_Man_t * Gia_ManDupAddPis( Gia_Man_t * p, int nMulti )
     return pNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Wec_t ** Gia_ManDupUifBuildMap( Gia_Man_t * p )
+{
+    Vec_Wec_t ** pvMap = ABC_ALLOC( Vec_Wec_t *, 2 ); 
+    Vec_Int_t * vBufs = Vec_IntAlloc( p->nBufs ); 
+    Gia_Obj_t * pObj; int i, Item, j, k = 0;
+    pvMap[0] = Vec_WecAlloc(10);
+    pvMap[1] = Vec_WecAlloc(10);
+    Gia_ManForEachObj1( p, pObj, i )
+        if ( Gia_ObjIsBuf(pObj) )
+            Vec_IntPush( vBufs, i );
+    assert( p->nBufs == Vec_IntSize(vBufs) );
+    Vec_IntForEachEntry( p->vBarBufs, Item, i )
+    {
+        Vec_Int_t * vVec = Vec_WecPushLevel(pvMap[Item&1]);
+        for ( j = 0; j < (Item >> 16); j++ )
+            Vec_IntPush( vVec, Vec_IntEntry(vBufs, k++) );
+    }
+    Vec_IntFree( vBufs );
+    assert( p->nBufs == k );
+    assert( Vec_WecSize(pvMap[0]) == Vec_WecSize(pvMap[1]) );
+    return pvMap;
+}
+int Gia_ManDupUifConstrOne( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Int_t * vVec0, Vec_Int_t * vVec1 )
+{
+    Vec_Int_t * vTemp = Vec_IntAlloc( Vec_IntSize(vVec0) );
+    int i, o0, o1, iRes;
+    Vec_IntForEachEntryTwo( vVec0, vVec1, o0, o1, i )
+        Vec_IntPush( vTemp, Gia_ManHashXor(pNew, Gia_ManObj(p, o0)->Value, Abc_LitNot(Gia_ManObj(p, o1)->Value)) );
+    iRes = Gia_ManHashAndMulti( pNew, vTemp );
+    Vec_IntFree( vTemp );
+    return iRes;
+}
+int Gia_ManDupUifConstr( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Wec_t ** pvMap )
+{
+    int i, k, iUif = 1;
+    assert( Vec_WecSize(pvMap[0]) == Vec_WecSize(pvMap[1]) );
+    for ( i = 0;     i < Vec_WecSize(pvMap[0]); i++ )
+    for ( k = i + 1; k < Vec_WecSize(pvMap[0]); k++ )
+    {
+        int iCond1 = Gia_ManDupUifConstrOne( pNew, p, Vec_WecEntry(pvMap[0], i), Vec_WecEntry(pvMap[0], k) );
+        int iCond2 = Gia_ManDupUifConstrOne( pNew, p, Vec_WecEntry(pvMap[1], i), Vec_WecEntry(pvMap[1], k) );
+        int iRes = Gia_ManHashOr( pNew, Abc_LitNot(iCond1), iCond2 );
+        iUif = Gia_ManHashAnd( pNew, iUif, iRes );
+    }
+    return iUif;
+}
+Gia_Man_t * Gia_ManDupUif( Gia_Man_t * p )
+{
+    Vec_Wec_t ** pvMap = Gia_ManDupUifBuildMap( p );
+    Gia_Man_t * pNew, * pTemp; Gia_Obj_t * pObj;
+    int i, iUif = 0;
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManHashAlloc( pNew );
+    Gia_ManForEachObj1( p, pObj, i )
+    {
+        if ( Gia_ObjIsBuf(pObj) )
+            pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
+        else if ( Gia_ObjIsAnd(pObj) )
+            pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        else if ( Gia_ObjIsCi(pObj) )
+            pObj->Value = Gia_ManAppendCi( pNew );
+        else if ( Gia_ObjIsCo(pObj) )
+            pObj->Value = Gia_ObjFanin0Copy(pObj);
+    }
+    iUif = Gia_ManDupUifConstr( pNew, p, pvMap );
+    Gia_ManForEachCo( p, pObj, i )
+        Gia_ManAppendCo( pNew, Gia_ManAppendAnd(pNew, pObj->Value, iUif) );
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    Vec_WecFree( pvMap[0] );
+    Vec_WecFree( pvMap[1] );
+    ABC_FREE( pvMap );
+    if ( p->vBarBufs )
+        pNew->vBarBufs = Vec_IntDup( p->vBarBufs );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Gia_ManDupBlackBoxBuildMap( Gia_Man_t * p )
+{
+    Vec_Int_t * vMap = Vec_IntAlloc( p->nBufs ); int i, Item;
+    Vec_IntForEachEntry( p->vBarBufs, Item, i )
+        Vec_IntFillExtra( vMap, Vec_IntSize(vMap) + (Item >> 16), Item & 1 );
+    assert( p->nBufs == Vec_IntSize(vMap) );
+    return vMap;
+}
+Gia_Man_t * Gia_ManDupBlackBox( Gia_Man_t * p )
+{
+    Vec_Int_t * vMap = Gia_ManDupBlackBoxBuildMap( p );
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj;
+    int i, k = 0;
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManHashAlloc( pNew );
+    Gia_ManForEachObj1( p, pObj, i )
+    {
+        if ( Gia_ObjIsBuf(pObj) )
+            pObj->Value = Vec_IntEntry(vMap, k++) ? Gia_ManAppendCi(pNew) : Gia_ObjFanin0Copy(pObj); // out/in
+        else if ( Gia_ObjIsAnd(pObj) )
+            pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        else if ( Gia_ObjIsCi(pObj) )
+            pObj->Value = Gia_ManAppendCi( pNew );
+        else if ( Gia_ObjIsCo(pObj) )
+            pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    }
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    Vec_IntFree( vMap );
+    return pNew;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaSimBase.c b/src/aig/gia/giaSimBase.c
index c31064fe..c8808532 100644
--- a/src/aig/gia/giaSimBase.c
+++ b/src/aig/gia/giaSimBase.c
@@ -750,7 +750,7 @@ void Gia_ManSimProfile( Gia_Man_t * pGia )
     Vec_Wrd_t * vSims = Gia_ManSimPatSim( pGia );
     int nWords = Vec_WrdSize(vSims) / Gia_ManObjNum(pGia);
     int nC0s = 0, nC1s = 0, nUnique = Gia_ManSimPatHashPatterns( pGia, nWords, vSims, &nC0s, &nC1s );
-    printf( "Simulating %d patterns leads to %d unique objects (%.2f %% out of %d), Const0 = %d. Const1 = %d.\n", 
+    printf( "Simulating %d patterns leads to %d unique objects (%.2f %% out of %d). Const0 = %d. Const1 = %d.\n", 
         64*nWords, nUnique, 100.0*nUnique/Gia_ManCandNum(pGia), Gia_ManCandNum(pGia), nC0s, nC1s );
     Vec_WrdFree( vSims );
 }
@@ -2700,6 +2700,77 @@ Vec_Ptr_t * Gia_ManPtrWrdReadBin( char * pFileName, int fVerbose )
     return p;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManCompareSims( Gia_Man_t * pHie, Gia_Man_t * pFlat, int nWords, int fVerbose )
+{
+    abctime clk = Abc_Clock();
+    Vec_Wrd_t * vSims  = pFlat->vSimsPi = pHie->vSimsPi = Vec_WrdStartRandom( Gia_ManCiNum(pFlat) * nWords );
+    Vec_Wrd_t * vSims0 = Gia_ManSimPatSim( pFlat );
+    Vec_Wrd_t * vSims1 = Gia_ManSimPatSim( pHie );
+    Gia_Obj_t * pObj; int * pSpot, * pSpot2, i, nC0s = 0, nC1s = 0, nUnique = 0, nFound[3] = {0}, nBoundary = 0, nMatched = 0;
+    Vec_Mem_t * vStore = Vec_MemAlloc( nWords, 12 ); // 2^12 N-word entries per page
+    pFlat->vSimsPi = NULL;
+    pHie->vSimsPi = NULL;
+    Vec_WrdFree( vSims );
+
+    printf( "Comparing two AIGs using %d simulation words.\n", nWords );
+    printf( "Hierarchical: " ); Gia_ManPrintStats( pHie, NULL );
+    printf( "Flat:         " ); Gia_ManPrintStats( pFlat, NULL );
+
+    Vec_MemHashAlloc( vStore, 1 << 12 );
+    Gia_ManForEachCand( pFlat, pObj, i )
+    {
+        word * pSim = Vec_WrdEntryP(vSims0, i*nWords);
+        nC0s += Abc_TtIsConst0(pSim, nWords);
+        nC1s += Abc_TtIsConst1(pSim, nWords);
+        Vec_MemHashInsert( vStore, pSim );
+    }
+    nUnique = Vec_MemEntryNum( vStore );
+    printf( "Simulating %d patterns through the second (flat) AIG leads to %d unique objects (%.2f %% out of %d). Const0 = %d. Const1 = %d.\n", 
+        64*nWords, nUnique, 100.0*nUnique/Gia_ManCandNum(pFlat), Gia_ManCandNum(pFlat), nC0s, nC1s );
+
+    assert( Gia_ManCiNum(pFlat) == Gia_ManCiNum(pHie) );
+    Gia_ManForEachCand( pHie, pObj, i ) 
+    {
+        word * pSim = Vec_WrdEntryP(vSims1, i*nWords);
+        pSpot  = Vec_MemHashLookup( vStore, pSim );
+        Abc_TtNot( pSim, nWords );
+        pSpot2 = Vec_MemHashLookup( vStore, pSim );
+        Abc_TtNot( pSim, nWords );
+        nBoundary += Gia_ObjIsBuf(pObj);
+        if ( *pSpot != -1 || *pSpot2 != -1 )
+        {
+            nMatched++;
+            continue;
+        }
+        //Extra_PrintBinary( stdout, (unsigned *)pSim, 64*nWords ); printf("\n");
+        nFound[1] += Gia_ObjIsBuf(pObj);
+        nFound[2]++;
+        //if ( Gia_ObjIsBuf(pObj) )
+        //    printf( "%d(%d) ", i, nBoundary-1 );
+    }
+    Vec_MemHashFree( vStore );
+    Vec_MemFree( vStore );
+    Vec_WrdFree( vSims0 );
+    Vec_WrdFree( vSims1 );
+
+    printf( "The first (hierarchical) AIG has %d (%.2f %%) matches, %d (%.2f %%) mismatches, including %d (%.2f %%) on the boundary.  ", 
+        nMatched,  100.0*nMatched /Abc_MaxInt(1, Gia_ManCandNum(pHie)), 
+        nFound[2], 100.0*nFound[2]/Abc_MaxInt(1, Gia_ManCandNum(pHie)), 
+        nFound[1], 100.0*nFound[1]/Abc_MaxInt(1, nBoundary) );
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 34f15cf2..e54b831d 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -519,6 +519,8 @@ static int Abc_CommandAbc9Iso                ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9IsoNpn             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9IsoSt              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Compare            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9RevEng             ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Uif                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9CexInfo            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Cycle              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Cone               ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -1263,6 +1265,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&isonpn",       Abc_CommandAbc9IsoNpn,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&isost",        Abc_CommandAbc9IsoSt,        0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&compare",      Abc_CommandAbc9Compare,      0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&reveng",       Abc_CommandAbc9RevEng,       0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&uif",          Abc_CommandAbc9Uif,          0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&cexinfo",      Abc_CommandAbc9CexInfo,      0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&cycle",        Abc_CommandAbc9Cycle,        0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&cone",         Abc_CommandAbc9Cone,         0 );
@@ -43724,6 +43728,144 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc9RevEng( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern void Gia_ManCompareSims( Gia_Man_t * pHie, Gia_Man_t * pFlat, int nWords, int fVerbose );
+    Gia_Man_t * pGia0, * pGia1;
+    char ** pArgvNew; int nArgcNew;
+    int c, nWords = 4, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Wvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'W':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nWords = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nWords < 0 )
+                goto usage;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9RevEng(): There is no AIG.\n" );
+        return 1;
+    }
+    pArgvNew = argv + globalUtilOptind;
+    nArgcNew = argc - globalUtilOptind;
+    if ( nArgcNew != 1 )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9RevEng(): This command expects one AIG file name on the command line.\n" );
+        return 1;
+    }
+    pGia0 = pAbc->pGia;
+    pGia1 = Gia_AigerRead( pArgvNew[0], 0, 0, 0 );
+    if ( pGia0 == NULL || pGia1 == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9RevEng(): Reading input files did not work.\n" );
+        return 1;
+    }
+    Gia_ManCompareSims( pGia0, pGia1, nWords, fVerbose );
+    Gia_ManStop( pGia1 );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &reveng [-W num] [-vh] <file>\n" );
+    Abc_Print( -2, "\t         compares two AIGs for structural similarity\n" );
+    Abc_Print( -2, "\t         the current AIG is expected to contain some hierarchy\n" );
+    Abc_Print( -2, "\t         the given AIG from <file> is expected to be flat\n" );
+    Abc_Print( -2, "\t-W num : the number of 64-bit words of simulation info [default = %d]\n", nWords );
+    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;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9Uif( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Gia_Man_t * Gia_ManDupUif( Gia_Man_t * p );
+    extern Gia_Man_t * Gia_ManDupBlackBox( Gia_Man_t * p );
+    Gia_Man_t * pNew = NULL, * pTemp = NULL;
+    int c, fBlackBox = 0, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "bvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'b':
+            fBlackBox ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Uif(): There is no AIG.\n" );
+        return 1;
+    }
+    if ( pAbc->pGia->vBarBufs == NULL || Vec_IntSize(pAbc->pGia->vBarBufs) == 0 )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Uif(): Hierarchy is not defined.\n" );
+        return 1;
+    }
+    pNew = Gia_ManDupUif( pAbc->pGia );
+    if ( fBlackBox )
+    {
+        pNew = Gia_ManDupBlackBox( pTemp = pNew );
+        Gia_ManStop( pTemp );
+    }
+    Abc_FrameUpdateGia( pAbc, pNew );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &uif [-bvh]\n" );
+    Abc_Print( -2, "\t         eagerly adds UIF constraints when hierarchy is present\n" );
+    Abc_Print( -2, "\t-b     : toggle blackboxing while adding constraints [default = %s]\n", fBlackBox? "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;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAbc9CexInfo( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern void Bmc_CexTest( Gia_Man_t * p, Abc_Cex_t * pCex, int fVerbose );
diff --git a/src/base/wln/wlnCom.c b/src/base/wln/wlnCom.c
index a010c7c2..dcf12229 100644
--- a/src/base/wln/wlnCom.c
+++ b/src/base/wln/wlnCom.c
@@ -28,6 +28,9 @@ ABC_NAMESPACE_IMPL_START
 ////////////////////////////////////////////////////////////////////////
 
 static int  Abc_CommandYosys      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int  Abc_CommandGraft      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int  Abc_CommandHierarchy  ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int  Abc_CommandCollapse   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandSolve      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandPrint      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
@@ -53,7 +56,10 @@ static inline void        Wln_AbcUpdateRtl( Abc_Frame_t * pAbc, Rtl_Lib_t * pLib
 void Wln_Init( Abc_Frame_t * pAbc )
 {
     Cmd_CommandAdd( pAbc, "Word level", "%yosys",       Abc_CommandYosys,      0 );
-    Cmd_CommandAdd( pAbc, "Word level", "%solve",       Abc_CommandSolve,      0 );
+    Cmd_CommandAdd( pAbc, "Word level", "%graft",       Abc_CommandGraft,      0 );
+    Cmd_CommandAdd( pAbc, "Word level", "%hierarchy",   Abc_CommandHierarchy,   0 );
+    Cmd_CommandAdd( pAbc, "Word level", "%collapse",    Abc_CommandCollapse,   0 );
+    //Cmd_CommandAdd( pAbc, "Word level", "%solve",       Abc_CommandSolve,      0 );
     Cmd_CommandAdd( pAbc, "Word level", "%print",       Abc_CommandPrint,      0 );
 }
 
@@ -213,6 +219,170 @@ usage:
   SeeAlso     []
 
 ******************************************************************************/
+int Abc_CommandGraft( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern void Wln_LibGraftOne( Rtl_Lib_t * p, char * pModule1, char * pModule2, int fVerbose );
+    Rtl_Lib_t * pLib = Wln_AbcGetRtl(pAbc);
+    char ** pArgvNew; int nArgcNew;
+    int c,  fVerbose  = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pLib == NULL )
+    {
+        printf( "The design is not entered.\n" );
+        return 1;
+    }
+    pArgvNew = argv + globalUtilOptind;
+    nArgcNew = argc - globalUtilOptind;
+    if ( nArgcNew != 2 )
+    {
+        Abc_Print( -1, "Abc_CommandGraft(): This command expects one AIG file name on the command line.\n" );
+        return 1;
+    }
+    Wln_LibGraftOne( pLib, pArgvNew[0], pArgvNew[1], fVerbose );
+    return 0;
+usage:
+    Abc_Print( -2, "usage: %%graft [-vh] <module1_name> <module2_name>\n" );
+    Abc_Print( -2, "\t         replace instances of module1 by those of module2\n" );
+    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;
+}
+
+/**Function********************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int Abc_CommandHierarchy( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern void Wln_LibMarkHierarchy( Rtl_Lib_t * p, char ** ppModule, int nModules, int fVerbose );
+    Rtl_Lib_t * pLib = Wln_AbcGetRtl(pAbc);
+    char ** pArgvNew; int nArgcNew;
+    int c,  fVerbose  = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pLib == NULL )
+    {
+        printf( "The design is not entered.\n" );
+        return 1;
+    }
+    pArgvNew = argv + globalUtilOptind;
+    nArgcNew = argc - globalUtilOptind;
+    if ( nArgcNew < 1 )
+    {
+        Abc_Print( -1, "Abc_CommandHierarchy(): This command expects one AIG file name on the command line.\n" );
+        return 1;
+    }
+    Wln_LibMarkHierarchy( pLib, pArgvNew, nArgcNew, fVerbose );
+    return 0;
+usage:
+    Abc_Print( -2, "usage: %%hierarchy [-vh] <module_name>\n" );
+    Abc_Print( -2, "\t         marks the module whose instances may later be treated as black boxes\n" );
+    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;
+}
+
+/**Function********************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Gia_Man_t * Rtl_LibCollapse( Rtl_Lib_t * p, char * pTopModule, int fVerbose );
+    Gia_Man_t * pNew = NULL;
+    Rtl_Lib_t * pLib = Wln_AbcGetRtl(pAbc);
+    char * pTopModule = NULL;
+    int c,  fVerbose  = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Tvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'T':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-T\" should be followed by a file name.\n" );
+                goto usage;
+            }
+            pTopModule = argv[globalUtilOptind];
+            globalUtilOptind++;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pLib == NULL )
+    {
+        printf( "The design is not entered.\n" );
+        return 1;
+    }
+    pNew = Rtl_LibCollapse( pLib, pTopModule, fVerbose );
+    Abc_FrameUpdateGia( pAbc, pNew );
+    return 0;
+usage:
+    Abc_Print( -2, "usage: %%collapse [-T <module>] [-vh] <file_name>\n" );
+    Abc_Print( -2, "\t         collapse hierarchical design into an AIG\n" );
+    Abc_Print( -2, "\t-T     : specify the top module of the design [default = none]\n" );
+    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;
+}
+
+/**Function********************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
 int Abc_CommandPrint( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern void Rtl_LibPrintStats( Rtl_Lib_t * p );
diff --git a/src/base/wln/wlnRead.c b/src/base/wln/wlnRead.c
index 43003075..8cd4af0c 100644
--- a/src/base/wln/wlnRead.c
+++ b/src/base/wln/wlnRead.c
@@ -157,6 +157,7 @@ static inline int         Rtl_SigIsConcat( int s )                         { ret
 
 extern Gia_Man_t * Cec4_ManSimulateTest3( Gia_Man_t * p, int nBTLimit, int fVerbose );
 extern int         Abc_NtkFromGiaCollapse( Gia_Man_t * pGia );
+extern int         Wln_ReadFindToken( char * pToken, Abc_Nam_t * p );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -1434,6 +1435,18 @@ void Rtl_LibReorderModules_rec( Rtl_Ntk_t * p, Vec_Ptr_t * vNew )
     p->iCopy = Vec_PtrSize(vNew);
     Vec_PtrPush( vNew, p );
 }
+int Rtl_LibCountInsts( Rtl_Lib_t * p, Rtl_Ntk_t * pOne )
+{
+    Rtl_Ntk_t * pNtk; int n, i, * pCell, Count = 0;
+    Vec_PtrForEachEntry( Rtl_Ntk_t *, p->vNtks, pNtk, n )
+        Rtl_NtkForEachCell( pNtk, pCell, i )
+        {
+            Rtl_Ntk_t * pMod = Rtl_CellNtk( pNtk, pCell );
+            if ( pMod && pMod == pOne ) 
+                Count++;
+        }
+    return Count;
+}
 void Rtl_NtkUpdateBoxes( Rtl_Ntk_t * p )
 {
     int i, * pCell;
@@ -1755,7 +1768,7 @@ void Rtl_NtkBlastHierarchy( Gia_Man_t * pNew, Rtl_Ntk_t * p, int * pCell )
     extern void Gia_ManDupRebuild( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Int_t * vLits, int fBufs );
     extern int Gia_ManFindFirst( Rtl_Ntk_t * p, int * pnOuts );
     Rtl_Ntk_t * pModel = Rtl_NtkModule( p, Rtl_CellModule(pCell)-ABC_INFINITY );
-    int nOuts1, iFirst1 = Gia_ManFindFirst( pModel, &nOuts1 );
+    int nIns = 0, nOuts = 0, nOuts1, iFirst1 = Gia_ManFindFirst( pModel, &nOuts1 );
     int k, Par, Val, nBits = 0;
     //printf( "Blasting %s -> %s...\n", Rtl_NtkName(p), Rtl_NtkName(pModel) );
     Vec_IntClear( &p->vBitTemp );
@@ -1766,19 +1779,22 @@ void Rtl_NtkBlastHierarchy( Gia_Man_t * pNew, Rtl_Ntk_t * p, int * pCell )
     assert( pModel->pGia );
     if ( pModel->fRoot )
     {
+        nIns = Vec_IntSize(&p->vBitTemp);
         Vec_IntForEachEntry( &p->vBitTemp, Val, k )
-            Vec_IntWriteEntry( &p->vBitTemp, k, (k >= iFirst1 && k < iFirst1 + nOuts1) ? Gia_ManAppendBuf(pNew, Val) : Val );
-        Vec_IntPush( pNew->vBarBufs, Abc_Var2Lit(pModel->NameId, 0) );
+            //Vec_IntWriteEntry( &p->vBitTemp, k, (k >= iFirst1 && k < iFirst1 + nOuts1) ? Gia_ManAppendBuf(pNew, Val) : Val );
+            Vec_IntWriteEntry( &p->vBitTemp, k, Gia_ManAppendBuf(pNew, Val) );
+        Vec_IntPush( pNew->vBarBufs, (nIns << 16) | Abc_Var2Lit(pModel->NameId, 0) );
     }
     Gia_ManDupRebuild( pNew, pModel->pGia, &p->vBitTemp, !pModel->fRoot );
     if ( !pModel->fRoot )
         Vec_IntAppend( pNew->vBarBufs, pModel->pGia->vBarBufs );
     if ( pModel->fRoot )
     {
+        nOuts = Vec_IntSize(&p->vBitTemp);
         Vec_IntForEachEntry( &p->vBitTemp, Val, k )
             Vec_IntWriteEntry( &p->vBitTemp, k, Gia_ManAppendBuf(pNew, Val) );
-        Vec_IntPush( pNew->vBarBufs, Abc_Var2Lit(pModel->NameId, 1) );
-        printf( "Added %d and %d output buffers for module %s.\n", nOuts1, Vec_IntSize(&p->vBitTemp), Rtl_NtkName(pModel) );
+        Vec_IntPush( pNew->vBarBufs, (nOuts << 16) | Abc_Var2Lit(pModel->NameId, 1) );
+        printf( "Added %d input buffers and %d output buffers for module %s.\n", nIns, nOuts, Rtl_NtkName(pModel) );
     }
     Rtl_CellForEachOutput( p, pCell, Par, Val, k )
         nBits += Rtl_NtkInsertSignalRange( p, Val, Vec_IntArray(&p->vBitTemp)+nBits, Vec_IntSize(&p->vBitTemp)-nBits );
@@ -1847,7 +1863,7 @@ void Rtl_NtkPrintBufs( Rtl_Ntk_t * p, Vec_Int_t * vBufs )
     if ( Vec_IntSize(vBufs) )
         printf( "Found %d buffers:  ", p->pGia->nBufs );
     Vec_IntForEachEntry( vBufs, Lit, i )
-        printf( "%s (%c)  ", Rtl_LibStr(p->pLib, Abc_Lit2Var(Lit)), Abc_LitIsCompl(Lit)? 'o' : 'i' );
+        printf( "%s (%c%d)  ", Rtl_LibStr(p->pLib, Abc_Lit2Var(Lit&0xFFFF)), Abc_LitIsCompl(Lit)? 'o' : 'i', Lit >> 16 );
     if ( Vec_IntSize(vBufs) )
         printf( "\n" );
 }
@@ -2145,11 +2161,11 @@ void Rtl_LibBlast2( Rtl_Lib_t * pLib, Vec_Int_t * vRoots, int fInv )
     if ( vRoots )
     {
         Vec_PtrForEachEntry( Rtl_Ntk_t *, pLib->vNtks, pNtk, i )
-            pNtk->iCopy = -2, pNtk->fRoot = 0;
+            pNtk->iCopy = -2;//, pNtk->fRoot = 0;
         Vec_IntForEachEntry( vRoots, iNtk, i )
         {
             Rtl_Ntk_t * pNtk = Rtl_LibNtk(pLib, iNtk);
-            pNtk->fRoot = fInv;
+            //pNtk->fRoot = fInv;
             Rtl_LibMark_rec( pNtk );
         }
     }
@@ -2259,6 +2275,9 @@ void Rtl_LibSolve( Rtl_Lib_t * pLib, void * pNtk )
     Gia_Man_t * pGia2 = Gia_ManReduceBuffers( pLib, pTop->pGia );
     Gia_Man_t * pSwp  = Cec4_ManSimulateTest3( pGia2, 1000000, 0 );
     int RetValue = Gia_ManAndNum(pSwp);
+    char * pFileName = "miter_to_solve.aig";
+    printf( "Dumped the miter into file \"%s\".\n", pFileName );
+    Gia_AigerWrite( pGia2, pFileName, 0, 0, 0 );
     Gia_ManStop( pSwp );
     Gia_ManStop( pGia2 );
     if ( RetValue == 0 )
@@ -2423,6 +2442,7 @@ void Wln_SolveInverse( Rtl_Lib_t * p, int iNtk1, int iNtk2 )
         Gia_Man_t * pGia2 = Gia_ManDupNoBuf( pGia );
         printf( "Dumping inverse miter into file \"%s\".\n", pFileName );
         Gia_AigerWrite( pGia2, pFileName, 0, 0, 0 );
+        printf( "Dumped the miter into file \"%s\".\n", pFileName );
         if ( Abc_NtkFromGiaCollapse( pGia2 ) )
             Abc_Print( 1, "Networks are equivalent after collapsing.  " );
         else
@@ -2534,6 +2554,122 @@ void Wln_SolveWithGuidance( char * pFileName, Rtl_Lib_t * p )
     Vec_IntFree( vRoots );
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Rtl_LibReturnNtk( Rtl_Lib_t * p, char * pModule )
+{
+    int NameId = Wln_ReadFindToken( pModule, p->pManName );
+    int iNtk   = NameId ? Rtl_LibFindModule( p, NameId )  : -1;
+    if ( iNtk == -1 )
+    {
+        printf( "Cannot find module \"%s\" in the current design.\n", pModule );
+        return -1;
+    }
+    return iNtk;
+}
+Gia_Man_t * Rtl_LibCollapse( Rtl_Lib_t * p, char * pTopModule, int fVerbose )
+{
+    Gia_Man_t * pGia = NULL;
+    int NameId = Wln_ReadFindToken( pTopModule, p->pManName );
+    int iNtk   = NameId ? Rtl_LibFindModule( p, NameId ) : -1;
+    if ( iNtk == -1 )
+    {
+        printf( "Cannot find top module \"%s\".\n", pTopModule );
+        return NULL;
+    }
+    else
+    {
+        abctime clk = Abc_Clock(); 
+        Rtl_Ntk_t * pTop = Rtl_LibNtk(p, iNtk);
+        Vec_Int_t * vRoots = Vec_IntAlloc( 1 );
+        Vec_IntPush( vRoots, iNtk );
+        Rtl_LibBlast2( p, vRoots, 1 );
+        pGia = Gia_ManDup( pTop->pGia );
+        if ( pTop->pGia->vBarBufs )
+            pGia->vBarBufs = Vec_IntDup( pTop->pGia->vBarBufs );
+        printf( "Finished computing global AIG for the top module \"%s\".  ", Rtl_NtkStr(pTop, NameId) );
+        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+        Rtl_NtkPrintBufs( pTop, pGia->vBarBufs );
+        Rtl_LibBlastClean( p );
+        Vec_IntFree( vRoots );
+    }
+    return pGia;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Wln_LibGraftOne( Rtl_Lib_t * p, char * pModule1, char * pModule2, int fVerbose )
+{
+    int Name1 = Wln_ReadFindToken( pModule1, p->pManName );
+    int Name2 = Wln_ReadFindToken( pModule2, p->pManName );
+    int iNtk  = Rtl_LibFindTwoModules( p, Name1, Name2 ); 
+    if ( iNtk == -1 )
+    {
+        printf( "Cannot find networks \"%s\" and \"%s\" in the design.\n", Rtl_LibStr(p, Name1), Rtl_LibStr(p, Name2) ); 
+        return;
+    }
+    else
+    {
+        int iNtk1 = iNtk >> 16;
+        int iNtk2 = iNtk & 0xFFFF;
+        Rtl_Ntk_t * pNtk1 = Rtl_LibNtk(p, iNtk1);
+        Rtl_Ntk_t * pNtk2 = Rtl_LibNtk(p, iNtk2);
+        assert( iNtk1 != iNtk2 );
+        printf( "Replacing \"%s\" (appearing %d times) by \"%s\" (appearing %d times).\n", 
+            Rtl_NtkName(pNtk1), Rtl_LibCountInsts(p, pNtk1), Rtl_NtkName(pNtk2), Rtl_LibCountInsts(p, pNtk2) );
+        pNtk1->iCopy = iNtk2;
+    //    Rtl_LibSetReplace( p, vGuide );
+        Rtl_LibUpdateBoxes( p );
+        Rtl_LibReorderModules( p );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Wln_LibMarkHierarchy( Rtl_Lib_t * p, char ** ppModule, int nModules, int fVerbose )
+{
+    Rtl_Ntk_t * pNtk; int i;
+    if ( nModules == 0 ) // clean labels
+        Vec_PtrForEachEntry( Rtl_Ntk_t *, p->vNtks, pNtk, i )
+            pNtk->fRoot = 0;
+    for ( i = 0; i < nModules; i++ )
+    {
+        int iNtk = Rtl_LibReturnNtk( p, ppModule[i] );
+        if ( iNtk == -1 )
+            continue;
+        pNtk = Rtl_LibNtk( p, iNtk );
+        pNtk->fRoot = 1;
+        printf( "Marking module \"%s\" (appearing %d times in the hierarchy).\n", ppModule[i], Rtl_LibCountInsts(p, pNtk) );
+    }
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////