Version abc61122

8 files changed, 2325 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..c7c18f79
--- /dev/null
+++ b/src/base/ver/ver.h
@@ -0,0 +1,114 @@
+/**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_
+{
+    // input file stream
+    char *          pFileName;
+    Ver_Stream_t *  pReader;
+    ProgressBar *   pProgress;
+    // current network and library
+    Abc_Ntk_t *     pNtkCur;       // the network under construction
+    Abc_Lib_t *     pDesign;       // the current design 
+    // parameters
+    int             fUseMemMan;    // allocate memory manager in the networks
+    int             fCheck;        // checks network for currectness
+    // error recovery
+    FILE *          Output;
+    int             fTopLevel;
+    int             fError;
+    char            sError[2000];
+    // intermediate structures
+    Vec_Ptr_t *     vNames;  
+    Vec_Ptr_t *     vStackFn;
+    Vec_Int_t *     vStackOp;
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      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..9048337b
--- /dev/null
+++ b/src/base/ver/verCore.c
@@ -0,0 +1,1092 @@
+/**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"
+
+////////////////////////////////////////////////////////////////////////
+///                        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, Ver_SignalType_t SigType );
+static int  Ver_ParseAssign( Ver_Man_t * p );
+static int  Ver_ParseAlways( Ver_Man_t * p );
+static int  Ver_ParseInitial( Ver_Man_t * p );
+static int  Ver_ParseGate( Ver_Man_t * p, Abc_Ntk_t * pNtkGate );
+static int  Ver_ParseGateStandard( Ver_Man_t * pMan, Ver_GateType_t GateType );
+
+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, char * pNetLI, char * pNetLO );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**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->fCheck     = fCheck;
+    p->fUseMemMan = fUseMemMan;
+    // 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    [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 );
+    p->Output    = stdout;
+    p->pProgress = Extra_ProgressBarStart( stdout, Ver_StreamGetFileSize(p->pReader) );
+    p->vNames    = Vec_PtrAlloc( 100 );
+    p->vStackFn  = Vec_PtrAlloc( 100 );
+    p->vStackOp  = Vec_IntAlloc( 100 );
+    // create the design library and assign the technology library
+    p->pDesign   = Abc_LibCreate( pFileName );
+    p->pDesign->pLibrary = pGateLib;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stop parser.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ver_ParseStop( Ver_Man_t * p )
+{
+    assert( p->pNtkCur == NULL );
+    Ver_StreamFree( p->pReader );
+    Extra_ProgressBarStop( p->pProgress );
+    Vec_PtrFree( p->vNames   );
+    Vec_PtrFree( p->vStackFn );
+    Vec_IntFree( p->vStackOp );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [File parser.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ver_ParseInternal( Ver_Man_t * pMan )
+{
+    char * pToken;
+    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;
+
+        // check the network for correctness
+        if ( pMan->fCheck && !Abc_NtkCheckRead( pMan->pNtkCur ) )
+        {
+            pMan->fTopLevel = 1;
+            sprintf( pMan->sError, "The network check has failed.", pMan->pNtkCur->pName );
+            Ver_ParsePrintErrorMessage( pMan );
+            return;
+        }
+        // add the module to the hash table
+        if ( st_is_member( pMan->pDesign->tModules, pMan->pNtkCur->pName ) )
+        {
+            pMan->fTopLevel = 1;
+            sprintf( pMan->sError, "Module \"%s\" is defined more than once.", pMan->pNtkCur->pName );
+            Ver_ParsePrintErrorMessage( pMan );
+            return;
+        }
+        Vec_PtrPush( pMan->pDesign->vModules, pMan->pNtkCur );
+        st_insert( pMan->pDesign->tModules, pMan->pNtkCur->pName, (char *)pMan->pNtkCur );
+        pMan->pNtkCur = NULL;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [File parser.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ver_ParseFreeData( Ver_Man_t * p )
+{
+    if ( p->pNtkCur )
+    {
+        p->pNtkCur->pManFunc = NULL;
+        Abc_NtkDelete( p->pNtkCur );
+        p->pNtkCur = NULL;
+    }
+    if ( p->pDesign )
+    {
+        Abc_LibFree( p->pDesign );
+        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    [Parses one Verilog module.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseModule( Ver_Man_t * pMan )
+{
+    Ver_Stream_t * p = pMan->pReader;
+    Abc_Ntk_t * pNtk, * pNtkTemp;
+    Abc_Obj_t * pNet;
+    char * pWord, Symbol;
+    int RetValue;
+
+    // start the current network
+    assert( pMan->pNtkCur == NULL );
+    pNtk = pMan->pNtkCur = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_BLACKBOX, pMan->fUseMemMan );
+    pNtk->ntkFunc  = ABC_FUNC_AIG;
+    pNtk->pManFunc = pMan->pDesign->pManFunc;
+
+    // get the network name
+    pWord = Ver_ParseGetName( pMan );
+    pNtk->pName = Extra_UtilStrsav( pWord );
+    pNtk->pSpec = NULL;
+
+    // create constant nets
+    Abc_NtkFindOrCreateNet( pNtk, "1'b0" );
+    Abc_NtkFindOrCreateNet( pNtk, "1'b1" );
+
+    // make sure we stopped at the opening paranthesis
+    if ( Ver_StreamPopChar(p) != '(' )
+    {
+        sprintf( pMan->sError, "Cannot find \"(\" after \"module\".", 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);
+    assert( Symbol == ';' );
+
+    // 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, VER_SIG_INPUT );
+        else if ( !strcmp( pWord, "output" ) )
+            RetValue = Ver_ParseSignal( pMan, VER_SIG_OUTPUT );
+        else if ( !strcmp( pWord, "reg" ) )
+            RetValue = Ver_ParseSignal( pMan, VER_SIG_REG );
+        else if ( !strcmp( pWord, "wire" ) )
+            RetValue = Ver_ParseSignal( pMan, VER_SIG_WIRE );
+        else if ( !strcmp( pWord, "inout" ) )
+            RetValue = Ver_ParseSignal( pMan, 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, VER_GATE_AND );
+        else if ( !strcmp( pWord, "or" ) )
+            RetValue = Ver_ParseGateStandard( pMan, VER_GATE_OR );
+        else if ( !strcmp( pWord, "xor" ) )
+            RetValue = Ver_ParseGateStandard( pMan, VER_GATE_XOR );
+        else if ( !strcmp( pWord, "buf" ) )
+            RetValue = Ver_ParseGateStandard( pMan, VER_GATE_BUF );
+        else if ( !strcmp( pWord, "nand" ) )
+            RetValue = Ver_ParseGateStandard( pMan, VER_GATE_NAND );
+        else if ( !strcmp( pWord, "nor" ) )
+            RetValue = Ver_ParseGateStandard( pMan, VER_GATE_NOR );
+        else if ( !strcmp( pWord, "xnor" ) )
+            RetValue = Ver_ParseGateStandard( pMan, VER_GATE_XNOR );
+        else if ( !strcmp( pWord, "not" ) )
+            RetValue = Ver_ParseGateStandard( pMan, VER_GATE_NOT );
+
+        else if ( !strcmp( pWord, "assign" ) )
+            RetValue = Ver_ParseAssign( pMan );
+        else if ( !strcmp( pWord, "always" ) )
+            RetValue = Ver_ParseAlways( pMan );
+        else if ( !strcmp( pWord, "initial" ) )
+            RetValue = Ver_ParseInitial( pMan );
+        else if ( !strcmp( pWord, "endmodule" ) )
+            break;
+        else if ( pMan->pDesign->pLibrary && st_lookup(pMan->pDesign->pLibrary->tModules, pWord, (char**)&pNtkTemp) ) // gate library
+            RetValue = Ver_ParseGate( pMan, pNtkTemp );
+        else if ( pMan->pDesign && st_lookup(pMan->pDesign->tModules, pWord, (char**)&pNtkTemp) ) // current design
+            RetValue = Ver_ParseGate( pMan, pNtkTemp );
+        else
+        {
+            printf( "Cannot find \"%s\".\n", pWord );
+            Ver_StreamSkipToChars( p, ";" );
+            Ver_StreamPopChar(p);
+
+//            sprintf( pMan->sError, "Cannot find \"%s\" in the library.", pWord );
+//            Ver_ParsePrintErrorMessage( pMan );
+//            return 0;
+        }
+        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;
+    }
+
+    // check if constant 0 net is used
+    pNet = Abc_NtkFindOrCreateNet( pNtk, "1'b0" );
+    if ( Abc_ObjFanoutNum(pNet) == 0 )
+        Abc_NtkDeleteObj(pNet);
+    else
+        Abc_ObjAddFanin( pNet, Abc_NtkCreateNodeConst0(pNtk) );
+    // check if constant 1 net is used
+    pNet = Abc_NtkFindOrCreateNet( pNtk, "1'b1" );
+    if ( Abc_ObjFanoutNum(pNet) == 0 )
+        Abc_NtkDeleteObj(pNet);
+    else
+        Abc_ObjAddFanin( pNet, Abc_NtkCreateNodeConst1(pNtk) );
+
+    // fix the dangling nets
+    Abc_NtkFinalizeRead( pNtk );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Parses one directive.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseSignal( Ver_Man_t * pMan, Ver_SignalType_t SigType )
+{
+    Ver_Stream_t * p = pMan->pReader;
+    Abc_Ntk_t * pNtk = pMan->pNtkCur;
+    char * pWord;
+    char Symbol;
+    while ( 1 )
+    {
+        pWord = Ver_ParseGetName( pMan );
+        if ( pWord == NULL )
+            return 0;
+        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 );
+        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_ParseAssign( Ver_Man_t * pMan )
+{
+    Ver_Stream_t * p = pMan->pReader;
+    Abc_Ntk_t * pNtk = pMan->pNtkCur;
+    Abc_Obj_t * pNode, * pNet;
+    char * pWord, * pName, * pEquation;
+    Hop_Obj_t * pFunc;
+    char Symbol;
+    int i, Length, fReduction;
+
+    // convert from the mapped netlist into the BDD netlist
+    if ( pNtk->ntkFunc == ABC_FUNC_BLACKBOX )
+    {
+        pNtk->ntkFunc = ABC_FUNC_AIG;
+        assert( pNtk->pManFunc == NULL );
+        pNtk->pManFunc = pMan->pDesign->pManFunc;
+    }
+    else if ( pNtk->ntkFunc != ABC_FUNC_AIG )
+    {
+        sprintf( pMan->sError, "The network %s appears to mapped gates and assign statements. Currently such network are not allowed. One way to fix this problem is to replace assigns by buffers from the library.", pMan->pNtkCur );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+
+    while ( 1 )
+    {
+        // get the name of the output signal
+        pWord = Ver_ParseGetName( pMan );
+        if ( pWord == NULL )
+            return 0;
+        // consider the case of reduction operations
+        fReduction = (pWord[0] == '{');
+        if ( fReduction )
+        {
+            pWord++;
+            pWord[strlen(pWord)-1] = 0;
+            assert( pWord[0] != '\\' );
+        }
+        // get the fanout net
+        pNet = Abc_NtkFindNet( 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 equal 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 )
+            return 0;
+
+        // parse the formula
+        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( pMan->pNtkCur );
+        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 = Abc_NtkFindNet( pNtk, pName );
+            if ( pNet == NULL )
+            {
+                sprintf( pMan->sError, "Cannot read the assign statement for %s (input wire %d 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_ParseAlways( Ver_Man_t * pMan )
+{
+    Ver_Stream_t * p = pMan->pReader;
+    Abc_Ntk_t * pNtk = pMan->pNtkCur;
+    Abc_Obj_t * pNet, * pNet2;
+    char * pWord, * pWord2;
+    char Symbol;
+    // parse the directive 
+    pWord = Ver_ParseGetName( pMan );
+    if ( pWord == NULL )
+        return 0;
+    if ( strcmp( pWord, "begin" ) )
+    {
+        sprintf( pMan->sError, "Cannot parse the always statement (expected \"begin\")." );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+    // iterate over the initial states
+    while ( 1 )
+    {
+        // 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 = Abc_NtkFindNet( 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 equal sign
+        if ( Ver_StreamPopChar(p) != '=' )
+        {
+            sprintf( pMan->sError, "Cannot read the always 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
+        pWord2 = Ver_ParseGetName( pMan );
+        if ( pWord2 == NULL )
+            return 0;
+        // get the fanin net
+        pNet2 = Abc_NtkFindNet( 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->pData, pNet->pData );
+        // remove the last symbol
+        Symbol = Ver_StreamPopChar(p);
+        assert( Symbol == ';' );
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Parses one directive.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseInitial( Ver_Man_t * pMan )
+{
+    Ver_Stream_t * p = pMan->pReader;
+    Abc_Ntk_t * pNtk = pMan->pNtkCur;
+    Abc_Obj_t * pNode, * pNet;
+    char * pWord, * pEquation;
+    char Symbol;
+    // parse the directive 
+    pWord = Ver_ParseGetName( pMan );
+    if ( pWord == NULL )
+        return 0;
+    if ( strcmp( pWord, "begin" ) )
+    {
+        sprintf( pMan->sError, "Cannot parse the initial statement (expected \"begin\")." );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+    // iterate over the initial states
+    while ( 1 )
+    {
+        // 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 = Abc_NtkFindNet( 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 equal sign
+        if ( Ver_StreamPopChar(p) != '=' )
+        {
+            sprintf( pMan->sError, "Cannot read the initial 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
+        pEquation = Ver_StreamGetWord( p, ";" );
+        if ( pEquation == NULL )
+            return 0;
+        // find the corresponding latch
+        pNode = Abc_ObjFanin0(pNet);
+        assert( Abc_ObjIsLatch(pNode) );
+        // set the initial state
+        if ( pEquation[0] == '2' )
+            Abc_LatchSetInitDc( pNode );
+        else if ( pEquation[0] == '1')
+            Abc_LatchSetInit1( pNode );
+        else if ( pEquation[0] == '0' )
+            Abc_LatchSetInit0( pNode );
+        else
+        {
+            sprintf( pMan->sError, "Incorrect initial value of the latch %s (expected equality sign).", pWord );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+        // remove the last symbol
+        Symbol = Ver_StreamPopChar(p);
+        assert( Symbol == ';' );
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Parses one directive.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtkGate )
+{
+    Ver_Stream_t * p = pMan->pReader;
+    Abc_Ntk_t * pNtk = pMan->pNtkCur;
+    Abc_Obj_t * pNetFormal, * pNetActual;
+    Abc_Obj_t * pObj, * pNode;
+    char * pWord, Symbol, * pGateName;
+    int i, fCompl, fComplUsed = 0;
+    unsigned * pPolarity;
+
+    // clean the PI/PO pointers
+    Abc_NtkForEachPi( pNtkGate, pObj, i )
+        pObj->pCopy = NULL;
+    Abc_NtkForEachPo( pNtkGate, pObj, i )
+        pObj->pCopy = NULL;
+    // 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
+    pGateName = pWord;
+    if ( Ver_StreamPopChar(p) != '(' )
+    {
+        sprintf( pMan->sError, "Cannot parse gate %s (expected opening paranthesis).", pNtkGate->pName );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+    // parse pairs of formal/actural inputs
+    while ( 1 )
+    {
+        // process one pair of formal/actual parameters
+        if ( Ver_StreamPopChar(p) != '.' )
+        {
+            sprintf( pMan->sError, "Cannot parse gate %s (expected .).", pNtkGate->pName );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+
+        // parse the formal name
+        pWord = Ver_ParseGetName( pMan );
+        if ( pWord == NULL )
+            return 0;
+        // get the formal net
+        if ( Abc_NtkIsNetlist(pNtkGate) )
+            pNetFormal = Abc_NtkFindNet( pNtkGate, pWord );
+        else // if ( Abc_NtkIsStrash(pNtkGate) )
+            assert( 0 );
+        if ( pNetFormal == NULL )
+        {
+            sprintf( pMan->sError, "Formal net is missing in gate %s.", pWord );
+            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, pNtkGate->pName );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+
+        // parse the actual name
+        pWord = Ver_ParseGetName( pMan );
+        if ( pWord == NULL )
+            return 0;
+        // check if the name is complemented
+        fCompl = (pWord[0] == '~');
+        if ( fCompl )
+        {
+            fComplUsed = 1;
+            pWord++;
+            if ( pMan->pNtkCur->pData == NULL )
+                pMan->pNtkCur->pData = Extra_MmFlexStart();
+        }
+        // get the actual net
+        pNetActual = Abc_NtkFindNet( pMan->pNtkCur, pWord );
+        if ( pNetActual == NULL )
+        {
+            sprintf( pMan->sError, "Actual net is missing in gate %s.", 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, pNtkGate->pName );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+
+        // process the pair
+        if ( Abc_ObjIsPi(Abc_ObjFanin0Ntk(pNetFormal)) )  // PI net (with polarity!)
+            Abc_ObjFanin0Ntk(pNetFormal)->pCopy = Abc_ObjNotCond( pNetActual, fCompl );
+        else if ( Abc_ObjIsPo(Abc_ObjFanout0Ntk(pNetFormal)) )  // P0 net
+        {
+            assert( fCompl == 0 );
+            Abc_ObjFanout0Ntk(pNetFormal)->pCopy = pNetActual; // Abc_ObjNotCond( pNetActual, fCompl );
+        }
+        else
+        {
+            sprintf( pMan->sError, "Cannot match formal net %s with PI or PO of the gate %s.", pWord, pNtkGate->pName );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+
+        // 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, pNtkGate->pName );
+            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 gate %s (expected closing semicolumn).", pNtkGate->pName );
+        Ver_ParsePrintErrorMessage( pMan );
+        return 0;
+    }
+
+    // make sure each input net is driven
+    Abc_NtkForEachPi( pNtkGate, pObj, i )
+        if ( pObj->pCopy == NULL )
+        {
+            sprintf( pMan->sError, "Formal input %s of gate %s has no actual input.", Abc_ObjFanout0(pObj)->pData, pNtkGate->pName );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+/*
+    // make sure each output net is driving something
+    Abc_NtkForEachPo( pNtkGate, pObj, i )
+        if ( pObj->pCopy == NULL )
+        {
+            sprintf( pMan->sError, "Formal output %s of gate %s has no actual output.", Abc_ObjFanin0(pObj)->pData, pNtkGate->pName );
+            Ver_ParsePrintErrorMessage( pMan );
+            return 0;
+        }
+*/
+
+    // allocate memory to remember the phase
+    pPolarity = NULL;
+    if ( fComplUsed )
+    {
+        int nBytes = 4 * Abc_BitWordNum( Abc_NtkPiNum(pNtkGate) );
+        pPolarity = (unsigned *)Extra_MmFlexEntryFetch( pMan->pNtkCur->pData, nBytes );
+        memset( pPolarity, 0, nBytes );
+    }
+    // create box to represent this gate
+    pNode = Abc_NtkCreateBlackbox( pMan->pNtkCur );
+/*
+    if ( pNode->Id == 57548 )
+    {
+        int x = 0;
+    }
+*/
+    pNode->pNext = (Abc_Obj_t *)pPolarity;
+    pNode->pData = pNtkGate;
+    // connect to fanin nets
+    Abc_NtkForEachPi( pNtkGate, pObj, i )
+    {
+        if ( pPolarity && Abc_ObjIsComplement(pObj->pCopy) )
+        {
+            Abc_InfoSetBit( pPolarity, i );
+            pObj->pCopy = Abc_ObjRegular( pObj->pCopy );
+        }
+        assert( !Abc_ObjIsComplement(pObj->pCopy) );
+        Abc_ObjAddFanin( pNode, pObj->pCopy );
+    }
+    // connect to fanout nets
+    Abc_NtkForEachPo( pNtkGate, pObj, i )
+    {
+        if ( pObj->pCopy )
+            Abc_ObjAddFanin( pObj->pCopy, pNode );
+        else
+            Abc_ObjAddFanin( Abc_NtkFindOrCreateNet(pNtk, NULL), pNode );
+    }
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Parses one directive.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ver_ParseGateStandard( Ver_Man_t * pMan, Ver_GateType_t GateType )
+{
+    Ver_Stream_t * p = pMan->pReader;
+    Hop_Man_t * pAig = pMan->pNtkCur->pManFunc;
+    Abc_Obj_t * pNet, * pNode;
+    char * pWord, Symbol;
+    // 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( pMan->pNtkCur );
+    // 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 = Abc_NtkFindNet( pMan->pNtkCur, 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( pAig, Abc_ObjFaninNum(pNode) );
+    else if ( GateType == VER_GATE_OR || GateType == VER_GATE_NOR )
+        pNode->pData = Hop_CreateOr( pAig, Abc_ObjFaninNum(pNode) );
+    else if ( GateType == VER_GATE_XOR || GateType == VER_GATE_XNOR )
+        pNode->pData = Hop_CreateExor( pAig, Abc_ObjFaninNum(pNode) );
+    else if ( GateType == VER_GATE_BUF || GateType == VER_GATE_NOT )
+        pNode->pData = Hop_CreateAnd( pAig, 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    [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  = Abc_NtkFindNet( 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  = Abc_NtkFindNet( 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 unknown (ABC_INIT_NONE).]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Ver_ParseCreateLatch( Abc_Ntk_t * pNtk, char * pNetLI, char * pNetLO )
+{
+    Abc_Obj_t * pLatch, * pNet;
+    // create a new latch and add it to the network
+    pLatch = Abc_NtkCreateLatch( pNtk );
+    // get the LI net
+    pNet = Abc_NtkFindOrCreateNet( pNtk, pNetLI );
+    Abc_ObjAddFanin( pLatch, pNet );
+    // get the LO net
+    pNet = Abc_NtkFindOrCreateNet( pNtk, pNetLO );
+    Abc_ObjAddFanin( pNet, pLatch );
+    return pLatch;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/ver/verFormula.c b/src/base/ver/verFormula.c
new file mode 100644
index 00000000..cfe3e0c8
--- /dev/null
+++ b/src/base/ver/verFormula.c
@@ -0,0 +1,469 @@
+/**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 )
+{
+    Hop_Obj_t * bFunc, * bTemp;
+    char * pTemp;
+    int nParans, Flag;
+    int Oper, Oper1, Oper2;
+    int v;
+
+    // clear the stacks and the names
+    Vec_PtrClear( vNames );
+    Vec_PtrClear( vStackFn );
+    Vec_IntClear( vStackOp );
+
+    // 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..8a78e75b
--- /dev/null
+++ b/src/base/ver/verParse.c
@@ -0,0 +1,115 @@
+/**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;
+    if ( !Ver_StreamIsOkey(p) )
+        return NULL;
+    if ( !Ver_ParseSkipComments( pMan ) )
+        return NULL;
+    Symbol = Ver_StreamScanChar( p );
+    if ( Symbol == '\\' )
+    {
+        Ver_StreamPopChar( p );
+        pWord = Ver_StreamGetWord( p, " " );
+    }
+    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..7956b13c
--- /dev/null
+++ b/src/base/ver/verStream.c
@@ -0,0 +1,435 @@
+/**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           4096    // 4K   - load new data when less than this is left
+#define VER_WORD_SIZE             4096    // 4K   - 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;
+    }
+    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++ )
+    {
+        // count the lines
+        if ( *pChar == '\n' )
+            p->nLineCounter++;
+        // 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;
+        }
+    }
+    // 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++ )
+    {
+        // count the lines
+        if ( *pChar == '\n' )
+            p->nLineCounter++;
+        // 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
+            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++ )
+    {
+        // count the lines
+        if ( *pChar == '\n' )
+            p->nLineCounter++;
+        // 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 )
+                return NULL;
+            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                                ///
+////////////////////////////////////////////////////////////////////////
+
+