Version abc80130_2

8 files changed, 4201 insertions, 0 deletions

diff --git a/src/base/ver/module.make b/src/base/ver/module.make
new file mode 100644
index 00000000..2cc37803
--- /dev/null
+++ b/src/base/ver/module.make
@@ -0,0 +1,4 @@
+SRC +=    src/base/ver/verCore.c \
+    src/base/ver/verFormula.c \
+    src/base/ver/verParse.c \
+    src/base/ver/verStream.c 
diff --git a/src/base/ver/ver.h b/src/base/ver/ver.h
new file mode 100644
index 00000000..9c538ac4
--- /dev/null
+++ b/src/base/ver/ver.h
@@ -0,0 +1,118 @@
+/**CFile****************************************************************
+
+  FileName    [ver.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Verilog parser.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - August 19, 2006.]
+
+  Revision    [$Id: ver.h,v 1.00 2006/08/19 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __VER_H__
+#define __VER_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif 
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include <stdio.h>
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Ver_Man_t_       Ver_Man_t;
+typedef struct Ver_Stream_t_    Ver_Stream_t;
+
+struct Ver_Man_t_
+{
+    // internal parameters
+    int             fMapped;       // mapped verilog
+    int             fUseMemMan;    // allocate memory manager in the networks
+    int             fCheck;        // checks network for currectness
+    // input file stream
+    char *          pFileName;
+    Ver_Stream_t *  pReader;
+    int             fNameLast;
+    ProgressBar *   pProgress;
+    // current design
+    Abc_Lib_t *     pDesign;
+    st_table *      tName2Suffix;
+    // error handling
+    FILE *          Output;
+    int             fTopLevel;
+    int             fError;
+    char            sError[2000];
+    // intermediate structures
+    Vec_Ptr_t *     vNames;  
+    Vec_Ptr_t *     vStackFn;
+    Vec_Int_t *     vStackOp;
+    Vec_Int_t *     vPerm;
+};
+
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                             ITERATORS                            ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== verCore.c ========================================================*/
+extern Abc_Lib_t *    Ver_ParseFile( char * pFileName, Abc_Lib_t * pGateLib, int fCheck, int fUseMemMan );
+extern void           Ver_ParsePrintErrorMessage( Ver_Man_t * p );
+/*=== verFormula.c ========================================================*/
+extern void *         Ver_FormulaParser( char * pFormula, void * pMan, Vec_Ptr_t * vNames, Vec_Ptr_t * vStackFn, Vec_Int_t * vStackOp, char * pErrorMessage );
+extern void *         Ver_FormulaReduction( char * pFormula, void * pMan, Vec_Ptr_t * vNames, char * pErrorMessage );
+/*=== verParse.c ========================================================*/
+extern int            Ver_ParseSkipComments( Ver_Man_t * p );
+extern char *         Ver_ParseGetName( Ver_Man_t * p );
+/*=== verStream.c ========================================================*/
+extern Ver_Stream_t * Ver_StreamAlloc( char * pFileName );
+extern void           Ver_StreamFree( Ver_Stream_t * p );
+extern char *         Ver_StreamGetFileName( Ver_Stream_t * p );
+extern int            Ver_StreamGetFileSize( Ver_Stream_t * p );
+extern int            Ver_StreamGetCurPosition( Ver_Stream_t * p );
+extern int            Ver_StreamGetLineNumber( Ver_Stream_t * p );
+
+extern int            Ver_StreamIsOkey( Ver_Stream_t * p );
+extern char           Ver_StreamScanChar( Ver_Stream_t * p );
+extern char           Ver_StreamPopChar( Ver_Stream_t * p );
+extern void           Ver_StreamSkipChars( Ver_Stream_t * p, char * pCharsToSkip );
+extern void           Ver_StreamSkipToChars( Ver_Stream_t * p, char * pCharsToStop );
+extern char *         Ver_StreamGetWord( Ver_Stream_t * p, char * pCharsToStop );
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/base/ver/verCore.c b/src/base/ver/verCore.c
new file mode 100644
index 00000000..322ce720
--- /dev/null
+++ b/src/base/ver/verCore.c
@@ -0,0 +1,2949 @@
+/**CFile****************************************************************
+
+  FileName    [verCore.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Verilog parser.]
+
+  Synopsis    [Parses several flavors of structural Verilog.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - August 19, 2006.]
+
+  Revision    [$Id: verCore.c,v 1.00 2006/08/19 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ver.h"
+#include "mio.h"
+#include "main.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// types of verilog signals
+typedef enum { 
+    VER_SIG_NONE = 0,
+    VER_SIG_INPUT,
+    VER_SIG_OUTPUT,
+    VER_SIG_INOUT,
+    VER_SIG_REG,
+    VER_SIG_WIRE
+} Ver_SignalType_t;
+
+// types of verilog gates
+typedef enum { 
+    VER_GATE_AND = 0,
+    VER_GATE_OR,
+    VER_GATE_XOR,
+    VER_GATE_BUF,
+    VER_GATE_NAND,
+    VER_GATE_NOR,
+    VER_GATE_XNOR,
+    VER_GATE_NOT
+} Ver_GateType_t;
+
+static Ver_Man_t * Ver_ParseStart( char * pFileName, Abc_Lib_t * pGateLib );
+static void Ver_ParseStop( Ver_Man_t * p );
+static void Ver_ParseFreeData( Ver_Man_t * p );
+static void Ver_ParseInternal( Ver_Man_t * p );
+static int  Ver_ParseModule( Ver_Man_t * p );
+static int  Ver_ParseSignal( Ver_Man_t * p, Abc_Ntk_t * pNtk, Ver_SignalType_t SigType );
+static int  Ver_ParseAlways( Ver_Man_t * p, Abc_Ntk_t * pNtk );
+static int  Ver_ParseInitial( Ver_Man_t * p, Abc_Ntk_t * pNtk );
+static int  Ver_ParseAssign( Ver_Man_t * p, Abc_Ntk_t * pNtk );
+static int  Ver_ParseGateStandard( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_GateType_t GateType );
+static int  Ver_ParseFlopStandard( Ver_Man_t * pMan, Abc_Ntk_t * pNtk );
+static int  Ver_ParseGate( Ver_Man_t * p, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate );
+static int  Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox );
+static int  Ver_ParseConnectBox( Ver_Man_t * pMan, Abc_Obj_t * pBox );
+static int  Ver_ParseAttachBoxes( Ver_Man_t * pMan );
+
+static Abc_Obj_t * Ver_ParseCreatePi( Abc_Ntk_t * pNtk, char * pName );
+static Abc_Obj_t * Ver_ParseCreatePo( Abc_Ntk_t * pNtk, char * pName );
+static Abc_Obj_t * Ver_ParseCreateLatch( Abc_Ntk_t * pNtk, Abc_Obj_t * pNetLI, Abc_Obj_t * pNetLO );
+static Abc_Obj_t * Ver_ParseCreateInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pNet );
+
+static void Ver_ParseRemoveSuffixTable( Ver_Man_t * pMan );
+
+static inline int Ver_NtkIsDefined( Abc_Ntk_t * pNtkBox )  { assert( pNtkBox->pName );     return Abc_NtkPiNum(pNtkBox) || Abc_NtkPoNum(pNtkBox);  }
+static inline int Ver_ObjIsConnected( Abc_Obj_t * pObj )   { assert( Abc_ObjIsBox(pObj) ); return Abc_ObjFaninNum(pObj) || Abc_ObjFanoutNum(pObj); }
+
+int glo_fMapped = 0; // this is bad!
+
+typedef struct Ver_Bundle_t_    Ver_Bundle_t;
+struct Ver_Bundle_t_
+{
+    char *          pNameFormal;   // the name of the formal net
+    Vec_Ptr_t *     vNetsActual;   // the vector of actual nets (MSB to LSB)
+};
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Start parser.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ver_Man_t * Ver_ParseStart( char * pFileName, Abc_Lib_t * pGateLib )
+{
+    Ver_Man_t * p;
+    p = ALLOC( Ver_Man_t, 1 );
+    memset( p, 0, sizeof(Ver_Man_t) );
+    p->pFileName = pFileName;
+    p->pReader   = Ver_StreamAlloc( pFileName );
+    if ( p->pReader == NULL )
+        return NULL;
+    p->Output    = stdout;
+    p->vNames    = Vec_PtrAlloc( 100 );
+    p->vStackFn  = Vec_PtrAlloc( 100 );
+    p->vStackOp  = Vec_IntAlloc( 100 );
+    p->vPerm     = Vec_IntAlloc( 100 );
+    // create the design library and assign the technology library
+    p->pDesign   = Abc_LibCreate( pFileName );
+    p->pDesign->pLibrary = pGateLib;
+    p->pDesign->pGenlib = Abc_FrameReadLibGen();
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stop parser.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ver_ParseStop( Ver_Man_t * p )
+{
+    if ( p->pProgress )
+        Extra_ProgressBarStop( p->pProgress );
+    Ver_StreamFree( p->pReader );
+    Vec_PtrFree( p->vNames   );
+    Vec_PtrFree( p->vStackFn );
+    Vec_IntFree( p->vStackOp );
+    Vec_IntFree( p->vPerm );
+    free( p );
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    [File parser.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Lib_t * Ver_ParseFile( char * pFileName, Abc_Lib_t * pGateLib, int fCheck, int fUseMemMan )
+{
+    Ver_Man_t * p;
+    Abc_Lib_t * pDesign;
+    // start the parser
+    p = Ver_ParseStart( pFileName, pGateLib );
+    p->fMapped    = glo_fMapped;
+    p->fCheck     = fCheck;
+    p->fUseMemMan = fUseMemMan;
+    if ( glo_fMapped )
+    {
+        Hop_ManStop(p->pDesign->pManFunc);
+        p->pDesign->pManFunc = NULL;
+    }
+    // parse the file
+    Ver_ParseInternal( p );
+    // save the result
+    pDesign = p->pDesign;
+    p->pDesign = NULL;
+    // stop the parser
+    Ver_ParseStop( p );
+    return pDesign;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [File parser.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ver_ParseInternal( Ver_Man_t * pMan )
+{
+    Abc_Ntk_t * pNtk;
+    char * pToken;
+    int i;
+
+    // preparse the modeles
+    pMan->pProgress = Extra_ProgressBarStart( stdout, Ver_StreamGetFileSize(pMan->pReader) );
+    while ( 1 )
+    {
+        // get the next token
+        pToken = Ver_ParseGetName( pMan );
+        if ( pToken == NULL )
+            break;
+        if ( strcmp( pToken, "module" ) )
+        {
+            sprintf( pMan->sError, "Cannot read \"module\" directive." );
+            Ver_ParsePrintErrorMessage( pMan );
+            return;
+        }
+        // parse the module
+        if ( !Ver_ParseModule(pMan) )
+            return;
+    }
+    Extra_ProgressBarStop( pMan->pProgress );
+    pMan->pProgress = NULL;
+
+    // process defined and undefined boxes
+    if ( !Ver_ParseAttachBoxes( pMan ) )
+        return;
+
+    // connect the boxes and check
+    Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
+    {
+        // fix the dangling nets
+        Abc_NtkFinalizeRead( pNtk );
+        // check the network for correctness
+        if ( pMan->fCheck && !Abc_NtkCheckRead( pNtk ) )
+        {
+            pMan->fTopLevel = 1;
+            sprintf( pMan->sError, "The network check has failed for network %s.", pNtk->pName );
+            Ver_ParsePrintErrorMessage( pMan );
+            return;
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [File parser.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ver_ParseFreeData( Ver_Man_t * p )
+{
+    if ( p->pDesign )
+    {
+        Abc_LibFree( p->pDesign, NULL );
+        p->pDesign = NULL;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the error message including the file name and line number.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ver_ParsePrintErrorMessage( Ver_Man_t * p )
+{
+    p->fError = 1;
+    if ( p->fTopLevel ) // the line number is not given
+        fprintf( p->Output, "%s: %s\n", p->pFileName, p->sError );
+    else // print the error message with the line number
+        fprintf( p->Output, "%s (line %d): %s\n", 
+            p->pFileName, Ver_StreamGetLineNumber(p->pReader), p->sError );
+    // free the data
+    Ver_ParseFreeData( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finds the network by name or create a new blackbox network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Ver_ParseFindOrCreateNetwork( Ver_Man_t * pMan, char * pName )
+{
+    Abc_Ntk_t * pNtkNew;
+    // check if the network exists
+    if ( pNtkNew = Abc_LibFindModelByName( pMan->pDesign, pName ) )
+        return pNtkNew;
+//printf( "Creating network %s.\n", pName );
+    // create new network
+    pNtkNew = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_BLACKBOX, pMan->fUseMemMan );
+    pNtkNew->pName = Extra_UtilStrsav( pName );
+    pNtkNew->pSpec = NULL;
+    // add module to the design
+    Abc_LibAddModel( pMan->pDesign, pNtkNew );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finds the network by name or create a new blackbox network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Ver_ParseFindNet( Abc_Ntk_t * pNtk, char * pName )
+{
+    Abc_Obj_t * pObj;
+    if ( pObj = Abc_NtkFindNet(pNtk, pName) )
+        return pObj;
+    if ( !strcmp( pName, "1\'b0" ) || !strcmp( pName, "1\'bx" ) )
+        return Abc_NtkFindOrCreateNet( pNtk, "1\'b0" );
+    if ( !strcmp( pName, "1\'b1" ) )
+        return Abc_NtkFindOrCreateNet( pNtk, "1\'b1" );
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts the network from the blackbox type into a different one.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseConvertNetwork( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, int fMapped )
+{
+    if ( fMapped )
+    {
+        // convert from the blackbox into the network with local functions representated by AIGs
+        if ( pNtk->ntkFunc == ABC_FUNC_BLACKBOX )
+        {
+            // change network type
+            assert( pNtk->pManFunc == NULL );
+            pNtk->ntkFunc = ABC_FUNC_MAP;
+            pNtk->pManFunc = pMan->pDesign->pGenlib;
+        }
+        else if ( pNtk->ntkFunc != ABC_FUNC_MAP )
+        {
+            sprintf( pMan->sError, "The network %s appears to have both gates and assign statements. Currently such network are not allowed. One way to fix this problem might be to replace assigns by buffers from the library.", pNtk->pName );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+    }
+    else
+    {
+        // convert from the blackbox into the network with local functions representated by AIGs
+        if ( pNtk->ntkFunc == ABC_FUNC_BLACKBOX )
+        {
+            // change network type
+            assert( pNtk->pManFunc == NULL );
+            pNtk->ntkFunc = ABC_FUNC_AIG;
+            pNtk->pManFunc = pMan->pDesign->pManFunc;
+        }
+        else if ( pNtk->ntkFunc != ABC_FUNC_AIG )
+        {
+            sprintf( pMan->sError, "The network %s appears to have both gates and assign statements. Currently such network are not allowed. One way to fix this problem might be to replace assigns by buffers from the library.", pNtk->pName );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Parses one Verilog module.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseModule( Ver_Man_t * pMan )
+{
+    Mio_Gate_t * pGate;
+    Ver_Stream_t * p = pMan->pReader;
+    Abc_Ntk_t * pNtk, * pNtkTemp;
+    char * pWord, Symbol;
+    int RetValue;
+
+    // get the network name
+    pWord = Ver_ParseGetName( pMan );
+
+    // get the network with this name
+    pNtk = Ver_ParseFindOrCreateNetwork( pMan, pWord );
+
+    // make sure we stopped at the opening paranthesis
+    if ( Ver_StreamPopChar(p) != '(' )
+    {
+        sprintf( pMan->sError, "Cannot find \"(\" after \"module\" in network %s.", pNtk->pName );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+
+    // skip to the end of parantheses
+    do {
+        if ( Ver_ParseGetName( pMan ) == NULL )
+            return 0;
+        Symbol = Ver_StreamPopChar(p);
+    } while ( Symbol == ',' );
+    assert( Symbol == ')' );
+    if ( !Ver_ParseSkipComments( pMan ) )
+        return 0;
+    Symbol = Ver_StreamPopChar(p);
+    if ( Symbol != ';' )
+    {
+        sprintf( pMan->sError, "Expected closing paranthesis after \"module\"." );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+
+    // parse the inputs/outputs/registers/wires/inouts
+    while ( 1 )
+    {
+        Extra_ProgressBarUpdate( pMan->pProgress, Ver_StreamGetCurPosition(p), NULL );
+        pWord = Ver_ParseGetName( pMan );
+        if ( pWord == NULL )
+            return 0;
+        if ( !strcmp( pWord, "input" ) )
+            RetValue = Ver_ParseSignal( pMan, pNtk, VER_SIG_INPUT );
+        else if ( !strcmp( pWord, "output" ) )
+            RetValue = Ver_ParseSignal( pMan, pNtk, VER_SIG_OUTPUT );
+        else if ( !strcmp( pWord, "reg" ) )
+            RetValue = Ver_ParseSignal( pMan, pNtk, VER_SIG_REG );
+        else if ( !strcmp( pWord, "wire" ) )
+            RetValue = Ver_ParseSignal( pMan, pNtk, VER_SIG_WIRE );
+        else if ( !strcmp( pWord, "inout" ) )
+            RetValue = Ver_ParseSignal( pMan, pNtk, VER_SIG_INOUT );
+        else 
+            break;
+        if ( RetValue == 0 )
+            return 0;
+    }
+
+    // parse the remaining statements
+    while ( 1 )
+    {
+        Extra_ProgressBarUpdate( pMan->pProgress, Ver_StreamGetCurPosition(p), NULL );
+
+        if ( !strcmp( pWord, "and" ) )
+            RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_AND );
+        else if ( !strcmp( pWord, "or" ) )
+            RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_OR );
+        else if ( !strcmp( pWord, "xor" ) )
+            RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_XOR );
+        else if ( !strcmp( pWord, "buf" ) )
+            RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_BUF );
+        else if ( !strcmp( pWord, "nand" ) )
+            RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_NAND );
+        else if ( !strcmp( pWord, "nor" ) )
+            RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_NOR );
+        else if ( !strcmp( pWord, "xnor" ) )
+            RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_XNOR );
+        else if ( !strcmp( pWord, "not" ) )
+            RetValue = Ver_ParseGateStandard( pMan, pNtk, VER_GATE_NOT );
+
+        else if ( !strcmp( pWord, "dff" ) )
+            RetValue = Ver_ParseFlopStandard( pMan, pNtk );
+
+        else if ( !strcmp( pWord, "assign" ) )
+            RetValue = Ver_ParseAssign( pMan, pNtk );
+        else if ( !strcmp( pWord, "always" ) )
+            RetValue = Ver_ParseAlways( pMan, pNtk );
+        else if ( !strcmp( pWord, "initial" ) )
+            RetValue = Ver_ParseInitial( pMan, pNtk );
+        else if ( !strcmp( pWord, "endmodule" ) )
+            break;
+        else if ( pMan->pDesign->pGenlib && (pGate = Mio_LibraryReadGateByName(pMan->pDesign->pGenlib, pWord)) ) // current design
+            RetValue = Ver_ParseGate( pMan, pNtk, pGate );
+//        else if ( pMan->pDesign->pLibrary && st_lookup(pMan->pDesign->pLibrary->tModules, pWord, (char**)&pNtkTemp) ) // gate library
+//            RetValue = Ver_ParseGate( pMan, pNtkTemp );
+        else // assume this is the box used in the current design
+        {
+            pNtkTemp = Ver_ParseFindOrCreateNetwork( pMan, pWord );
+            RetValue = Ver_ParseBox( pMan, pNtk, pNtkTemp );
+        }
+        if ( RetValue == 0 )
+            return 0;
+        // skip the comments
+        if ( !Ver_ParseSkipComments( pMan ) )
+            return 0;
+        // get new word
+        pWord = Ver_ParseGetName( pMan );
+        if ( pWord == NULL )
+            return 0;
+    }
+
+    // convert from the blackbox into the network with local functions representated by AIGs
+    if ( pNtk->ntkFunc == ABC_FUNC_BLACKBOX )
+    {
+        if ( Abc_NtkNodeNum(pNtk) > 0 || Abc_NtkBoxNum(pNtk) > 0 )
+        {
+            if ( !Ver_ParseConvertNetwork( pMan, pNtk, pMan->fMapped ) )
+                return 0;
+        }
+        else
+        {
+            Abc_Obj_t * pObj, * pBox, * pTerm;
+            int i; 
+            pBox = Abc_NtkCreateBlackbox(pNtk);
+            Abc_NtkForEachPi( pNtk, pObj, i )
+            {
+                pTerm = Abc_NtkCreateBi(pNtk);
+                Abc_ObjAddFanin( pTerm, Abc_ObjFanout0(pObj) );
+                Abc_ObjAddFanin( pBox, pTerm );
+            }
+            Abc_NtkForEachPo( pNtk, pObj, i )
+            {
+                pTerm = Abc_NtkCreateBo(pNtk);
+                Abc_ObjAddFanin( pTerm, pBox );
+                Abc_ObjAddFanin( Abc_ObjFanin0(pObj), pTerm );
+            }
+        }
+    }
+
+    // remove the table if needed
+    Ver_ParseRemoveSuffixTable( pMan );
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Lookups the suffix of the signal of the form [m:n].]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseLookupSuffix( Ver_Man_t * pMan, char * pWord, int * pnMsb, int * pnLsb )
+{
+    unsigned Value;
+    *pnMsb = *pnLsb = -1;
+    if ( pMan->tName2Suffix == NULL )
+        return 1;
+    if ( !st_lookup( pMan->tName2Suffix, (char *)pWord, (char **)&Value ) )
+        return 1;
+    *pnMsb = (Value >> 8) & 0xff;
+    *pnLsb = Value & 0xff;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Lookups the suffix of the signal of the form [m:n].]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseInsertsSuffix( Ver_Man_t * pMan, char * pWord, int nMsb, int nLsb )
+{
+    unsigned Value;
+    if ( pMan->tName2Suffix == NULL )
+        pMan->tName2Suffix = st_init_table( strcmp, st_strhash );
+    if ( st_is_member( pMan->tName2Suffix, pWord ) )
+        return 1;
+    assert( nMsb >= 0 && nMsb < 128 );
+    assert( nLsb >= 0 && nLsb < 128 );
+    Value = (nMsb << 8) | nLsb;
+    st_insert( pMan->tName2Suffix, Extra_UtilStrsav(pWord), (char *)Value );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Lookups the suffic of the signal of the form [m:n].]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ver_ParseRemoveSuffixTable( Ver_Man_t * pMan )
+{
+    st_generator * gen;
+    char * pKey, * pValue;
+    if ( pMan->tName2Suffix == NULL )
+        return;
+    st_foreach_item( pMan->tName2Suffix, gen, (char **)&pKey, (char **)&pValue )
+        free( pKey );
+    st_free_table( pMan->tName2Suffix );
+    pMan->tName2Suffix = NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Determine signal prefix of the form [Beg:End].]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseSignalPrefix( Ver_Man_t * pMan, char ** ppWord, int * pnMsb, int * pnLsb )
+{
+    char * pWord = *ppWord;
+    int nMsb, nLsb;
+    assert( pWord[0] == '[' );
+    // get the beginning
+    nMsb = atoi( pWord + 1 );
+    // find the splitter
+    while ( *pWord && *pWord != ':' && *pWord != ']' )
+        pWord++;
+    if ( *pWord == 0 )
+    {
+        sprintf( pMan->sError, "Cannot find closing bracket in this line." );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+    if ( *pWord == ']' )
+        nLsb = nMsb;
+    else
+    {
+        assert( *pWord == ':' );
+        nLsb = atoi( pWord + 1 );
+        // find the closing paranthesis
+        while ( *pWord && *pWord != ']' )
+            pWord++;
+        if ( *pWord == 0 )
+        {
+            sprintf( pMan->sError, "Cannot find closing bracket in this line." );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+        assert( *pWord == ']' );
+        pWord++;
+    }
+    assert( nMsb >= 0 && nLsb >= 0 );
+    // return
+    *ppWord = pWord;
+    *pnMsb = nMsb;
+    *pnLsb = nLsb;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Determine signal suffix of the form [m:n].]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseSignalSuffix( Ver_Man_t * pMan, char * pWord, int * pnMsb, int * pnLsb )
+{
+    char * pCur;
+    int Length;
+    Length = strlen(pWord);
+    assert( pWord[Length-1] == ']' );
+    // walk backward
+    for ( pCur = pWord + Length - 2; pCur != pWord; pCur-- )
+        if ( *pCur == ':' || *pCur == '[' )
+            break;
+    if ( pCur == pWord )
+    {
+        sprintf( pMan->sError, "Cannot find opening bracket in signal name %s.", pWord );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+    if ( *pCur == '[' )
+    {
+        *pnMsb = *pnLsb = atoi(pCur+1);
+        *pCur = 0;
+        return 1;
+    }
+    assert( *pCur == ':' );
+    // get the end of the interval
+    *pnLsb = atoi(pCur+1);
+    // find the beginning
+    for ( pCur = pWord + Length - 2; pCur != pWord; pCur-- )
+        if ( *pCur == '[' )
+            break;
+    if ( pCur == pWord )
+    {
+        sprintf( pMan->sError, "Cannot find opening bracket in signal name %s.", pWord );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+    assert( *pCur == '[' );
+    // get the beginning of the interval
+    *pnMsb = atoi(pCur+1);
+    // cut the word
+    *pCur = 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the values of constant bits.]
+
+  Description [The resulting bits are in MSB to LSB order.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseConstant( Ver_Man_t * pMan, char * pWord )
+{
+    int nBits, i;
+    assert( pWord[0] >= '1' && pWord[1] <= '9' );
+    nBits = atoi(pWord);
+    // find the next symbol \'
+    while ( *pWord && *pWord != '\'' )
+        pWord++;
+    if ( *pWord == 0 )
+    {
+        sprintf( pMan->sError, "Cannot find symbol \' in the constant." );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+    assert( *pWord == '\'' );
+    pWord++;
+    if ( *pWord != 'b' )
+    {
+        sprintf( pMan->sError, "Currently can only handle binary constants." );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+    pWord++;
+    // scan the bits
+    Vec_PtrClear( pMan->vNames );
+    for ( i = 0; i < nBits; i++ )
+    {
+      if ( pWord[i] != '0' && pWord[i] != '1' && pWord[i] != 'x' )
+      {
+         sprintf( pMan->sError, "Having problem parsing the binary constant." );
+         Ver_ParsePrintErrorMessage( pMan );
+         return 0;
+      }
+      if ( pWord[i] == 'x' ) 
+          Vec_PtrPush( pMan->vNames, (void *)0 );
+      else 
+          Vec_PtrPush( pMan->vNames, (void *)(pWord[i]-'0') );
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Parses one directive.]
+
+  Description [The signals are added in the order from LSB to MSB.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseSignal( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_SignalType_t SigType )
+{
+    Ver_Stream_t * p = pMan->pReader;
+    char Buffer[1000], Symbol, * pWord;
+    int nMsb, nLsb, Bit, Limit, i;
+    nMsb = nLsb = -1;
+    while ( 1 )
+    {
+        // get the next word
+        pWord = Ver_ParseGetName( pMan );
+        if ( pWord == NULL )
+            return 0;
+
+        // check if the range is specified
+        if ( pWord[0] == '[' && !pMan->fNameLast )
+        {
+            assert( nMsb == -1 && nLsb == -1 );
+            Ver_ParseSignalPrefix( pMan, &pWord, &nMsb, &nLsb );
+            // check the case when there is space between bracket and the next word
+            if ( *pWord == 0 )
+            {
+                // get the signal name
+                pWord = Ver_ParseGetName( pMan );
+                if ( pWord == NULL )
+                    return 0;
+            }
+        }
+
+        // create signals
+        if ( nMsb == -1 && nLsb == -1 )
+        {
+            if ( SigType == VER_SIG_INPUT || SigType == VER_SIG_INOUT )
+                Ver_ParseCreatePi( pNtk, pWord );
+            if ( SigType == VER_SIG_OUTPUT || SigType == VER_SIG_INOUT )
+                Ver_ParseCreatePo( pNtk, pWord );
+            if ( SigType == VER_SIG_WIRE || SigType == VER_SIG_REG )
+                Abc_NtkFindOrCreateNet( pNtk, pWord );
+        }
+        else
+        {
+            assert( nMsb >= 0 && nLsb >= 0 );
+            // add to the hash table
+            Ver_ParseInsertsSuffix( pMan, pWord, nMsb, nLsb );
+            // add signals from Lsb to Msb
+            Limit = nMsb > nLsb? nMsb - nLsb + 1: nLsb - nMsb + 1;
+            for ( i = 0, Bit = nLsb; i < Limit; i++, Bit = nMsb > nLsb ? Bit + 1: Bit - 1  )
+            {
+                sprintf( Buffer, "%s[%d]", pWord, Bit );
+                if ( SigType == VER_SIG_INPUT || SigType == VER_SIG_INOUT )
+                    Ver_ParseCreatePi( pNtk, Buffer );
+                if ( SigType == VER_SIG_OUTPUT || SigType == VER_SIG_INOUT )
+                    Ver_ParseCreatePo( pNtk, Buffer );
+                if ( SigType == VER_SIG_WIRE || SigType == VER_SIG_REG )
+                    Abc_NtkFindOrCreateNet( pNtk, Buffer );
+            }
+        }
+
+        Symbol = Ver_StreamPopChar(p);
+        if ( Symbol == ',' )
+            continue;
+        if ( Symbol == ';' )
+            return 1;
+        break;
+    }
+    sprintf( pMan->sError, "Cannot parse signal line (expected , or ;)." );
+    Ver_ParsePrintErrorMessage( pMan );
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Parses one directive.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseAlways( Ver_Man_t * pMan, Abc_Ntk_t * pNtk )
+{
+    Ver_Stream_t * p = pMan->pReader;
+    Abc_Obj_t * pNet, * pNet2;
+    int fStopAfterOne;
+    char * pWord, * pWord2;
+    char Symbol;
+    // parse the directive 
+    pWord = Ver_ParseGetName( pMan );
+    if ( pWord == NULL )
+        return 0;
+    if ( pWord[0] == '@' )
+    {
+        Ver_StreamSkipToChars( p, ")" );
+        Ver_StreamPopChar(p);
+        // parse the directive 
+        pWord = Ver_ParseGetName( pMan );
+        if ( pWord == NULL )
+            return 0;
+    }
+    // decide how many statements to parse
+    fStopAfterOne = 0;
+    if ( strcmp( pWord, "begin" ) )
+        fStopAfterOne = 1;
+    // iterate over the initial states
+    while ( 1 )
+    {
+        if ( !fStopAfterOne )
+        {
+            // get the name of the output signal
+            pWord = Ver_ParseGetName( pMan );
+            if ( pWord == NULL )
+                return 0;
+            // look for the end of directive
+            if ( !strcmp( pWord, "end" ) )
+                break;
+        }
+        // get the fanout net
+        pNet = Ver_ParseFindNet( pNtk, pWord );
+        if ( pNet == NULL )
+        {
+            sprintf( pMan->sError, "Cannot read the always statement for %s (output wire is not defined).", pWord );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+        // get the equality sign
+        Symbol = Ver_StreamPopChar(p);
+        if ( Symbol != '<' && Symbol != '=' )
+        {
+            sprintf( pMan->sError, "Cannot read the assign statement for %s (expected <= or =).", pWord );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+        if ( Symbol == '<' )
+            Ver_StreamPopChar(p);
+        // skip the comments
+        if ( !Ver_ParseSkipComments( pMan ) )
+            return 0;
+        // get the second name
+        pWord2 = Ver_ParseGetName( pMan );
+        if ( pWord2 == NULL )
+            return 0;
+        // check if the name is complemented
+        if ( pWord2[0] == '~' )
+        {
+            pNet2 = Ver_ParseFindNet( pNtk, pWord2+1 );
+            pNet2 = Ver_ParseCreateInv( pNtk, pNet2 );
+        }
+        else
+            pNet2 = Ver_ParseFindNet( pNtk, pWord2 );
+        if ( pNet2 == NULL )
+        {
+            sprintf( pMan->sError, "Cannot read the always statement for %s (input wire is not defined).", pWord2 );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+        // create the latch
+        Ver_ParseCreateLatch( pNtk, pNet2, pNet );
+        // remove the last symbol
+        Symbol = Ver_StreamPopChar(p);
+        assert( Symbol == ';' );
+        // quit if only one directive
+        if ( fStopAfterOne )
+            break;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Parses one directive.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseInitial( Ver_Man_t * pMan, Abc_Ntk_t * pNtk )
+{
+    Ver_Stream_t * p = pMan->pReader;
+    Abc_Obj_t * pNode, * pNet;
+    int fStopAfterOne;
+    char * pWord, * pEquation;
+    char Symbol;
+    // parse the directive 
+    pWord = Ver_ParseGetName( pMan );
+    if ( pWord == NULL )
+        return 0;
+    // decide how many statements to parse
+    fStopAfterOne = 0;
+    if ( strcmp( pWord, "begin" ) )
+        fStopAfterOne = 1;
+    // iterate over the initial states
+    while ( 1 )
+    {
+        if ( !fStopAfterOne )
+        {
+            // get the name of the output signal
+            pWord = Ver_ParseGetName( pMan );
+            if ( pWord == NULL )
+                return 0;
+            // look for the end of directive
+            if ( !strcmp( pWord, "end" ) )
+                break;
+        }
+        // get the fanout net
+        pNet = Ver_ParseFindNet( pNtk, pWord );
+        if ( pNet == NULL )
+        {
+            sprintf( pMan->sError, "Cannot read the initial statement for %s (output wire is not defined).", pWord );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+        // get the equality sign
+        Symbol = Ver_StreamPopChar(p);
+        if ( Symbol != '<' && Symbol != '=' )
+        {
+            sprintf( pMan->sError, "Cannot read the assign statement for %s (expected <= or =).", pWord );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+        if ( Symbol == '<' )
+            Ver_StreamPopChar(p);
+        // skip the comments
+        if ( !Ver_ParseSkipComments( pMan ) )
+            return 0;
+        // get the second name
+        pEquation = Ver_StreamGetWord( p, ";" );
+        if ( pEquation == NULL )
+            return 0;
+        // find the corresponding latch
+        if ( Abc_ObjFaninNum(pNet) == 0 )
+        {
+            sprintf( pMan->sError, "Cannot find the latch to assign the initial value." );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+        pNode = Abc_ObjFanin0(Abc_ObjFanin0(pNet));
+        assert( Abc_ObjIsLatch(pNode) );
+        // set the initial state
+        if ( !strcmp(pEquation, "0") || !strcmp(pEquation, "1\'b0") )
+            Abc_LatchSetInit0( pNode );
+        else if ( !strcmp(pEquation, "1") || !strcmp(pEquation, "1\'b1") )
+            Abc_LatchSetInit1( pNode );
+//        else if ( !strcmp(pEquation, "2") )
+//            Abc_LatchSetInitDc( pNode );
+        else 
+        {
+            sprintf( pMan->sError, "Incorrect initial value of the latch %s.", Abc_ObjName(pNet) );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+        // remove the last symbol
+        Symbol = Ver_StreamPopChar(p);
+        assert( Symbol == ';' );
+        // quit if only one directive
+        if ( fStopAfterOne )
+            break;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Parses one directive.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseAssign( Ver_Man_t * pMan, Abc_Ntk_t * pNtk )
+{
+    char Buffer[1000], Buffer2[1000];
+    Ver_Stream_t * p = pMan->pReader;
+    Abc_Obj_t * pNode, * pNet;
+    char * pWord, * pName, * pEquation;
+    Hop_Obj_t * pFunc;
+    char Symbol;
+    int i, Bit, Limit, Length, fReduction;
+    int nMsb, nLsb;
+
+//    if ( Ver_StreamGetLineNumber(p) == 2756 )
+//    {
+//        int x = 0;
+//    }
+
+    // convert from the blackbox into the network with local functions representated by AIGs
+    if ( !Ver_ParseConvertNetwork( pMan, pNtk, pMan->fMapped ) )
+        return 0;
+
+    while ( 1 )
+    {
+        // get the name of the output signal
+        pWord = Ver_ParseGetName( pMan );
+        if ( pWord == NULL )
+            return 0;
+        // check for vector-inputs
+        if ( !Ver_ParseLookupSuffix( pMan, pWord, &nMsb, &nLsb ) )
+            return 0;
+        // handle special case of constant assignment
+        if ( nMsb >= 0 && nLsb >= 0 )
+        {
+            // save the fanout name
+            strcpy( Buffer, pWord );
+            // get the equality sign
+            if ( Ver_StreamPopChar(p) != '=' )
+            {
+                sprintf( pMan->sError, "Cannot read the assign statement for %s (expected equality sign).", pWord );
+                Ver_ParsePrintErrorMessage( pMan );
+                return 0;
+            }
+            // get the constant
+            pWord = Ver_ParseGetName( pMan );
+            if ( pWord == NULL )
+                return 0;
+            // check if it is indeed a constant
+            if ( !(pWord[0] >= '0' && pWord[0] <= '9') )
+            {
+                sprintf( pMan->sError, "Currently can only assign vector-signal \"%s\" to be a constant.", Buffer );
+                Ver_ParsePrintErrorMessage( pMan );
+                return 0;
+            }
+
+            // get individual bits of the constant
+            if ( !Ver_ParseConstant( pMan, pWord ) )
+                return 0;
+            // check that the constant has the same size
+            Limit = nMsb > nLsb? nMsb - nLsb + 1: nLsb - nMsb + 1;
+            if ( Limit != Vec_PtrSize(pMan->vNames) )
+            {
+                sprintf( pMan->sError, "The constant size (%d) is different from the signal\"%s\" size (%d).", 
+                    Vec_PtrSize(pMan->vNames), Buffer, Limit );
+                Ver_ParsePrintErrorMessage( pMan );
+                return 0;
+            }
+            // iterate through the bits
+            for ( i = 0, Bit = nLsb; i < Limit; i++, Bit = nMsb > nLsb ? Bit + 1: Bit - 1  )
+            {
+                // get the fanin net
+                if ( Vec_PtrEntry( pMan->vNames, Limit-1-i ) )
+                    pNet = Ver_ParseFindNet( pNtk, "1\'b1" );
+                else
+                    pNet = Ver_ParseFindNet( pNtk, "1\'b0" );
+                assert( pNet != NULL );
+
+                // create the buffer
+                pNode = Abc_NtkCreateNodeBuf( pNtk, pNet );
+
+                // get the fanout net
+                sprintf( Buffer2, "%s[%d]", Buffer, Bit );
+                pNet = Ver_ParseFindNet( pNtk, Buffer2 );
+                if ( pNet == NULL )
+                {
+                    sprintf( pMan->sError, "Cannot read the assign statement for %s (output wire is not defined).", pWord );
+                    Ver_ParsePrintErrorMessage( pMan );
+                    return 0;
+                }
+                Abc_ObjAddFanin( pNet, pNode );
+            }
+            // go to the end of the line
+            Ver_ParseSkipComments( pMan );
+        }
+        else
+        {
+            // consider the case of reduction operations
+            fReduction = 0;
+            if ( pWord[0] == '{' && !pMan->fNameLast )
+                fReduction = 1;
+            if ( fReduction )
+            {
+                pWord++;
+                pWord[strlen(pWord)-1] = 0;
+                assert( pWord[0] != '\\' );
+            }
+            // get the fanout net
+            pNet = Ver_ParseFindNet( pNtk, pWord );
+            if ( pNet == NULL )
+            {
+                sprintf( pMan->sError, "Cannot read the assign statement for %s (output wire is not defined).", pWord );
+                Ver_ParsePrintErrorMessage( pMan );
+                return 0;
+            }
+            // get the equality sign
+            if ( Ver_StreamPopChar(p) != '=' )
+            {
+                sprintf( pMan->sError, "Cannot read the assign statement for %s (expected equality sign).", pWord );
+                Ver_ParsePrintErrorMessage( pMan );
+                return 0;
+            }
+            // skip the comments
+            if ( !Ver_ParseSkipComments( pMan ) )
+                return 0;
+            // get the second name
+            if ( fReduction )
+                pEquation = Ver_StreamGetWord( p, ";" );
+            else
+                pEquation = Ver_StreamGetWord( p, ",;" );
+            if ( pEquation == NULL )
+            {
+                sprintf( pMan->sError, "Cannot read the equation for %s.", Abc_ObjName(pNet) );
+                Ver_ParsePrintErrorMessage( pMan );
+                return 0;
+            }
+
+            // consider the case of mapped network
+            Vec_PtrClear( pMan->vNames );
+            if ( pMan->fMapped )
+            {
+                if ( !strcmp( pEquation, "1\'b0" ) )
+                    pFunc = (Hop_Obj_t *)Mio_LibraryReadConst0(Abc_FrameReadLibGen());
+                else if ( !strcmp( pEquation, "1\'b1" ) )
+                    pFunc = (Hop_Obj_t *)Mio_LibraryReadConst1(Abc_FrameReadLibGen());
+                else
+                {
+                    // "assign foo = \bar ;"
+                    if ( *pEquation == '\\' )
+                    {
+                        pEquation++;
+                        pEquation[strlen(pEquation) - 1] = 0;
+                    }
+                    if ( Ver_ParseFindNet(pNtk, pEquation) == NULL )
+                    {
+                        sprintf( pMan->sError, "Cannot read Verilog with non-trivial assignments in the mapped netlist." );
+                        Ver_ParsePrintErrorMessage( pMan );
+                        return 0;
+                    }
+                    Vec_PtrPush( pMan->vNames, (void *)strlen(pEquation) );
+                    Vec_PtrPush( pMan->vNames, pEquation );
+                    // get the buffer
+                    pFunc = (Hop_Obj_t *)Mio_LibraryReadBuf(Abc_FrameReadLibGen());
+                    if ( pFunc == NULL )
+                    {
+                        sprintf( pMan->sError, "Reading assign statement for node %s has failed because the genlib library has no buffer.", Abc_ObjName(pNet) );
+                        Ver_ParsePrintErrorMessage( pMan );
+                        return 0;
+                    }
+                }
+            }
+            else
+            {
+                if ( !strcmp(pEquation, "0") || !strcmp(pEquation, "1\'b0") || !strcmp(pEquation, "1\'bx") )
+                    pFunc = Hop_ManConst0(pNtk->pManFunc);
+                else if ( !strcmp(pEquation, "1") || !strcmp(pEquation, "1\'b1") )
+                    pFunc = Hop_ManConst1(pNtk->pManFunc);
+                else if ( fReduction )
+                    pFunc = Ver_FormulaReduction( pEquation, pNtk->pManFunc, pMan->vNames, pMan->sError );  
+                else
+                    pFunc = Ver_FormulaParser( pEquation, pNtk->pManFunc, pMan->vNames, pMan->vStackFn, pMan->vStackOp, pMan->sError );  
+                if ( pFunc == NULL )
+                {
+                    Ver_ParsePrintErrorMessage( pMan );
+                    return 0;
+                }
+            }
+
+            // create the node with the given inputs
+            pNode = Abc_NtkCreateNode( pNtk );
+            pNode->pData = pFunc;
+            Abc_ObjAddFanin( pNet, pNode );
+            // connect to fanin nets
+            for ( i = 0; i < Vec_PtrSize(pMan->vNames)/2; i++ )
+            {
+                // get the name of this signal
+                Length = (int)Vec_PtrEntry( pMan->vNames, 2*i );
+                pName  = Vec_PtrEntry( pMan->vNames, 2*i + 1 );
+                pName[Length] = 0;
+                // find the corresponding net
+                pNet = Ver_ParseFindNet( pNtk, pName );
+                if ( pNet == NULL )
+                {
+                    sprintf( pMan->sError, "Cannot read the assign statement for %s (input wire %s is not defined).", pWord, pName );
+                    Ver_ParsePrintErrorMessage( pMan );
+                    return 0;
+                }
+                Abc_ObjAddFanin( pNode, pNet );
+            }
+        }
+
+        Symbol = Ver_StreamPopChar(p);
+        if ( Symbol == ',' )
+            continue;
+        if ( Symbol == ';' )
+            return 1;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Parses one directive.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseGateStandard( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_GateType_t GateType )
+{
+    Ver_Stream_t * p = pMan->pReader;
+    Abc_Obj_t * pNet, * pNode;
+    char * pWord, Symbol;
+
+    // convert from the blackbox into the network with local functions representated by AIGs
+    if ( !Ver_ParseConvertNetwork( pMan, pNtk, pMan->fMapped ) )
+        return 0;
+
+    // this is gate name - throw it away
+    if ( Ver_StreamPopChar(p) != '(' )
+    {
+        sprintf( pMan->sError, "Cannot parse a standard gate (expected opening paranthesis)." );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+    Ver_ParseSkipComments( pMan );
+
+    // create the node
+    pNode = Abc_NtkCreateNode( pNtk );
+
+    // parse pairs of formal/actural inputs
+    while ( 1 )
+    {
+        // parse the output name
+        pWord = Ver_ParseGetName( pMan );
+        if ( pWord == NULL )
+            return 0;
+        // get the net corresponding to this output
+        pNet = Ver_ParseFindNet( pNtk, pWord );
+        if ( pNet == NULL )
+        {
+            sprintf( pMan->sError, "Net is missing in gate %s.", pWord );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+        // if this is the first net, add it as an output
+        if ( Abc_ObjFanoutNum(pNode) == 0 )
+            Abc_ObjAddFanin( pNet, pNode );
+        else
+            Abc_ObjAddFanin( pNode, pNet );
+        // check if it is the end of gate
+        Ver_ParseSkipComments( pMan );
+        Symbol = Ver_StreamPopChar(p);
+        if ( Symbol == ')' )
+            break;
+        // skip comma
+        if ( Symbol != ',' )
+        {
+            sprintf( pMan->sError, "Cannot parse a standard gate %s (expected closing paranthesis).", Abc_ObjName(Abc_ObjFanout0(pNode)) );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+        Ver_ParseSkipComments( pMan );
+    }
+    if ( (GateType == VER_GATE_BUF || GateType == VER_GATE_NOT) && Abc_ObjFaninNum(pNode) != 1 )
+    {
+        sprintf( pMan->sError, "Buffer or interver with multiple fanouts %s (currently not supported).", Abc_ObjName(Abc_ObjFanout0(pNode)) );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+
+    // check if it is the end of gate
+    Ver_ParseSkipComments( pMan );
+    if ( Ver_StreamPopChar(p) != ';' )
+    {
+        sprintf( pMan->sError, "Cannot read standard gate %s (expected closing semicolumn).", Abc_ObjName(Abc_ObjFanout0(pNode)) );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+    // add logic function
+    if ( GateType == VER_GATE_AND || GateType == VER_GATE_NAND )
+        pNode->pData = Hop_CreateAnd( pNtk->pManFunc, Abc_ObjFaninNum(pNode) );
+    else if ( GateType == VER_GATE_OR || GateType == VER_GATE_NOR )
+        pNode->pData = Hop_CreateOr( pNtk->pManFunc, Abc_ObjFaninNum(pNode) );
+    else if ( GateType == VER_GATE_XOR || GateType == VER_GATE_XNOR )
+        pNode->pData = Hop_CreateExor( pNtk->pManFunc, Abc_ObjFaninNum(pNode) );
+    else if ( GateType == VER_GATE_BUF || GateType == VER_GATE_NOT )
+        pNode->pData = Hop_CreateAnd( pNtk->pManFunc, Abc_ObjFaninNum(pNode) );
+    if ( GateType == VER_GATE_NAND || GateType == VER_GATE_NOR || GateType == VER_GATE_XNOR || GateType == VER_GATE_NOT )
+        pNode->pData = Hop_Not( pNode->pData );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Parses one directive.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseFlopStandard( Ver_Man_t * pMan, Abc_Ntk_t * pNtk )
+{
+    Ver_Stream_t * p = pMan->pReader;
+    Abc_Obj_t * pNetLi, * pNetLo, * pLatch;
+    char * pWord, Symbol;
+
+    // convert from the blackbox into the network with local functions representated by AIGs
+    if ( !Ver_ParseConvertNetwork( pMan, pNtk, pMan->fMapped ) )
+        return 0;
+
+    // this is gate name - throw it away
+    if ( Ver_StreamPopChar(p) != '(' )
+    {
+        sprintf( pMan->sError, "Cannot parse a standard gate (expected opening paranthesis)." );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+    Ver_ParseSkipComments( pMan );
+
+    // parse the output name
+    pWord = Ver_ParseGetName( pMan );
+    if ( pWord == NULL )
+        return 0;
+    // get the net corresponding to this output
+    pNetLo = Ver_ParseFindNet( pNtk, pWord );
+    if ( pNetLo == NULL )
+    {
+        sprintf( pMan->sError, "Net is missing in gate %s.", pWord );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+
+    // check if it is the end of gate
+    Ver_ParseSkipComments( pMan );
+    Symbol = Ver_StreamPopChar(p);
+    if ( Symbol == ')' )
+    {
+        sprintf( pMan->sError, "Cannot parse the flop." );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+    // skip comma
+    if ( Symbol != ',' )
+    {
+        sprintf( pMan->sError, "Cannot parse the flop." );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+    Ver_ParseSkipComments( pMan );
+
+    // parse the output name
+    pWord = Ver_ParseGetName( pMan );
+    if ( pWord == NULL )
+        return 0;
+    // get the net corresponding to this output
+    pNetLi = Ver_ParseFindNet( pNtk, pWord );
+    if ( pNetLi == NULL )
+    {
+        sprintf( pMan->sError, "Net is missing in gate %s.", pWord );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+
+    // check if it is the end of gate
+    Ver_ParseSkipComments( pMan );
+    Symbol = Ver_StreamPopChar(p);
+    if ( Symbol != ')' )
+    {
+        sprintf( pMan->sError, "Cannot parse the flop." );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+
+    // check if it is the end of gate
+    Ver_ParseSkipComments( pMan );
+    if ( Ver_StreamPopChar(p) != ';' )
+    {
+        sprintf( pMan->sError, "Cannot parse the flop." );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+
+    // create the latch
+    pLatch = Ver_ParseCreateLatch( pNtk, pNetLi, pNetLo );
+    Abc_LatchSetInit0( pLatch );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the index of the given pin the gate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_FindGateInput( Mio_Gate_t * pGate, char * pName )
+{
+    Mio_Pin_t * pGatePin;
+    int i;
+    for ( i = 0, pGatePin = Mio_GateReadPins(pGate); pGatePin != NULL; pGatePin = Mio_PinReadNext(pGatePin), i++ )
+        if ( strcmp(pName, Mio_PinReadName(pGatePin)) == 0 )
+            return i;
+    if ( strcmp(pName, Mio_GateReadOutName(pGate)) == 0 )
+        return i;
+    return -1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Parses one directive.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate )
+{
+    Ver_Stream_t * p = pMan->pReader;
+    Abc_Obj_t * pNetActual, * pNode;
+    char * pWord, Symbol;
+    int Input, i, nFanins = Mio_GateReadInputs(pGate);
+
+    // convert from the blackbox into the network with local functions representated by gates
+    if ( 1 != pMan->fMapped )
+    {
+        sprintf( pMan->sError, "The network appears to be mapped. Use \"r -m\" to read mapped Verilog." );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+
+    // update the network type if needed
+    if ( !Ver_ParseConvertNetwork( pMan, pNtk, 1 ) )
+        return 0;
+
+    // parse the directive and set the pointers to the PIs/POs of the gate
+    pWord = Ver_ParseGetName( pMan );
+    if ( pWord == NULL )
+        return 0;
+    // this is gate name - throw it away
+    if ( Ver_StreamPopChar(p) != '(' )
+    {
+        sprintf( pMan->sError, "Cannot parse gate %s (expected opening paranthesis).", Mio_GateReadName(pGate) );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+    Ver_ParseSkipComments( pMan );
+
+    // start the node
+    pNode = Abc_NtkCreateNode( pNtk );
+    pNode->pData = pGate;
+
+    // parse pairs of formal/actural inputs
+    Vec_IntClear( pMan->vPerm );
+    while ( 1 )
+    {
+        // process one pair of formal/actual parameters
+        if ( Ver_StreamPopChar(p) != '.' )
+        {
+            sprintf( pMan->sError, "Cannot parse gate %s (expected .).", Mio_GateReadName(pGate) );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+
+        // parse the formal name
+        pWord = Ver_ParseGetName( pMan );
+        if ( pWord == NULL )
+            return 0;
+
+        // find the corresponding pin of the gate
+        Input = Ver_FindGateInput( pGate, pWord );
+        if ( Input == -1 )
+        {
+            sprintf( pMan->sError, "Formal input name %s cannot be found in the gate %s.", pWord, Mio_GateReadOutName(pGate) );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+
+        // open the paranthesis
+        if ( Ver_StreamPopChar(p) != '(' )
+        {
+            sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected opening paranthesis).", pWord, Mio_GateReadName(pGate) );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+
+        // parse the actual name
+        pWord = Ver_ParseGetName( pMan );
+        if ( pWord == NULL )
+            return 0;
+        // check if the name is complemented
+        assert( pWord[0] != '~' );
+/*
+        fCompl = (pWord[0] == '~');
+        if ( fCompl )
+        {
+            fComplUsed = 1;
+            pWord++;
+            if ( pNtk->pData == NULL )
+                pNtk->pData = Extra_MmFlexStart();
+        }
+*/
+        // get the actual net
+        pNetActual = Ver_ParseFindNet( pNtk, pWord );
+        if ( pNetActual == NULL )
+        {
+            sprintf( pMan->sError, "Actual net %s is missing.", pWord );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+
+        // close the paranthesis
+        if ( Ver_StreamPopChar(p) != ')' )
+        {
+            sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected closing paranthesis).", pWord, Mio_GateReadName(pGate) );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+
+        // add the fanin
+        if ( Input < nFanins )
+        {
+            Vec_IntPush( pMan->vPerm, Input );
+            Abc_ObjAddFanin( pNode, pNetActual ); // fanin
+        }
+        else
+            Abc_ObjAddFanin( pNetActual, pNode ); // fanout
+
+        // check if it is the end of gate
+        Ver_ParseSkipComments( pMan );
+        Symbol = Ver_StreamPopChar(p);
+        if ( Symbol == ')' )
+            break;
+
+        // skip comma
+        if ( Symbol != ',' )
+        {
+            sprintf( pMan->sError, "Cannot formal parameter %s of gate %s (expected closing paranthesis).", pWord, Mio_GateReadName(pGate) );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+        Ver_ParseSkipComments( pMan );
+    }
+
+    // check that the gate as the same number of input
+    if ( !(Abc_ObjFaninNum(pNode) == nFanins && Abc_ObjFanoutNum(pNode) == 1) )
+    {
+        sprintf( pMan->sError, "Parsing of gate %s has failed.", Mio_GateReadName(pGate) );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+
+    // check if it is the end of gate
+    Ver_ParseSkipComments( pMan );
+    if ( Ver_StreamPopChar(p) != ';' )
+    {
+        sprintf( pMan->sError, "Cannot read gate %s (expected closing semicolumn).", Mio_GateReadName(pGate) );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+    
+    // check if we need to permute the inputs
+    Vec_IntForEachEntry( pMan->vPerm, Input, i )
+        if ( Input != i )
+            break;
+    if ( i < Vec_IntSize(pMan->vPerm) )
+    {
+        // add the fanin numnbers to the end of the permuation array
+        for ( i = 0; i < nFanins; i++ )
+            Vec_IntPush( pMan->vPerm, Abc_ObjFaninId(pNode, i) );
+        // write the fanin numbers into their corresponding places (according to the gate) 
+        for ( i = 0; i < nFanins; i++ )
+            Vec_IntWriteEntry( &pNode->vFanins, Vec_IntEntry(pMan->vPerm, i), Vec_IntEntry(pMan->vPerm, i+nFanins) );
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Parses one directive.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox )
+{
+    char Buffer[1000];
+    Ver_Stream_t * p = pMan->pReader;
+    Ver_Bundle_t * pBundle;
+    Vec_Ptr_t * vBundles;
+    Abc_Obj_t * pNetActual; 
+    Abc_Obj_t * pNode;
+    char * pWord, Symbol;
+    int fCompl, fFormalIsGiven;
+    int i, k, Bit, Limit, nMsb, nLsb, fQuit, flag;
+
+    // gate the name of the box
+    pWord = Ver_ParseGetName( pMan );
+    if ( pWord == NULL )
+        return 0;
+
+    // create a box with this name
+    pNode = Abc_NtkCreateBlackbox( pNtk );
+    pNode->pData = pNtkBox;
+    Abc_ObjAssignName( pNode, pWord, NULL );
+
+    // continue parsing the box
+    if ( Ver_StreamPopChar(p) != '(' )
+    {
+        sprintf( pMan->sError, "Cannot parse box %s (expected opening paranthesis).", Abc_ObjName(pNode) );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+    Ver_ParseSkipComments( pMan );
+ 
+    // parse pairs of formal/actual inputs
+    vBundles = Vec_PtrAlloc( 16 );
+    pNode->pCopy = (Abc_Obj_t *)vBundles;
+    while ( 1 )
+    {
+/*
+        if ( Ver_StreamGetLineNumber(pMan->pReader) == 5967 )
+        {
+           int x = 0;
+        }
+*/
+        // allocate the bundle (formal name + array of actual nets)
+        pBundle = ALLOC( Ver_Bundle_t, 1 );
+        pBundle->pNameFormal = NULL;
+        pBundle->vNetsActual = Vec_PtrAlloc( 4 );
+        Vec_PtrPush( vBundles, pBundle );
+
+        // process one pair of formal/actual parameters
+        fFormalIsGiven = 0;
+        if ( Ver_StreamScanChar(p) == '.' )
+        {
+            fFormalIsGiven = 1;
+            if ( Ver_StreamPopChar(p) != '.' )
+            {
+                sprintf( pMan->sError, "Cannot parse box %s (expected .).", Abc_ObjName(pNode) );
+                Ver_ParsePrintErrorMessage( pMan );
+                return 0;
+            }
+
+            // parse the formal name
+            pWord = Ver_ParseGetName( pMan );
+            if ( pWord == NULL )
+                return 0;
+
+            // save the name
+            pBundle->pNameFormal = Extra_UtilStrsav( pWord );
+
+            // open the paranthesis
+            if ( Ver_StreamPopChar(p) != '(' )
+            {
+                sprintf( pMan->sError, "Cannot formal parameter %s of box %s (expected opening paranthesis).", pWord, Abc_ObjName(pNode));
+                Ver_ParsePrintErrorMessage( pMan );
+                return 0;
+            }
+            Ver_ParseSkipComments( pMan );
+        }
+
+        // check if this is the beginning of {} expression
+        Symbol = Ver_StreamScanChar(p);
+
+        // consider the case of vector-inputs
+        if ( Symbol == '{' )
+        {
+            // skip this char
+            Ver_StreamPopChar(p);
+
+            // read actual names
+            i = 0;
+            fQuit = 0;
+            while ( 1 )
+            {
+                // parse the formal name
+                Ver_ParseSkipComments( pMan );
+                pWord = Ver_ParseGetName( pMan );
+                if ( pWord == NULL )
+                    return 0;
+
+                // check if the last char is a closing brace
+                if ( pWord[strlen(pWord)-1] == '}' )
+                {
+                    pWord[strlen(pWord)-1] = 0;
+                    fQuit = 1;
+                }
+                if ( pWord[0] == 0 )
+                    break;
+
+                // check for constant
+                if ( pWord[0] >= '1' && pWord[0] <= '9' )
+                {
+                    if ( !Ver_ParseConstant( pMan, pWord ) )
+                        return 0;
+                    // add constant MSB to LSB
+                    for ( k = 0; k < Vec_PtrSize(pMan->vNames); k++, i++ )
+                    {
+                        // get the actual net
+                        sprintf( Buffer, "1\'b%d", (int)(Vec_PtrEntry(pMan->vNames,k) != NULL) );
+                        pNetActual = Ver_ParseFindNet( pNtk, Buffer );
+                        if ( pNetActual == NULL )
+                        {
+                            sprintf( pMan->sError, "Actual net \"%s\" is missing in gate \"%s\".", Buffer, Abc_ObjName(pNode) );
+                            Ver_ParsePrintErrorMessage( pMan );
+                            return 0;
+                        }
+                        Vec_PtrPush( pBundle->vNetsActual, pNetActual );
+                    }
+                }
+                else
+                {
+                    // get the suffix of the form [m:n]
+                    if ( pWord[strlen(pWord)-1] == ']' && !pMan->fNameLast )
+                        Ver_ParseSignalSuffix( pMan, pWord, &nMsb, &nLsb );
+                    else
+                        Ver_ParseLookupSuffix( pMan, pWord, &nMsb, &nLsb );
+
+                    // generate signals
+                    if ( nMsb == -1 && nLsb == -1 )
+                    {
+                        // get the actual net
+                        pNetActual = Ver_ParseFindNet( pNtk, pWord );
+                        if ( pNetActual == NULL )
+                        {
+                            if ( !strncmp(pWord, "Open_", 5) ||
+                                !strncmp(pWord, "dct_unconnected", 15) ) 
+                                pNetActual = Abc_NtkCreateNet( pNtk );
+                            else
+                            {
+                                sprintf( pMan->sError, "Actual net \"%s\" is missing in box \"%s\".", pWord, Abc_ObjName(pNode) );
+                                Ver_ParsePrintErrorMessage( pMan );
+                                return 0;
+                            }
+                        }
+                        Vec_PtrPush( pBundle->vNetsActual, pNetActual );
+                        i++;
+                    }
+                    else
+                    {
+                        // go from MSB to LSB
+                        assert( nMsb >= 0 && nLsb >= 0 );
+                        Limit = (nMsb > nLsb) ? nMsb - nLsb + 1: nLsb - nMsb + 1;  
+                        for ( Bit = nMsb, k = Limit - 1; k >= 0; Bit = (nMsb > nLsb ? Bit - 1: Bit + 1), k--, i++ )
+                        {
+                            // get the actual net
+                            sprintf( Buffer, "%s[%d]", pWord, Bit );
+                            pNetActual = Ver_ParseFindNet( pNtk, Buffer );
+                            if ( pNetActual == NULL )
+                            {
+                                if ( !strncmp(pWord, "Open_", 5) ||
+                                    !strncmp(pWord, "dct_unconnected", 15) ) 
+                                    pNetActual = Abc_NtkCreateNet( pNtk );
+                                else
+                                {
+                                    sprintf( pMan->sError, "Actual net \"%s\" is missing in box \"%s\".", pWord, Abc_ObjName(pNode) );
+                                    Ver_ParsePrintErrorMessage( pMan );
+                                    return 0;
+                                }
+                            }
+                            Vec_PtrPush( pBundle->vNetsActual, pNetActual );
+                        }
+                    }
+                }
+
+                if ( fQuit )
+                    break;
+
+                // skip comma
+                Ver_ParseSkipComments( pMan );
+                Symbol = Ver_StreamPopChar(p);
+                if ( Symbol == '}' )
+                    break;
+                if ( Symbol != ',' )
+                {
+                    sprintf( pMan->sError, "Cannot parse formal parameter %s of gate %s (expected comma).", pWord, Abc_ObjName(pNode) );
+                    Ver_ParsePrintErrorMessage( pMan );
+                    return 0;
+                }
+            }
+        }
+        else
+        {
+            // get the next word
+            pWord = Ver_ParseGetName( pMan );
+            if ( pWord == NULL )
+                return 0;
+            // consider the case of empty name
+            fCompl = 0;
+            if ( pWord[0] == 0 )
+            {
+                pNetActual = Abc_NtkCreateNet( pNtk );
+                Vec_PtrPush( pBundle->vNetsActual, Abc_ObjNotCond( pNetActual, fCompl ) );
+            }
+            else
+            {
+                // get the actual net
+                flag=0;
+                pNetActual = Ver_ParseFindNet( pNtk, pWord );
+                if ( pNetActual == NULL ) 
+                {
+                    Ver_ParseLookupSuffix( pMan, pWord, &nMsb, &nLsb );
+                    if ( nMsb == -1 && nLsb == -1 ) 
+                    {
+                        Ver_ParseSignalSuffix( pMan, pWord, &nMsb, &nLsb );
+                        if ( nMsb == -1 && nLsb == -1 ) 
+                        {
+                            if ( !strncmp(pWord, "Open_", 5) ||
+                                !strncmp(pWord, "dct_unconnected", 15) ) 
+                            {
+                                pNetActual = Abc_NtkCreateNet( pNtk );
+                                Vec_PtrPush( pBundle->vNetsActual, pNetActual );
+                            } 
+                            else 
+                            {
+                                sprintf( pMan->sError, "Actual net \"%s\" is missing in box \"%s\".", pWord, Abc_ObjName(pNode) );
+                                Ver_ParsePrintErrorMessage( pMan );
+                                return 0;
+                            }
+                        } 
+                        else 
+                        {
+                            flag=1;
+                        }
+                    } 
+                    else 
+                    {
+                        flag=1;
+                    }
+                    if (flag) 
+                    {
+                        Limit = (nMsb > nLsb) ? nMsb - nLsb + 1: nLsb - nMsb + 1;  
+                        for ( Bit = nMsb, k = Limit - 1; k >= 0; Bit = (nMsb > nLsb ? Bit - 1: Bit + 1), k--)
+                        {
+                            // get the actual net
+                            sprintf( Buffer, "%s[%d]", pWord, Bit );
+                            pNetActual = Ver_ParseFindNet( pNtk, Buffer );
+                            if ( pNetActual == NULL )
+                            {
+                                if ( !strncmp(pWord, "Open_", 5) ||
+                                    !strncmp(pWord, "dct_unconnected", 15)) 
+                                    pNetActual = Abc_NtkCreateNet( pNtk );
+                                else
+                                {
+                                    sprintf( pMan->sError, "Actual net \"%s\" is missing in box \"%s\".", pWord, Abc_ObjName(pNode) );
+                                    Ver_ParsePrintErrorMessage( pMan );
+                                    return 0;
+                                }
+                            }
+                            Vec_PtrPush( pBundle->vNetsActual, pNetActual );
+                        }
+                    }
+                } 
+                else 
+                {
+                    Vec_PtrPush( pBundle->vNetsActual, Abc_ObjNotCond( pNetActual, fCompl ) );
+                }
+            }
+        }
+
+        if ( fFormalIsGiven )
+        {
+            // close the paranthesis
+            Ver_ParseSkipComments( pMan );
+            if ( Ver_StreamPopChar(p) != ')' )
+            {
+                sprintf( pMan->sError, "Cannot parse formal parameter %s of box %s (expected closing paranthesis).", pWord, Abc_ObjName(pNode) );
+                Ver_ParsePrintErrorMessage( pMan );
+                return 0;
+            }
+            Ver_ParseSkipComments( pMan );
+        }
+
+        // check if it is the end of gate
+        Symbol = Ver_StreamPopChar(p);
+        if ( Symbol == ')' )
+            break;
+        // skip comma
+        if ( Symbol != ',' )
+        {
+            sprintf( pMan->sError, "Cannot parse formal parameter %s of box %s (expected comma).", pWord, Abc_ObjName(pNode) );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+        Ver_ParseSkipComments( pMan );
+    }
+
+    // check if it is the end of gate
+    Ver_ParseSkipComments( pMan );
+    if ( Ver_StreamPopChar(p) != ';' )
+    {
+        sprintf( pMan->sError, "Cannot read box %s (expected closing semicolumn).", Abc_ObjName(pNode) );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Connects one box to the network]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ver_ParseFreeBundle( Ver_Bundle_t * pBundle )
+{
+    FREE( pBundle->pNameFormal );
+    Vec_PtrFree( pBundle->vNetsActual );
+    free( pBundle );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Connects one box to the network]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseConnectBox( Ver_Man_t * pMan, Abc_Obj_t * pBox )
+{
+    Vec_Ptr_t * vBundles = (Vec_Ptr_t *)pBox->pCopy;
+    Abc_Ntk_t * pNtk = pBox->pNtk;
+    Abc_Ntk_t * pNtkBox = pBox->pData;
+    Abc_Obj_t * pTerm, * pTermNew, * pNetAct;
+    Ver_Bundle_t * pBundle;
+    char * pNameFormal;
+    int i, k, j, iBundle, Length;
+
+    assert( !Ver_ObjIsConnected(pBox) );
+    assert( Ver_NtkIsDefined(pNtkBox) );
+    assert( !Abc_NtkHasBlackbox(pNtkBox) || Abc_NtkBoxNum(pNtkBox) == 1 );
+/*
+    // clean the PI/PO nets
+    Abc_NtkForEachPi( pNtkBox, pTerm, i )
+        Abc_ObjFanout0(pTerm)->pCopy = NULL;
+    Abc_NtkForEachPo( pNtkBox, pTerm, i )
+        Abc_ObjFanin0(pTerm)->pCopy = NULL;
+*/
+    // check if some of them do not have formal names
+    Vec_PtrForEachEntry( vBundles, pBundle, k )
+        if ( pBundle->pNameFormal == NULL )
+            break;
+    if ( k < Vec_PtrSize(vBundles) )
+    {
+        printf( "Warning: The instance %s of network %s will be connected without using formal names.\n", pNtkBox->pName, Abc_ObjName(pBox) );
+        // add all actual nets in the bundles
+        iBundle = 0;
+        Vec_PtrForEachEntry( vBundles, pBundle, j )
+            iBundle += Vec_PtrSize(pBundle->vNetsActual);
+
+        // check the number of actual nets is the same as the number of formal nets
+        if ( iBundle != Abc_NtkPiNum(pNtkBox) + Abc_NtkPoNum(pNtkBox) )
+        {
+            sprintf( pMan->sError, "The number of actual IOs (%d) is different from the number of formal IOs (%d) when instantiating network %s in box %s.", 
+                Vec_PtrSize(vBundles), Abc_NtkPiNum(pNtkBox) + Abc_NtkPoNum(pNtkBox), pNtkBox->pName, Abc_ObjName(pBox) );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+        // connect bundles in the natural order
+        iBundle = 0;
+        Abc_NtkForEachPi( pNtkBox, pTerm, i )
+        {
+            pBundle = Vec_PtrEntry( vBundles, iBundle++ );
+            // the bundle is found - add the connections - using order LSB to MSB
+            Vec_PtrForEachEntryReverse( pBundle->vNetsActual, pNetAct, k )
+            {
+                pTermNew = Abc_NtkCreateBi( pNtk );
+                Abc_ObjAddFanin( pBox, pTermNew );
+                Abc_ObjAddFanin( pTermNew, pNetAct );
+                i++;
+            }
+            i--;
+        }
+        // create fanins of the box
+        Abc_NtkForEachPo( pNtkBox, pTerm, i )
+        {
+            pBundle = Vec_PtrEntry( vBundles, iBundle++ );
+            // the bundle is found - add the connections - using order LSB to MSB
+            Vec_PtrForEachEntryReverse( pBundle->vNetsActual, pNetAct, k )
+            {
+                pTermNew = Abc_NtkCreateBo( pNtk );
+                Abc_ObjAddFanin( pTermNew, pBox );
+                Abc_ObjAddFanin( pNetAct, pTermNew );
+                i++;
+            }
+            i--;
+        }
+
+        // free the bundling
+        Vec_PtrForEachEntry( vBundles, pBundle, k )
+            Ver_ParseFreeBundle( pBundle );
+        Vec_PtrFree( vBundles );
+        pBox->pCopy = NULL;
+        return 1;
+    }
+
+    // bundles arrive in any order - but inside each bundle the order is MSB to LSB
+    // make sure every formal PI has a corresponding net
+    Abc_NtkForEachPi( pNtkBox, pTerm, i )
+    {
+        // get the name of this formal net
+        pNameFormal = Abc_ObjName( Abc_ObjFanout0(pTerm) );
+        // try to find the bundle with this formal net
+        pBundle = NULL;
+        Vec_PtrForEachEntry( vBundles, pBundle, k )
+            if ( !strcmp(pBundle->pNameFormal, pNameFormal) )
+                break;
+        assert( pBundle != NULL );
+        // if the bundle is not found, try without parantheses
+        if ( k == Vec_PtrSize(vBundles) )
+        {
+            pBundle = NULL;
+            Length = strlen(pNameFormal);
+            if ( pNameFormal[Length-1] == ']' )
+            {
+                // find the opening brace
+                for ( Length--; Length >= 0; Length-- )
+                    if ( pNameFormal[Length] == '[' )
+                        break;
+                // compare names before brace
+                if ( Length > 0 )
+                {
+                    Vec_PtrForEachEntry( vBundles, pBundle, j )
+                        if ( !strncmp(pBundle->pNameFormal, pNameFormal, Length) )
+                            break;
+                    if ( j == Vec_PtrSize(vBundles) )
+                        pBundle = NULL;
+                }
+            }
+            if ( pBundle == NULL )
+            {
+                sprintf( pMan->sError, "Cannot find an actual net for the formal net %s when instantiating network %s in box %s.", 
+                    pNameFormal, pNtkBox->pName, Abc_ObjName(pBox) );
+                Ver_ParsePrintErrorMessage( pMan );
+                return 0;
+            }
+        }
+        // the bundle is found - add the connections - using order LSB to MSB
+        Vec_PtrForEachEntryReverse( pBundle->vNetsActual, pNetAct, k )
+        {
+            pTermNew = Abc_NtkCreateBi( pNtk );
+            Abc_ObjAddFanin( pBox, pTermNew );
+            Abc_ObjAddFanin( pTermNew, pNetAct );
+            i++;
+        }
+        i--;
+    }
+
+    // connect those formal POs that do have nets
+    Abc_NtkForEachPo( pNtkBox, pTerm, i )
+    {
+        // get the name of this PI
+        pNameFormal = Abc_ObjName( Abc_ObjFanin0(pTerm) );
+        // try to find this formal net in the bundle
+        pBundle = NULL;
+        Vec_PtrForEachEntry( vBundles, pBundle, k )
+            if ( !strcmp(pBundle->pNameFormal, pNameFormal) )
+                break;
+        assert( pBundle != NULL );
+        // if the name is not found, try without parantheses
+        if ( k == Vec_PtrSize(vBundles) )
+        {
+            pBundle = NULL;
+            Length = strlen(pNameFormal);
+            if ( pNameFormal[Length-1] == ']' )
+            {
+                // find the opening brace
+                for ( Length--; Length >= 0; Length-- )
+                    if ( pNameFormal[Length] == '[' )
+                        break;
+                // compare names before brace
+                if ( Length > 0 )
+                {
+                    Vec_PtrForEachEntry( vBundles, pBundle, j )
+                        if ( !strncmp(pBundle->pNameFormal, pNameFormal, Length) )
+                            break;
+                    if ( j == Vec_PtrSize(vBundles) )
+                        pBundle = NULL;
+                }
+            }
+            if ( pBundle == NULL )
+            {
+//                printf( "Warning: The formal output %s is not driven when instantiating network %s in box %s.", 
+//                    pNameFormal, pNtkBox->pName, Abc_ObjName(pBox) );
+                continue;
+            }
+        }
+        // the bundle is found - add the connections
+        Vec_PtrForEachEntryReverse( pBundle->vNetsActual, pNetAct, k )
+        {
+            if ( !strcmp(Abc_ObjName(pNetAct), "1\'b0") || !strcmp(Abc_ObjName(pNetAct), "1\'b1") )
+            {
+                sprintf( pMan->sError, "It looks like formal output %s is driving a constant net (%s) when instantiating network %s in box %s.", 
+                    pBundle->pNameFormal, Abc_ObjName(pNetAct), pNtkBox->pName, Abc_ObjName(pBox) );
+                Ver_ParsePrintErrorMessage( pMan );
+                return 0;
+            }
+            pTermNew = Abc_NtkCreateBo( pNtk );
+            Abc_ObjAddFanin( pTermNew, pBox );
+            Abc_ObjAddFanin( pNetAct, pTermNew );
+            i++;
+        }
+        i--;
+    }
+
+    // free the bundling
+    Vec_PtrForEachEntry( vBundles, pBundle, k )
+        Ver_ParseFreeBundle( pBundle );
+    Vec_PtrFree( vBundles );
+    pBox->pCopy = NULL;
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Connects the defined boxes.]
+
+  Description [Returns 2 if there are any undef boxes.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseConnectDefBoxes( Ver_Man_t * pMan )
+{
+    Abc_Ntk_t * pNtk;
+    Abc_Obj_t * pBox;
+    int i, k, RetValue = 1;
+    // go through all the modules
+    Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
+    {
+        // go through all the boxes of this module
+        Abc_NtkForEachBox( pNtk, pBox, k )
+        {
+            if ( Abc_ObjIsLatch(pBox) )
+                continue;
+            // skip internal boxes of the blackboxes
+            if ( pBox->pData == NULL )
+                continue;
+            // if the network is undefined, it will be connected later
+            if ( !Ver_NtkIsDefined(pBox->pData) )
+            {
+                RetValue = 2;
+                continue;
+            }
+            // connect the box
+            if ( !Ver_ParseConnectBox( pMan, pBox ) )
+                return 0;
+            // if the network is a true blackbox, skip
+            if ( Abc_NtkHasBlackbox(pBox->pData) )
+                continue;
+            // convert the box to the whitebox
+            Abc_ObjBlackboxToWhitebox( pBox );
+        }
+    }
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the undef boxes and maps them into their instances.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Ver_ParseCollectUndefBoxes( Ver_Man_t * pMan )
+{
+    Vec_Ptr_t * vUndefs;
+    Abc_Ntk_t * pNtk, * pNtkBox;
+    Abc_Obj_t * pBox;
+    int i, k;
+    // clear the module structures
+    Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
+        pNtk->pData = NULL;
+    // go through all the blackboxes
+    vUndefs = Vec_PtrAlloc( 16 );
+    Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
+    {
+        Abc_NtkForEachBlackbox( pNtk, pBox, k )
+        {
+            pNtkBox = pBox->pData;
+            if ( pNtkBox == NULL )
+                continue;
+            if ( Ver_NtkIsDefined(pNtkBox) )
+                continue;
+            if ( pNtkBox->pData == NULL )
+            {
+                // save the box
+                Vec_PtrPush( vUndefs, pNtkBox );
+                pNtkBox->pData = Vec_PtrAlloc( 16 );
+            }
+            // save the instance
+            Vec_PtrPush( pNtkBox->pData, pBox );
+        }
+    }
+    return vUndefs;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reports how many times each type of undefined box occurs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ver_ParseReportUndefBoxes( Ver_Man_t * pMan )
+{
+    Abc_Ntk_t * pNtk;
+    Abc_Obj_t * pBox;
+    int i, k, nBoxes;
+    // clean 
+    nBoxes = 0;
+    Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
+    {
+        pNtk->fHiePath = 0;
+        if ( !Ver_NtkIsDefined(pNtk) )
+            nBoxes++;
+    }
+    // count
+    Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
+        Abc_NtkForEachBlackbox( pNtk, pBox, k )
+            if ( pBox->pData && !Ver_NtkIsDefined(pBox->pData) )
+                ((Abc_Ntk_t *)pBox->pData)->fHiePath++;
+    // print the stats
+    printf( "Warning: The design contains %d undefined objects interpreted as blackboxes:\n", nBoxes );
+    Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
+        if ( !Ver_NtkIsDefined(pNtk) )
+            printf( "%s (%d)  ", Abc_NtkName(pNtk), pNtk->fHiePath );
+    printf( "\n" );
+    // clean 
+    Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
+        pNtk->fHiePath = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if there are non-driven nets.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseCheckNondrivenNets( Vec_Ptr_t * vUndefs )
+{
+    Abc_Ntk_t * pNtk;
+    Ver_Bundle_t * pBundle;
+    Abc_Obj_t * pBox, * pNet;
+    int i, k, j, m;
+    // go through undef box types
+    Vec_PtrForEachEntry( vUndefs, pNtk, i )
+        // go through instances of this type
+        Vec_PtrForEachEntry( pNtk->pData, pBox, k )
+            // go through the bundles of this instance
+            Vec_PtrForEachEntryReverse( (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
+                // go through the actual nets of this bundle
+                if ( pBundle )
+                Vec_PtrForEachEntry( pBundle->vNetsActual, pNet, m )
+                {
+                    char * pName = Abc_ObjName(pNet);
+                    if ( Abc_ObjFaninNum(pNet) == 0 ) // non-driven
+                        if ( strcmp(Abc_ObjName(pNet), "1\'b0") && strcmp(Abc_ObjName(pNet), "1\'b1") ) // diff from a const
+                            return 1;
+                }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks if formal nets with the given name are driven in any of the instances of undef boxes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseFormalNetsAreDriven( Abc_Ntk_t * pNtk, char * pNameFormal )
+{
+    Ver_Bundle_t * pBundle;
+    Abc_Obj_t * pBox, * pNet;
+    int k, j, m;
+    // go through instances of this type
+    Vec_PtrForEachEntry( pNtk->pData, pBox, k )
+    {
+        // find a bundle with the given name in this instance
+        Vec_PtrForEachEntryReverse( (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
+            if ( pBundle && !strcmp( pBundle->pNameFormal, pNameFormal ) )
+                break;
+        // skip non-driven bundles
+        if ( j == Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) )
+            continue;
+        // check if all nets are driven in this bundle
+        Vec_PtrForEachEntry( pBundle->vNetsActual, pNet, m )
+            if ( Abc_ObjFaninNum(pNet) > 0 )
+                return 1;
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the non-driven bundle that is given distance from the end.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ver_Bundle_t * Ver_ParseGetNondrivenBundle( Abc_Ntk_t * pNtk, int Counter )
+{
+    Ver_Bundle_t * pBundle;
+    Abc_Obj_t * pBox, * pNet;
+    int k, m;
+    // go through instances of this type
+    Vec_PtrForEachEntry( pNtk->pData, pBox, k )
+    {
+        if ( Counter >= Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) )
+            continue;
+        // get the bundle given distance away
+        pBundle = Vec_PtrEntry( (Vec_Ptr_t *)pBox->pCopy, Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) - 1 - Counter );
+        if ( pBundle == NULL )
+            continue;
+        // go through the actual nets of this bundle
+        Vec_PtrForEachEntry( pBundle->vNetsActual, pNet, m )
+            if ( !Abc_ObjFaninNum(pNet) && !Ver_ParseFormalNetsAreDriven(pNtk, pBundle->pNameFormal) ) // non-driven
+                return pBundle;
+    }
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Drives the bundle in the given undef box.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseDriveFormal( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_Bundle_t * pBundle0 )
+{
+    char Buffer[200];
+    char * pName;
+    Ver_Bundle_t * pBundle;
+    Abc_Obj_t * pBox, * pTerm, * pTermNew, * pNetAct, * pNetFormal;
+    int k, j, m;
+
+    // drive this net in the undef box
+    Vec_PtrForEachEntry( pBundle0->vNetsActual, pNetAct, m )
+    {
+        // create the formal net
+        if ( Vec_PtrSize(pBundle0->vNetsActual) == 1 )
+            sprintf( Buffer, "%s", pBundle0->pNameFormal );
+        else
+            sprintf( Buffer, "%s[%d]", pBundle0->pNameFormal, m );
+        assert( Abc_NtkFindNet( pNtk, Buffer ) == NULL );
+        pNetFormal = Abc_NtkFindOrCreateNet( pNtk, Buffer );
+        // connect it to the box
+        pTerm = Abc_NtkCreateBo( pNtk );
+        assert( Abc_NtkBoxNum(pNtk) <= 1 );
+        pBox = Abc_NtkBoxNum(pNtk)? Abc_NtkBox(pNtk,0) : Abc_NtkCreateBlackbox(pNtk);
+        Abc_ObjAddFanin( Abc_NtkCreatePo(pNtk), pNetFormal );
+        Abc_ObjAddFanin( pNetFormal, pTerm );
+        Abc_ObjAddFanin( pTerm, pBox );
+    }
+
+    // go through instances of this type
+    pName = Extra_UtilStrsav(pBundle0->pNameFormal);
+    Vec_PtrForEachEntry( pNtk->pData, pBox, k )
+    {
+        // find a bundle with the given name in this instance
+        Vec_PtrForEachEntryReverse( (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
+            if ( pBundle && !strcmp( pBundle->pNameFormal, pName ) )
+                break;
+        // skip non-driven bundles
+        if ( j == Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) )
+            continue;
+        // check if any nets are driven in this bundle
+        Vec_PtrForEachEntry( pBundle->vNetsActual, pNetAct, m )
+            if ( Abc_ObjFaninNum(pNetAct) > 0 )
+            {
+                sprintf( pMan->sError, "Internal error while trying to connect undefined boxes. It is likely that the algorithm currently used has its limitations." );
+                Ver_ParsePrintErrorMessage( pMan );
+                return 0;
+            }
+        // drive the nets by the undef box
+        Vec_PtrForEachEntryReverse( pBundle->vNetsActual, pNetAct, m )
+        {
+            pTermNew = Abc_NtkCreateBo( pNetAct->pNtk );
+            Abc_ObjAddFanin( pTermNew, pBox );
+            Abc_ObjAddFanin( pNetAct, pTermNew );
+        }
+        // remove the bundle
+        Ver_ParseFreeBundle( pBundle );
+        Vec_PtrWriteEntry( (Vec_Ptr_t *)pBox->pCopy, j, NULL );
+    }
+    free( pName );
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Drives the bundle in the given undef box.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseDriveInputs( Ver_Man_t * pMan, Vec_Ptr_t * vUndefs )
+{
+    char Buffer[200];
+    Ver_Bundle_t * pBundle;
+    Abc_Ntk_t * pNtk;
+    Abc_Obj_t * pBox, * pBox2, * pTerm, * pTermNew, * pNetFormal, * pNetAct;
+    int i, k, j, m, CountCur, CountTotal = -1;
+    // iterate through the undef boxes
+    Vec_PtrForEachEntry( vUndefs, pNtk, i )
+    {
+        // count the number of unconnected bundles for instances of this type of box
+        CountTotal = -1;
+        Vec_PtrForEachEntry( pNtk->pData, pBox, k )
+        {
+            CountCur = 0;
+            Vec_PtrForEachEntry( (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
+                CountCur += (pBundle != NULL);
+            if ( CountTotal == -1 )
+                CountTotal = CountCur;
+            else if ( CountTotal != CountCur )
+            {
+                sprintf( pMan->sError, "The number of formal inputs (%d) is different from the expected one (%d) when instantiating network %s in box %s.", 
+                    CountCur, CountTotal, pNtk->pName, Abc_ObjName(pBox) );
+                Ver_ParsePrintErrorMessage( pMan );
+                return 0;
+            }
+        }
+
+        // create formals
+        pBox = Vec_PtrEntry( pNtk->pData, 0 );
+        Vec_PtrForEachEntry( (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
+        {
+            if ( pBundle == NULL )
+                continue;
+            Vec_PtrForEachEntry( pBundle->vNetsActual, pNetAct, m )
+            {
+                // find create the formal net
+                if ( Vec_PtrSize(pBundle->vNetsActual) == 1 )
+                    sprintf( Buffer, "%s", pBundle->pNameFormal );
+                else
+                    sprintf( Buffer, "%s[%d]", pBundle->pNameFormal, m );
+                assert( Abc_NtkFindNet( pNtk, Buffer ) == NULL );
+                pNetFormal = Abc_NtkFindOrCreateNet( pNtk, Buffer );
+                // connect
+                pTerm = Abc_NtkCreateBi( pNtk );
+                assert( Abc_NtkBoxNum(pNtk) <= 1 );
+                pBox2 = Abc_NtkBoxNum(pNtk)? Abc_NtkBox(pNtk,0) : Abc_NtkCreateBlackbox(pNtk);
+                Abc_ObjAddFanin( pNetFormal, Abc_NtkCreatePi(pNtk) );
+                Abc_ObjAddFanin( pTerm, pNetFormal );
+                Abc_ObjAddFanin( pBox2, pTerm );
+            }
+        }
+
+        // go through all the boxes
+        Vec_PtrForEachEntry( pNtk->pData, pBox, k )
+        {
+            // go through all the bundles
+            Vec_PtrForEachEntry( (Vec_Ptr_t *)pBox->pCopy, pBundle, j )
+            {
+                if ( pBundle == NULL )
+                    continue;
+                // drive the nets by the undef box
+                Vec_PtrForEachEntryReverse( pBundle->vNetsActual, pNetAct, m )
+                {
+                    pTermNew = Abc_NtkCreateBi( pNetAct->pNtk );
+                    Abc_ObjAddFanin( pBox, pTermNew );
+                    Abc_ObjAddFanin( pTermNew, pNetAct );
+                }
+                // remove the bundle
+                Ver_ParseFreeBundle( pBundle );
+                Vec_PtrWriteEntry( (Vec_Ptr_t *)pBox->pCopy, j, NULL );
+            }
+
+            // free the bundles
+            Vec_PtrFree( (Vec_Ptr_t *)pBox->pCopy );
+            pBox->pCopy = NULL;
+        }
+    }
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the max size of any undef box.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseMaxBoxSize( Vec_Ptr_t * vUndefs )
+{
+    Abc_Ntk_t * pNtk;
+    Abc_Obj_t * pBox;
+    int i, k, nMaxSize = 0;
+    // go through undef box types
+    Vec_PtrForEachEntry( vUndefs, pNtk, i )
+        // go through instances of this type
+        Vec_PtrForEachEntry( pNtk->pData, pBox, k )
+            // check the number of bundles of this instance
+            if ( nMaxSize < Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) )
+                nMaxSize = Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy);
+    return nMaxSize;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the comprehensive report into a log file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ver_ParsePrintLog( Ver_Man_t * pMan )
+{
+    Abc_Ntk_t * pNtk, * pNtkBox;
+    Abc_Obj_t * pBox;
+    FILE * pFile;
+    char * pNameGeneric;
+    char Buffer[1000];
+    int i, k;
+
+    // open the log file
+    pNameGeneric = Extra_FileNameGeneric( pMan->pFileName );
+    sprintf( Buffer, "%s.log", pNameGeneric );
+    free( pNameGeneric );
+    pFile = fopen( Buffer, "w" );
+
+    // count the total number of instances and how many times they occur
+    Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
+        pNtk->fHieVisited = 0;
+    Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
+        Abc_NtkForEachBox( pNtk, pBox, k )
+        {
+            if ( Abc_ObjIsLatch(pBox) )
+                continue;
+            pNtkBox = pBox->pData;
+            if ( pNtkBox == NULL )
+                continue;
+            pNtkBox->fHieVisited++;
+        }
+    // print each box and its stats
+    fprintf( pFile, "The hierarhical design %s contains %d modules:\n", pMan->pFileName, Vec_PtrSize(pMan->pDesign->vModules) );
+    Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
+    {
+        fprintf( pFile, "%-24s : ", Abc_NtkName(pNtk) );
+        if ( !Ver_NtkIsDefined(pNtk) )
+            fprintf( pFile, "undefbox" );
+        else if ( Abc_NtkHasBlackbox(pNtk) )
+            fprintf( pFile, "blackbox" );
+        else
+            fprintf( pFile, "logicbox" );
+        fprintf( pFile, " instantiated %6d times ", pNtk->fHieVisited );
+//        fprintf( pFile, "\n   " );
+        fprintf( pFile, " pi = %4d", Abc_NtkPiNum(pNtk) );
+        fprintf( pFile, " po = %4d", Abc_NtkPiNum(pNtk) );
+        fprintf( pFile, " nd = %8d",  Abc_NtkNodeNum(pNtk) );
+        fprintf( pFile, " lat = %6d",  Abc_NtkLatchNum(pNtk) );
+        fprintf( pFile, " box = %6d", Abc_NtkBoxNum(pNtk)-Abc_NtkLatchNum(pNtk) );
+        fprintf( pFile, "\n" );
+    }
+    Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
+        pNtk->fHieVisited = 0;
+
+    // report instances with dangling outputs
+    if ( Vec_PtrSize(pMan->pDesign->vModules) > 1 )
+    {
+        Vec_Ptr_t * vBundles;
+        Ver_Bundle_t * pBundle;
+        int j, nActNets, Counter = 0, CounterBoxes = 0;
+        // count the number of instances with dangling outputs
+        Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
+        {
+            Abc_NtkForEachBox( pNtk, pBox, k )
+            {
+                if ( Abc_ObjIsLatch(pBox) )
+                    continue;
+                vBundles = (Vec_Ptr_t *)pBox->pCopy;
+                pNtkBox = pBox->pData;
+                if ( pNtkBox == NULL )
+                    continue;
+                if ( !Ver_NtkIsDefined(pNtkBox) )
+                    continue;
+                // count the number of actual nets
+                nActNets = 0;
+                Vec_PtrForEachEntry( vBundles, pBundle, j )
+                    nActNets += Vec_PtrSize(pBundle->vNetsActual);
+                // the box is defined and will be connected
+                if ( nActNets != Abc_NtkPiNum(pNtkBox) + Abc_NtkPoNum(pNtkBox) )
+                    Counter++;
+            }
+        }
+        if ( Counter == 0 )
+            fprintf( pFile, "The outputs of all box instances are connected.\n" );
+        else
+        {
+            fprintf( pFile, "\n" );
+            fprintf( pFile, "The outputs of %d box instances are not connected:\n", Counter );
+            // enumerate through the boxes
+            Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
+            {
+                Abc_NtkForEachBox( pNtk, pBox, k )
+                {
+                    if ( Abc_ObjIsLatch(pBox) )
+                        continue;
+                    vBundles = (Vec_Ptr_t *)pBox->pCopy;
+                    pNtkBox = pBox->pData;
+                    if ( pNtkBox == NULL )
+                        continue;
+                    if ( !Ver_NtkIsDefined(pNtkBox) )
+                        continue;
+                    // count the number of actual nets
+                    nActNets = 0;
+                    Vec_PtrForEachEntry( vBundles, pBundle, j )
+                        nActNets += Vec_PtrSize(pBundle->vNetsActual);
+                    // the box is defined and will be connected
+                    if ( nActNets != Abc_NtkPiNum(pNtkBox) + Abc_NtkPoNum(pNtkBox) )
+                        fprintf( pFile, "In module \"%s\" instance \"%s\" of box \"%s\" has different numbers of actual/formal nets (%d/%d).\n",
+                            Abc_NtkName(pNtk), Abc_ObjName(pBox), Abc_NtkName(pNtkBox), nActNets, Abc_NtkPiNum(pNtkBox) + Abc_NtkPoNum(pNtkBox) );
+                }
+            }
+        }
+    }
+    fclose( pFile );
+    printf( "Hierarchy statistics can be found in log file \"%s\".\n", Buffer );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Attaches the boxes to the network.]
+
+  Description [This procedure is called after the design is parsed. 
+  At that point, all the defined models have their PIs present. 
+  They are connected first. Next undef boxes are processed (if present).
+  Iteratively, one bundle is selected to be driven by the undef boxes in such 
+  a way that there is no conflict (if it is driven by an instance of the box,
+  no other net will be driven twice by the same formal net of some other instance 
+  of the same box). In the end, all the remaining nets that cannot be driven 
+  by the undef boxes are connected to the undef boxes as inputs.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseAttachBoxes( Ver_Man_t * pMan )
+{
+    Abc_Ntk_t * pNtk;
+    Ver_Bundle_t * pBundle;
+    Vec_Ptr_t * vUndefs;
+    int i, RetValue, Counter, nMaxBoxSize;
+
+    // print the log file
+    if ( pMan->pDesign->vModules && Vec_PtrSize(pMan->pDesign->vModules) > 1 )
+        Ver_ParsePrintLog( pMan );
+
+    // connect defined boxes
+    RetValue = Ver_ParseConnectDefBoxes( pMan );
+    if ( RetValue < 2 )
+        return RetValue;
+
+    // report the boxes
+    Ver_ParseReportUndefBoxes( pMan );
+
+    // collect undef box types and their actual instances
+    vUndefs = Ver_ParseCollectUndefBoxes( pMan );
+    assert( Vec_PtrSize( vUndefs ) > 0 );
+
+    // go through all undef box types
+    Counter = 0;
+    nMaxBoxSize = Ver_ParseMaxBoxSize( vUndefs );
+    while ( Ver_ParseCheckNondrivenNets(vUndefs) && Counter < nMaxBoxSize )
+    {
+        // go through undef box types
+        pBundle = NULL;
+        Vec_PtrForEachEntry( vUndefs, pNtk, i )
+            if ( pBundle = Ver_ParseGetNondrivenBundle( pNtk, Counter ) )
+                break;
+        if ( pBundle == NULL )
+        {
+            Counter++;
+            continue;
+        }
+        // drive this bundle by this box
+        if ( !Ver_ParseDriveFormal( pMan, pNtk, pBundle ) )
+            return 0;
+    }
+
+    // make all the remaining bundles the drivers of undefs
+    if ( !Ver_ParseDriveInputs( pMan, vUndefs ) )
+        return 0;
+
+    // cleanup
+    Vec_PtrForEachEntry( vUndefs, pNtk, i )
+    {
+        Vec_PtrFree( pNtk->pData );
+        pNtk->pData = NULL;
+    }
+    Vec_PtrFree( vUndefs ); 
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Creates PI terminal and net.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Ver_ParseCreatePi( Abc_Ntk_t * pNtk, char * pName )
+{
+    Abc_Obj_t * pNet, * pTerm;
+    // get the PI net
+//    pNet  = Ver_ParseFindNet( pNtk, pName );
+//    if ( pNet )
+//        printf( "Warning: PI \"%s\" appears twice in the list.\n", pName );
+    pNet  = Abc_NtkFindOrCreateNet( pNtk, pName );
+    // add the PI node
+    pTerm = Abc_NtkCreatePi( pNtk );
+    Abc_ObjAddFanin( pNet, pTerm );
+    return pTerm;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates PO terminal and net.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Ver_ParseCreatePo( Abc_Ntk_t * pNtk, char * pName )
+{
+    Abc_Obj_t * pNet, * pTerm;
+    // get the PO net
+//    pNet  = Ver_ParseFindNet( pNtk, pName );
+//    if ( pNet && Abc_ObjFaninNum(pNet) == 0 )
+//        printf( "Warning: PO \"%s\" appears twice in the list.\n", pName );
+    pNet  = Abc_NtkFindOrCreateNet( pNtk, pName );
+    // add the PO node
+    pTerm = Abc_NtkCreatePo( pNtk );
+    Abc_ObjAddFanin( pTerm, pNet );
+    return pTerm;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Create a latch with the given input/output.]
+
+  Description [By default, the latch value is a don't-care.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Ver_ParseCreateLatch( Abc_Ntk_t * pNtk, Abc_Obj_t * pNetLI, Abc_Obj_t * pNetLO )
+{
+    Abc_Obj_t * pLatch, * pTerm;
+    // add the BO terminal
+    pTerm = Abc_NtkCreateBi( pNtk );
+    Abc_ObjAddFanin( pTerm, pNetLI );
+    // add the latch box
+    pLatch = Abc_NtkCreateLatch( pNtk );
+    Abc_ObjAddFanin( pLatch, pTerm  );
+    // add the BI terminal
+    pTerm = Abc_NtkCreateBo( pNtk );
+    Abc_ObjAddFanin( pTerm, pLatch );
+    // get the LO net
+    Abc_ObjAddFanin( pNetLO, pTerm );
+    // set latch name
+    Abc_ObjAssignName( pLatch, Abc_ObjName(pNetLO), "L" );
+    Abc_LatchSetInitDc( pLatch );
+    return pLatch;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates inverter and returns its net.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Ver_ParseCreateInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pNet )
+{
+    Abc_Obj_t * pObj;
+    pObj = Abc_NtkCreateNodeInv( pNtk, pNet );
+    pNet = Abc_NtkCreateNet( pNtk );
+    Abc_ObjAddFanin( pNet, pObj );
+    return pNet;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/ver/verFormula.c b/src/base/ver/verFormula.c
new file mode 100644
index 00000000..19a2c523
--- /dev/null
+++ b/src/base/ver/verFormula.c
@@ -0,0 +1,474 @@
+/**CFile****************************************************************
+
+  FileName    [verFormula.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Verilog parser.]
+
+  Synopsis    [Formula parser to read Verilog assign statements.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - August 19, 2006.]
+
+  Revision    [$Id: verFormula.c,v 1.00 2006/08/19 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ver.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// the list of operation symbols to be used in expressions
+#define VER_PARSE_SYM_OPEN    '('   // opening paranthesis
+#define VER_PARSE_SYM_CLOSE   ')'   // closing paranthesis
+#define VER_PARSE_SYM_CONST0  '0'   // constant 0
+#define VER_PARSE_SYM_CONST1  '1'   // constant 1
+#define VER_PARSE_SYM_NEGBEF1 '!'   // negation before the variable
+#define VER_PARSE_SYM_NEGBEF2 '~'   // negation before the variable
+#define VER_PARSE_SYM_AND     '&'   // logic AND
+#define VER_PARSE_SYM_OR      '|'   // logic OR
+#define VER_PARSE_SYM_XOR     '^'   // logic XOR
+#define VER_PARSE_SYM_MUX1    '?'   // first symbol of MUX
+#define VER_PARSE_SYM_MUX2    ':'   // second symbol of MUX
+
+// the list of opcodes (also specifying operation precedence)
+#define VER_PARSE_OPER_NEG     7    // negation (highest precedence)
+#define VER_PARSE_OPER_AND     6    // logic AND
+#define VER_PARSE_OPER_XOR     5    // logic EXOR   (a'b | ab')   
+#define VER_PARSE_OPER_OR      4    // logic OR
+#define VER_PARSE_OPER_EQU     3    // equvalence   (a'b'| ab )
+#define VER_PARSE_OPER_MUX     2    // MUX(a,b,c)   (ab | a'c )
+#define VER_PARSE_OPER_MARK    1    // OpStack token standing for an opening paranthesis
+
+// these are values of the internal Flag
+#define VER_PARSE_FLAG_START   1    // after the opening parenthesis 
+#define VER_PARSE_FLAG_VAR     2    // after operation is received
+#define VER_PARSE_FLAG_OPER    3    // after operation symbol is received
+#define VER_PARSE_FLAG_ERROR   4    // when error is detected
+
+static Hop_Obj_t * Ver_FormulaParserTopOper( Hop_Man_t * pMan, Vec_Ptr_t * vStackFn, int Oper );
+static int         Ver_FormulaParserFindVar( char * pString, Vec_Ptr_t * vNames );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Parser of the formula encountered in assign statements.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void * Ver_FormulaParser( char * pFormula, void * pMan, Vec_Ptr_t * vNames, Vec_Ptr_t * vStackFn, Vec_Int_t * vStackOp, char * pErrorMessage )
+{
+    char * pTemp;
+    Hop_Obj_t * bFunc, * bTemp;
+    int nParans, Flag;
+    int Oper, Oper1, Oper2;
+    int v;
+
+    // clear the stacks and the names
+    Vec_PtrClear( vNames );
+    Vec_PtrClear( vStackFn );
+    Vec_IntClear( vStackOp );
+
+    if ( !strcmp(pFormula, "0") || !strcmp(pFormula, "1\'b0") )
+        return Hop_ManConst0(pMan);
+    if ( !strcmp(pFormula, "1") || !strcmp(pFormula, "1\'b1") )
+        return Hop_ManConst1(pMan);
+
+    // make sure that the number of opening and closing parantheses is the same
+    nParans = 0;
+    for ( pTemp = pFormula; *pTemp; pTemp++ )
+        if ( *pTemp == '(' )
+            nParans++;
+        else if ( *pTemp == ')' )
+            nParans--;
+    if ( nParans != 0 )
+    {
+        sprintf( pErrorMessage, "Parse_FormulaParser(): Different number of opening and closing parantheses ()." );
+        return NULL;
+    }
+ 
+    // add parantheses
+    pTemp = pFormula + strlen(pFormula) + 2;
+    *pTemp-- = 0; *pTemp = ')';
+    while ( --pTemp != pFormula )
+        *pTemp = *(pTemp - 1);
+    *pTemp = '(';
+
+    // perform parsing
+    Flag = VER_PARSE_FLAG_START;
+    for ( pTemp = pFormula; *pTemp; pTemp++ )
+    {
+        switch ( *pTemp )
+        {
+        // skip all spaces, tabs, and end-of-lines
+        case ' ':
+        case '\t':
+        case '\r':
+        case '\n':
+            continue;
+/*
+        // treat Constant 0 as a variable
+        case VER_PARSE_SYM_CONST0:
+            Vec_PtrPush( vStackFn, Hop_ManConst0(pMan) );  // Cudd_Ref( Hop_ManConst0(pMan) );
+            if ( Flag == VER_PARSE_FLAG_VAR )
+            {
+                sprintf( pErrorMessage, "Parse_FormulaParser(): No operation symbol before constant 0." );
+                Flag = VER_PARSE_FLAG_ERROR; 
+                break;
+            }
+            Flag = VER_PARSE_FLAG_VAR; 
+            break;
+
+        // the same for Constant 1
+        case VER_PARSE_SYM_CONST1:
+            Vec_PtrPush( vStackFn, Hop_ManConst1(pMan) );  //  Cudd_Ref( Hop_ManConst1(pMan) );
+            if ( Flag == VER_PARSE_FLAG_VAR )
+            {
+                sprintf( pErrorMessage, "Parse_FormulaParser(): No operation symbol before constant 1." );
+                Flag = VER_PARSE_FLAG_ERROR; 
+                break;
+            }
+            Flag = VER_PARSE_FLAG_VAR; 
+            break;
+*/
+        case VER_PARSE_SYM_NEGBEF1:
+        case VER_PARSE_SYM_NEGBEF2:
+            if ( Flag == VER_PARSE_FLAG_VAR )
+            {// if NEGBEF follows a variable, AND is assumed
+                sprintf( pErrorMessage, "Parse_FormulaParser(): Variable before negation." );
+                Flag = VER_PARSE_FLAG_ERROR; 
+                break;
+            }
+            Vec_IntPush( vStackOp, VER_PARSE_OPER_NEG );
+            break;
+
+        case VER_PARSE_SYM_AND:
+        case VER_PARSE_SYM_OR:
+        case VER_PARSE_SYM_XOR:
+        case VER_PARSE_SYM_MUX1:
+        case VER_PARSE_SYM_MUX2:
+            if ( Flag != VER_PARSE_FLAG_VAR )
+            {
+                sprintf( pErrorMessage, "Parse_FormulaParser(): There is no variable before AND, EXOR, or OR." );
+                Flag = VER_PARSE_FLAG_ERROR; 
+                break;
+            }
+            if ( *pTemp == VER_PARSE_SYM_AND )
+                Vec_IntPush( vStackOp, VER_PARSE_OPER_AND );
+            else if ( *pTemp == VER_PARSE_SYM_OR )
+                Vec_IntPush( vStackOp, VER_PARSE_OPER_OR );
+            else if ( *pTemp == VER_PARSE_SYM_XOR )
+                Vec_IntPush( vStackOp, VER_PARSE_OPER_XOR );
+            else if ( *pTemp == VER_PARSE_SYM_MUX1 )
+                Vec_IntPush( vStackOp, VER_PARSE_OPER_MUX );
+//            else if ( *pTemp == VER_PARSE_SYM_MUX2 )
+//                Vec_IntPush( vStackOp, VER_PARSE_OPER_MUX );
+            Flag = VER_PARSE_FLAG_OPER; 
+            break;
+
+        case VER_PARSE_SYM_OPEN:
+            if ( Flag == VER_PARSE_FLAG_VAR )
+            {
+                sprintf( pErrorMessage, "Parse_FormulaParser(): Variable before a paranthesis." );
+                Flag = VER_PARSE_FLAG_ERROR; 
+                break;
+            }
+            Vec_IntPush( vStackOp, VER_PARSE_OPER_MARK );
+            // after an opening bracket, it feels like starting over again
+            Flag = VER_PARSE_FLAG_START; 
+            break;
+
+        case VER_PARSE_SYM_CLOSE:
+            if ( Vec_IntSize( vStackOp ) )
+            {
+                while ( 1 )
+                {
+                    if ( !Vec_IntSize( vStackOp ) )
+                    {
+                        sprintf( pErrorMessage, "Parse_FormulaParser(): There is no opening paranthesis\n" );
+                        Flag = VER_PARSE_FLAG_ERROR; 
+                        break;
+                    }
+                    Oper = Vec_IntPop( vStackOp );
+                    if ( Oper == VER_PARSE_OPER_MARK )
+                        break;
+                    // skip the second MUX operation
+//                    if ( Oper == VER_PARSE_OPER_MUX2 )
+//                    {
+//                        Oper = Vec_IntPop( vStackOp );
+//                        assert( Oper == VER_PARSE_OPER_MUX1 );
+//                    }
+
+                    // perform the given operation
+                    if ( Ver_FormulaParserTopOper( pMan, vStackFn, Oper ) == NULL )
+                    {
+                        sprintf( pErrorMessage, "Parse_FormulaParser(): Unknown operation\n" );
+                        return NULL;
+                    }
+                }
+            }
+            else
+            {
+                sprintf( pErrorMessage, "Parse_FormulaParser(): There is no opening paranthesis\n" );
+                Flag = VER_PARSE_FLAG_ERROR; 
+                break;
+            }
+            if ( Flag != VER_PARSE_FLAG_ERROR )
+                Flag = VER_PARSE_FLAG_VAR; 
+            break;
+
+
+        default:
+            // scan the next name
+            v = Ver_FormulaParserFindVar( pTemp, vNames );
+            if ( *pTemp == '\\' )
+                pTemp++;
+            pTemp += (int)Vec_PtrEntry( vNames, 2*v ) - 1;
+
+            // assume operation AND, if vars follow one another
+            if ( Flag == VER_PARSE_FLAG_VAR )
+            {
+                sprintf( pErrorMessage, "Parse_FormulaParser(): Incorrect state." );
+                return NULL;
+            }
+            bTemp = Hop_IthVar( pMan, v );
+            Vec_PtrPush( vStackFn, bTemp ); //  Cudd_Ref( bTemp );
+            Flag = VER_PARSE_FLAG_VAR; 
+            break;
+        }
+
+        if ( Flag == VER_PARSE_FLAG_ERROR )
+            break;      // error exit
+        else if ( Flag == VER_PARSE_FLAG_START )
+            continue;  //  go on parsing
+        else if ( Flag == VER_PARSE_FLAG_VAR )
+            while ( 1 )
+            {  // check if there are negations in the OpStack     
+                if ( !Vec_IntSize(vStackOp) )
+                    break;
+                Oper = Vec_IntPop( vStackOp );
+                if ( Oper != VER_PARSE_OPER_NEG )
+                {
+                    Vec_IntPush( vStackOp, Oper );
+                    break;
+                }
+                else
+                {
+//                      Vec_PtrPush( vStackFn, Cudd_Not(Vec_PtrPop(vStackFn)) );
+                      Vec_PtrPush( vStackFn, Hop_Not(Vec_PtrPop(vStackFn)) );
+                }
+            }
+        else // if ( Flag == VER_PARSE_FLAG_OPER )
+            while ( 1 )
+            {  // execute all the operations in the OpStack
+               // with precedence higher or equal than the last one
+                Oper1 = Vec_IntPop( vStackOp ); // the last operation
+                if ( !Vec_IntSize(vStackOp) ) 
+                {  // if it is the only operation, push it back
+                    Vec_IntPush( vStackOp, Oper1 );
+                    break;
+                }
+                Oper2 = Vec_IntPop( vStackOp ); // the operation before the last one
+                if ( Oper2 >= Oper1 && !(Oper1 == Oper2 && Oper1 == VER_PARSE_OPER_MUX) )  
+                {  // if Oper2 precedence is higher or equal, execute it
+                    if ( Ver_FormulaParserTopOper( pMan, vStackFn, Oper2 ) == NULL )
+                    {
+                        sprintf( pErrorMessage, "Parse_FormulaParser(): Unknown operation\n" );
+                        return NULL;
+                    }
+                    Vec_IntPush( vStackOp,  Oper1 );     // push the last operation back
+                }
+                else
+                {  // if Oper2 precedence is lower, push them back and done
+                    Vec_IntPush( vStackOp, Oper2 );
+                    Vec_IntPush( vStackOp, Oper1 );
+                    break;
+                }
+            }
+    }
+
+    if ( Flag != VER_PARSE_FLAG_ERROR )
+    {
+        if ( Vec_PtrSize(vStackFn) )
+        {    
+            bFunc = Vec_PtrPop(vStackFn);
+            if ( !Vec_PtrSize(vStackFn) )
+                if ( !Vec_IntSize(vStackOp) )
+                {
+//                    Cudd_Deref( bFunc );
+                    return bFunc;
+                }
+                else
+                    sprintf( pErrorMessage, "Parse_FormulaParser(): Something is left in the operation stack\n" );
+            else
+                sprintf( pErrorMessage, "Parse_FormulaParser(): Something is left in the function stack\n" );
+        }
+        else
+            sprintf( pErrorMessage, "Parse_FormulaParser(): The input string is empty\n" );
+    }
+//    Cudd_Ref( bFunc );
+//    Cudd_RecursiveDeref( dd, bFunc );
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs the operation on the top entries in the stack.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Hop_Obj_t * Ver_FormulaParserTopOper( Hop_Man_t * pMan, Vec_Ptr_t * vStackFn, int Oper )
+{
+    Hop_Obj_t * bArg0, * bArg1, * bArg2, * bFunc;
+    // perform the given operation
+    bArg2 = Vec_PtrPop( vStackFn );
+    bArg1 = Vec_PtrPop( vStackFn );
+    if ( Oper == VER_PARSE_OPER_AND )
+        bFunc = Hop_And( pMan, bArg1, bArg2 );
+    else if ( Oper == VER_PARSE_OPER_XOR )
+        bFunc = Hop_Exor( pMan, bArg1, bArg2 );
+    else if ( Oper == VER_PARSE_OPER_OR )
+        bFunc = Hop_Or( pMan, bArg1, bArg2 );
+    else if ( Oper == VER_PARSE_OPER_EQU )
+        bFunc = Hop_Not( Hop_Exor( pMan, bArg1, bArg2 ) );
+    else if ( Oper == VER_PARSE_OPER_MUX )
+    {
+        bArg0 = Vec_PtrPop( vStackFn );
+//        bFunc = Cudd_bddIte( dd, bArg0, bArg1, bArg2 );  Cudd_Ref( bFunc );
+        bFunc = Hop_Mux( pMan, bArg0, bArg1, bArg2 ); 
+//        Cudd_RecursiveDeref( dd, bArg0 );
+//        Cudd_Deref( bFunc );
+    }
+    else
+        return NULL;
+//    Cudd_Ref( bFunc );
+//    Cudd_RecursiveDeref( dd, bArg1 );
+//    Cudd_RecursiveDeref( dd, bArg2 );
+    Vec_PtrPush( vStackFn,  bFunc );
+    return bFunc;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the index of the new variable found.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_FormulaParserFindVar( char * pString, Vec_Ptr_t * vNames )
+{
+    char * pTemp, * pTemp2;
+    int nLength, nLength2, i;
+    // start the string
+    pTemp = pString;
+    // find the end of the string delimited by other characters
+    if ( *pTemp == '\\' )
+    {
+        pString++;
+        while ( *pTemp && *pTemp != ' ' )
+            pTemp++;
+    }
+    else
+    {
+        while ( *pTemp && *pTemp != ' ' && *pTemp != '\t' && *pTemp != '\r' && *pTemp != '\n' && *pTemp != ',' && *pTemp != '}' && 
+                *pTemp != VER_PARSE_SYM_OPEN && *pTemp != VER_PARSE_SYM_CLOSE && 
+                *pTemp != VER_PARSE_SYM_NEGBEF1 && *pTemp != VER_PARSE_SYM_NEGBEF2 && 
+                *pTemp != VER_PARSE_SYM_AND && *pTemp != VER_PARSE_SYM_OR && *pTemp != VER_PARSE_SYM_XOR && 
+                *pTemp != VER_PARSE_SYM_MUX1 && *pTemp != VER_PARSE_SYM_MUX2 )
+                pTemp++;
+    }
+    // look for this string in the array
+    nLength = pTemp - pString;
+    for ( i = 0; i < Vec_PtrSize(vNames)/2; i++ )
+    {
+        nLength2 = (int)Vec_PtrEntry( vNames, 2*i + 0 );
+        if ( nLength2 != nLength )
+            continue;
+        pTemp2   = Vec_PtrEntry( vNames, 2*i + 1 );
+        if ( strncmp( pString, pTemp2, nLength ) )
+            continue;
+        return i;
+    }
+    // could not find - add and return the number
+    Vec_PtrPush( vNames, (void *)nLength );
+    Vec_PtrPush( vNames, pString );
+    return i;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the AIG representation of the reduction formula.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void * Ver_FormulaReduction( char * pFormula, void * pMan, Vec_Ptr_t * vNames, char * pErrorMessage )
+{
+    Hop_Obj_t * pRes;
+    int v, fCompl;
+    char Symbol;
+
+    // get the operation
+    Symbol = *pFormula++;
+    fCompl = ( Symbol == '~' );
+    if ( fCompl )
+        Symbol = *pFormula++;
+    // check the operation
+    if ( Symbol != '&' && Symbol != '|' && Symbol != '^' )
+    {
+        sprintf( pErrorMessage, "Ver_FormulaReduction(): Unknown operation (%c)\n", Symbol );
+        return NULL;
+    }
+    // skip the brace
+    while ( *pFormula++ != '{' );
+    // parse the names
+    Vec_PtrClear( vNames );
+    while ( *pFormula != '}' )
+    {
+        v = Ver_FormulaParserFindVar( pFormula, vNames );
+        pFormula += (int)Vec_PtrEntry( vNames, 2*v );
+        while ( *pFormula == ' ' || *pFormula == ',' )
+            pFormula++;
+    }
+    // compute the function
+    if ( Symbol == '&' )
+        pRes = Hop_CreateAnd( pMan, Vec_PtrSize(vNames)/2 );
+    else if ( Symbol == '|' )
+        pRes = Hop_CreateOr( pMan, Vec_PtrSize(vNames)/2 );
+    else if ( Symbol == '^' )
+        pRes = Hop_CreateExor( pMan, Vec_PtrSize(vNames)/2 );
+    return Hop_NotCond( pRes, fCompl );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/ver/verParse.c b/src/base/ver/verParse.c
new file mode 100644
index 00000000..9462fc8b
--- /dev/null
+++ b/src/base/ver/verParse.c
@@ -0,0 +1,117 @@
+/**CFile****************************************************************
+
+  FileName    [verParse.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Verilog parser.]
+
+  Synopsis    [Performs some Verilog parsing tasks.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - August 19, 2006.]
+
+  Revision    [$Id: verParse.c,v 1.00 2006/08/19 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ver.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Skips the comments of they are present.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseSkipComments( Ver_Man_t * pMan )
+{
+    Ver_Stream_t * p = pMan->pReader;
+    char Symbol;
+    // skip spaces
+    Ver_StreamSkipChars( p, " \t\n\r" );
+    if ( !Ver_StreamIsOkey(pMan->pReader) )
+        return 1;
+    // read the first symbol
+    Symbol = Ver_StreamScanChar( p );
+    if ( Symbol != '/' )
+        return 1;
+    Ver_StreamPopChar( p );
+    // read the second symbol
+    Symbol = Ver_StreamScanChar( p );
+    if ( Symbol == '/' )
+    { // skip till the end of line
+        Ver_StreamSkipToChars( p, "\n" );
+        return Ver_ParseSkipComments( pMan );
+    }
+    if ( Symbol == '*' )
+    { // skip till the next occurance of */
+        Ver_StreamPopChar( p );
+        do {
+            Ver_StreamSkipToChars( p, "*" );
+            Ver_StreamPopChar( p );
+        } while ( Ver_StreamScanChar( p ) != '/' );
+        Ver_StreamPopChar( p );
+        return Ver_ParseSkipComments( pMan );
+    }
+    sprintf( pMan->sError, "Cannot parse after symbol \"/\"." );
+    Ver_ParsePrintErrorMessage( pMan );
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Parses a Verilog name that can be being with a slash.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Ver_ParseGetName( Ver_Man_t * pMan )
+{
+    Ver_Stream_t * p = pMan->pReader;
+    char Symbol;
+    char * pWord;
+    pMan->fNameLast = 0;
+    if ( !Ver_StreamIsOkey(p) )
+        return NULL;
+    if ( !Ver_ParseSkipComments( pMan ) )
+        return NULL;
+    Symbol = Ver_StreamScanChar( p );
+    if ( Symbol == '\\' )
+    {
+        pMan->fNameLast = 1;
+        Ver_StreamPopChar( p );
+        pWord = Ver_StreamGetWord( p, " \r\n" );
+    }
+    else
+        pWord = Ver_StreamGetWord( p, " \t\n\r(),;" );
+    if ( !Ver_ParseSkipComments( pMan ) )
+        return NULL;
+    return pWord;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/ver/verStream.c b/src/base/ver/verStream.c
new file mode 100644
index 00000000..9b56bb3f
--- /dev/null
+++ b/src/base/ver/verStream.c
@@ -0,0 +1,443 @@
+/**CFile****************************************************************
+
+  FileName    [verStream.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Verilog parser.]
+
+  Synopsis    [Input file stream, which knows nothing about Verilog.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - August 19, 2006.]
+
+  Revision    [$Id: verStream.c,v 1.00 2006/08/19 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ver.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+#define VER_BUFFER_SIZE        1048576    // 1M  - size of the data chunk stored in memory
+#define VER_OFFSET_SIZE          65536    // 64K - load new data when less than this is left
+#define VER_WORD_SIZE            65536    // 64K - the largest token that can be returned
+
+#define VER_MINIMUM(a,b)       (((a) < (b))? (a) : (b))
+
+struct Ver_Stream_t_
+{
+    // the input file
+    char *           pFileName;     // the input file name
+    FILE *           pFile;         // the input file pointer
+    int              nFileSize;     // the total number of bytes in the file
+    int              nFileRead;     // the number of bytes currently read from file
+    int              nLineCounter;  // the counter of lines processed
+    // temporary storage for data 
+    char *           pBuffer;       // the buffer
+    int              nBufferSize;   // the size of the buffer
+    char *           pBufferCur;    // the current reading position
+    char *           pBufferEnd;    // the first position not used by currently loaded data
+    char *           pBufferStop;   // the position where loading new data will be done
+    // tokens given to the user
+    char             pChars[VER_WORD_SIZE+5]; // temporary storage for a word (plus end-of-string and two parantheses)
+    int              nChars;        // the total number of characters in the word
+    // status of the parser
+    int              fStop;         // this flag goes high when the end of file is reached
+};
+
+static void Ver_StreamReload( Ver_Stream_t * p );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the file reader for the given file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ver_Stream_t * Ver_StreamAlloc( char * pFileName )
+{
+    Ver_Stream_t * p;
+    FILE * pFile;
+    int nCharsToRead;
+    // check if the file can be opened
+    pFile = fopen( pFileName, "rb" );
+    if ( pFile == NULL )
+    {
+        printf( "Ver_StreamAlloc(): Cannot open input file \"%s\".\n", pFileName );
+        return NULL;
+    }
+    // start the file reader    
+    p = ALLOC( Ver_Stream_t, 1 );
+    memset( p, 0, sizeof(Ver_Stream_t) );
+    p->pFileName   = pFileName;
+    p->pFile       = pFile;
+    // get the file size, in bytes
+    fseek( pFile, 0, SEEK_END );  
+    p->nFileSize = ftell( pFile );  
+    rewind( pFile ); 
+    // allocate the buffer
+    p->pBuffer = ALLOC( char, VER_BUFFER_SIZE+1 );
+    p->nBufferSize = VER_BUFFER_SIZE;
+    p->pBufferCur  = p->pBuffer;
+    // determine how many chars to read
+    nCharsToRead = VER_MINIMUM(p->nFileSize, VER_BUFFER_SIZE);
+    // load the first part into the buffer
+    fread( p->pBuffer, nCharsToRead, 1, p->pFile );
+    p->nFileRead = nCharsToRead;
+    // set the ponters to the end and the stopping point
+    p->pBufferEnd  = p->pBuffer + nCharsToRead;
+    p->pBufferStop = (p->nFileRead == p->nFileSize)? p->pBufferEnd : p->pBuffer + VER_BUFFER_SIZE - VER_OFFSET_SIZE;
+    // start the arrays
+    p->nLineCounter = 1; // 1-based line counting
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Loads new data into the file reader.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ver_StreamReload( Ver_Stream_t * p )
+{
+    int nCharsUsed, nCharsToRead;
+    assert( !p->fStop );
+    assert( p->pBufferCur > p->pBufferStop );
+    assert( p->pBufferCur < p->pBufferEnd );
+    // figure out how many chars are still not processed
+    nCharsUsed = p->pBufferEnd - p->pBufferCur;
+    // move the remaining data to the beginning of the buffer
+    memmove( p->pBuffer, p->pBufferCur, nCharsUsed );
+    p->pBufferCur = p->pBuffer;
+    // determine how many chars we will read
+    nCharsToRead = VER_MINIMUM( p->nBufferSize - nCharsUsed, p->nFileSize - p->nFileRead );
+    // read the chars
+    fread( p->pBuffer + nCharsUsed, nCharsToRead, 1, p->pFile );
+    p->nFileRead += nCharsToRead;
+    // set the ponters to the end and the stopping point
+    p->pBufferEnd  = p->pBuffer + nCharsUsed + nCharsToRead;
+    p->pBufferStop = (p->nFileRead == p->nFileSize)? p->pBufferEnd : p->pBuffer + VER_BUFFER_SIZE - VER_OFFSET_SIZE;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the file reader.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ver_StreamFree( Ver_Stream_t * p )
+{
+    if ( p->pFile )
+        fclose( p->pFile );
+    FREE( p->pBuffer );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the file size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Ver_StreamGetFileName( Ver_Stream_t * p )
+{
+    return p->pFileName;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the file size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_StreamGetFileSize( Ver_Stream_t * p )
+{
+    return p->nFileSize;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the current reading position.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_StreamGetCurPosition( Ver_Stream_t * p )
+{
+    return p->nFileRead - (p->pBufferEnd - p->pBufferCur);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the line number for the given token.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_StreamGetLineNumber( Ver_Stream_t * p )
+{
+    return p->nLineCounter;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Returns current symbol.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_StreamIsOkey( Ver_Stream_t * p )
+{
+    return !p->fStop;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns current symbol.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char Ver_StreamScanChar( Ver_Stream_t * p )
+{
+    assert( !p->fStop );
+    return *p->pBufferCur;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns current symbol and moves to the next.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char Ver_StreamPopChar( Ver_Stream_t * p )
+{
+    assert( !p->fStop );
+    // check if the new data should to be loaded
+    if ( p->pBufferCur > p->pBufferStop )
+        Ver_StreamReload( p );
+    // check if there are symbols left
+    if ( p->pBufferCur == p->pBufferEnd ) // end of file
+    {
+        p->fStop = 1;
+        return -1;
+    }
+    // count the lines
+    if ( *p->pBufferCur == '\n' )
+        p->nLineCounter++;
+    return *p->pBufferCur++;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Skips the current symbol and all symbols from the list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ver_StreamSkipChars( Ver_Stream_t * p, char * pCharsToSkip )
+{
+    char * pChar, * pTemp;
+    assert( !p->fStop );
+    assert( pCharsToSkip != NULL );
+    // check if the new data should to be loaded
+    if ( p->pBufferCur > p->pBufferStop )
+        Ver_StreamReload( p );
+    // skip the symbols
+    for ( pChar = p->pBufferCur; pChar < p->pBufferEnd; pChar++ )
+    {
+        // skip symbols as long as they are in the list
+        for ( pTemp = pCharsToSkip; *pTemp; pTemp++ )
+            if ( *pChar == *pTemp )
+                break;
+        if ( *pTemp == 0 ) // pChar is not found in the list
+        {
+            p->pBufferCur = pChar;
+            return;
+        }
+        // count the lines
+        if ( *pChar == '\n' )
+            p->nLineCounter++;
+    }
+    // the file is finished or the last part continued 
+    // through VER_OFFSET_SIZE chars till the end of the buffer
+    if ( p->pBufferStop == p->pBufferEnd ) // end of file
+    {
+        p->fStop = 1;
+        return;
+    }
+    printf( "Ver_StreamSkipSymbol() failed to parse the file \"%s\".\n", p->pFileName );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Skips all symbols until encountering one from the list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ver_StreamSkipToChars( Ver_Stream_t * p, char * pCharsToStop )
+{
+    char * pChar, * pTemp;
+    assert( !p->fStop );
+    assert( pCharsToStop != NULL );
+    // check if the new data should to be loaded
+    if ( p->pBufferCur > p->pBufferStop )
+        Ver_StreamReload( p );
+    // skip the symbols
+    for ( pChar = p->pBufferCur; pChar < p->pBufferEnd; pChar++ )
+    {
+        // skip symbols as long as they are NOT in the list
+        for ( pTemp = pCharsToStop; *pTemp; pTemp++ )
+            if ( *pChar == *pTemp )
+                break;
+        if ( *pTemp == 0 ) // pChar is not found in the list
+        {
+            // count the lines
+            if ( *pChar == '\n' )
+                p->nLineCounter++;
+            continue;
+        }
+        // the symbol is found - move position and return
+        p->pBufferCur = pChar;
+        return;
+    }
+    // the file is finished or the last part continued 
+    // through VER_OFFSET_SIZE chars till the end of the buffer
+    if ( p->pBufferStop == p->pBufferEnd ) // end of file
+    {
+        p->fStop = 1;
+        return;
+    }
+    printf( "Ver_StreamSkipToSymbol() failed to parse the file \"%s\".\n", p->pFileName );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns current word delimited by the set of symbols.]
+
+  Description [Modifies the stream by inserting 0 at the first encounter
+  of one of the symbols in the list.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Ver_StreamGetWord( Ver_Stream_t * p, char * pCharsToStop )
+{
+    char * pChar, * pTemp;
+    if ( p->fStop )
+        return NULL;
+    assert( pCharsToStop != NULL );
+    // check if the new data should to be loaded
+    if ( p->pBufferCur > p->pBufferStop )
+        Ver_StreamReload( p );
+    // skip the symbols
+    p->nChars = 0;
+    for ( pChar = p->pBufferCur; pChar < p->pBufferEnd; pChar++ )
+    {
+        // skip symbols as long as they are NOT in the list
+        for ( pTemp = pCharsToStop; *pTemp; pTemp++ )
+            if ( *pChar == *pTemp )
+                break;
+        if ( *pTemp == 0 ) // pChar is not found in the list
+        {
+            p->pChars[p->nChars++] = *pChar;
+            if ( p->nChars == VER_WORD_SIZE )
+            {
+                printf( "Ver_StreamGetWord(): The buffer size is exceeded.\n" );
+                return NULL;
+            }
+            // count the lines
+            if ( *pChar == '\n' )
+                p->nLineCounter++;
+            continue;
+        }
+        // the symbol is found - move the position, set the word end, return the word
+        p->pBufferCur = pChar;
+        p->pChars[p->nChars] = 0;
+        return p->pChars;
+    }
+    // the file is finished or the last part continued 
+    // through VER_OFFSET_SIZE chars till the end of the buffer
+    if ( p->pBufferStop == p->pBufferEnd ) // end of file
+    {
+        p->fStop = 1;
+        p->pChars[p->nChars] = 0;
+        return p->pChars;
+    }
+    printf( "Ver_StreamGetWord() failed to parse the file \"%s\".\n", p->pFileName );
+    return NULL;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/ver/verWords.c b/src/base/ver/verWords.c
new file mode 100644
index 00000000..f9d27010
--- /dev/null
+++ b/src/base/ver/verWords.c
@@ -0,0 +1,48 @@
+/**CFile****************************************************************
+
+  FileName    [verWords.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Verilog parser.]
+
+  Synopsis    [Handles keywords that are currently supported.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - August 19, 2006.]
+
+  Revision    [$Id: verWords.c,v 1.00 2006/08/19 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ver.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/ver/ver_.c b/src/base/ver/ver_.c
new file mode 100644
index 00000000..76599dac
--- /dev/null
+++ b/src/base/ver/ver_.c
@@ -0,0 +1,48 @@
+/**CFile****************************************************************
+
+  FileName    [ver_.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Verilog parser.]
+
+  Synopsis    [Parses several flavors of structural Verilog.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - August 19, 2006.]
+
+  Revision    [$Id: ver_.c,v 1.00 2006/08/19 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ver.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+