Version abc51009

10 files changed, 18 insertions, 1011 deletions

diff --git a/abc.opt b/abc.opt
index 599d7688..801ad037 100644
--- a/abc.opt
+++ b/abc.opt
diff --git a/abc.plg b/abc.plg
index 2c576993..6b48f938 100644
--- a/abc.plg
+++ b/abc.plg
@@ -6,13 +6,13 @@
 --------------------Configuration: abc - Win32 Release--------------------
 </h3>
 <h3>Command Lines</h3>
-Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP194C.tmp" with contents
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1B74.tmp" with contents
 [
 /nologo /ML /W3 /GX /O2 /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\map\fpga" /I "src\map\pga" /I "src\map\mapper" /I "src\map\mapp" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /FR"Release/" /Fp"Release/abc.pch" /YX /Fo"Release/" /Fd"Release/" /FD /c 
-"C:\_projects\abc\src\base\abci\abcVanImp.c"
+"C:\_projects\abc\src\opt\sim\simSupp.c"
 ]
-Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP194C.tmp" 
-Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP194D.tmp" with contents
+Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1B74.tmp" 
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1B75.tmp" with contents
 [
 kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib /nologo /subsystem:console /incremental:no /pdb:"Release/abc.pdb" /machine:I386 /out:"_TEST/abc.exe" 
 .\Release\abcAig.obj
@@ -55,6 +55,7 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32
 .\Release\abcTiming.obj
 .\Release\abcUnreach.obj
 .\Release\abcVanEijk.obj
+.\Release\abcVanImp.obj
 .\Release\abcVerify.obj
 .\Release\abcFpgaDelay.obj
 .\Release\abcFpgaSeq.obj
@@ -178,6 +179,7 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32
 .\Release\msatClause.obj
 .\Release\msatClauseVec.obj
 .\Release\msatMem.obj
+.\Release\msatOrderH.obj
 .\Release\msatQueue.obj
 .\Release\msatRead.obj
 .\Release\msatSolverApi.obj
@@ -233,6 +235,7 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32
 .\Release\decUtil.obj
 .\Release\simMan.obj
 .\Release\simSat.obj
+.\Release\simSeq.obj
 .\Release\simSupp.obj
 .\Release\simSwitch.obj
 .\Release\simSym.obj
@@ -320,16 +323,13 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32
 .\Release\mvcPrint.obj
 .\Release\mvcSort.obj
 .\Release\mvcUtils.obj
-.\Release\abcVanImp.obj
-.\Release\simSeq.obj
-.\Release\msatOrderH.obj
 ]
-Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP194D.tmp"
+Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1B75.tmp"
 <h3>Output Window</h3>
 Compiling...
-abcVanImp.c
+simSupp.c
 Linking...
-Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP194F.tmp" with contents
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1B77.tmp" with contents
 [
 /nologo /o"Release/abc.bsc" 
 .\Release\abcAig.sbr
@@ -372,6 +372,7 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP194F.tmp" with cont
 .\Release\abcTiming.sbr
 .\Release\abcUnreach.sbr
 .\Release\abcVanEijk.sbr
+.\Release\abcVanImp.sbr
 .\Release\abcVerify.sbr
 .\Release\abcFpgaDelay.sbr
 .\Release\abcFpgaSeq.sbr
@@ -495,6 +496,7 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP194F.tmp" with cont
 .\Release\msatClause.sbr
 .\Release\msatClauseVec.sbr
 .\Release\msatMem.sbr
+.\Release\msatOrderH.sbr
 .\Release\msatQueue.sbr
 .\Release\msatRead.sbr
 .\Release\msatSolverApi.sbr
@@ -550,6 +552,7 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP194F.tmp" with cont
 .\Release\decUtil.sbr
 .\Release\simMan.sbr
 .\Release\simSat.sbr
+.\Release\simSeq.sbr
 .\Release\simSupp.sbr
 .\Release\simSwitch.sbr
 .\Release\simSym.sbr
@@ -636,11 +639,8 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP194F.tmp" with cont
 .\Release\mvcOpBool.sbr
 .\Release\mvcPrint.sbr
 .\Release\mvcSort.sbr
-.\Release\mvcUtils.sbr
-.\Release\abcVanImp.sbr
-.\Release\simSeq.sbr
-.\Release\msatOrderH.sbr]
-Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP194F.tmp"
+.\Release\mvcUtils.sbr]
+Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1B77.tmp"
 Creating browse info file...
 <h3>Output Window</h3>
 
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 24301ac3..aa5dedad 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -844,7 +844,7 @@ int Abc_CommandPrintSymms( Abc_Frame_t * pAbc, int argc, char ** argv )
 usage:
     fprintf( pErr, "usage: print_symm [-nbvh]\n" );
     fprintf( pErr, "\t         computes symmetries of the PO functions\n" );
-    fprintf( pErr, "\t-b     : toggle BDD-based or SAT-based computations [default = %s].\n", fUseBdds? "bdd": "sat" );  
+    fprintf( pErr, "\t-b     : toggle BDD-based or SAT-based computations [default = %s].\n", fUseBdds? "BDD": "SAT" );  
     fprintf( pErr, "\t-n     : enable naive BDD-based computation [default = %s].\n", fNaive? "yes": "no" );  
     fprintf( pErr, "\t-v     : enable verbose output [default = %s].\n", fVerbose? "yes": "no" );  
     fprintf( pErr, "\t-h     : print the command usage\n");
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index 4466cf99..660aee63 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -23,4 +23,5 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcTiming.c \
     src/base/abci/abcUnreach.c \
     src/base/abci/abcVanEijk.c \
+    src/base/abci/abcVanImp.c \
     src/base/abci/abcVerify.c 
diff --git a/src/misc/npn/npn.c b/src/misc/npn/npn.c
deleted file mode 100644
index ad4b4de6..00000000
--- a/src/misc/npn/npn.c
+++ /dev/null
@@ -1,202 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [npn.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName []
-
-  Synopsis    []
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: npn.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "extra.h"
-#include "npn.h"
-#include "vec.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-static int Npn_CompareVecs( void ** p0, void ** p1 );
-static Vec_Int_t * Npn_GetSignature( unsigned uTruth, int nVars );
-static void Npn_VecPrint( FILE * pFile, Vec_Int_t * vVec );
-static int Npn_VecProperty( Vec_Int_t * vVec );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Npn_Experiment()
-{
-    Vec_Int_t ** pVecs;
-    FILE * pFile;
-    int nFuncs, Num, i;
-
-    pFile = fopen( "npn5.txt", "r" );
-    pVecs = ALLOC( Vec_Int_t *, 1000000 );
-    for ( i = 0; ; i++ )
-    {
-        if ( fscanf( pFile, "%x", &Num ) != 1 )
-            break;
-        pVecs[i] = Npn_GetSignature( Num, 5 );
-        if ( Npn_VecProperty( pVecs[i] ) )
-        {
-            printf( "1s = %2d. ", Extra_CountOnes((unsigned char *)&Num, (1 << 5) / 8) );
-            Extra_PrintHex( stdout, Num, 5 ); fprintf( stdout, "\n" );
-        }
-        
-    }
-    nFuncs = i;
-    printf( "Read %d numbers.\n", nFuncs );
-    fclose( pFile );
-    /*
-    // sort the vectors
-    qsort( (void *)pVecs, nFuncs, sizeof(void *), 
-            (int (*)(const void *, const void *)) Npn_CompareVecs );
-    pFile = fopen( "npn5ar.txt", "w" );
-    for ( i = 0; i < nFuncs; i++ )
-    {
-        Npn_VecPrint( pFile, pVecs[i] );
-        Vec_IntFree( pVecs[i] );
-    }
-    fclose( pFile );
-    */
-
-    free( pVecs );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Npn_GetSignature( unsigned uTruth, int nVars )
-{
-    // elementary truth tables
-    static unsigned Signs[5] = {
-        0xAAAAAAAA,    // 1010 1010 1010 1010 1010 1010 1010 1010
-        0xCCCCCCCC,    // 1010 1010 1010 1010 1010 1010 1010 1010
-        0xF0F0F0F0,    // 1111 0000 1111 0000 1111 0000 1111 0000
-        0xFF00FF00,    // 1111 1111 0000 0000 1111 1111 0000 0000
-        0xFFFF0000     // 1111 1111 1111 1111 0000 0000 0000 0000
-    };
-    Vec_Int_t * vVec;
-    unsigned uCofactor;
-    int Count0, Count1, i;
-    int nBytes = (1 << nVars) / 8;
-
-    // collect the number of 1s in each cofactor
-    vVec = Vec_IntAlloc( 5 );
-    for ( i = 0; i < nVars; i++ )
-    {
-        uCofactor = uTruth & ~Signs[i];
-        Count0 = Extra_CountOnes( (unsigned char *)&uCofactor, nBytes );
-        uCofactor = uTruth &  Signs[i];
-        Count1 = Extra_CountOnes( (unsigned char *)&uCofactor, nBytes );
-        if ( Count0 < Count1 )
-            Vec_IntPush( vVec, Count0 );
-        else
-            Vec_IntPush( vVec, Count1 );
-    }
-    // sort them
-    Vec_IntSort( vVec, 0 );
-    return vVec;
-    
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Npn_CompareVecs( void ** p0, void ** p1 )
-{
-    Vec_Int_t * vVec0 = *p0;
-    Vec_Int_t * vVec1 = *p1;
-    int i;
-    assert( vVec0->nSize == vVec1->nSize );
-    for ( i = 0; i < vVec0->nSize; i++ )
-        if ( vVec0->pArray[i] < vVec1->pArray[i] )
-            return -1;
-        else if ( vVec0->pArray[i] > vVec1->pArray[i] )
-            return 1;
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Npn_VecPrint( FILE * pFile, Vec_Int_t * vVec )
-{
-    int i;
-    for ( i = 0; i < vVec->nSize; i++ )
-        fprintf( pFile, "%2d ", vVec->pArray[i] );
-    fprintf( pFile, "\n" );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Npn_VecProperty( Vec_Int_t * vVec )
-{
-    int i;
-    for ( i = 0; i < vVec->nSize; i++ )
-        if ( vVec->pArray[i] != i + 1 )
-            return 0;
-    return 1;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/misc/npn/npn.h b/src/misc/npn/npn.h
deleted file mode 100644
index 61aa6297..00000000
--- a/src/misc/npn/npn.h
+++ /dev/null
@@ -1,105 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [npn.h]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName []
-
-  Synopsis    [External declarations.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: npn.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
- 
-#ifndef __NPN_H__
-#define __NPN_H__
-
-////////////////////////////////////////////////////////////////////////
-///                          INCLUDES                                ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                         PARAMETERS                               ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                         BASIC TYPES                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                      MACRO DEFITIONS                             ///
-////////////////////////////////////////////////////////////////////////
-
-#define EXTRA_WORD_VARS     5
-
-////////////////////////////////////////////////////////////////////////
-///                    FUNCTION DEFINITIONS                          ///
-////////////////////////////////////////////////////////////////////////
-
-static inline int Extra_BitCharNum( int nVars )  {  if ( nVars <= 3 )  return 1;                return 1 << (nVars - 3); }
-static inline int Extra_BitWordNum( int nVars )  {  if ( nVars <= EXTRA_WORD_VARS )  return 1;  return 1 << (nVars - EXTRA_WORD_VARS); }
-
-static inline int  Extra_BitRead( uint8 * pBits, int iBit )  { return ( (pBits[iBit/8] & (1 << (iBit%8))) > 0 ); }
-static inline void Extra_BitSet( uint8 * pBits, int iBit )   { pBits[iBit/8] |= (1 << (iBit%8));                 }
-static inline void Extra_BitXor( uint8 * pBits, int iBit )   { pBits[iBit/8] ^= (1 << (iBit%8));                 }
-
-static inline void Extra_BitClean( int nVars, uint8 * pBits )
-{
-    unsigned * pWords = (unsigned *)pBits;
-    int i;
-    for ( i = Extra_BitWordNum(nVars) - 1; i >= 0; i-- )
-        pWords[i] = 0;
-}
-static inline void Extra_BitNot( int nVars, uint8 * pBits )
-{
-    unsigned * pWords = (unsigned *)pBits;
-    int i;
-    for ( i = Extra_BitWordNum(nVars) - 1; i >= 0; i-- )
-        pWords[i] = ~pWords[i];
-}
-static inline void Extra_BitCopy( int nVars, uint8 * pBits1, uint8 * pBits )
-{
-    unsigned * pWords  = (unsigned *)pBits;
-    unsigned * pWords1 = (unsigned *)pBits1;
-    int i;
-    for ( i = Extra_BitWordNum(nVars) - 1; i >= 0; i-- )
-        pWords[i] = pWords1[i];
-}
-static inline void Extra_BitAnd( int nVars, uint8 * pBits1, uint8 * pBits2, uint8 * pBits )
-{
-    unsigned * pWords  = (unsigned *)pBits;
-    unsigned * pWords1 = (unsigned *)pBits1;
-    unsigned * pWords2 = (unsigned *)pBits2;
-    int i;
-    for ( i = Extra_BitWordNum(nVars) - 1; i >= 0; i-- )
-        pWords[i] = pWords1[i] & pWords2[i];
-}
-static inline void Extra_BitSharp( int nVars, uint8 * pBits1, uint8 * pBits2, uint8 * pBits )
-{
-    unsigned * pWords  = (unsigned *)pBits;
-    unsigned * pWords1 = (unsigned *)pBits1;
-    unsigned * pWords2 = (unsigned *)pBits2;
-    int i;
-    for ( i = Extra_BitWordNum(nVars) - 1; i >= 0; i-- )
-        pWords[i] = pWords1[i] & ~pWords2[i];
-}
-
-////////////////////////////////////////////////////////////////////////
-///                    FUNCTION DECLARATIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/*=== zzz.c ==========================================================*/
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-#endif
-
diff --git a/src/misc/npn/npnGenStr.c b/src/misc/npn/npnGenStr.c
deleted file mode 100644
index adbfdcdf..00000000
--- a/src/misc/npn/npnGenStr.c
+++ /dev/null
@@ -1,473 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [npnUtil.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName []
-
-  Synopsis    []
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: npnUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "extra.h"
-#include "npn.h"
-#include "vec.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-static Vec_Ptr_t * Npn_Generate_rec( int nVars, int fFold );
-static void Npn_GenerateMerge( Vec_Ptr_t * vVec1, Vec_Ptr_t * vVec2, Vec_Ptr_t * vVec );
-static void Npn_GenerateFree( Vec_Ptr_t * vVec );
-static Vec_Ptr_t * Npn_GenerateFold( Vec_Ptr_t * vVec );
-static void Npn_GenerateEmbed( Vec_Ptr_t * vVec );
-static void Npn_GeneratePrint( Vec_Ptr_t * vVec );
-
-
-static void Npn_RewritePrint( Vec_Ptr_t * vVec );
-static Vec_Ptr_t * Npn_Rewrite( char * pStruct );
-
-static int Npn_RewriteNumEntries( char * pString );
-static int Npn_RewriteLastAnd( char * pBeg, char * pString );
-static int Npn_RewriteLastExor( char * pBeg, char * pString );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Npn_Generate()
-{
-    Vec_Ptr_t * vVec;
-    vVec = Npn_Generate_rec( 7, 1 );
-    Npn_GenerateEmbed( vVec );
-    Npn_GeneratePrint( vVec );
-    Npn_GenerateFree( vVec );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Npn_Generate_rec( int nVars, int fFold )
-{
-    char Buffer[20], * pChar;
-    Vec_Ptr_t * vVec, * vVec1, * vVec2, * pTemp;
-    int i;
-
-    vVec = Vec_PtrAlloc( 100 );
-
-    // generate the combination
-    pChar = Buffer;
-    for ( i = 0; i < nVars; i++ )
-        *pChar++ = '.';
-    *pChar++ = 0;
-
-    Vec_PtrPush( vVec, util_strsav(Buffer) );
-    if ( nVars == 2 || !fFold )
-        return vVec;
-
-    assert( nVars > 2 );
-    for ( i = 2; i < nVars; i++ )
-    {
-        vVec1 = Npn_Generate_rec( i, 1 );
-        vVec1 = Npn_GenerateFold( pTemp = vVec1 );
-        Npn_GenerateFree( pTemp );
-        // add folded pairs
-        if ( nVars - i > 1 )
-        {
-            vVec2 = Npn_Generate_rec( nVars - i, 1 );
-            vVec2 = Npn_GenerateFold( pTemp = vVec2 );
-            Npn_GenerateFree( pTemp );
-            Npn_GenerateMerge( vVec1, vVec2, vVec );
-            Npn_GenerateFree( vVec2 );
-        }
-        // add unfolded pairs
-        vVec2 = Npn_Generate_rec( nVars - i, 0 );
-        Npn_GenerateMerge( vVec1, vVec2, vVec );
-        Npn_GenerateFree( vVec2 );
-        Npn_GenerateFree( vVec1 );
-    }
-    return vVec;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Npn_GenerateMerge( Vec_Ptr_t * vVec1, Vec_Ptr_t * vVec2, Vec_Ptr_t * vVec )
-{
-    char Buffer[100];
-    char * pEntry1, * pEntry2, * pEntry;
-    int i, k, m;
-    Vec_PtrForEachEntry( vVec1, pEntry1, i )
-    Vec_PtrForEachEntry( vVec2, pEntry2, k )
-    {
-        if ( *pEntry1 == '(' && *pEntry2 == '(' )
-            if ( strcmp( pEntry1, pEntry2 ) > 0 )
-                continue;
-
-        // get the new entry
-        sprintf( Buffer, "%s%s", pEntry1, pEntry2 );
-        // skip duplicates
-        Vec_PtrForEachEntry( vVec, pEntry, m )
-            if ( strcmp( pEntry, Buffer ) == 0 )
-                break;
-        if ( m != Vec_PtrSize(vVec) )
-            continue;
-        // add the new entry
-        Vec_PtrPush( vVec, util_strsav(Buffer) );
-    }    
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Npn_GenerateFree( Vec_Ptr_t * vVec )
-{
-    char * pEntry;
-    int i;
-    Vec_PtrForEachEntry( vVec, pEntry, i )
-        free( pEntry );
-    Vec_PtrFree( vVec );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Npn_GenerateFold( Vec_Ptr_t * vVec )
-{
-    Vec_Ptr_t * vVecR;
-    char Buffer[100];
-    char * pEntry;
-    int i;
-    vVecR = Vec_PtrAlloc( 10 );
-    Vec_PtrForEachEntry( vVec, pEntry, i )
-    {
-        // add entry without folding if the second part is folded
-        if ( pEntry[strlen(pEntry) - 1] == ')' )
-            Vec_PtrPush( vVecR, util_strsav(pEntry) );
-        // add the entry with folding
-        sprintf( Buffer, "(%s)", pEntry );
-        Vec_PtrPush( vVecR, util_strsav(Buffer) );
-    }
-    return vVecR;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Npn_GenerateEmbed( Vec_Ptr_t * vVec )
-{
-    char Buffer[100];
-    char * pEntry;
-    int i;
-    Vec_PtrForEachEntry( vVec, pEntry, i )
-    {
-        sprintf( Buffer, "(%s)", pEntry );
-        Vec_PtrWriteEntry( vVec, i, util_strsav(Buffer) );
-        free( pEntry );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Npn_GeneratePrint( Vec_Ptr_t * vVec )
-{
-    char * pEntry;
-    int i;
-    Vec_PtrForEachEntry( vVec, pEntry, i )
-    {
-        printf( "%5d : %s\n", i, pEntry );
-
-        {
-            Vec_Ptr_t * vFuncs;
-            vFuncs = Npn_Rewrite( pEntry );
-            Npn_RewritePrint( vFuncs );
-            Vec_PtrFree( vFuncs );
-        }
-    }
-}
-
-
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Npn_RewritePrint( Vec_Ptr_t * vVec )
-{
-    char * pEntry;
-    int i;
-    Vec_PtrForEachEntry( vVec, pEntry, i )
-        printf( "    %3d : %s\n", i, pEntry );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Npn_Rewrite_rec( char * pStruct, Vec_Ptr_t * vVec, Vec_Str_t * vForm )
-{
-    int nSizeOld;
-    char * pCur;
-    // find the next opening paranthesis
-    for ( pCur = pStruct; *pCur; pCur++ )
-    {
-        if ( *pCur == '(' )
-            break;
-        Vec_StrPush( vForm, *pCur );
-    }
-    // the paranthesis is not found quit
-    if ( *pCur == 0 )
-    {
-        Vec_StrPush( vForm, 0 );
-        Vec_PtrPush( vVec, util_strsav( vForm->pArray ) );
-        return;
-    }
-    assert( *pCur == '(' );
-    pCur++;
-    // remember the current size
-    nSizeOld = vForm->nSize;
-    // add different types
-    if ( Npn_RewriteLastAnd(vForm->pArray, vForm->pArray+vForm->nSize) )
-    {
-        Vec_StrPush( vForm, 'N' );
-        Vec_StrPush( vForm, '(' );
-        Npn_Rewrite_rec( pCur, vVec, vForm );
-        Vec_StrShrink( vForm, nSizeOld );
-    }
-    else
-    {
-        Vec_StrPush( vForm, 'A' );
-        Vec_StrPush( vForm, '(' );
-        Npn_Rewrite_rec( pCur, vVec, vForm );
-        Vec_StrShrink( vForm, nSizeOld );
-    }
-    // add different types
-    if ( Npn_RewriteNumEntries(pCur) == 3 )
-    {
-        Vec_StrPush( vForm, 'P' );
-        Vec_StrPush( vForm, '(' );
-        Npn_Rewrite_rec( pCur, vVec, vForm );
-        Vec_StrShrink( vForm, nSizeOld );
-    }
-    // add different types
-    if ( !Npn_RewriteLastExor(vForm->pArray, vForm->pArray+vForm->nSize) )
-    {
-        Vec_StrPush( vForm, 'X' );
-        Vec_StrPush( vForm, '(' );
-        Npn_Rewrite_rec( pCur, vVec, vForm );
-        Vec_StrShrink( vForm, nSizeOld );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Npn_Rewrite( char * pStruct )
-{
-    Vec_Ptr_t * vVec;
-    Vec_Str_t * vForm;
-    vVec  = Vec_PtrAlloc( 10 );
-    vForm = Vec_StrAlloc( 10 );
-    Npn_Rewrite_rec( pStruct, vVec, vForm );
-    Vec_StrFree( vForm );
-    return vVec;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Npn_RewriteNumEntries( char * pString )
-{
-    char * pCur;
-    int Counter = 0;
-    int nPars = 0;
-    for ( pCur = pString; *pCur; pCur++ )
-    {
-        if ( nPars == 0 )
-        {
-            if ( *pCur == '.' )
-                Counter++;
-            else if ( *pCur == '(' )
-            {
-                Counter++;
-                nPars++;
-            }
-            else if ( *pCur == ')' )
-                nPars--;
-        }
-        else if ( nPars > 0 )
-        {
-            if ( *pCur == '(' )
-                nPars++;
-            else if ( *pCur == ')' )
-                nPars--;
-        }
-        else
-            break;
-    }
-    return Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if the last was EXOR.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Npn_RewriteLastAnd( char * pBeg, char * pEnd )
-{
-    char * pCur;
-    int nPars = 1;
-    for ( pCur = pEnd - 1; pCur >= pBeg; pCur-- )
-    {
-            if ( *pCur == ')' )
-                nPars++;
-            else if ( *pCur == '(' )
-                nPars--;
-
-            if ( nPars == 0 && *pCur == 'A' )
-                return 1;
-    }
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if the last was EXOR.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Npn_RewriteLastExor( char * pBeg, char * pEnd )
-{
-    char * pCur;
-    int nPars = 1;
-    for ( pCur = pEnd - 1; pCur >= pBeg; pCur-- )
-    {
-            if ( *pCur == ')' )
-                nPars++;
-            else if ( *pCur == '(' )
-                nPars--;
-
-            if ( nPars == 0 && *pCur == 'X' )
-                return 1;
-    }
-    return 0;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/misc/npn/npnTruth.c b/src/misc/npn/npnTruth.c
deleted file mode 100644
index b6be775b..00000000
--- a/src/misc/npn/npnTruth.c
+++ /dev/null
@@ -1,137 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [npnUtil.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName []
-
-  Synopsis    []
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: npnUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "extra.h"
-#include "npn.h"
-#include "vec.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Checks if the variable belongs to the support.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Extra_TruthCofactors( int nVars, uint8 * puTruth, uint8 * puElem[][32], 
-    uint8 * puTruthCofs0[][32], uint8 * puTruthCofs1[][32] )
-{
-    int v;
-    for ( v = 0; v < nVars; v++ )
-    {
-        Extra_BitSharp( nVars, puTruth, puElem[v], (uint8 *)puTruthCofs0[v] );
-        Extra_BitAnd  ( nVars, puTruth, puElem[v], (uint8 *)puTruthCofs1[v] );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Checks if the variable belongs to the support.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Extra_TruthCountCofactorOnes( int nVars, uint8 * puTruthCofs[][32], int * pCounts )
-{
-    int v, nBytes;
-    nBytes = Extra_BitCharNum( nVars );
-    for ( v = 0; v < nVars; v++ )
-        pCounts[v] = Extra_CountOnes( puTruthCofs[v], nBytes );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Checks if the variable belongs to the support.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Extra_TruthHasVar( int nVars, uint8 * puTruth, int iVar )
-{
-    // elementary truth tables
-    static uint8 Signs[3] = {
-        0xAA,    // 1010 1010
-        0xCC,    // 1100 1100
-        0xF0     // 1111 0000
-    };
-    int nChars, nShift, i;
-    assert( iVar < nVars );
-    nChars = Extra_BitCharNum( nVars );
-    if ( iVar < 3 )
-    {
-        nShift = (1 << iVar);
-        for ( i = 0; i < nChars; i++ )
-            if ( ((puTruth[i] & Signs[iVar]) >> nShift) != (puTruth[i] & ~Signs[iVar]) )
-                return 1;
-    }
-    else
-    {
-        nShift = (1 << (iVar-3));
-        for ( i = 0; i < nChars; i++, i = (i % nShift)? i : i + nShift )
-            if ( puTruth[i] != puTruth[i+nShift] )
-                return 1;
-    }
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Checks if the variable belongs to the support.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Npn_VarsTest( int nVars, uint8 * puTruth )
-{
-    int v;
-    int Counter = 0;
-    for ( v = 0; v < nVars; v++ )
-        Counter += Extra_TruthHasVar( nVars, puTruth, v );
-    return Counter;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/misc/npn/npnUtil.c b/src/misc/npn/npnUtil.c
deleted file mode 100644
index b12ad092..00000000
--- a/src/misc/npn/npnUtil.c
+++ /dev/null
@@ -1,78 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [npnUtil.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName []
-
-  Synopsis    []
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: npnUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "extra.h"
-#include "npn.h"
-#include "vec.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Npn_StartTruth8( uint8 uTruths[][32] )
-{
-    // elementary truth tables
-    static uint8 Signs[3] = {
-        0xAA,    // 1010 1010
-        0xCC,    // 1100 1100
-        0xF0     // 1111 0000
-    };
-    int v, i, nShift;
-    for ( v = 0; v < 3; v++ )
-        for ( i = 0; i < 32; i++ )
-            uTruths[v][i] = Signs[v];
-    for ( v = 3; v < 8; v++ )
-    {
-        nShift = (1 << (v-3));
-        for ( i = 0; i < 32; i++, i = (i % nShift)? i : i + nShift )
-        {
-            uTruths[v][i]          = 0;
-            uTruths[v][i + nShift] = 0xFF;
-        }
-    }
-/*
-    for ( v = 0; v < 8; v++ )
-    {
-        Extra_PrintBinary( stdout, (unsigned int*)uTruths[v], 90 );
-        printf( "\n" );
-    }
-*/
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/opt/sim/module.make b/src/opt/sim/module.make
index 43d0a125..54058402 100644
--- a/src/opt/sim/module.make
+++ b/src/opt/sim/module.make
@@ -1,5 +1,6 @@
 SRC +=  src/opt/sim/simMan.c \
     src/opt/sim/simSat.c \
+    src/opt/sim/simSeq.c \
     src/opt/sim/simSupp.c \
     src/opt/sim/simSwitch.c \
     src/opt/sim/simSym.c \