Version abc61122

8 files changed, 0 insertions, 2325 deletions

diff --git a/src/temp/ver/module.make b/src/temp/ver/module.make
deleted file mode 100644
index a58a2c60..00000000
--- a/src/temp/ver/module.make
+++ /dev/null
@@ -1,4 +0,0 @@
-SRC +=    src/temp/ver/verCore.c \
-    src/temp/ver/verFormula.c \
-    src/temp/ver/verParse.c \
-    src/temp/ver/verStream.c 
diff --git a/src/temp/ver/ver.h b/src/temp/ver/ver.h
deleted file mode 100644
index c7c18f79..00000000
--- a/src/temp/ver/ver.h
+++ /dev/null
@@ -1,114 +0,0 @@
-/**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/temp/ver/verCore.c b/src/temp/ver/verCore.c
deleted file mode 100644
index 352a4361..00000000
--- a/src/temp/ver/verCore.c
+++ /dev/null
@@ -1,1092 +0,0 @@
-/**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;
-    Aig_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;
-    Aig_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 = Aig_CreateAnd( pAig, Abc_ObjFaninNum(pNode) );
-    else if ( GateType == VER_GATE_OR || GateType == VER_GATE_NOR )
-        pNode->pData = Aig_CreateOr( pAig, Abc_ObjFaninNum(pNode) );
-    else if ( GateType == VER_GATE_XOR || GateType == VER_GATE_XNOR )
-        pNode->pData = Aig_CreateExor( pAig, Abc_ObjFaninNum(pNode) );
-    else if ( GateType == VER_GATE_BUF || GateType == VER_GATE_NOT )
-        pNode->pData = Aig_CreateAnd( pAig, Abc_ObjFaninNum(pNode) );
-    if ( GateType == VER_GATE_NAND || GateType == VER_GATE_NOR || GateType == VER_GATE_XNOR || GateType == VER_GATE_NOT )
-        pNode->pData = Aig_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/temp/ver/verFormula.c b/src/temp/ver/verFormula.c
deleted file mode 100644
index fd8777c3..00000000
--- a/src/temp/ver/verFormula.c
+++ /dev/null
@@ -1,469 +0,0 @@
-/**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 Aig_Obj_t * Ver_FormulaParserTopOper( Aig_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 )
-{
-    Aig_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, Aig_ManConst0(pMan) );  // Cudd_Ref( Aig_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, Aig_ManConst1(pMan) );  //  Cudd_Ref( Aig_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 = Aig_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, Aig_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     []
-
-***********************************************************************/
-Aig_Obj_t * Ver_FormulaParserTopOper( Aig_Man_t * pMan, Vec_Ptr_t * vStackFn, int Oper )
-{
-    Aig_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 = Aig_And( pMan, bArg1, bArg2 );
-    else if ( Oper == VER_PARSE_OPER_XOR )
-        bFunc = Aig_Exor( pMan, bArg1, bArg2 );
-    else if ( Oper == VER_PARSE_OPER_OR )
-        bFunc = Aig_Or( pMan, bArg1, bArg2 );
-    else if ( Oper == VER_PARSE_OPER_EQU )
-        bFunc = Aig_Not( Aig_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 = Aig_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 )
-{
-    Aig_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 = Aig_CreateAnd( pMan, Vec_PtrSize(vNames)/2 );
-    else if ( Symbol == '|' )
-        pRes = Aig_CreateOr( pMan, Vec_PtrSize(vNames)/2 );
-    else if ( Symbol == '^' )
-        pRes = Aig_CreateExor( pMan, Vec_PtrSize(vNames)/2 );
-    return Aig_NotCond( pRes, fCompl );
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/temp/ver/verParse.c b/src/temp/ver/verParse.c
deleted file mode 100644
index 8a78e75b..00000000
--- a/src/temp/ver/verParse.c
+++ /dev/null
@@ -1,115 +0,0 @@
-/**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/temp/ver/verStream.c b/src/temp/ver/verStream.c
deleted file mode 100644
index 7956b13c..00000000
--- a/src/temp/ver/verStream.c
+++ /dev/null
@@ -1,435 +0,0 @@
-/**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/temp/ver/verWords.c b/src/temp/ver/verWords.c
deleted file mode 100644
index f9d27010..00000000
--- a/src/temp/ver/verWords.c
+++ /dev/null
@@ -1,48 +0,0 @@
-/**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/temp/ver/ver_.c b/src/temp/ver/ver_.c
deleted file mode 100644
index 76599dac..00000000
--- a/src/temp/ver/ver_.c
+++ /dev/null
@@ -1,48 +0,0 @@
-/**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                                ///
-////////////////////////////////////////////////////////////////////////
-
-