Experiments with word-level data structures.

8 files changed, 570 insertions, 224 deletions

diff --git a/abclib.dsp b/abclib.dsp
index f5e9f5f8..23c2ce28 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -1131,6 +1131,14 @@ SOURCE=.\src\base\wln\wlnBlast.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\base\wln\wlnCom.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\wln\wlnGuide.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\base\wln\wlnMem.c
 # End Source File
 # Begin Source File
diff --git a/src/base/main/mainInit.c b/src/base/main/mainInit.c
index 693cea90..d3ce672f 100644
--- a/src/base/main/mainInit.c
+++ b/src/base/main/mainInit.c
@@ -49,6 +49,8 @@ extern void Scl_Init( Abc_Frame_t * pAbc );
 extern void Scl_End( Abc_Frame_t * pAbc );
 extern void Wlc_Init( Abc_Frame_t * pAbc );
 extern void Wlc_End( Abc_Frame_t * pAbc );
+extern void Wln_Init( Abc_Frame_t * pAbc );
+extern void Wln_End( Abc_Frame_t * pAbc );
 extern void Bac_Init( Abc_Frame_t * pAbc );
 extern void Bac_End( Abc_Frame_t * pAbc );
 extern void Cba_Init( Abc_Frame_t * pAbc );
@@ -116,6 +118,7 @@ void Abc_FrameInit( Abc_Frame_t * pAbc )
     Load_Init( pAbc );
     Scl_Init( pAbc );
     Wlc_Init( pAbc );
+    Wln_Init( pAbc );
     Bac_Init( pAbc );
     Cba_Init( pAbc );
     Pla_Init( pAbc );
@@ -156,6 +159,7 @@ void Abc_FrameEnd( Abc_Frame_t * pAbc )
     Load_End( pAbc );
     Scl_End( pAbc );
     Wlc_End( pAbc );
+    Wln_End( pAbc );
     Bac_End( pAbc );
     Cba_End( pAbc );
     Pla_End( pAbc );
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index 2ea17169..dd7a3e32 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -54,20 +54,12 @@ static int  Abc_CommandInvPut     ( Abc_Frame_t * pAbc, int argc, char ** argv )
 static int  Abc_CommandInvMin     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandTest       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
-static int  Abc_CommandYosys      ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int  Abc_CommandSolve      ( Abc_Frame_t * pAbc, int argc, char ** argv );
-
 static inline Wlc_Ntk_t * Wlc_AbcGetNtk( Abc_Frame_t * pAbc )                       { return (Wlc_Ntk_t *)pAbc->pAbcWlc;                      }
 static inline void        Wlc_AbcFreeNtk( Abc_Frame_t * pAbc )                      { if ( pAbc->pAbcWlc ) Wlc_NtkFree(Wlc_AbcGetNtk(pAbc));  }
 static inline void        Wlc_AbcUpdateNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk )  { Wlc_AbcFreeNtk(pAbc); pAbc->pAbcWlc = pNtk;             }
 
 static inline Vec_Int_t * Wlc_AbcGetInv( Abc_Frame_t * pAbc )                       { return pAbc->pAbcWlcInv;                                }
 
-
-static inline Rtl_Lib_t * Wlc_AbcGetRtl( Abc_Frame_t * pAbc )                       { return (Rtl_Lib_t *)pAbc->pAbcRtl;                      }
-static inline void        Wlc_AbcFreeRtl( Abc_Frame_t * pAbc )                      { if ( pAbc->pAbcRtl ) Rtl_LibFree(Wlc_AbcGetRtl(pAbc));  }
-static inline void        Wlc_AbcUpdateRtl( Abc_Frame_t * pAbc, Rtl_Lib_t * pLib )  { Wlc_AbcFreeRtl(pAbc); pAbc->pAbcRtl = pLib;             }
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -103,9 +95,6 @@ void Wlc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Word level", "%show",        Abc_CommandShow,       0 );
     Cmd_CommandAdd( pAbc, "Word level", "%test",        Abc_CommandTest,       0 );
 
-    Cmd_CommandAdd( pAbc, "Word level", "%yosys",       Abc_CommandYosys,      0 );
-    Cmd_CommandAdd( pAbc, "Word level", "%solve",       Abc_CommandSolve,      0 );
-
     Cmd_CommandAdd( pAbc, "Word level", "inv_ps",       Abc_CommandInvPs,      0 );
     Cmd_CommandAdd( pAbc, "Word level", "inv_print",    Abc_CommandInvPrint,   0 );
     Cmd_CommandAdd( pAbc, "Word level", "inv_check",    Abc_CommandInvCheck,   0 );
@@ -1982,215 +1971,6 @@ usage:
     return 1;
 }
 
-
-/**Function********************************************************************
-
-  Synopsis    []
-
-  Description []
-
-  SideEffects []
-
-  SeeAlso     []
-
-******************************************************************************/
-int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    extern Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pTopModule, int fSkipStrash, int fInvert, int fTechMap, int fVerbose );
-    extern Rtl_Lib_t * Wln_ReadSystemVerilog( char * pFileName, char * pTopModule, int fCollapse, int fVerbose );
-
-    FILE * pFile;
-    char * pFileName = NULL;
-    char * pTopModule= NULL;
-    int fBlast       =    0;
-    int fInvert      =    0;
-    int fTechMap     =    1;
-    int fSkipStrash  =    0;
-    int fCollapse    =    0;
-    int c, fVerbose  =    0;
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Tbismcvh" ) ) != 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 'b':
-            fBlast ^= 1;
-            break;
-        case 'i':
-            fInvert ^= 1;
-            break;
-        case 's':
-            fSkipStrash ^= 1;
-            break;
-        case 'm':
-            fTechMap ^= 1;
-            break;
-        case 'c':
-            fCollapse ^= 1;
-            break;
-        case 'v':
-            fVerbose ^= 1;
-            break;
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-    if ( argc != globalUtilOptind + 1 )
-    {
-        printf( "Abc_CommandReadWlc(): Input file name should be given on the command line.\n" );
-        return 0;
-    }
-    // get the file name
-    pFileName = argv[globalUtilOptind];
-    if ( (pFile = fopen( pFileName, "r" )) == NULL )
-    {
-        Abc_Print( 1, "Cannot open input file \"%s\". ", pFileName );
-        if ( (pFileName = Extra_FileGetSimilarName( pFileName, ".v", ".sv", NULL, NULL, NULL )) )
-            Abc_Print( 1, "Did you mean \"%s\"?", pFileName );
-        Abc_Print( 1, "\n" );
-        return 0;
-    }
-    fclose( pFile );
-
-    // perform reading
-    if ( fBlast )
-    {
-        Gia_Man_t * pNew = NULL;
-        if ( !strcmp( Extra_FileNameExtension(pFileName), "v" )  )
-            pNew = Wln_BlastSystemVerilog( pFileName, pTopModule, fSkipStrash, fInvert, fTechMap, fVerbose );
-        else if ( !strcmp( Extra_FileNameExtension(pFileName), "sv" )  )
-            pNew = Wln_BlastSystemVerilog( pFileName, pTopModule, fSkipStrash, fInvert, fTechMap, fVerbose );
-        else if ( !strcmp( Extra_FileNameExtension(pFileName), "rtlil" )  )
-            pNew = Wln_BlastSystemVerilog( pFileName, pTopModule, fSkipStrash, fInvert, fTechMap, fVerbose );
-        else
-        {
-            printf( "Abc_CommandYosys(): Unknown file extension.\n" );
-            return 0;
-        }
-        Abc_FrameUpdateGia( pAbc, pNew );
-    }
-    else
-    {
-        Rtl_Lib_t * pLib = NULL;
-        if ( !strcmp( Extra_FileNameExtension(pFileName), "v" )  )
-            pLib = Wln_ReadSystemVerilog( pFileName, pTopModule, fCollapse, fVerbose );
-        else if ( !strcmp( Extra_FileNameExtension(pFileName), "sv" )  )
-            pLib = Wln_ReadSystemVerilog( pFileName, pTopModule, fCollapse, fVerbose );
-        else if ( !strcmp( Extra_FileNameExtension(pFileName), "rtlil" )  )
-            pLib = Wln_ReadSystemVerilog( pFileName, pTopModule, fCollapse, fVerbose );
-        else
-        {
-            printf( "Abc_CommandYosys(): Unknown file extension.\n" );
-            return 0;
-        }
-        Wlc_AbcUpdateRtl( pAbc, pLib );
-    }
-    return 0;
-usage:
-    Abc_Print( -2, "usage: %%yosys [-T <module>] [-bismcvh] <file_name>\n" );
-    Abc_Print( -2, "\t         reads Verilog or SystemVerilog using Yosys\n" );
-    Abc_Print( -2, "\t-T     : specify the top module name (default uses \"-auto-top\"\n" );
-    Abc_Print( -2, "\t-b     : toggle bit-blasting the design into an AIG using Yosys [default = %s]\n", fBlast? "yes": "no" );
-    Abc_Print( -2, "\t-i     : toggle interting the outputs (useful for miters) [default = %s]\n", fInvert? "yes": "no" );
-    Abc_Print( -2, "\t-s     : toggle no structural hashing during bit-blasting [default = %s]\n", fSkipStrash? "no strash": "strash" );
-    Abc_Print( -2, "\t-m     : toggle using \"techmap\" to blast operators [default = %s]\n", fTechMap? "yes": "no" );
-    Abc_Print( -2, "\t-c     : toggle collapsing design hierarchy using Yosys [default = %s]\n", fCollapse? "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_CommandSolve( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    extern void Rtl_LibPrintStats( Rtl_Lib_t * p );
-    extern void Rtl_LibPrint( char * pFileName, Rtl_Lib_t * p );
-    extern void Rtl_LibNormRanges( Rtl_Lib_t * pLib );
-    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, fOldBlast = 0, fPrepro = 0, fVerbose  = 0;
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "opvh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'o':
-            fOldBlast ^= 1;
-            break;
-        case 'p':
-            fPrepro ^= 1;
-            break;
-        case 'v':
-            fVerbose ^= 1;
-            break;
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-    Rtl_LibPrintStats( pLib );
-    //Rtl_LibPrint( NULL, pLib );
-    Rtl_LibOrderWires( pLib );
-
-    if ( fOldBlast )
-    {
-        Rtl_LibOrderCells( pLib );
-        Rtl_LibBlast( pLib );
-    }
-    else
-        Rtl_LibBlast2( pLib );
-    //Rtl_LibReorderModules( pLib );
-    //Rtl_LibPrintStats( pLib );
-
-    if ( fPrepro )
-        Rtl_LibPreprocess( pLib );
-    Rtl_LibSolve( pLib );
-
-    //Rtl_LibPrint( NULL, pLib );
-    Wlc_AbcUpdateRtl( pAbc, NULL );
-    Gia_ManStopP( &pGia );
-    return 0;
-usage:
-    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");
-    return 1;
-}
-
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/wln/module.make b/src/base/wln/module.make
index 7277f30b..c1939126 100644
--- a/src/base/wln/module.make
+++ b/src/base/wln/module.make
@@ -1,5 +1,7 @@
 SRC +=    src/base/wln/wln.c \
     src/base/wln/wlnBlast.c \
+    src/base/wln/wlnCom.c \
+    src/base/wln/wlnGuide.c \
     src/base/wln/wlnMem.c \
     src/base/wln/wlnNdr.c \
     src/base/wln/wlnNtk.c \
diff --git a/src/base/wln/wlnCom.c b/src/base/wln/wlnCom.c
new file mode 100644
index 00000000..3db27785
--- /dev/null
+++ b/src/base/wln/wlnCom.c
@@ -0,0 +1,353 @@
+/**CFile****************************************************************
+
+  FileName    [wlnCom.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Word-level network.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - September 23, 2018.]
+
+  Revision    [$Id: wlnCom.c,v 1.00 2018/09/23 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "wln.h"
+#include "base/main/mainInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static int  Abc_CommandYosys      ( 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 );
+
+static inline Rtl_Lib_t * Wln_AbcGetRtl( Abc_Frame_t * pAbc )                       { return (Rtl_Lib_t *)pAbc->pAbcRtl;                      }
+static inline void        Wln_AbcFreeRtl( Abc_Frame_t * pAbc )                      { if ( pAbc->pAbcRtl ) Rtl_LibFree(Wln_AbcGetRtl(pAbc));  }
+static inline void        Wln_AbcUpdateRtl( Abc_Frame_t * pAbc, Rtl_Lib_t * pLib )  { Wln_AbcFreeRtl(pAbc); pAbc->pAbcRtl = pLib;             }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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", "%print",       Abc_CommandPrint,      0 );
+}
+
+/**Function********************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+void Wln_End( Abc_Frame_t * pAbc )
+{
+    Wln_AbcUpdateRtl( pAbc, NULL );
+}
+
+
+/**Function********************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pTopModule, int fSkipStrash, int fInvert, int fTechMap, int fVerbose );
+    extern Rtl_Lib_t * Wln_ReadSystemVerilog( char * pFileName, char * pTopModule, int fCollapse, int fVerbose );
+
+    FILE * pFile;
+    char * pFileName = NULL;
+    char * pTopModule= NULL;
+    int fBlast       =    0;
+    int fInvert      =    0;
+    int fTechMap     =    1;
+    int fSkipStrash  =    0;
+    int fCollapse    =    0;
+    int c, fVerbose  =    0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Tbismcvh" ) ) != 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 'b':
+            fBlast ^= 1;
+            break;
+        case 'i':
+            fInvert ^= 1;
+            break;
+        case 's':
+            fSkipStrash ^= 1;
+            break;
+        case 'm':
+            fTechMap ^= 1;
+            break;
+        case 'c':
+            fCollapse ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( argc != globalUtilOptind + 1 )
+    {
+        printf( "Abc_CommandReadWlc(): Input file name should be given on the command line.\n" );
+        return 0;
+    }
+    // get the file name
+    pFileName = argv[globalUtilOptind];
+    if ( (pFile = fopen( pFileName, "r" )) == NULL )
+    {
+        Abc_Print( 1, "Cannot open input file \"%s\". ", pFileName );
+        if ( (pFileName = Extra_FileGetSimilarName( pFileName, ".v", ".sv", NULL, NULL, NULL )) )
+            Abc_Print( 1, "Did you mean \"%s\"?", pFileName );
+        Abc_Print( 1, "\n" );
+        return 0;
+    }
+    fclose( pFile );
+
+    // perform reading
+    if ( fBlast )
+    {
+        Gia_Man_t * pNew = NULL;
+        if ( !strcmp( Extra_FileNameExtension(pFileName), "v" )  )
+            pNew = Wln_BlastSystemVerilog( pFileName, pTopModule, fSkipStrash, fInvert, fTechMap, fVerbose );
+        else if ( !strcmp( Extra_FileNameExtension(pFileName), "sv" )  )
+            pNew = Wln_BlastSystemVerilog( pFileName, pTopModule, fSkipStrash, fInvert, fTechMap, fVerbose );
+        else if ( !strcmp( Extra_FileNameExtension(pFileName), "rtlil" )  )
+            pNew = Wln_BlastSystemVerilog( pFileName, pTopModule, fSkipStrash, fInvert, fTechMap, fVerbose );
+        else
+        {
+            printf( "Abc_CommandYosys(): Unknown file extension.\n" );
+            return 0;
+        }
+        Abc_FrameUpdateGia( pAbc, pNew );
+    }
+    else
+    {
+        Rtl_Lib_t * pLib = NULL;
+        if ( !strcmp( Extra_FileNameExtension(pFileName), "v" )  )
+            pLib = Wln_ReadSystemVerilog( pFileName, pTopModule, fCollapse, fVerbose );
+        else if ( !strcmp( Extra_FileNameExtension(pFileName), "sv" )  )
+            pLib = Wln_ReadSystemVerilog( pFileName, pTopModule, fCollapse, fVerbose );
+        else if ( !strcmp( Extra_FileNameExtension(pFileName), "rtlil" )  )
+            pLib = Wln_ReadSystemVerilog( pFileName, pTopModule, fCollapse, fVerbose );
+        else
+        {
+            printf( "Abc_CommandYosys(): Unknown file extension.\n" );
+            return 0;
+        }
+        Wln_AbcUpdateRtl( pAbc, pLib );
+    }
+    return 0;
+usage:
+    Abc_Print( -2, "usage: %%yosys [-T <module>] [-bismcvh] <file_name>\n" );
+    Abc_Print( -2, "\t         reads Verilog or SystemVerilog using Yosys\n" );
+    Abc_Print( -2, "\t-T     : specify the top module name (default uses \"-auto-top\"\n" );
+    Abc_Print( -2, "\t-b     : toggle bit-blasting the design into an AIG using Yosys [default = %s]\n", fBlast? "yes": "no" );
+    Abc_Print( -2, "\t-i     : toggle interting the outputs (useful for miters) [default = %s]\n", fInvert? "yes": "no" );
+    Abc_Print( -2, "\t-s     : toggle no structural hashing during bit-blasting [default = %s]\n", fSkipStrash? "no strash": "strash" );
+    Abc_Print( -2, "\t-m     : toggle using \"techmap\" to blast operators [default = %s]\n", fTechMap? "yes": "no" );
+    Abc_Print( -2, "\t-c     : toggle collapsing design hierarchy using Yosys [default = %s]\n", fCollapse? "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_CommandPrint( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern void Rtl_LibPrintStats( Rtl_Lib_t * p );
+    extern void Rtl_LibPrintHieStats( Rtl_Lib_t * p );
+    extern void Rtl_LibPrint( char * pFileName, Rtl_Lib_t * p );
+    Rtl_Lib_t * pLib = Wln_AbcGetRtl(pAbc);
+    int c, fHie = 0, fDesign = 0, fVerbose  = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "pdvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'p':
+            fHie ^= 1;
+            break;
+        case 'd':
+            fDesign ^= 1;
+            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;
+    }
+    Rtl_LibPrintStats( pLib );
+    if ( fHie )
+        Rtl_LibPrintHieStats( pLib );
+    if ( fDesign )
+        Rtl_LibPrint( NULL, pLib );
+    return 0;
+usage:
+    Abc_Print( -2, "usage: %%print [-pdvh]\n" );
+    Abc_Print( -2, "\t         print statistics about the hierarchical design\n" );
+    Abc_Print( -2, "\t-p     : toggle printing of the hierarchy [default = %s]\n", fHie? "yes": "no" );
+    Abc_Print( -2, "\t-d     : toggle printing of the design [default = %s]\n", fDesign? "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");
+    Abc_Print( -2, "\t<file> : text file name with guidance for solving\n");
+    return 1;
+}
+
+/**Function********************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int Abc_CommandSolve( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern void Rtl_LibBlast( Rtl_Lib_t * pLib );
+    extern void Rtl_LibBlast2( Rtl_Lib_t * pLib );
+    extern void Rtl_LibSolve( Rtl_Lib_t * pLib, void * pNtk );
+    extern void Rtl_LibPreprocess( Rtl_Lib_t * pLib );
+    extern void Wln_SolveWithGuidance( char * pFileName, Rtl_Lib_t * p );
+
+    Rtl_Lib_t * pLib = Wln_AbcGetRtl(pAbc);
+    int c, fOldBlast = 0, fPrepro = 0, fVerbose  = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "opvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'o':
+            fOldBlast ^= 1;
+            break;
+        case 'p':
+            fPrepro ^= 1;
+            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;
+    }
+    if ( argc == globalUtilOptind + 1 )
+    {
+        char * pFileName = argv[globalUtilOptind];
+        FILE * pFile = fopen( pFileName, "r" );
+        if ( pFile == NULL )
+        {
+            Abc_Print( -1, "Cannot open file \"%s\" with the input test patterns.\n", pFileName );
+            return 0;
+        }
+        fclose( pFile );
+        printf( "Using guidance from file \"%s\".\n", pFileName );
+        Wln_SolveWithGuidance( pFileName, pLib );
+    }
+    else
+    {
+        printf( "Solving the miter without guidance.\n" );
+        if ( fOldBlast )
+            Rtl_LibBlast( pLib );
+        else
+            Rtl_LibBlast2( pLib );
+        if ( fPrepro )
+            Rtl_LibPreprocess( pLib );
+        Rtl_LibSolve( pLib, NULL );
+    }
+    return 0;
+usage:
+    Abc_Print( -2, "usage: %%solve [-opvh] <file>\n" );
+    Abc_Print( -2, "\t         solving properties for the hierarchical design\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");
+    Abc_Print( -2, "\t<file> : text file name with guidance for solving\n");
+    return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/wln/wlnGuide.c b/src/base/wln/wlnGuide.c
new file mode 100644
index 00000000..abe9a6d8
--- /dev/null
+++ b/src/base/wln/wlnGuide.c
@@ -0,0 +1,73 @@
+/**CFile****************************************************************
+
+  FileName    [wln.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Word-level network.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - September 23, 2018.]
+
+  Revision    [$Id: wln.c,v 1.00 2018/09/23 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "wln.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Wln_ReadGuidance( char * pFileName, Abc_Nam_t * p )
+{
+    char Buffer[1000] = {'\\'}, * pBuffer = Buffer+1;
+    Vec_Int_t * vTokens = Vec_IntAlloc( 100 );
+    FILE * pFile = fopen( pFileName, "rb" );
+    while ( fscanf( pFile, "%s", pBuffer ) == 1 )
+    {
+        if ( pBuffer[(int)strlen(pBuffer)-1] == '\r' )
+            pBuffer[(int)strlen(pBuffer)-1] = 0;
+        if ( !strcmp(pBuffer, "prove") && Vec_IntSize(vTokens) % 4 == 3 ) // account for "property"
+            Vec_IntPush( vTokens, -1 );
+        if ( Vec_IntSize(vTokens) % 4 == 2 || Vec_IntSize(vTokens) % 4 == 3 )
+            Vec_IntPush( vTokens, Abc_NamStrFindOrAdd(p, Buffer, NULL) );
+        else
+            Vec_IntPush( vTokens, Abc_NamStrFindOrAdd(p, pBuffer, NULL) );
+    }
+    fclose( pFile );
+    if ( Vec_IntSize(vTokens) % 4 == 3 ) // account for "property"
+        Vec_IntPush( vTokens, -1 );
+    assert( Vec_IntSize(vTokens) % 4 == 0 );
+    return vTokens;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/wln/wlnRead.c b/src/base/wln/wlnRead.c
index 62cb70c6..bc4211ac 100644
--- a/src/base/wln/wlnRead.c
+++ b/src/base/wln/wlnRead.c
@@ -78,6 +78,8 @@ struct Rtl_Ntk_t_
 static inline int         Rtl_LibNtkNum( Rtl_Lib_t * pLib )                { return Vec_PtrSize(pLib->vNtks);                  }
 static inline Rtl_Ntk_t * Rtl_LibNtk( Rtl_Lib_t * pLib, int i )            { return (Rtl_Ntk_t *)Vec_PtrEntry(pLib->vNtks, i); }
 static inline Rtl_Ntk_t * Rtl_LibTop( Rtl_Lib_t * pLib )                   { return Rtl_LibNtk( pLib, Rtl_LibNtkNum(pLib)-1 ); }
+static inline char *      Rtl_LibStr( Rtl_Lib_t * pLib, int h )            { return Abc_NamStr(pLib->pManName, h);             }
+static inline int         Rtl_LibStrId( Rtl_Lib_t * pLib, char * s )       { return Abc_NamStrFind(pLib->pManName, s);         }
 
 static inline Rtl_Ntk_t * Rtl_NtkModule( Rtl_Ntk_t * p, int i )            { return Rtl_LibNtk( p->pLib, i );                  }
 
@@ -254,6 +256,50 @@ void Rtl_NtkPrintStats( Rtl_Ntk_t * p, int nNameSymbs )
   SeeAlso     []
 
 ***********************************************************************/
+void Rtl_NtkPrintHieStats( Rtl_Ntk_t * p, int nOffset )
+{
+    Vec_Int_t * vFound = Vec_IntAlloc( 100 );
+    int i, * pCell;
+    for ( i = 0; i < 5*(nOffset-1); i++ )
+        printf( " " );
+    if ( nOffset )
+        printf( "|--> " );
+    printf( "%s\n", Rtl_NtkName(p) );
+    Rtl_NtkForEachCell( p, pCell, i )
+        if ( Rtl_CellModule(pCell) >= ABC_INFINITY )
+        {
+            Rtl_Ntk_t * pModel = Rtl_NtkModule( p, Rtl_CellModule(pCell)-ABC_INFINITY );
+            assert( pCell[6] == pModel->nInputs+pModel->nOutputs );
+            if ( Vec_IntFind(vFound, pModel->NameId) >= 0 )
+                continue;
+            Vec_IntPush( vFound, pModel->NameId );
+            Rtl_NtkPrintHieStats( pModel, nOffset+1 );
+        }
+    Vec_IntFree( vFound );
+}
+void Rtl_LibPrintHieStats( Rtl_Lib_t * p )
+{
+    Rtl_Ntk_t * pNtk; int i;
+    printf( "Hierarchy found in \"%s\":\n", p->pSpec );
+    Vec_PtrForEachEntry( Rtl_Ntk_t *, p->vNtks, pNtk, i )
+    {
+        printf( "\n" );
+        printf( "MODULE %d: ", i );
+        Rtl_NtkPrintHieStats( pNtk, 0 );  
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Rtl_Lib_t * Rtl_LibAlloc()
 {
     Rtl_Lib_t * p = ABC_CALLOC( Rtl_Lib_t, 1 );
@@ -1398,6 +1444,7 @@ Rtl_Lib_t * Rtl_LibReadFile( char * pFileName, char * pFileSpec )
             i = Rtl_NtkReadAttribute2( p, i+1 );
     Rtl_LibSetParents( p );
     Rtl_LibReorderModules( p );
+    Rtl_LibOrderWires( p );
     return p;
 }
 
@@ -1733,7 +1780,7 @@ char * Rtl_ShortenName( char * pName, int nSize )
         return pName;
     Buffer[0] = 0;
     strcat( Buffer, pName );
-    Buffer[nSize-4] = ' ';
+    //Buffer[nSize-4] = ' ';
     Buffer[nSize-3] = '.';
     Buffer[nSize-2] = '.';
     Buffer[nSize-1] = '.';
@@ -1941,6 +1988,7 @@ void Rtl_NtkBlastPrepareInputs( Rtl_Ntk_t * p, int * pCell )
 }
 void Rtl_NtkBlast2_rec( Rtl_Ntk_t * p, int iBit, int * pDriver )
 {
+    //char * pName = Rtl_NtkName(p);
     assert( pDriver[0] != -1 );
     if ( pDriver[0] == -3 )
     {
@@ -1981,6 +2029,7 @@ Gia_Man_t * Rtl_NtkBlast2( Rtl_Ntk_t * p )
     int i, b, nBits = Rtl_NtkRangeWires( p );
     char Buffer[100]; static int counter = 0;
     Vec_IntFill( &p->vLits, nBits, -1 );
+printf( "Blasting %s...\r", Rtl_NtkName(p) );
     Rtl_NtkMapWires( p, 0 );
     Rtl_NtkBlastMap( p, nBits );
     assert( p->pGia == NULL );
@@ -2066,11 +2115,11 @@ finish:
     //Rtl_LibBlast( pLib );
     Rtl_LibBlast2( pLib );
 }
-void Rtl_LibSolve( Rtl_Lib_t * pLib )
+void Rtl_LibSolve( Rtl_Lib_t * pLib, void * pNtk )
 {
     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 );
+    Rtl_Ntk_t * pTop = pNtk ? (Rtl_Ntk_t *)pNtk : Rtl_LibTop( pLib );
     Gia_Man_t * pSwp = Cec4_ManSimulateTest3( pTop->pGia, 1000000, 0 );
     int RetValue = Gia_ManAndNum(pSwp) == 0;
     Gia_ManStop( pSwp );
@@ -2092,6 +2141,83 @@ void Rtl_LibSolve( Rtl_Lib_t * pLib )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Wln_SolveEqual( Rtl_Lib_t * p, int iNtk1, int iNtk2 )
+{
+    Rtl_Ntk_t * pNtk1 = Rtl_LibNtk( p, iNtk1 );
+    Rtl_Ntk_t * pNtk2 = Rtl_LibNtk( p, iNtk2 );
+    printf( "Proving equivalence of \"%s\" and \"%s\".\n", Rtl_NtkName(pNtk1), Rtl_NtkName(pNtk2) );
+/*
+    if ( Gia_ManCiNum(pNtk1->pGia) != Gia_ManCiNum(pNtk2->pGia) || 
+         Gia_ManCoNum(pNtk1->pGia) != Gia_ManCoNum(pNtk2->pGia) )
+    {
+        printf( "The number of inputs/outputs does not match.\n" );
+    }
+    else
+    {
+        int Status = Cec_ManVerifyTwo( pNtk1->pGia, pNtk2->pGia, 0 );
+        if ( Status == 1 )
+            printf( "The networks are equivalence.\n" );
+        else
+            printf( "The networks are NOT equivalent.\n" );
+    }
+*/
+}
+void Wln_SolveInverse( Rtl_Lib_t * p, int iNtk1, int iNtk2 )
+{
+    Rtl_Ntk_t * pNtk1 = Rtl_LibNtk( p, iNtk1 );
+    Rtl_Ntk_t * pNtk2 = Rtl_LibNtk( p, iNtk2 );
+    printf( "Proving inverse equivalence of \"%s\" and \"%s\".\n", Rtl_NtkName(pNtk1), Rtl_NtkName(pNtk2) );
+}
+void Wln_SolveProperty( Rtl_Lib_t * p, int iNtk )
+{
+    Rtl_Ntk_t * pNtk = Rtl_LibNtk( p, iNtk );
+    printf( "Proving property \"%s\".\n", Rtl_NtkName(pNtk) );
+    Rtl_LibSolve( p, pNtk );
+}
+void Wln_SolveWithGuidance( char * pFileName, Rtl_Lib_t * p )
+{
+    extern Vec_Int_t * Wln_ReadGuidance( char * pFileName, Abc_Nam_t * p );
+    Vec_Int_t * vGuide = Wln_ReadGuidance( pFileName, p->pManName ); int i;
+    Vec_IntFillExtra( p->vMap, Abc_NamObjNumMax(p->pManName), -1 );
+    Rtl_LibBlast2( p );
+    for ( i = 0; i < Vec_IntSize(vGuide); i += 4 )
+    {
+        int Prove = Vec_IntEntry( vGuide, i+0 );
+        int Type  = Vec_IntEntry( vGuide, i+1 );
+        int Name1 = Vec_IntEntry( vGuide, i+2 );
+        int Name2 = Vec_IntEntry( vGuide, i+3 );
+        int iNtk1 = Rtl_LibFindModule( p, Name1 );
+        int iNtk2 = Name2 == -1 ? -1 : Rtl_LibFindModule( p, Name2 );
+        if ( Prove != Rtl_LibStrId(p, "prove") )
+            printf( "Unknown task in line %d.\n", i/4 );
+        else if ( iNtk1 == -1 )
+            printf( "Network %s cannot be found in this design.\n", Rtl_LibStr(p, Name1) );
+        else
+        {
+            if ( Type == Rtl_LibStrId(p, "equal") )
+                Wln_SolveEqual( p, iNtk1, iNtk2 );
+            else if ( Type == Rtl_LibStrId(p, "inverse") )
+                Wln_SolveInverse( p, iNtk1, iNtk2 );
+            else if ( Type == Rtl_LibStrId(p, "property") )
+                Wln_SolveProperty( p, iNtk1 );
+            continue;
+        }
+        break;
+    }
+    Vec_IntFree( vGuide );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/wln/wlnRtl.c b/src/base/wln/wlnRtl.c
index 97cc9714..fa0f0cd5 100644
--- a/src/base/wln/wlnRtl.c
+++ b/src/base/wln/wlnRtl.c
@@ -145,7 +145,7 @@ Rtl_Lib_t * Wln_ReadSystemVerilog( char * pFileName, char * pTopModule, int fCol
         return Rtl_LibReadFile( pFileName, pFileName );
     sprintf( Command, "%s -qp \"read_verilog %s%s; hierarchy %s%s; %sproc; write_rtlil %s\"", 
         Wln_GetYosysName(), fSVlog ? "-sv ":"", pFileName, 
-        pTopModule ? "-top " : "-auto-top", 
+        pTopModule ? "-top "    : "", 
         pTopModule ? pTopModule : "", 
         fCollapse ? "flatten; " : "",
         pFileTemp );