Version abc51007

18 files changed, 1952 insertions, 118 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 968dc596..2ef7d83a 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -536,6 +536,7 @@ extern void               Abc_NtkAddDummyPiNames( Abc_Ntk_t * pNtk );
 extern void               Abc_NtkAddDummyPoNames( Abc_Ntk_t * pNtk );
 extern void               Abc_NtkAddDummyLatchNames( Abc_Ntk_t * pNtk );
 extern void               Abc_NtkShortNames( Abc_Ntk_t * pNtk );
+extern stmm_table *       Abc_NtkNamesToTable( Vec_Ptr_t * vNodes );
 /*=== abcNetlist.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkNetlistToLogic( Abc_Ntk_t * pNtk );
 extern Abc_Ntk_t *        Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk );
diff --git a/src/base/abc/abcNames.c b/src/base/abc/abcNames.c
index 0abccd0a..dd97820d 100644
--- a/src/base/abc/abcNames.c
+++ b/src/base/abc/abcNames.c
@@ -547,6 +547,28 @@ void Abc_NtkShortNames( Abc_Ntk_t * pNtk )
     Abc_NtkAddDummyLatchNames( pNtk );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Returns the hash table with these names.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+stmm_table * Abc_NtkNamesToTable( Vec_Ptr_t * vNodes )
+{
+    stmm_table * tTable;
+    Abc_Obj_t * pObj;
+    int i;
+    tTable = stmm_init_table(strcmp, stmm_strhash);
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        stmm_insert( tTable, Abc_ObjName(pObj), (char *)pObj );
+    return tTable;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index cde9c16b..24301ac3 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -2293,7 +2293,7 @@ int Abc_CommandFrames( Abc_Frame_t * pAbc, int argc, char ** argv )
             }
             nFrames = atoi(argv[util_optind]);
             util_optind++;
-            if ( nFrames < 0 ) 
+            if ( nFrames <= 0 ) 
                 goto usage;
             break;
         case 'i':
@@ -5114,8 +5114,10 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     int nFrames;
     int fExdc;
+    int fImp;
     int fVerbose;
     extern Abc_Ntk_t * Abc_NtkVanEijk( Abc_Ntk_t * pNtk, int nFrames, int fExdc, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkVanImp( Abc_Ntk_t * pNtk, int nFrames, int fExdc, int fVerbose );
 
     pNtk = Abc_FrameReadNet(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -5124,9 +5126,10 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     nFrames  = 1;
     fExdc    = 1;
+    fImp     = 0;
     fVerbose = 1;
     util_getopt_reset();
-    while ( ( c = util_getopt( argc, argv, "Fevh" ) ) != EOF )
+    while ( ( c = util_getopt( argc, argv, "Feivh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -5138,12 +5141,15 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
             }
             nFrames = atoi(argv[util_optind]);
             util_optind++;
-            if ( nFrames < 0 ) 
+            if ( nFrames <= 0 ) 
                 goto usage;
             break;
         case 'e':
             fExdc ^= 1;
             break;
+        case 'i':
+            fImp ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -5179,7 +5185,10 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the new network
-    pNtkRes = Abc_NtkVanEijk( pNtk, nFrames, fExdc, fVerbose );
+    if ( fImp )
+        pNtkRes = Abc_NtkVanImp( pNtk, nFrames, fExdc, fVerbose );
+    else
+        pNtkRes = Abc_NtkVanEijk( pNtk, nFrames, fExdc, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Sequential FPGA mapping has failed.\n" );
@@ -5190,10 +5199,11 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: seq_sweep [-F num] [-vh]\n" );
+    fprintf( pErr, "usage: seq_sweep [-F num] [-eivh]\n" );
     fprintf( pErr, "\t         performs sequential sweep using van Eijk's method\n" );
     fprintf( pErr, "\t-F num : number of time frames in the base case [default = %d]\n", nFrames );
     fprintf( pErr, "\t-e     : toggle writing EXDC network [default = %s]\n", fExdc? "yes": "no" );
+    fprintf( pErr, "\t-i     : toggle computing implications [default = %s]\n", fImp? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
@@ -5342,7 +5352,7 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
             }
             nFrames = atoi(argv[util_optind]);
             util_optind++;
-            if ( nFrames < 0 ) 
+            if ( nFrames <= 0 ) 
                 goto usage;
             break;
         case 'T':
diff --git a/src/base/abci/abcUnreach.c b/src/base/abci/abcUnreach.c
index e932d076..a8ecef5c 100644
--- a/src/base/abci/abcUnreach.c
+++ b/src/base/abci/abcUnreach.c
@@ -285,7 +285,7 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn
 
     // start the new network
     pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_BDD );
-    pNtkNew->pName = util_strsav("exdc");
+    pNtkNew->pName = util_strsav( "exdc" );
     pNtkNew->pSpec = NULL;
 
     // create PIs corresponding to LOs
diff --git a/src/base/abci/abcVanEijk.c b/src/base/abci/abcVanEijk.c
index d0179514..d7406ba6 100644
--- a/src/base/abci/abcVanEijk.c
+++ b/src/base/abci/abcVanEijk.c
@@ -35,10 +35,12 @@ static int            Abc_NtkVanEijkClassesRefine( Abc_Ntk_t * pNtk, Vec_Ptr_t *
 static void           Abc_NtkVanEijkClassesOrder( Vec_Ptr_t * vClasses );
 static int            Abc_NtkVanEijkClassesCountPairs( Vec_Ptr_t * vClasses );
 static void           Abc_NtkVanEijkClassesTest( Abc_Ntk_t * pNtkSingle, Vec_Ptr_t * vClasses );
-static Abc_Ntk_t *    Abc_NtkVanEijkFrames( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int nFrames, int fAddLast, int fShortNames );
-static void           Abc_NtkVanEijkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_Ptr_t * vCorresp, Vec_Ptr_t * vOrder, int fShortNames );
-static Fraig_Man_t *  Abc_NtkVanEijkFraig( Abc_Ntk_t * pMulti, int fInit );
-static Abc_Ntk_t *    Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtkInit, Abc_Ntk_t * pNtk, Vec_Ptr_t * vClasses );
+
+extern Abc_Ntk_t *    Abc_NtkVanEijkFrames( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int nFrames, int fAddLast, int fShortNames );
+extern void           Abc_NtkVanEijkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_Ptr_t * vCorresp, Vec_Ptr_t * vOrder, int fShortNames );
+extern Fraig_Man_t *  Abc_NtkVanEijkFraig( Abc_Ntk_t * pMulti, int fInit );
+
+static Abc_Ntk_t *    Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vClasses );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     INLINED FUNCTIONS                            ///
@@ -99,6 +101,7 @@ Abc_Ntk_t * Abc_NtkVanEijk( Abc_Ntk_t * pNtk, int nFrames, int fExdc, int fVerbo
     Fraig_ParamsSetDefaultFull( &Params );
     pNtkSingle = Abc_NtkFraig( pNtk, &Params, 0, 0 );
     Abc_AigSetNodePhases( pNtkSingle );
+    Abc_NtkCleanNext(pNtkSingle);
 
     // get the equivalence classes
     vClasses = Abc_NtkVanEijkClasses( pNtkSingle, nFrames, fVerbose );
@@ -109,7 +112,7 @@ Abc_Ntk_t * Abc_NtkVanEijk( Abc_Ntk_t * pNtk, int nFrames, int fExdc, int fVerbo
 //        pNtkNew = Abc_NtkDup( pNtkSingle );  
         // derive the EXDC network if asked
         if ( fExdc )
-            pNtkNew->pExdc = Abc_NtkVanEijkDeriveExdc( pNtk, pNtkSingle, vClasses );
+            pNtkNew->pExdc = Abc_NtkVanEijkDeriveExdc( pNtkSingle, vClasses );
     }
     else
         pNtkNew = Abc_NtkDup( pNtkSingle );  
@@ -137,23 +140,23 @@ Vec_Ptr_t * Abc_NtkVanEijkClasses( Abc_Ntk_t * pNtkSingle, int nFrames, int fVer
     Abc_Ntk_t * pNtkMulti;
     Vec_Ptr_t * vCorresp, * vClasses;
     int nIter, RetValue;
+    int nAddFrames = 0;
 
     if ( fVerbose )
         printf( "The number of ANDs after FRAIGing = %d.\n", Abc_NtkNodeNum(pNtkSingle) );
 
     // get the AIG of the base case
     vCorresp = Vec_PtrAlloc( 100 );
-    Abc_NtkCleanNext(pNtkSingle);
-    pNtkMulti = Abc_NtkVanEijkFrames( pNtkSingle, vCorresp, nFrames, 0, 0 );
+    pNtkMulti = Abc_NtkVanEijkFrames( pNtkSingle, vCorresp, nFrames + nAddFrames, 0, 0 );
     if ( fVerbose )
-        printf( "The number of ANDs in %d timeframes = %d.\n", nFrames, Abc_NtkNodeNum(pNtkMulti) );
+        printf( "The number of ANDs in %d timeframes = %d.\n", nFrames + nAddFrames, Abc_NtkNodeNum(pNtkMulti) );
 
     // FRAIG the initialized frames (labels the nodes of pNtkMulti with FRAIG nodes to be used as hash keys)
     pFraig = Abc_NtkVanEijkFraig( pNtkMulti, 1 );
     Fraig_ManFree( pFraig );
 
     // find initial equivalence classes
-    vClasses = Abc_NtkVanEijkClassesDeriveBase( pNtkSingle, vCorresp, nFrames );
+    vClasses = Abc_NtkVanEijkClassesDeriveBase( pNtkSingle, vCorresp, nFrames + nAddFrames );
     if ( fVerbose )
         printf( "The number of classes in the base case    = %5d.  Pairs = %8d.\n", Vec_PtrSize(vClasses), Abc_NtkVanEijkClassesCountPairs(vClasses) );
     Abc_NtkDelete( pNtkMulti );
@@ -192,6 +195,12 @@ Vec_Ptr_t * Abc_NtkVanEijkClasses( Abc_Ntk_t * pNtkSingle, int nFrames, int fVer
             for ( pObj = pClass; pObj; pObj = pObj->pNext )
                 Counter++;
             printf( " %d", Counter );
+/*
+            printf( " = {" );
+            for ( pObj = pClass; pObj; pObj = pObj->pNext )
+                printf( " %d", pObj->Id );
+            printf( " } " );
+*/
         }
         printf( "\n" );
     }
@@ -541,7 +550,9 @@ Abc_Ntk_t * Abc_NtkVanEijkFrames( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int nF
         pLatch->pNext = NULL;
     }
     // remove dangling nodes
-    Abc_AigCleanup( pNtkFrames->pManFunc );
+//    Abc_AigCleanup( pNtkFrames->pManFunc );
+    // otherwise some external nodes may have dandling pointers
+
     // make sure that everything is okay
     if ( !Abc_NtkCheck( pNtkFrames ) )
         printf( "Abc_NtkVanEijkFrames: The network check has failed.\n" );
@@ -699,7 +710,7 @@ Fraig_Man_t * Abc_NtkVanEijkFraig( Abc_Ntk_t * pMulti, int fInit )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtkInit, Abc_Ntk_t * pNtk, Vec_Ptr_t * vClasses )
+Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vClasses )
 {
     Abc_Ntk_t * pNtkNew; 
     Abc_Obj_t * pClass, * pNode, * pRepr, * pObj;
@@ -707,6 +718,8 @@ Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtkInit, Abc_Ntk_t * pNtk, Ve
     Vec_Ptr_t * vCone;
     int i, k;
 
+    assert( Abc_NtkIsStrash(pNtk) );
+
     // start the network
     pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc );
     pNtkNew->pName = util_strsav("exdc");
@@ -716,7 +729,7 @@ Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtkInit, Abc_Ntk_t * pNtk, Ve
     Abc_AigConst1(pNtk->pManFunc)->pCopy = Abc_AigConst1(pNtkNew->pManFunc);
     // for each CI, create PI
     Abc_NtkForEachCi( pNtk, pObj, i )
-        Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePi(pNtkNew), Abc_ObjName( Abc_NtkCi(pNtkInit,i) ) );
+        Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePi(pNtkNew), Abc_ObjName(pObj) );
     // cannot add latches here because pLatch->pCopy pointers are used
 
     // create the cones for each pair of nodes in an equivalence class
@@ -756,9 +769,9 @@ Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtkInit, Abc_Ntk_t * pNtk, Ve
     // for each CO, create PO (skip POs equal to CIs because of name conflict)
     Abc_NtkForEachPo( pNtk, pObj, i )
         if ( !Abc_ObjIsCi(Abc_ObjFanin0(pObj)) )
-            Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjName( Abc_NtkPo(pNtkInit,i) ) );
+            Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjName(pObj) );
     Abc_NtkForEachLatch( pNtk, pObj, i )
-        Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjNameSuffix( Abc_NtkLatch(pNtkInit,i), "_in") );
+        Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjNameSuffix( pObj, "_in") );
 
     // link to the POs of the network
     Abc_NtkForEachPo( pNtk, pObj, i )
diff --git a/src/base/abci/abcVanImp.c b/src/base/abci/abcVanImp.c
new file mode 100644
index 00000000..28320028
--- /dev/null
+++ b/src/base/abci/abcVanImp.c
@@ -0,0 +1,978 @@
+/**CFile****************************************************************
+
+  FileName    [abcVanImp.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Implementation of van Eijk's method for implications.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - October 2, 2005.]
+
+  Revision    [$Id: abcVanImp.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "fraig.h"
+#include "sim.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Van_Man_t_ Van_Man_t;
+struct Van_Man_t_
+{
+    // single frame representation
+    Abc_Ntk_t *      pNtkSingle;    // single frame
+    Vec_Int_t *      vCounters;     // the counters of 1s in the simulation info
+    Vec_Ptr_t *      vZeros;        // the set of constant 0 candidates
+    Vec_Int_t *      vImps;         // the set of all implications
+    Vec_Int_t *      vImpsMis;      // the minimum independent set of implications
+    // multiple frame representation
+    Abc_Ntk_t *      pNtkMulti;     // multiple frame
+    Vec_Ptr_t *      vCorresp;      // the correspondence between single frame and multiple frames
+    // parameters
+    int              nFrames;       // the number of timeframes
+    int              nWords;        // the number of simulation words
+    int              nIdMax;        // the maximum ID in the single frame
+    int              fVerbose;      // the verbosiness flag
+    // statistics
+    int              nPairsAll;
+    int              nImpsAll;
+    int              nEquals;
+    int              nZeros;
+    // runtime
+    int              timeAll;
+    int              timeSim;
+    int              timeAdd;
+    int              timeCheck;
+    int              timeInfo;
+    int              timeMis;
+};
+
+static void           Abc_NtkVanImpCompute( Van_Man_t * p );
+static Vec_Ptr_t *    Abc_NtkVanImpSortByOnes( Van_Man_t * p );
+static void           Abc_NtkVanImpComputeAll( Van_Man_t * p );
+static Vec_Int_t *    Abc_NtkVanImpComputeMis( Van_Man_t * p );
+static void           Abc_NtkVanImpManFree( Van_Man_t * p );
+static void           Abc_NtkVanImpFilter( Van_Man_t * p, Fraig_Man_t * pFraig, Vec_Ptr_t * vZeros, Vec_Int_t * vImps );
+static int            Abc_NtkVanImpCountEqual( Van_Man_t * p );
+
+static Abc_Ntk_t *    Abc_NtkVanImpDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vZeros, Vec_Int_t * vImps );
+
+extern Abc_Ntk_t *    Abc_NtkVanEijkFrames( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int nFrames, int fAddLast, int fShortNames );
+extern void           Abc_NtkVanEijkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_Ptr_t * vCorresp, Vec_Ptr_t * vOrder, int fShortNames );
+extern Fraig_Man_t *  Abc_NtkVanEijkFraig( Abc_Ntk_t * pMulti, int fInit );
+
+////////////////////////////////////////////////////////////////////////
+///                     INLINED FUNCTIONS                            ///
+////////////////////////////////////////////////////////////////////////
+
+// returns the correspondence of the node in the frame
+static inline Abc_Obj_t * Abc_NodeVanImpReadCorresp( Abc_Obj_t * pNode, Vec_Ptr_t * vCorresp, int iFrame ) 
+{
+    return Vec_PtrEntry( vCorresp, iFrame * Abc_NtkObjNumMax(pNode->pNtk) + pNode->Id ); 
+}
+// returns the left node of the implication
+static inline Abc_Obj_t * Abc_NodeVanGetLeft( Abc_Ntk_t * pNtk, unsigned Imp ) 
+{
+    return Abc_NtkObj( pNtk, Imp >> 16 );
+}
+// returns the right node of the implication
+static inline Abc_Obj_t * Abc_NodeVanGetRight( Abc_Ntk_t * pNtk, unsigned Imp ) 
+{
+    return Abc_NtkObj( pNtk, Imp & 0xFFFF );
+}
+// returns the implication
+static inline unsigned Abc_NodeVanGetImp( Abc_Obj_t * pLeft, Abc_Obj_t * pRight ) 
+{
+    return (pLeft->Id << 16) | pRight->Id;
+}
+// returns the right node of the implication
+static inline void Abc_NodeVanPrintImp( unsigned Imp ) 
+{
+    printf( "%d -> %d  ", Imp >> 16, Imp & 0xFFFF );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Derives implications that hold sequentially.]
+
+  Description [Adds EXDC network to the current network to record the 
+  set of computed sequentially equivalence implications, representing
+  a subset of unreachable states.]
+               
+  SideEffects []
+ 
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkVanImp( Abc_Ntk_t * pNtk, int nFrames, int fExdc, int fVerbose )
+{
+    Fraig_Params_t Params;
+    Abc_Ntk_t * pNtkNew;
+    Van_Man_t * p;
+
+    assert( Abc_NtkIsStrash(pNtk) );
+
+    // start the manager
+    p = ALLOC( Van_Man_t, 1 );
+    memset( p, 0, sizeof(Van_Man_t) );
+    p->nFrames  = nFrames;
+    p->fVerbose = fVerbose;
+    p->vCorresp = Vec_PtrAlloc( 100 );
+
+    // FRAIG the network to get rid of combinational equivalences
+    Fraig_ParamsSetDefaultFull( &Params );
+    p->pNtkSingle = Abc_NtkFraig( pNtk, &Params, 0, 0 );
+    p->nIdMax     = Abc_NtkObjNumMax( p->pNtkSingle );
+    Abc_AigSetNodePhases( p->pNtkSingle );
+    Abc_NtkCleanNext( p->pNtkSingle );
+//    if ( fVerbose )
+//        printf( "The number of ANDs in 1 timeframe  = %d.\n", Abc_NtkNodeNum(p->pNtkSingle) );
+
+    // derive multiple time-frames and node correspondence (to be used in the inductive case)
+    p->pNtkMulti = Abc_NtkVanEijkFrames( p->pNtkSingle, p->vCorresp, nFrames, 1, 0 );
+//    if ( fVerbose )
+//        printf( "The number of ANDs in %d timeframes = %d.\n", nFrames + 1, Abc_NtkNodeNum(p->pNtkMulti) );
+
+    // get the implications
+    Abc_NtkVanImpCompute( p );
+
+    // create the new network with EXDC correspondingn to the computed implications
+    if ( fExdc && (Vec_PtrSize(p->vZeros) > 0 || Vec_IntSize(p->vImpsMis) > 0) )
+    {
+        if ( p->pNtkSingle->pExdc )
+        {
+            printf( "The old EXDC network is thrown away.\n" );
+            Abc_NtkDelete( p->pNtkSingle->pExdc );
+            p->pNtkSingle->pExdc = NULL;
+        }
+        pNtkNew = Abc_NtkDup( p->pNtkSingle );  
+        pNtkNew->pExdc = Abc_NtkVanImpDeriveExdc( p->pNtkSingle, p->vZeros, p->vImpsMis );
+    }
+    else
+        pNtkNew = Abc_NtkDup( p->pNtkSingle );  
+
+    // free stuff
+    Abc_NtkVanImpManFree( p );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Frees the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkVanImpManFree( Van_Man_t * p )
+{
+    Abc_NtkDelete( p->pNtkMulti );
+    Abc_NtkDelete( p->pNtkSingle );
+    Vec_PtrFree( p->vCorresp );
+    Vec_PtrFree( p->vZeros );
+    Vec_IntFree( p->vCounters );
+    Vec_IntFree( p->vImpsMis );
+    Vec_IntFree( p->vImps );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the minimum independent set of sequential implications.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkVanImpCompute( Van_Man_t * p )
+{
+    Fraig_Man_t * pFraig;
+    Vec_Ptr_t * vZeros;
+    Vec_Int_t * vImps, * vImpsTemp;
+    int nIters, clk;
+
+    // compute all implications and count 1s in the simulation info
+clk = clock();
+    Abc_NtkVanImpComputeAll( p );
+p->timeAll += clock() - clk;
+
+    // compute the MIS
+clk = clock();
+    p->vImpsMis = Abc_NtkVanImpComputeMis( p );
+p->timeMis += clock() - clk;
+
+    if ( p->fVerbose )
+    {
+        printf( "Pairs = %8d. Imps = %8d. Seq = %7d. MIS = %7d. Equ = %5d. Const = %5d.\n", 
+            p->nPairsAll, p->nImpsAll, Vec_IntSize(p->vImps), Vec_IntSize(p->vImpsMis), p->nEquals, p->nZeros );
+        printf( "Start    :  Seq = %7d.  MIS = %7d.  Const = %5d.\n", Vec_IntSize(p->vImps), Vec_IntSize(p->vImpsMis), Vec_PtrSize(p->vZeros) );
+    }
+
+    // iterate to perform the iterative filtering of implications
+    for ( nIters = 1; Vec_PtrSize(p->vZeros) > 0 || Vec_IntSize(p->vImps) > 0; nIters++ )
+    {
+        // FRAIG the ununitialized frames
+        pFraig = Abc_NtkVanEijkFraig( p->pNtkMulti, 0 );
+
+        // assuming that zeros and imps hold in the first k-1 frames 
+        // check if they hold in the k-th frame
+        vZeros = Vec_PtrAlloc( 100 );
+        vImps = Vec_IntAlloc( 100 );
+        Abc_NtkVanImpFilter( p, pFraig, vZeros, vImps );
+        Fraig_ManFree( pFraig );
+
+clk = clock();
+        vImpsTemp = p->vImps;
+        p->vImps = vImps;
+        Vec_IntFree( p->vImpsMis );
+        p->vImpsMis = Abc_NtkVanImpComputeMis( p );
+        p->vImps = vImpsTemp;
+p->timeMis += clock() - clk;
+
+        // report the results
+        if ( p->fVerbose )
+            printf( "Iter = %2d:  Seq = %7d.  MIS = %7d.  Const = %5d.\n", nIters, Vec_IntSize(vImps), Vec_IntSize(p->vImpsMis), Vec_PtrSize(vZeros) );
+
+        // if the fixed point is reaches, quit the loop
+        if ( Vec_PtrSize(vZeros) == Vec_PtrSize(p->vZeros) && Vec_IntSize(vImps) == Vec_IntSize(p->vImps) )
+        { // no change
+            Vec_PtrFree(vZeros);
+            Vec_IntFree(vImps);
+            break;
+        }
+
+        // update the sets
+        Vec_PtrFree( p->vZeros );  p->vZeros = vZeros;
+        Vec_IntFree( p->vImps );   p->vImps  = vImps;
+    }
+
+    // compute the MIS
+clk = clock();
+    Vec_IntFree( p->vImpsMis );
+    p->vImpsMis = Abc_NtkVanImpComputeMis( p );
+//    p->vImpsMis = Vec_IntDup( p->vImps );
+p->timeMis += clock() - clk;
+    if ( p->fVerbose )
+        printf( "Final    :  Seq = %7d.  MIS = %7d.  Const = %5d.\n", Vec_IntSize(p->vImps), Vec_IntSize(p->vImpsMis), Vec_PtrSize(p->vZeros) );
+
+
+/*
+    if ( p->fVerbose )
+    {
+        PRT( "All   ", p->timeAll   );
+        PRT( "Sim   ", p->timeSim   );
+        PRT( "Add   ", p->timeAdd   );
+        PRT( "Check ", p->timeCheck );
+        PRT( "Mis   ", p->timeMis   );
+    }
+*/
+
+/*
+    // print the implications in the MIS
+    if ( p->fVerbose )
+    {
+        Abc_Obj_t * pNode, * pNode1, * pNode2;
+        unsigned Imp;
+        int i;
+        if ( Vec_PtrSize(p->vZeros) )
+        {
+            printf( "The const nodes are: " );
+            Vec_PtrForEachEntry( p->vZeros, pNode, i )
+                printf( "%d(%d) ", pNode->Id, pNode->fPhase );
+            printf( "\n" );
+        }
+        if ( Vec_IntSize(p->vImpsMis) )
+        {
+            printf( "The implications are: " );
+            Vec_IntForEachEntry( p->vImpsMis, Imp, i )
+            {
+                pNode1  = Abc_NodeVanGetLeft( p->pNtkSingle, Imp );
+                pNode2  = Abc_NodeVanGetRight( p->pNtkSingle, Imp );
+                printf( "%d(%d)=>%d(%d) ", pNode1->Id, pNode1->fPhase, pNode2->Id, pNode2->fPhase );
+            }
+            printf( "\n" );
+        }
+    }
+*/
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Filters zeros and implications by performing one inductive step.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkVanImpFilter( Van_Man_t * p, Fraig_Man_t * pFraig, Vec_Ptr_t * vZeros, Vec_Int_t * vImps )
+{
+    ProgressBar * pProgress;
+    Abc_Obj_t * pNode, * pNodeM1, * pNodeM2, * pNode1, * pNode2, * pObj;
+    Fraig_Node_t * pFNode1, * pFNode2;
+    Fraig_Node_t * ppFNodes[2];
+    unsigned Imp;
+    int i, f, k, clk;
+
+clk = clock();
+    for ( f = 0; f < p->nFrames; f++ )
+    {
+        // add new clauses for zeros
+        Vec_PtrForEachEntry( p->vZeros, pNode, i )
+        {
+            pNodeM1 = Abc_NodeVanImpReadCorresp( pNode, p->vCorresp, f );
+            pFNode1 = Fraig_NotCond( Abc_ObjRegular(pNodeM1)->pCopy, Abc_ObjIsComplement(pNodeM1) );
+            pFNode1 = Fraig_NotCond( pFNode1, !pNode->fPhase );
+            Fraig_ManAddClause( pFraig, &pFNode1, 1 );
+        }
+        // add new clauses for imps
+        Vec_IntForEachEntry( p->vImps, Imp, i )
+        {
+            pNode1  = Abc_NodeVanGetLeft( p->pNtkSingle, Imp );
+            pNode2  = Abc_NodeVanGetRight( p->pNtkSingle, Imp );
+            pNodeM1 = Abc_NodeVanImpReadCorresp( pNode1, p->vCorresp, f );
+            pNodeM2 = Abc_NodeVanImpReadCorresp( pNode2, p->vCorresp, f );
+            pFNode1 = Fraig_NotCond( Abc_ObjRegular(pNodeM1)->pCopy, Abc_ObjIsComplement(pNodeM1) );
+            pFNode2 = Fraig_NotCond( Abc_ObjRegular(pNodeM2)->pCopy, Abc_ObjIsComplement(pNodeM2) );
+            ppFNodes[0] = Fraig_NotCond( pFNode1, !pNode1->fPhase );
+            ppFNodes[1] = Fraig_NotCond( pFNode2,  pNode2->fPhase );
+//            assert( Fraig_Regular(ppFNodes[0]) != Fraig_Regular(ppFNodes[1]) );
+            Fraig_ManAddClause( pFraig, ppFNodes, 2 );
+        }
+    }
+p->timeAdd += clock() - clk;
+
+    // check the zero nodes
+clk = clock();
+    Vec_PtrClear( vZeros );
+    Vec_PtrForEachEntry( p->vZeros, pNode, i )
+    {
+        pNodeM1 = Abc_NodeVanImpReadCorresp( pNode, p->vCorresp, p->nFrames );
+        pFNode1 = Fraig_NotCond( Abc_ObjRegular(pNodeM1)->pCopy, Abc_ObjIsComplement(pNodeM1) );
+        pFNode1 = Fraig_Regular(pFNode1);
+        pFNode2 = Fraig_ManReadConst1(pFraig);
+        if ( pFNode1 == pFNode2 || Fraig_NodeIsEquivalent( pFraig, pFNode1, pFNode2, -1, 100 ) )
+            Vec_PtrPush( vZeros, pNode );
+        else
+        {
+            // since we disproved this zero, we should add all possible implications to p->vImps
+            // these implications will be checked below and only correct ones will remain
+            Abc_NtkForEachObj( p->pNtkSingle, pObj, k )
+            {
+                if ( Abc_ObjIsPo(pObj) )
+                    continue;
+                if ( Vec_IntEntry( p->vCounters, pObj->Id ) > 0 )
+                    Vec_IntPush( p->vImps, Abc_NodeVanGetImp(pNode, pObj) );
+            }
+        }
+    }
+
+    // check implications
+    pProgress = Extra_ProgressBarStart( stdout, p->vImps->nSize );
+    Vec_IntClear( vImps );
+    Vec_IntForEachEntry( p->vImps, Imp, i )
+    {
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        pNode1  = Abc_NodeVanGetLeft( p->pNtkSingle, Imp );
+        pNode2  = Abc_NodeVanGetRight( p->pNtkSingle, Imp );
+        pNodeM1 = Abc_NodeVanImpReadCorresp( pNode1, p->vCorresp, p->nFrames );
+        pNodeM2 = Abc_NodeVanImpReadCorresp( pNode2, p->vCorresp, p->nFrames );
+        pFNode1 = Fraig_NotCond( Abc_ObjRegular(pNodeM1)->pCopy, Abc_ObjIsComplement(pNodeM1) );
+        pFNode2 = Fraig_NotCond( Abc_ObjRegular(pNodeM2)->pCopy, Abc_ObjIsComplement(pNodeM2) );
+        pFNode1 = Fraig_NotCond( pFNode1, !pNode1->fPhase );
+        pFNode2 = Fraig_NotCond( pFNode2,  pNode2->fPhase );
+        if ( pFNode1 == Fraig_Not(pFNode2) )
+        {
+            Vec_IntPush( vImps, Imp );
+            continue;
+        }
+        if ( pFNode1 == pFNode2 )
+        {
+            if ( pFNode1 == Fraig_Not( Fraig_ManReadConst1(pFraig) ) )
+                continue;
+            if ( pFNode1 == Fraig_ManReadConst1(pFraig) )
+            {
+                Vec_IntPush( vImps, Imp );
+                continue;
+            }
+            pFNode1 = Fraig_Regular(pFNode1);
+            pFNode2 = Fraig_ManReadConst1(pFraig);
+            if ( Fraig_NodeIsEquivalent( pFraig, pFNode1, pFNode2, -1, 100 ) )
+                Vec_IntPush( vImps, Imp );
+            continue;
+        }
+            
+        if ( Fraig_ManCheckClauseUsingSat( pFraig, pFNode1, pFNode2, -1 ) )
+            Vec_IntPush( vImps, Imp );
+    }
+    Extra_ProgressBarStop( pProgress );
+p->timeCheck += clock() - clk;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes all implications.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkVanImpComputeAll( Van_Man_t * p )
+{
+    ProgressBar * pProgress;
+    Fraig_Man_t * pManSingle;
+    Vec_Ptr_t * vInfo;
+    Abc_Obj_t * pObj, * pNode1, * pNode2, * pConst1;
+    Fraig_Node_t * pFNode1, * pFNode2;
+    unsigned * pPats1, * pPats2;
+    int nFrames, nUnsigned, RetValue;
+    int clk, i, k, Count1, Count2;
+
+    // decide how many frames to simulate
+    nFrames   = 32;
+    nUnsigned = 32;
+    p->nWords = nFrames * nUnsigned;
+
+    // simulate randomly the initialized frames
+clk = clock();
+    vInfo = Sim_SimulateSeqRandom( p->pNtkSingle, nFrames, nUnsigned );
+
+    // complement the info for those nodes whose phase is 1
+    Abc_NtkForEachObj( p->pNtkSingle, pObj, i )
+        if ( pObj->fPhase )
+            Sim_UtilSetCompl( Sim_SimInfoGet(vInfo, pObj), p->nWords );
+
+    // compute the number of ones for each node
+    p->vCounters = Sim_UtilCountOnesArray( vInfo, p->nWords );
+p->timeSim += clock() - clk;
+
+    // FRAIG the uninitialized frame
+    pManSingle = Abc_NtkVanEijkFraig( p->pNtkSingle, 0 );
+    // now pNode->pCopy are assigned the pointers to the corresponding FRAIG nodes
+
+/*
+Abc_NtkForEachPi( p->pNtkSingle, pNode1, i )
+printf( "PI = %d\n", pNode1->Id );
+Abc_NtkForEachLatch( p->pNtkSingle, pNode1, i )
+printf( "Latch = %d\n", pNode1->Id );
+Abc_NtkForEachPo( p->pNtkSingle, pNode1, i )
+printf( "PO = %d\n", pNode1->Id );
+*/
+
+    // go through the pairs of signals in the frames
+    pProgress = Extra_ProgressBarStart( stdout, p->nIdMax );
+    pConst1 = Abc_AigConst1( p->pNtkSingle->pManFunc );
+    p->vImps = Vec_IntAlloc( 100 );
+    p->vZeros = Vec_PtrAlloc( 100 );
+    Abc_NtkForEachObj( p->pNtkSingle, pNode1, i )
+    {
+        if ( Abc_ObjIsPo(pNode1) )
+            continue;
+        if ( pNode1 == pConst1 )
+            continue;
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+
+        // get the number of zeros of this node
+        Count1 = Vec_IntEntry( p->vCounters, pNode1->Id );
+        if ( Count1 == 0 )
+        {
+            Vec_PtrPush( p->vZeros, pNode1 );
+            p->nZeros++;
+            continue;
+        }
+        pPats1 = Sim_SimInfoGet(vInfo, pNode1);
+
+        Abc_NtkForEachObj( p->pNtkSingle, pNode2, k )
+        {
+            if ( k >= i )
+                break;
+            if ( Abc_ObjIsPo(pNode2) )
+                continue;
+            if ( pNode2 == pConst1 )
+                continue;
+            p->nPairsAll++;
+
+            // here we have a pair of nodes (pNode1 and pNode2) 
+            // such that Id(pNode1) < Id(pNode2)
+            assert( pNode2->Id < pNode1->Id );
+
+            // get the number of zeros of this node
+            Count2 = Vec_IntEntry( p->vCounters, pNode2->Id );
+            if ( Count2 == 0 )
+                continue;
+            pPats2 = Sim_SimInfoGet(vInfo, pNode2);
+
+            // check for implications
+            if ( Count1 < Count2 )
+            { 
+//clk = clock();
+                RetValue = Sim_UtilInfoIsImp( pPats1, pPats2, p->nWords );
+//p->timeInfo += clock() - clk;
+                if ( !RetValue )
+                    continue;
+                p->nImpsAll++;
+                // pPats1 => pPats2  or  pPats1' v pPats2
+                pFNode1 = Fraig_NotCond( pNode1->pCopy, !pNode1->fPhase );
+                pFNode2 = Fraig_NotCond( pNode2->pCopy,  pNode2->fPhase );
+                // check if this implication is combinational
+                if ( Fraig_ManCheckClauseUsingSimInfo( pManSingle, pFNode1, pFNode2 ) )
+                    continue;
+                // otherwise record it
+                Vec_IntPush( p->vImps, Abc_NodeVanGetImp(pNode1, pNode2) );
+            }
+            else if ( Count2 < Count1 )
+            { 
+//clk = clock();
+                RetValue = Sim_UtilInfoIsImp( pPats2, pPats1, p->nWords );
+//p->timeInfo += clock() - clk;
+                if ( !RetValue )
+                    continue;
+                p->nImpsAll++;
+                // pPats2 => pPats2  or  pPats2' v pPats1
+                pFNode2 = Fraig_NotCond( pNode2->pCopy, !pNode2->fPhase );
+                pFNode1 = Fraig_NotCond( pNode1->pCopy,  pNode1->fPhase );
+                // check if this implication is combinational
+                if ( Fraig_ManCheckClauseUsingSimInfo( pManSingle, pFNode1, pFNode2 ) )
+                    continue;
+                // otherwise record it
+                Vec_IntPush( p->vImps, Abc_NodeVanGetImp(pNode2, pNode1) );
+            }
+            else
+            {
+//clk = clock();
+                RetValue = Sim_UtilInfoIsEqual(pPats1, pPats2, p->nWords);
+//p->timeInfo += clock() - clk;
+                if ( !RetValue )
+                    continue;
+                p->nEquals++;
+                // get the FRAIG nodes
+                pFNode1 = Fraig_NotCond( pNode1->pCopy, pNode1->fPhase );
+                pFNode2 = Fraig_NotCond( pNode2->pCopy, pNode2->fPhase );
+
+                // check if this implication is combinational
+                if ( Fraig_ManCheckClauseUsingSimInfo( pManSingle, Fraig_Not(pFNode1), pFNode2 ) )
+                {
+                    if ( !Fraig_ManCheckClauseUsingSimInfo( pManSingle, pFNode1, Fraig_Not(pFNode2) ) )
+                        Vec_IntPush( p->vImps, Abc_NodeVanGetImp(pNode2, pNode1) );
+                    else
+                        assert( 0 ); // impossible for FRAIG
+                }
+                else
+                {
+                    Vec_IntPush( p->vImps, Abc_NodeVanGetImp(pNode1, pNode2) );
+                    if ( !Fraig_ManCheckClauseUsingSimInfo( pManSingle, pFNode1, Fraig_Not(pFNode2) ) )
+                        Vec_IntPush( p->vImps, Abc_NodeVanGetImp(pNode2, pNode1) );
+                }
+            }
+//            printf( "Implication %d %d -> %d %d \n", pNode1->Id, pNode1->fPhase, pNode2->Id, pNode2->fPhase );
+        }
+    }
+    Fraig_ManFree( pManSingle );
+    Sim_UtilInfoFree( vInfo );
+    Extra_ProgressBarStop( pProgress );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Sorts the nodes.]
+
+  Description [Sorts the nodes appearing in the left-hand sides of the 
+  implications by the number of 1s in their simulation info.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkVanImpSortByOnes( Van_Man_t * p )
+{
+    Abc_Obj_t * pNode, * pList;
+    Vec_Ptr_t * vSorted;
+    unsigned Imp;
+    int i, nOnes;
+
+    // start the sorted array
+    vSorted = Vec_PtrStart( p->nWords * 32 );
+    // go through the implications
+    Abc_NtkIncrementTravId( p->pNtkSingle );
+    Vec_IntForEachEntry( p->vImps, Imp, i )
+    {
+        pNode = Abc_NodeVanGetLeft( p->pNtkSingle, Imp );
+        assert( !Abc_ObjIsPo(pNode) );
+        // if this node is already visited, skip
+        if ( Abc_NodeIsTravIdCurrent( pNode ) )
+            continue;
+        // mark the node as visited
+        Abc_NodeSetTravIdCurrent( pNode );
+
+        // add the node to the list
+        nOnes = Vec_IntEntry( p->vCounters, pNode->Id );
+        pList = Vec_PtrEntry( vSorted, nOnes );
+        pNode->pNext = pList;
+        Vec_PtrWriteEntry( vSorted, nOnes, pNode );
+    }
+    return vSorted;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the array of beginnings.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Abc_NtkVanImpComputeBegs( Van_Man_t * p )
+{
+    Vec_Int_t * vBegins;
+    unsigned Imp;
+    int i, ItemLast, ItemCur;
+
+    // sort the implications (by the number of the left-hand-side node)
+    Vec_IntSort( p->vImps, 0 );
+
+    // start the array of beginnings
+    vBegins = Vec_IntStart( p->nIdMax + 1 );
+
+    // mark the begining of each node's implications
+    ItemLast = 0;
+    Vec_IntForEachEntry( p->vImps, Imp, i )
+    {
+        ItemCur = (Imp >> 16);
+        if ( ItemCur == ItemLast )
+            continue;
+        Vec_IntWriteEntry( vBegins, ItemCur, i );
+        ItemLast = ItemCur;
+    }
+    // fill in the empty spaces
+    ItemLast = Vec_IntSize(p->vImps);
+    Vec_IntWriteEntry( vBegins, p->nIdMax, ItemLast );
+    Vec_IntForEachEntryReverse( vBegins, ItemCur, i )
+    {
+        if ( ItemCur == 0 )
+            Vec_IntWriteEntry( vBegins, i, ItemLast );
+        else 
+            ItemLast = ItemCur;
+    }
+
+    Imp = Vec_IntEntry( p->vImps, 0 );
+    ItemCur = (Imp >> 16);
+    for ( i = 0; i <= ItemCur; i++ )
+        Vec_IntWriteEntry( vBegins, i, 0 );
+    return vBegins;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the minimum subset of implications.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkVanImpMark_rec( Abc_Obj_t * pNode, Vec_Vec_t * vImpsMis )
+{
+    Vec_Int_t * vNexts;
+    int i, Next;
+    // if this node is already visited, skip
+    if ( Abc_NodeIsTravIdCurrent( pNode ) )
+        return;
+    // mark the node as visited
+    Abc_NodeSetTravIdCurrent( pNode );
+    // mark the children
+    vNexts = Vec_VecEntry( vImpsMis, pNode->Id );
+    Vec_IntForEachEntry( vNexts, Next, i )
+        Abc_NtkVanImpMark_rec( Abc_NtkObj(pNode->pNtk, Next), vImpsMis );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the minimum subset of implications.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Abc_NtkVanImpComputeMis( Van_Man_t * p )
+{
+    Abc_Obj_t * pNode, * pNext, * pList;
+    Vec_Vec_t * vMatrix;
+    Vec_Ptr_t * vSorted;
+    Vec_Int_t * vBegins;
+    Vec_Int_t * vImpsMis;
+    int i, k, iStart, iStop;
+    void * pEntry;
+    unsigned Imp;
+
+    if ( Vec_IntSize(p->vImps) == 0 )
+        return Vec_IntAlloc(0);
+
+    // compute the sorted list of nodes by the number of 1s
+    Abc_NtkCleanNext( p->pNtkSingle );
+    vSorted = Abc_NtkVanImpSortByOnes( p );
+
+    // compute the array of beginnings
+    vBegins = Abc_NtkVanImpComputeBegs( p );
+
+/*
+Vec_IntForEachEntry( p->vImps, Imp, i )
+{
+    printf( "%d: ", i );
+    Abc_NodeVanPrintImp( Imp );
+}
+printf( "\n\n" );
+Vec_IntForEachEntry( vBegins, Imp, i )
+    printf( "%d=%d ", i, Imp );
+printf( "\n\n" );
+*/
+
+    // compute the MIS by considering nodes in the reverse order of ones
+    vMatrix = Vec_VecStart( p->nIdMax );
+    Vec_PtrForEachEntryReverse( vSorted, pList, i )
+    {
+        for ( pNode = pList; pNode; pNode = pNode->pNext )
+        {
+            // get the starting and stopping implication of this node
+            iStart = Vec_IntEntry( vBegins, pNode->Id );
+            iStop  = Vec_IntEntry( vBegins, pNode->Id + 1 );
+            if ( iStart == iStop )
+                continue;
+            assert( iStart < iStop );
+            // go through all the implications of this node
+            Abc_NtkIncrementTravId( p->pNtkSingle );
+            Abc_NodeIsTravIdCurrent( pNode );
+            Vec_IntForEachEntryStartStop( p->vImps, Imp, k, iStart, iStop )
+            {
+                assert( pNode == Abc_NodeVanGetLeft(p->pNtkSingle, Imp) );
+                pNext = Abc_NodeVanGetRight(p->pNtkSingle, Imp);
+                // if this node is already visited, skip
+                if ( Abc_NodeIsTravIdCurrent( pNext ) )
+                    continue;
+                assert( pNode->Id != pNext->Id );
+                // add implication
+                Vec_VecPush( vMatrix, pNode->Id, (void *)pNext->Id );
+                // recursively mark dependent nodes
+                Abc_NtkVanImpMark_rec( pNext, vMatrix );
+            }
+        }
+    }
+    Vec_IntFree( vBegins );
+    Vec_PtrFree( vSorted );
+
+    // transfer the MIS into the normal array
+    vImpsMis = Vec_IntAlloc( 100 );
+    Vec_VecForEachEntry( vMatrix, pEntry, i, k )
+    {
+        assert( (i << 16) != ((int)pEntry) );
+        Vec_IntPush( vImpsMis, (i << 16) | ((int)pEntry) );
+    }
+    Vec_VecFree( vMatrix );
+    return vImpsMis;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Count equal pairs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkVanImpCountEqual( Van_Man_t * p )
+{
+    Abc_Obj_t * pNode1, * pNode2, * pNode3;
+    Vec_Int_t * vBegins;
+    int iStart, iStop;
+    unsigned Imp, ImpR;
+    int i, k, Counter;
+
+    // compute the array of beginnings
+    vBegins = Abc_NtkVanImpComputeBegs( p );
+
+    // go through each node and out
+    Counter = 0;
+    Vec_IntForEachEntry( p->vImps, Imp, i )
+    {
+        pNode1 = Abc_NodeVanGetLeft( p->pNtkSingle, Imp );
+        pNode2 = Abc_NodeVanGetRight( p->pNtkSingle, Imp );
+        if ( pNode1->Id > pNode2->Id )
+            continue;
+        iStart = Vec_IntEntry( vBegins, pNode2->Id );
+        iStop  = Vec_IntEntry( vBegins, pNode2->Id + 1 );
+        Vec_IntForEachEntryStartStop( p->vImps, ImpR, k, iStart, iStop )
+        {
+            assert( pNode2 == Abc_NodeVanGetLeft(p->pNtkSingle, ImpR) );
+            pNode3 = Abc_NodeVanGetRight(p->pNtkSingle, ImpR);
+            if ( pNode1 == pNode3 )
+            {
+                Counter++;
+                break;
+            }
+        }
+    }
+    Vec_IntFree( vBegins );
+    return Counter;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Create EXDC from the equivalence classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkVanImpDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vZeros, Vec_Int_t * vImps )
+{
+    Abc_Ntk_t * pNtkNew; 
+    Vec_Ptr_t * vCone;
+    Abc_Obj_t * pObj, * pMiter, * pTotal, * pNode, * pNode1, * pNode2;
+    unsigned Imp;
+    int i, k;
+
+    assert( Abc_NtkIsStrash(pNtk) );
+
+    // start the network
+    pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc );
+    pNtkNew->pName = util_strsav( "exdc" );
+    pNtkNew->pSpec = NULL;
+
+    // map the constant nodes
+    Abc_AigConst1(pNtk->pManFunc)->pCopy = Abc_AigConst1(pNtkNew->pManFunc);
+    // for each CI, create PI
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePi(pNtkNew), Abc_ObjName(pObj) );
+    // cannot add latches here because pLatch->pCopy pointers are used
+
+    // build logic cone for zero nodes
+    pTotal = Abc_ObjNot( Abc_AigConst1(pNtkNew->pManFunc) );
+    Vec_PtrForEachEntry( vZeros, pNode, i )
+    {
+        // build the logic cone for the node
+        if ( Abc_ObjFaninNum(pNode) == 2 )
+        {
+            vCone = Abc_NtkDfsNodes( pNtk, &pNode, 1 );
+            Vec_PtrForEachEntry( vCone, pObj, k )
+                pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
+            Vec_PtrFree( vCone );
+            assert( pObj == pNode );
+        }
+        // complement if there is phase difference
+        pNode->pCopy = Abc_ObjNotCond( pNode->pCopy, pNode->fPhase );
+
+        // add it to the EXDC
+        pTotal = Abc_AigOr( pNtkNew->pManFunc, pTotal, pNode->pCopy );
+    }
+
+    // create logic cones for the implications
+    Vec_IntForEachEntry( vImps, Imp, i )
+    {
+        pNode1 = Abc_NtkObj(pNtk, Imp >> 16);
+        pNode2 = Abc_NtkObj(pNtk, Imp & 0xFFFF);
+
+        // build the logic cone for the first node
+        if ( Abc_ObjFaninNum(pNode1) == 2 )
+        {
+            vCone = Abc_NtkDfsNodes( pNtk, &pNode1, 1 );
+            Vec_PtrForEachEntry( vCone, pObj, k )
+                pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
+            Vec_PtrFree( vCone );
+            assert( pObj == pNode1 );
+        }
+        // complement if there is phase difference
+        pNode1->pCopy = Abc_ObjNotCond( pNode1->pCopy, pNode1->fPhase );
+
+        // build the logic cone for the second node
+        if ( Abc_ObjFaninNum(pNode2) == 2 )
+        {
+            vCone = Abc_NtkDfsNodes( pNtk, &pNode2, 1 );
+            Vec_PtrForEachEntry( vCone, pObj, k )
+                pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
+            Vec_PtrFree( vCone );
+            assert( pObj == pNode2 );
+        }
+        // complement if there is phase difference
+        pNode2->pCopy = Abc_ObjNotCond( pNode2->pCopy, pNode2->fPhase );
+
+        // build the implication and add it to the EXDC
+        pMiter = Abc_AigAnd( pNtkNew->pManFunc, pNode1->pCopy, Abc_ObjNot(pNode2->pCopy) );
+        pTotal = Abc_AigOr( pNtkNew->pManFunc, pTotal, pMiter );
+    }
+
+    // for each CO, create PO (skip POs equal to CIs because of name conflict)
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        if ( !Abc_ObjIsCi(Abc_ObjFanin0(pObj)) )
+            Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjName(pObj) );
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+        Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjNameSuffix(pObj, "_in") );
+
+    // link to the POs of the network
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        if ( !Abc_ObjIsCi(Abc_ObjFanin0(pObj)) )
+            Abc_ObjAddFanin( pObj->pCopy, pTotal );
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+        Abc_ObjAddFanin( pObj->pCopy, pTotal );
+
+    // remove the extra nodes
+    Abc_AigCleanup( pNtkNew->pManFunc );
+
+    // check the result
+    if ( !Abc_NtkCheck( pNtkNew ) )
+    {
+        printf( "Abc_NtkVanImpDeriveExdc: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkNew );
+        return NULL;
+    }
+    return pNtkNew;
+}
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index 08a54e80..4e73d42b 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -20,14 +20,16 @@
 
 #include "abc.h"
 #include "fraig.h"
+#include "sim.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
  
-static int * Abc_NtkVerifyGetCleanModel( Abc_Ntk_t * pNtk );
+static int * Abc_NtkVerifyGetCleanModel( Abc_Ntk_t * pNtk, int nFrames );
 static int * Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel );
 static void  Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel );
+static void  Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
@@ -62,7 +64,7 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds )
     {
         printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
         // report the error
-        pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter );
+        pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, 1 );
         Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel );
         FREE( pMiter->pModel );
         Abc_NtkDelete( pMiter );
@@ -129,7 +131,7 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV
     {
         printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
         // report the error
-        pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter );
+        pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, 1 );
         Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel );
         FREE( pMiter->pModel );
         Abc_NtkDelete( pMiter );
@@ -278,8 +280,12 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nF
     RetValue = Abc_NtkMiterIsConstant( pMiter );
     if ( RetValue == 0 )
     {
-        Abc_NtkDelete( pMiter );
         printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
+        // report the error
+        pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, nFrames );
+        Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pMiter->pModel, nFrames );
+        FREE( pMiter->pModel );
+        Abc_NtkDelete( pMiter );
         return;
     }
     if ( RetValue == 1 )
@@ -300,8 +306,12 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nF
     RetValue = Abc_NtkMiterIsConstant( pFrames );
     if ( RetValue == 0 )
     {
-        Abc_NtkDelete( pFrames );
         printf( "Networks are NOT EQUIVALENT after framing.\n" );
+        // report the error
+        pFrames->pModel = Abc_NtkVerifyGetCleanModel( pFrames, 1 );
+        Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pFrames->pModel, nFrames );
+        FREE( pFrames->pModel );
+        Abc_NtkDelete( pFrames );
         return;
     }
     if ( RetValue == 1 )
@@ -328,7 +338,7 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nF
     else if ( RetValue == 0 )
     {
         printf( "Networks are NOT EQUIVALENT after fraiging.\n" );
-//        Abc_NtkVerifyReportError( pNtk1, pNtk2, Fraig_ManReadModel(pMan) );
+        Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, Fraig_ManReadModel(pMan), nFrames );
     }
     else assert( 0 );
     // delete the fraig manager
@@ -339,6 +349,75 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nF
 
 /**Function*************************************************************
 
+  Synopsis    [Returns a dummy pattern full of zeros.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int * Abc_NtkVerifyGetCleanModel( Abc_Ntk_t * pNtk, int nFrames )
+{
+    int * pModel = ALLOC( int, Abc_NtkCiNum(pNtk) * nFrames );
+    memset( pModel, 0, sizeof(int) * Abc_NtkCiNum(pNtk) * nFrames );
+    return pModel;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the PO values under the given input pattern.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int * Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel )
+{
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pNode;
+    int * pValues, Value0, Value1, i;
+    int fStrashed = 0;
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        pNtk = Abc_NtkStrash(pNtk, 0, 0);
+        fStrashed = 1;
+    }
+    // increment the trav ID
+    Abc_NtkIncrementTravId( pNtk );
+    // set the CI values
+    Abc_NtkForEachCi( pNtk, pNode, i )
+        pNode->pCopy = (void *)pModel[i];
+    // simulate in the topological order
+    vNodes = Abc_NtkDfs( pNtk, 1 );
+    Vec_PtrForEachEntry( vNodes, pNode, i )
+    {
+        if ( Abc_NodeIsConst(pNode) )
+            pNode->pCopy = NULL;
+        else
+        {
+            Value0 = ((int)Abc_ObjFanin0(pNode)->pCopy) ^ Abc_ObjFaninC0(pNode);
+            Value1 = ((int)Abc_ObjFanin1(pNode)->pCopy) ^ Abc_ObjFaninC1(pNode);
+            pNode->pCopy = (void *)(Value0 & Value1);
+        }
+    }
+    Vec_PtrFree( vNodes );
+    // fill the output values
+    pValues = ALLOC( int, Abc_NtkCoNum(pNtk) );
+    Abc_NtkForEachCo( pNtk, pNode, i )
+        pValues[i] = ((int)Abc_ObjFanin0(pNode)->pCopy) ^ Abc_ObjFaninC0(pNode);
+    if ( fStrashed )
+        Abc_NtkDelete( pNtk );
+    return pValues;
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Reports mismatch between the two networks.]
 
   Description []
@@ -353,7 +432,7 @@ void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pMode
     Vec_Ptr_t * vNodes;
     Abc_Obj_t * pNode;
     int * pValues1, * pValues2;
-    int nMisses, nPrinted, i, iNode = -1;
+    int nErrors, nPrinted, i, iNode = -1;
 
     assert( Abc_NtkCiNum(pNtk1) == Abc_NtkCiNum(pNtk2) );
     assert( Abc_NtkCoNum(pNtk1) == Abc_NtkCoNum(pNtk2) );
@@ -361,10 +440,10 @@ void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pMode
     pValues1 = Abc_NtkVerifySimulatePattern( pNtk1, pModel );
     pValues2 = Abc_NtkVerifySimulatePattern( pNtk2, pModel );
     // count the mismatches
-    nMisses = 0;
+    nErrors = 0;
     for ( i = 0; i < Abc_NtkCoNum(pNtk1); i++ )
-        nMisses += (int)( pValues1[i] != pValues2[i] );
-    printf( "Verification failed for %d outputs: ", nMisses );
+        nErrors += (int)( pValues1[i] != pValues2[i] );
+    printf( "Verification failed for %d outputs: ", nErrors );
     // print the first 3 outputs
     nPrinted = 0;
     for ( i = 0; i < Abc_NtkCoNum(pNtk1); i++ )
@@ -376,7 +455,7 @@ void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pMode
             if ( ++nPrinted == 3 )
                 break;
         }
-    if ( nPrinted != nMisses )
+    if ( nPrinted != nErrors )
         printf( " ..." );
     printf( "\n" );
     // report mismatch for the first output
@@ -404,9 +483,10 @@ void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pMode
     free( pValues2 );
 }
 
+
 /**Function*************************************************************
 
-  Synopsis    [Returns a dummy pattern full of zeros.]
+  Synopsis    [Computes the COs in the support of the PO in the given frame.]
 
   Description []
                
@@ -415,16 +495,43 @@ void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pMode
   SeeAlso     []
 
 ***********************************************************************/
-int * Abc_NtkVerifyGetCleanModel( Abc_Ntk_t * pNtk )
+void Abc_NtkGetSeqPoSupp( Abc_Ntk_t * pNtk, int iFrame, int iNumPo )
 {
-    int * pModel = ALLOC( int, Abc_NtkCiNum(pNtk) );
-    memset( pModel, 0, sizeof(int) * Abc_NtkCiNum(pNtk) );
-    return pModel;
+    Abc_Ntk_t * pFrames;
+    Abc_Obj_t * pObj, * pNodePo;
+    Vec_Ptr_t * vSupp;
+    int i, k;
+    // get the timeframes of the network
+    pFrames = Abc_NtkFrames( pNtk, iFrame + 1, 0 );
+//Abc_NtkShowAig( pFrames );
+
+    // get the PO of the timeframes
+    pNodePo = Abc_NtkPo( pFrames, iFrame * Abc_NtkPoNum(pNtk) + iNumPo );
+    // set the support
+    vSupp   = Abc_NtkNodeSupport( pFrames, &pNodePo, 1 );
+    // mark the support of the frames
+    Abc_NtkForEachCi( pFrames, pObj, i )
+        pObj->pCopy = NULL;
+    Vec_PtrForEachEntry( vSupp, pObj, i )
+        pObj->pCopy = (void *)1;
+    // mark the support of the network if the support of the timeframes is marked
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        pObj->pCopy = NULL;
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+        if ( Abc_NtkLatch(pFrames, i)->pCopy )
+            pObj->pCopy = (void *)1;
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        for ( k = 0; k <= iFrame; k++ )
+            if ( Abc_NtkPi(pFrames, k*Abc_NtkPiNum(pNtk) + i)->pCopy )
+                pObj->pCopy = (void *)1;
+    // free stuff
+    Vec_PtrFree( vSupp );
+    Abc_NtkDelete( pFrames );
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Returns the PO values under the given input pattern.]
+  Synopsis    [Reports mismatch between the two sequential networks.]
 
   Description []
                
@@ -433,45 +540,157 @@ int * Abc_NtkVerifyGetCleanModel( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-int * Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel )
+void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames )
 {
-    Vec_Ptr_t * vNodes;
-    Abc_Obj_t * pNode;
-    int * pValues, Value0, Value1, i;
-    int fStrashed = 0;
-    if ( !Abc_NtkIsStrash(pNtk) )
+    Vec_Ptr_t * vInfo1, * vInfo2;
+    Abc_Obj_t * pObj, * pObjError, * pObj1, * pObj2;
+    int ValueError1, ValueError2;
+    unsigned * pPats1, * pPats2;
+    int i, o, k, nErrors, iFrameError, iNodePo, nPrinted;
+    int fRemove1 = 0, fRemove2 = 0;
+
+    if ( !Abc_NtkIsStrash(pNtk1) )
+        fRemove1 = 1, pNtk1 = Abc_NtkStrash( pNtk1, 0, 0 );
+    if ( !Abc_NtkIsStrash(pNtk2) )
+        fRemove2 = 1, pNtk2 = Abc_NtkStrash( pNtk2, 0, 0 );
+
+    // simulate sequential circuits
+    vInfo1 = Sim_SimulateSeqModel( pNtk1, nFrames, pModel );
+    vInfo2 = Sim_SimulateSeqModel( pNtk2, nFrames, pModel );
+
+    // look for a discrepancy in the PO values
+    nErrors = 0;
+    pObjError = NULL;
+    for ( i = 0; i < nFrames; i++ )
     {
-        pNtk = Abc_NtkStrash(pNtk, 0, 0);
-        fStrashed = 1;
-    }
-    // increment the trav ID
-    Abc_NtkIncrementTravId( pNtk );
-    // set the CI values
-    Abc_NtkForEachCi( pNtk, pNode, i )
-        pNode->pCopy = (void *)pModel[i];
-    // simulate in the topological order
-    vNodes = Abc_NtkDfs( pNtk, 1 );
-    Vec_PtrForEachEntry( vNodes, pNode, i )
-    {
-        if ( Abc_NodeIsConst(pNode) )
-            pNode->pCopy = NULL;
-        else
+        if ( pObjError )
+            break;
+        Abc_NtkForEachPo( pNtk1, pObj1, o )
         {
-            Value0 = ((int)Abc_ObjFanin0(pNode)->pCopy) ^ Abc_ObjFaninC0(pNode);
-            Value1 = ((int)Abc_ObjFanin1(pNode)->pCopy) ^ Abc_ObjFaninC1(pNode);
-            pNode->pCopy = (void *)(Value0 & Value1);
+            pObj2  = Abc_NtkPo( pNtk2, o );
+            pPats1 = Sim_SimInfoGet(vInfo1, pObj1);
+            pPats2 = Sim_SimInfoGet(vInfo2, pObj2);
+            if ( pPats1[i] == pPats2[i] )
+                continue;
+            nErrors++;
+            if ( pObjError == NULL )
+            {
+                pObjError   = pObj1;
+                iFrameError = i;
+                iNodePo     = o;
+                ValueError1 = (pPats1[i] > 0);
+                ValueError2 = (pPats2[i] > 0);
+            }
         }
     }
-    Vec_PtrFree( vNodes );
-    // fill the output values
-    pValues = ALLOC( int, Abc_NtkCoNum(pNtk) );
-    Abc_NtkForEachCo( pNtk, pNode, i )
-        pValues[i] = ((int)Abc_ObjFanin0(pNode)->pCopy) ^ Abc_ObjFaninC0(pNode);
-    if ( fStrashed )
-        Abc_NtkDelete( pNtk );
-    return pValues;
+
+    if ( pObjError == NULL )
+    {
+        printf( "No output mismatches detected.\n" );
+        Sim_UtilInfoFree( vInfo1 );
+        Sim_UtilInfoFree( vInfo2 );
+        if ( fRemove1 ) Abc_NtkDelete( pNtk1 );
+        if ( fRemove2 ) Abc_NtkDelete( pNtk2 );
+        return;
+    }
+
+    printf( "Verification failed for %d output%s of frame %d: ", nErrors, (nErrors>1? "s":""), iFrameError+1 );
+    // print the first 3 outputs
+    nPrinted = 0;
+    Abc_NtkForEachPo( pNtk1, pObj1, o )
+    {
+        pObj2 = Abc_NtkPo( pNtk2, o );
+        pPats1 = Sim_SimInfoGet(vInfo1, pObj1);
+        pPats2 = Sim_SimInfoGet(vInfo2, pObj2);
+        if ( pPats1[iFrameError] == pPats2[iFrameError] )
+            continue;
+        printf( " %s", Abc_ObjName(pObj1) );
+        if ( ++nPrinted == 3 )
+            break;
+    }
+    if ( nPrinted != nErrors )
+        printf( " ..." );
+    printf( "\n" );
+
+    // mark CIs of the networks in the cone of influence of this output
+    Abc_NtkGetSeqPoSupp( pNtk1, iFrameError, iNodePo );
+    Abc_NtkGetSeqPoSupp( pNtk2, iFrameError, iNodePo );
+
+    // report mismatch for the first output
+    printf( "Output %s: Value in Network1 = %d. Value in Network2 = %d.\n", 
+        Abc_ObjName(pObjError), ValueError1, ValueError2 );
+
+    printf( "The cone of influence of output %s in Network1:\n", Abc_ObjName(pObjError) );
+    printf( "PIs: " );
+    Abc_NtkForEachPi( pNtk1, pObj, i )
+        if ( pObj->pCopy )
+            printf( "%s ", Abc_ObjName(pObj) );
+    printf( "\n" );
+    printf( "Latches: " );
+    Abc_NtkForEachLatch( pNtk1, pObj, i )
+        if ( pObj->pCopy )
+            printf( "%s ", Abc_ObjName(pObj) );
+    printf( "\n" );
+
+    printf( "The cone of influence of output %s in Network2:\n", Abc_ObjName(pObjError) );
+    printf( "PIs: " );
+    Abc_NtkForEachPi( pNtk2, pObj, i )
+        if ( pObj->pCopy )
+            printf( "%s ", Abc_ObjName(pObj) );
+    printf( "\n" );
+    printf( "Latches: " );
+    Abc_NtkForEachLatch( pNtk2, pObj, i )
+        if ( pObj->pCopy )
+            printf( "%s ", Abc_ObjName(pObj) );
+    printf( "\n" );
+
+    // print the patterns
+    for ( i = 0; i <= iFrameError; i++ )
+    {
+        printf( "Frame %d:  ", i+1 );
+
+        printf( "PI(1):" );
+        Abc_NtkForEachPi( pNtk1, pObj, k )
+            if ( pObj->pCopy )
+                printf( "%d", Sim_SimInfoGet(vInfo1, pObj)[i] > 0 );
+        printf( " " );
+        printf( "L(1):" );
+        Abc_NtkForEachLatch( pNtk1, pObj, k )
+            if ( pObj->pCopy )
+                printf( "%d", Sim_SimInfoGet(vInfo1, pObj)[i] > 0 );
+        printf( " " );
+        printf( "%s(1):", Abc_ObjName(pObjError) );
+        printf( "%d", Sim_SimInfoGet(vInfo1, pObjError)[i] > 0 );
+
+        printf( "  " );
+
+        printf( "PI(2):" );
+        Abc_NtkForEachPi( pNtk2, pObj, k )
+            if ( pObj->pCopy )
+                printf( "%d", Sim_SimInfoGet(vInfo2, pObj)[i] > 0 );
+        printf( " " );
+        printf( "L(2):" );
+        Abc_NtkForEachLatch( pNtk2, pObj, k )
+            if ( pObj->pCopy )
+                printf( "%d", Sim_SimInfoGet(vInfo2, pObj)[i] > 0 );
+        printf( " " );
+        printf( "%s(2):", Abc_ObjName(pObjError) );
+        printf( "%d", Sim_SimInfoGet(vInfo2, pObjError)[i] > 0 );
+
+        printf( "\n" );
+    }
+    Abc_NtkForEachCi( pNtk1, pObj, i )
+        pObj->pCopy = NULL;
+    Abc_NtkForEachCi( pNtk2, pObj, i )
+        pObj->pCopy = NULL;
+
+    Sim_UtilInfoFree( vInfo1 );
+    Sim_UtilInfoFree( vInfo2 );
+    if ( fRemove1 ) Abc_NtkDelete( pNtk1 );
+    if ( fRemove2 ) Abc_NtkDelete( pNtk2 );
 }
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h
index 7556dd87..3f3d04e5 100644
--- a/src/misc/vec/vecInt.h
+++ b/src/misc/vec/vecInt.h
@@ -52,6 +52,10 @@ struct Vec_Int_t_
     for ( i = 0; (i < Vec_IntSize(vVec)) && (((Entry) = Vec_IntEntry(vVec, i)), 1); i++ )
 #define Vec_IntForEachEntryStart( vVec, Entry, i, Start )                                   \
     for ( i = Start; (i < Vec_IntSize(vVec)) && (((Entry) = Vec_IntEntry(vVec, i)), 1); i++ )
+#define Vec_IntForEachEntryStartStop( vVec, Entry, i, Start, Stop )                         \
+    for ( i = Start; (i < Stop) && (((Entry) = Vec_IntEntry(vVec, i)), 1); i++ )
+#define Vec_IntForEachEntryReverse( vVec, pEntry, i )                                       \
+    for ( i = Vec_IntSize(vVec) - 1; (i >= 0) && (((pEntry) = Vec_IntEntry(vVec, i)), 1); i-- )
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
diff --git a/src/opt/sim/sim.h b/src/opt/sim/sim.h
index afed7190..c561236b 100644
--- a/src/opt/sim/sim.h
+++ b/src/opt/sim/sim.h
@@ -17,7 +17,7 @@
   Revision    [$Id: sim.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
- 
+
 #ifndef __SIM_H__
 #define __SIM_H__
 
@@ -162,6 +162,7 @@ struct Sim_Pat_t_
 #define Sim_SuppFunHasVar(vSupps,Output,v)    Sim_HasBit((unsigned*)(vSupps)->pArray[Output],(v))
 #define Sim_SimInfoSetVar(vSupps,pNode,v)     Sim_SetBit((unsigned*)(vSupps)->pArray[(pNode)->Id],(v))
 #define Sim_SimInfoHasVar(vSupps,pNode,v)     Sim_HasBit((unsigned*)(vSupps)->pArray[(pNode)->Id],(v))
+#define Sim_SimInfoGet(vInfo,pNode)           ((unsigned *)((vInfo)->pArray[(pNode)->Id]))
 
 ////////////////////////////////////////////////////////////////////////
 ///                    FUNCTION DECLARATIONS                         ///
@@ -176,6 +177,9 @@ extern void            Sim_ManStop( Sim_Man_t * p );
 extern void            Sim_ManPrintStats( Sim_Man_t * p );
 extern Sim_Pat_t *     Sim_ManPatAlloc( Sim_Man_t * p );
 extern void            Sim_ManPatFree( Sim_Man_t * p, Sim_Pat_t * pPat );
+/*=== simSeq.c ==========================================================*/
+extern Vec_Ptr_t *     Sim_SimulateSeqRandom( Abc_Ntk_t * pNtk, int nFrames, int nWords );
+extern Vec_Ptr_t *     Sim_SimulateSeqModel( Abc_Ntk_t * pNtk, int nFrames, int * pModel );
 /*=== simSupp.c ==========================================================*/
 extern Vec_Ptr_t *     Sim_ComputeStrSupp( Abc_Ntk_t * pNtk );
 extern Vec_Ptr_t *     Sim_ComputeFunSupp( Abc_Ntk_t * pNtk, int fVerbose );
@@ -197,10 +201,17 @@ extern void            Sim_UtilInfoFlip( Sim_Man_t * p, Abc_Obj_t * pNode );
 extern bool            Sim_UtilInfoCompare( Sim_Man_t * p, Abc_Obj_t * pNode );
 extern void            Sim_UtilSimulate( Sim_Man_t * p, bool fFirst );
 extern void            Sim_UtilSimulateNode( Sim_Man_t * p, Abc_Obj_t * pNode, bool fType, bool fType1, bool fType2 );
-extern void            Sim_UtilSimulateNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords );
+extern void            Sim_UtilSimulateNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords, int nOffset );
+extern void            Sim_UtilTransferNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords, int nOffset, int fShift );
 extern int             Sim_UtilCountSuppSizes( Sim_Man_t * p, int fStruct );
 extern int             Sim_UtilCountOnes( unsigned * pSimInfo, int nSimWords );
-extern void            Sim_UtilGetRandom( unsigned * pPatRand, int nSimWords );
+extern Vec_Int_t *     Sim_UtilCountOnesArray( Vec_Ptr_t * vInfo, int nSimWords );
+extern void            Sim_UtilSetRandom( unsigned * pPatRand, int nSimWords );
+extern void            Sim_UtilSetCompl( unsigned * pPatRand, int nSimWords );
+extern void            Sim_UtilSetConst( unsigned * pPatRand, int nSimWords, int fConst1 );
+extern int             Sim_UtilInfoIsEqual( unsigned * pPats1, unsigned * pPats2, int nSimWords );
+extern int             Sim_UtilInfoIsImp( unsigned * pPats1, unsigned * pPats2, int nSimWords );
+extern int             Sim_UtilInfoIsClause( unsigned * pPats1, unsigned * pPats2, int nSimWords );
 extern int             Sim_UtilCountAllPairs( Vec_Ptr_t * vSuppFun, int nSimWords, Vec_Int_t * vCounters );
 extern void            Sim_UtilCountPairsAll( Sym_Man_t * p );
 extern int             Sim_UtilMatrsAreDisjoint( Sym_Man_t * p );
diff --git a/src/opt/sim/simSeq.c b/src/opt/sim/simSeq.c
new file mode 100644
index 00000000..2bf59f44
--- /dev/null
+++ b/src/opt/sim/simSeq.c
@@ -0,0 +1,171 @@
+/**CFile****************************************************************
+
+  FileName    [simSeq.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Simulation for sequential circuits.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: simUtils.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "sim.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void Sim_SimulateSeqFrame( Vec_Ptr_t * vInfo, Abc_Ntk_t * pNtk, int iFrames, int nWords, int fTransfer );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Simulates sequential circuit.]
+
+  Description [Takes sequential circuit (pNtk). Simulates the given number
+  (nFrames) of the circuit with the given number of machine words (nWords)
+  of random simulation data, starting from the initial state. If the initial
+  state of some latches is a don't-care, uses random input for that latch.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Sim_SimulateSeqRandom( Abc_Ntk_t * pNtk, int nFrames, int nWords )
+{
+    Vec_Ptr_t * vInfo;
+    Abc_Obj_t * pNode;
+    int i;
+    assert( Abc_NtkIsStrash(pNtk) );
+    vInfo = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), nWords * nFrames, 0 );
+    // set the constant data
+    pNode = Abc_AigConst1(pNtk->pManFunc);
+    Sim_UtilSetConst( Sim_SimInfoGet(vInfo,pNode), nWords * nFrames, 1 );
+    // set the random PI data
+    Abc_NtkForEachPi( pNtk, pNode, i )
+        Sim_UtilSetRandom( Sim_SimInfoGet(vInfo,pNode), nWords * nFrames );
+    // set the initial state data
+    Abc_NtkForEachLatch( pNtk, pNode, i )
+        if ( Abc_LatchIsInit0(pNode) )
+            Sim_UtilSetConst( Sim_SimInfoGet(vInfo,pNode), nWords, 0 );
+        else if ( Abc_LatchIsInit1(pNode) )
+            Sim_UtilSetConst( Sim_SimInfoGet(vInfo,pNode), nWords, 1 );
+        else 
+            Sim_UtilSetRandom( Sim_SimInfoGet(vInfo,pNode), nWords );
+    // simulate the nodes for the given number of timeframes
+    for ( i = 0; i < nFrames; i++ )
+        Sim_SimulateSeqFrame( vInfo, pNtk, i, nWords, (int)(i < nFrames-1) );
+    return vInfo;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Simulates sequential circuit.]
+
+  Description [Takes sequential circuit (pNtk). Simulates the given number
+  (nFrames) of the circuit with the given model. The model is assumed to 
+  contain values of PIs for each frame. The latches are initialized to
+  the initial state. One word of data is simulated.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Sim_SimulateSeqModel( Abc_Ntk_t * pNtk, int nFrames, int * pModel )
+{
+    Vec_Ptr_t * vInfo;
+    Abc_Obj_t * pNode;
+    unsigned * pUnsigned;
+    int i, k;
+    vInfo = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), nFrames, 0 );
+    // set the constant data
+    pNode = Abc_AigConst1(pNtk->pManFunc);
+    Sim_UtilSetConst( Sim_SimInfoGet(vInfo,pNode), nFrames, 1 );
+    // set the random PI data
+    Abc_NtkForEachPi( pNtk, pNode, i )
+    {
+        pUnsigned = Sim_SimInfoGet(vInfo,pNode);
+        for ( k = 0; k < nFrames; k++ )
+            pUnsigned[k] = pModel[k * Abc_NtkPiNum(pNtk) + i] ? ~((unsigned)0) : 0;
+    }
+    // set the initial state data
+    Abc_NtkForEachLatch( pNtk, pNode, i )
+    {
+        pUnsigned = Sim_SimInfoGet(vInfo,pNode);
+        if ( Abc_LatchIsInit0(pNode) )
+            pUnsigned[0] = 0;
+        else if ( Abc_LatchIsInit1(pNode) )
+            pUnsigned[0] = ~((unsigned)0);
+        else 
+            pUnsigned[0] = SIM_RANDOM_UNSIGNED;
+    }
+    // simulate the nodes for the given number of timeframes
+    for ( i = 0; i < nFrames; i++ )
+        Sim_SimulateSeqFrame( vInfo, pNtk, i, 1, (int)(i < nFrames-1) );
+/*
+    // print the simulated values
+    for ( i = 0; i < nFrames; i++ )
+    {
+        printf( "Frame %d : ", i+1 );
+        Abc_NtkForEachPi( pNtk, pNode, k )
+            printf( "%d", Sim_SimInfoGet(vInfo,pNode)[i] > 0 );
+        printf( " " );
+        Abc_NtkForEachLatch( pNtk, pNode, k )
+            printf( "%d", Sim_SimInfoGet(vInfo,pNode)[i] > 0 );
+        printf( " " );
+        Abc_NtkForEachPo( pNtk, pNode, k )
+            printf( "%d", Sim_SimInfoGet(vInfo,pNode)[i] > 0 );
+        printf( "\n" );
+    }
+    printf( "\n" );
+*/
+    return vInfo;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Simulates one frame of sequential circuit.]
+
+  Description [Assumes that the latches and POs are already initialized.
+  In the end transfers the data to the latches of the next frame.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sim_SimulateSeqFrame( Vec_Ptr_t * vInfo, Abc_Ntk_t * pNtk, int iFrames, int nWords, int fTransfer )
+{
+    Abc_Obj_t * pNode;
+    int i;
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        Sim_UtilSimulateNodeOne( pNode, vInfo, nWords, iFrames * nWords );
+    Abc_NtkForEachPo( pNtk, pNode, i )
+        Sim_UtilTransferNodeOne( pNode, vInfo, nWords, iFrames * nWords, 0 );
+    if ( !fTransfer )
+        return;
+    Abc_NtkForEachLatch( pNtk, pNode, i )
+        Sim_UtilTransferNodeOne( pNode, vInfo, nWords, iFrames * nWords, 1 );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/sim/simSwitch.c b/src/opt/sim/simSwitch.c
index b43597f3..30377611 100644
--- a/src/opt/sim/simSwitch.c
+++ b/src/opt/sim/simSwitch.c
@@ -65,7 +65,7 @@ Vec_Int_t * Sim_NtkComputeSwitching( Abc_Ntk_t * pNtk, int nPatterns )
     Abc_NtkForEachCi( pNtk, pNode, i )
     {
         pSimInfo = Vec_PtrEntry(vSimInfo, pNode->Id);
-        Sim_UtilGetRandom( pSimInfo, nSimWords );
+        Sim_UtilSetRandom( pSimInfo, nSimWords );
         pSwitching[pNode->Id] = Sim_ComputeSwitching( pSimInfo, nSimWords );
     }
     // simulate the internal nodes
@@ -73,7 +73,7 @@ Vec_Int_t * Sim_NtkComputeSwitching( Abc_Ntk_t * pNtk, int nPatterns )
     Vec_PtrForEachEntry( vNodes, pNode, i )
     {
         pSimInfo = Vec_PtrEntry(vSimInfo, pNode->Id);
-        Sim_UtilSimulateNodeOne( pNode, vSimInfo, nSimWords );
+        Sim_UtilSimulateNodeOne( pNode, vSimInfo, nSimWords, 0 );
         pSwitching[pNode->Id] = Sim_ComputeSwitching( pSimInfo, nSimWords );
     }
     Vec_PtrFree( vNodes );
diff --git a/src/opt/sim/simSym.c b/src/opt/sim/simSym.c
index c452bb1b..93e0426e 100644
--- a/src/opt/sim/simSym.c
+++ b/src/opt/sim/simSym.c
@@ -71,7 +71,7 @@ p->timeStruct = clock() - clk;
     for ( i = 1; i <= 1000; i++ )
     {
         // simulate this pattern
-        Sim_UtilGetRandom( p->uPatRand, p->nSimWords );
+        Sim_UtilSetRandom( p->uPatRand, p->nSimWords );
         Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
         if ( i % 50 != 0 )
             continue;
diff --git a/src/opt/sim/simSymSim.c b/src/opt/sim/simSymSim.c
index 94028c47..e798654f 100644
--- a/src/opt/sim/simSymSim.c
+++ b/src/opt/sim/simSymSim.c
@@ -57,7 +57,7 @@ clk = clock();
     {
         if ( Abc_NodeIsConst(pNode) )
             continue;
-        Sim_UtilSimulateNodeOne( pNode, p->vSim, p->nSimWords );
+        Sim_UtilSimulateNodeOne( pNode, p->vSim, p->nSimWords, 0 );
     }
 p->timeSim += clock() - clk;
     // collect info into the CO matrices
diff --git a/src/opt/sim/simUtils.c b/src/opt/sim/simUtils.c
index 4b89c650..6a3a911b 100644
--- a/src/opt/sim/simUtils.c
+++ b/src/opt/sim/simUtils.c
@@ -299,7 +299,7 @@ void Sim_UtilSimulateNode( Sim_Man_t * p, Abc_Obj_t * pNode, bool fType, bool fT
   SeeAlso     []
 
 ***********************************************************************/
-void Sim_UtilSimulateNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords )
+void Sim_UtilSimulateNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords, int nOffset )
 {
     unsigned * pSimmNode, * pSimmNode1, * pSimmNode2;
     int k, fComp1, fComp2;
@@ -310,6 +310,9 @@ void Sim_UtilSimulateNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimW
     pSimmNode  = Vec_PtrEntry(vSimInfo, pNode->Id);
     pSimmNode1 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId0(pNode));
     pSimmNode2 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId1(pNode));
+    pSimmNode  += nOffset;
+    pSimmNode1 += nOffset;
+    pSimmNode2 += nOffset;
     fComp1 = Abc_ObjFaninC0(pNode);
     fComp2 = Abc_ObjFaninC1(pNode);
     if ( fComp1 && fComp2 )
@@ -328,6 +331,36 @@ void Sim_UtilSimulateNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimW
 
 /**Function*************************************************************
 
+  Synopsis    [Simulates one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sim_UtilTransferNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords, int nOffset, int fShift )
+{
+    unsigned * pSimmNode, * pSimmNode1;
+    int k, fComp1;
+    // simulate the internal nodes
+    assert( Abc_ObjIsCo(pNode) );
+    pSimmNode  = Vec_PtrEntry(vSimInfo, pNode->Id);
+    pSimmNode1 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId0(pNode));
+    pSimmNode  += nOffset + (fShift > 0)*nSimWords;
+    pSimmNode1 += nOffset;
+    fComp1 = Abc_ObjFaninC0(pNode);
+    if ( fComp1 )
+        for ( k = 0; k < nSimWords; k++ )
+            pSimmNode[k] = ~pSimmNode1[k];
+    else 
+        for ( k = 0; k < nSimWords; k++ )
+            pSimmNode[k] =  pSimmNode1[k];
+}
+
+/**Function*************************************************************
+
   Synopsis    [Returns 1 if the simulation infos are equal.]
 
   Description []
@@ -380,10 +413,31 @@ int Sim_UtilCountOnes( unsigned * pSimInfo, int nSimWords )
     return nOnes;    
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of 1's in the bitstring.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Sim_UtilCountOnesArray( Vec_Ptr_t * vInfo, int nSimWords )
+{
+    Vec_Int_t * vCounters;
+    unsigned * pSimInfo;
+    int i;
+    vCounters = Vec_IntStart( Vec_PtrSize(vInfo) );
+    Vec_PtrForEachEntry( vInfo, pSimInfo, i )
+        Vec_IntWriteEntry( vCounters, i, Sim_UtilCountOnes(pSimInfo, nSimWords) );
+    return vCounters;
+}
 
 /**Function*************************************************************
 
-  Synopsis    [Returns the random pattern.]
+  Synopsis    [Returns random patterns.]
 
   Description []
                
@@ -392,7 +446,7 @@ int Sim_UtilCountOnes( unsigned * pSimInfo, int nSimWords )
   SeeAlso     []
 
 ***********************************************************************/
-void Sim_UtilGetRandom( unsigned * pPatRand, int nSimWords )
+void Sim_UtilSetRandom( unsigned * pPatRand, int nSimWords )
 {
     int k;
     for ( k = 0; k < nSimWords; k++ )
@@ -401,6 +455,104 @@ void Sim_UtilGetRandom( unsigned * pPatRand, int nSimWords )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns complemented patterns.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sim_UtilSetCompl( unsigned * pPatRand, int nSimWords )
+{
+    int k;
+    for ( k = 0; k < nSimWords; k++ )
+        pPatRand[k] = ~pPatRand[k];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns constant patterns.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sim_UtilSetConst( unsigned * pPatRand, int nSimWords, int fConst1 )
+{
+    int k;
+    for ( k = 0; k < nSimWords; k++ )
+        pPatRand[k] = 0;
+    if ( fConst1 )
+        Sim_UtilSetCompl( pPatRand, nSimWords );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if equal.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sim_UtilInfoIsEqual( unsigned * pPats1, unsigned * pPats2, int nSimWords )
+{
+    int k;
+    for ( k = 0; k < nSimWords; k++ )
+        if ( pPats1[k] != pPats2[k] )
+            return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if Node1 implies Node2.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sim_UtilInfoIsImp( unsigned * pPats1, unsigned * pPats2, int nSimWords )
+{
+    int k;
+    for ( k = 0; k < nSimWords; k++ )
+        if ( pPats1[k] & ~pPats2[k] )
+            return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if Node1 v Node2 is always true.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sim_UtilInfoIsClause( unsigned * pPats1, unsigned * pPats2, int nSimWords )
+{
+    int k;
+    for ( k = 0; k < nSimWords; k++ )
+        if ( ~pPats1[k] & ~pPats2[k] )
+            return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Counts the total number of pairs.]
 
   Description []
diff --git a/src/sat/fraig/fraig.h b/src/sat/fraig/fraig.h
index dc679907..33ae1e49 100644
--- a/src/sat/fraig/fraig.h
+++ b/src/sat/fraig/fraig.h
@@ -153,6 +153,9 @@ extern void                Fraig_ParamsSetDefaultFull( Fraig_Params_t * pParams
 extern Fraig_Man_t *       Fraig_ManCreate( Fraig_Params_t * pParams );
 extern void                Fraig_ManFree( Fraig_Man_t * pMan );
 extern void                Fraig_ManPrintStats( Fraig_Man_t * p );
+extern Fraig_NodeVec_t *   Fraig_ManGetSimInfo( Fraig_Man_t * p );
+extern int                 Fraig_ManCheckClauseUsingSimInfo( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2 );
+extern void                Fraig_ManAddClause( Fraig_Man_t * p, Fraig_Node_t ** ppNodes, int nNodes );
 
 /*=== fraigDfs.c =============================================================*/
 extern Fraig_NodeVec_t *   Fraig_Dfs( Fraig_Man_t * pMan, int fEquiv );
@@ -168,6 +171,7 @@ extern int                 Fraig_NodesAreEqual( Fraig_Man_t * p, Fraig_Node_t *
 extern int                 Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit, int nTimeLimit );
 extern void                Fraig_ManProveMiter( Fraig_Man_t * p );
 extern int                 Fraig_ManCheckMiter( Fraig_Man_t * p );
+extern int                 Fraig_ManCheckClauseUsingSat( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit );
 
 /*=== fraigVec.c ===============================================================*/
 extern Fraig_NodeVec_t *   Fraig_NodeVecAlloc( int nCap );
diff --git a/src/sat/fraig/fraigInt.h b/src/sat/fraig/fraigInt.h
index f14fb4c1..a5da2263 100644
--- a/src/sat/fraig/fraigInt.h
+++ b/src/sat/fraig/fraigInt.h
@@ -280,9 +280,9 @@ struct Fraig_NodeStruct_t_
 // the vector of nodes
 struct Fraig_NodeVecStruct_t_
 {
-    Fraig_Node_t **       pArray;        // the array of nodes
-    int                   nSize;         // the number of entries in the array
     int                   nCap;          // the number of allocated entries
+    int                   nSize;         // the number of entries in the array
+    Fraig_Node_t **       pArray;        // the array of nodes
 };
 
 // the hash table 
@@ -381,6 +381,8 @@ extern void                Fraig_FeedBackTest( Fraig_Man_t * p );
 extern int                 Fraig_FeedBackCompress( Fraig_Man_t * p );
 extern int *               Fraig_ManAllocCounterExample( Fraig_Man_t * p );
 extern int *               Fraig_ManSaveCounterExample( Fraig_Man_t * p, Fraig_Node_t * pNode );
+/*=== fraigMan.c =============================================================*/
+extern void                Fraig_ManCreateSolver( Fraig_Man_t * p );
 /*=== fraigMem.c =============================================================*/
 extern Fraig_MemFixed_t *  Fraig_MemFixedStart( int nEntrySize );
 extern void                Fraig_MemFixedStop( Fraig_MemFixed_t * p, int fVerbose );
diff --git a/src/sat/fraig/fraigMan.c b/src/sat/fraig/fraigMan.c
index 1a34af86..ca6df9c1 100644
--- a/src/sat/fraig/fraigMan.c
+++ b/src/sat/fraig/fraigMan.c
@@ -225,6 +225,31 @@ void Fraig_ManFree( Fraig_Man_t * p )
     FREE( p );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Prepares the SAT solver to run on the two nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fraig_ManCreateSolver( Fraig_Man_t * p )
+{
+    extern int timeSelect;
+    extern int timeAssign;
+    assert( p->pSat == NULL );
+    // allocate data for SAT solving
+    p->pSat       = Msat_SolverAlloc( 500, 1, 1, 1, 1, 0 );
+    p->vVarsInt   = Msat_SolverReadConeVars( p->pSat );   
+    p->vAdjacents = Msat_SolverReadAdjacents( p->pSat );
+    p->vVarsUsed  = Msat_SolverReadVarsUsed( p->pSat );
+    timeSelect = 0;
+    timeAssign = 0;
+}
+
  
 /**Function*************************************************************
 
@@ -264,6 +289,168 @@ void Fraig_ManPrintStats( Fraig_Man_t * p )
 //    PRT( "Assignment", timeAssign );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Allocates simulation information for all nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Fraig_NodeVec_t * Fraig_UtilInfoAlloc( int nSize, int nWords, bool fClean )
+{
+    Fraig_NodeVec_t * vInfo;
+    unsigned * pUnsigned;
+    int i;
+    assert( nSize > 0 && nWords > 0 );
+    vInfo = Fraig_NodeVecAlloc( nSize );
+    pUnsigned = ALLOC( unsigned, nSize * nWords );
+    vInfo->pArray[0] = (Fraig_Node_t *)pUnsigned;
+    if ( fClean )
+        memset( pUnsigned, 0, sizeof(unsigned) * nSize * nWords );
+    for ( i = 1; i < nSize; i++ )
+        vInfo->pArray[i] = (Fraig_Node_t *)(((unsigned *)vInfo->pArray[i-1]) + nWords);
+    vInfo->nSize = nSize;
+    return vInfo;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns simulation info of all nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Fraig_NodeVec_t * Fraig_ManGetSimInfo( Fraig_Man_t * p )
+{
+    Fraig_NodeVec_t * vInfo;
+    Fraig_Node_t * pNode;
+    unsigned * pUnsigned;
+    int nRandom, nDynamic;
+    int i, k, nWords;
+
+    nRandom  = Fraig_ManReadPatternNumRandom( p );
+    nDynamic = Fraig_ManReadPatternNumDynamic( p );
+    nWords = nRandom / 32 + nDynamic / 32;
+
+    vInfo = Fraig_UtilInfoAlloc( p->vNodes->nSize, nWords, 0 );
+    for ( i = 0; i < p->vNodes->nSize; i++ )
+    {
+        pNode = p->vNodes->pArray[i];
+        assert( i == pNode->Num );
+        pUnsigned = (unsigned *)vInfo->pArray[i];
+        for ( k = 0; k < nRandom / 32; k++ )
+            pUnsigned[k] = pNode->puSimR[k];
+        for ( k = 0; k < nDynamic / 32; k++ )
+            pUnsigned[nRandom / 32 + k] = pNode->puSimD[k];
+    }
+    return vInfo;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if A v B is always true based on the siminfo.]
+
+  Description [A v B is always true iff A' * B' is always false.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fraig_ManCheckClauseUsingSimInfo( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2 )
+{
+    int fCompl1, fCompl2, i;
+
+    fCompl1 = 1 ^ Fraig_IsComplement(pNode1) ^ Fraig_Regular(pNode1)->fInv;
+    fCompl2 = 1 ^ Fraig_IsComplement(pNode2) ^ Fraig_Regular(pNode2)->fInv;
+
+    pNode1 = Fraig_Regular(pNode1);
+    pNode2 = Fraig_Regular(pNode2);
+    assert( pNode1 != pNode2 );
+    
+    // check the simulation info
+    if ( fCompl1 && fCompl2 )
+    {
+        for ( i = 0; i < p->nWordsRand; i++ )
+            if ( ~pNode1->puSimR[i] & ~pNode2->puSimR[i] )
+                return 0;
+        for ( i = 0; i < p->iWordStart; i++ )
+            if ( ~pNode1->puSimD[i] & ~pNode2->puSimD[i] )
+                return 0;
+        return 1;
+    }
+    if ( !fCompl1 && fCompl2 )
+    {
+        for ( i = 0; i < p->nWordsRand; i++ )
+            if ( pNode1->puSimR[i] & ~pNode2->puSimR[i] )
+                return 0;
+        for ( i = 0; i < p->iWordStart; i++ )
+            if ( pNode1->puSimD[i] & ~pNode2->puSimD[i] )
+                return 0;
+        return 1;
+    }
+    if ( fCompl1 && !fCompl2 )
+    {
+        for ( i = 0; i < p->nWordsRand; i++ )
+            if ( ~pNode1->puSimR[i] & pNode2->puSimR[i] )
+                return 0;
+        for ( i = 0; i < p->iWordStart; i++ )
+            if ( ~pNode1->puSimD[i] & pNode2->puSimD[i] )
+                return 0;
+        return 1;
+    }
+//    if ( fCompl1 && fCompl2 )
+    {
+        for ( i = 0; i < p->nWordsRand; i++ )
+            if ( pNode1->puSimR[i] & pNode2->puSimR[i] )
+                return 0;
+        for ( i = 0; i < p->iWordStart; i++ )
+            if ( pNode1->puSimD[i] & pNode2->puSimD[i] )
+                return 0;
+        return 1;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds clauses to the solver.]
+
+  Description [This procedure is used to add external clauses to the solver.
+  The clauses are given by sets of nodes. Each node stands for one literal.
+  If the node is complemented, the literal is negated.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fraig_ManAddClause( Fraig_Man_t * p, Fraig_Node_t ** ppNodes, int nNodes )
+{
+    Fraig_Node_t * pNode;
+    int i, fComp, RetValue;
+    if ( p->pSat == NULL )
+        Fraig_ManCreateSolver( p );
+    // create four clauses
+    Msat_IntVecClear( p->vProj );
+    for ( i = 0; i < nNodes; i++ )
+    {
+        pNode = Fraig_Regular(ppNodes[i]);
+        fComp = Fraig_IsComplement(ppNodes[i]);
+        Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode->Num, fComp) );
+//        printf( "%d(%d) ", pNode->Num, fComp );
+    }
+//    printf( "\n" );
+    RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
+    assert( RetValue );
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c
index d54a3119..e6b1667e 100644
--- a/src/sat/fraig/fraigSat.c
+++ b/src/sat/fraig/fraigSat.c
@@ -97,7 +97,7 @@ void Fraig_ManProveMiter( Fraig_Man_t * p )
             continue;
         if ( Fraig_NodeIsEquivalent( p, p->pConst1, pNode, -1, p->nSeconds ) )
         {
-            if ( Fraig_IsComplement(p->vOutputs->pArray[i]) )
+            if ( Fraig_IsComplement(p->vOutputs->pArray[i]) ^ Fraig_NodeComparePhase(p->pConst1, pNode) )
                 p->vOutputs->pArray[i] = Fraig_Not(p->pConst1);
             else
                 p->vOutputs->pArray[i] = p->pConst1;
@@ -180,17 +180,7 @@ int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t *
 
     // make sure the solver is allocated and has enough variables
     if ( p->pSat == NULL )
-    {
-        extern int timeSelect;
-        extern int timeAssign;
-        // allocate data for SAT solving
-        p->pSat       = Msat_SolverAlloc( 500, 1, 1, 1, 1, 0 );
-        p->vVarsInt   = Msat_SolverReadConeVars( p->pSat );   
-        p->vAdjacents = Msat_SolverReadAdjacents( p->pSat );
-        p->vVarsUsed  = Msat_SolverReadVarsUsed( p->pSat );
-        timeSelect = 0;
-        timeAssign = 0;
-    }
+        Fraig_ManCreateSolver( p );
     // make sure the SAT solver has enough variables
     for ( i = Msat_SolverReadVarNum(p->pSat); i < p->vNodes->nSize; i++ )
         Msat_SolverAddVar( p->pSat );
@@ -365,32 +355,12 @@ int Fraig_NodeIsImplication( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t
 
     // make sure the solver is allocated and has enough variables
     if ( p->pSat == NULL )
-    {
-        extern int timeSelect;
-        extern int timeAssign;
-        // allocate data for SAT solving
-        p->pSat       = Msat_SolverAlloc( 500, 1, 1, 1, 1, 0 );
-        p->vVarsInt   = Msat_SolverReadConeVars( p->pSat );   
-        p->vAdjacents = Msat_SolverReadAdjacents( p->pSat );
-        p->vVarsUsed  = Msat_SolverReadVarsUsed( p->pSat );
-        timeSelect = 0;
-        timeAssign = 0;
-    }
+        Fraig_ManCreateSolver( p );
     // make sure the SAT solver has enough variables
     for ( i = Msat_SolverReadVarNum(p->pSat); i < p->vNodes->nSize; i++ )
         Msat_SolverAddVar( p->pSat );
 
-
-/*
-    {
-        Fraig_Node_t * ppNodes[2] = { pOld, pNew };
-        extern void Fraig_MappingShowNodes( Fraig_Man_t * pMan, Fraig_Node_t ** ppRoots, int nRoots, char * pFileName );
-        Fraig_MappingShowNodes( p, ppNodes, 2, "temp_aig" );
-    }
-*/
-
-
-    // get the logic cone
+   // get the logic cone
 clk = clock();
     Fraig_OrderVariables( p, pOld, pNew );
 //    Fraig_PrepareCones( p, pOld, pNew );
@@ -449,8 +419,8 @@ if ( fVerbose )
 PRT( "time", clock() - clk );
 }
         // record the counter example
-//        Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pOld, pNew );
-//        p->nSatCounterImp++;
+        Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pOld, pNew );
+        p->nSatCounterImp++;
         return 0;
     }
     else // if ( RetValue1 == MSAT_UNKNOWN )
@@ -461,6 +431,96 @@ p->time3 += clock() - clk;
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Prepares the SAT solver to run on the two nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fraig_ManCheckClauseUsingSat( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit )
+{
+    Fraig_Node_t * pNode1R, * pNode2R;
+    int RetValue, RetValue1, i, clk;
+    int fVerbose = 0;
+
+    pNode1R = Fraig_Regular(pNode1);
+    pNode2R = Fraig_Regular(pNode2);
+    assert( pNode1R != pNode2R );
+
+    // make sure the solver is allocated and has enough variables
+    if ( p->pSat == NULL )
+        Fraig_ManCreateSolver( p );
+    // make sure the SAT solver has enough variables
+    for ( i = Msat_SolverReadVarNum(p->pSat); i < p->vNodes->nSize; i++ )
+        Msat_SolverAddVar( p->pSat );
+
+   // get the logic cone
+clk = clock();
+    Fraig_OrderVariables( p, pNode1R, pNode2R );
+//    Fraig_PrepareCones( p, pNode1R, pNode2R );
+p->timeTrav += clock() - clk;
+
+    ////////////////////////////////////////////
+    // prepare the solver to run incrementally on these variables
+//clk = clock();
+    Msat_SolverPrepare( p->pSat, p->vVarsInt );
+//p->time3 += clock() - clk;
+
+    // solve under assumptions
+    // A = 1; B = 0     OR     A = 1; B = 1 
+    Msat_IntVecClear( p->vProj );
+    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode1R->Num, !Fraig_IsComplement(pNode1)) );
+    Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode2R->Num, !Fraig_IsComplement(pNode2)) );
+    // run the solver
+clk = clock();
+    RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, 1000000 );
+p->timeSat += clock() - clk;
+
+    if ( RetValue1 == MSAT_FALSE )
+    {
+//p->time1 += clock() - clk;
+
+if ( fVerbose )
+{
+    printf( "unsat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
+PRT( "time", clock() - clk );
+}
+
+        // add the clause
+        Msat_IntVecClear( p->vProj );
+        Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode1R->Num, Fraig_IsComplement(pNode1)) );
+        Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode2R->Num, Fraig_IsComplement(pNode2)) );
+        RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
+        assert( RetValue );
+//        p->nSatProofImp++;
+        return 1;
+    }
+    else if ( RetValue1 == MSAT_TRUE )
+    {
+//p->time2 += clock() - clk;
+
+if ( fVerbose )
+{
+    printf( "sat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
+PRT( "time", clock() - clk );
+}
+        // record the counter example
+//        Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pNode1R, pNode2R );
+        p->nSatCounterImp++;
+        return 0;
+    }
+    else // if ( RetValue1 == MSAT_UNKNOWN )
+    {
+p->time3 += clock() - clk;
+        p->nSatFailsImp++;
+        return 0;
+    }
+}
 
 
 /**Function*************************************************************