Version abc50908

10 files changed, 420 insertions, 139 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index c9e0df68..dfe3ccc8 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -1672,26 +1672,31 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
     int c;
+    bool fUpdateLevel;
     bool fPrecompute;
     bool fUseZeros;
     bool fVerbose;
     // external functions
-    extern void   Rwr_Precompute();
-    extern int    Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUseZeros, int fVerbose );
+    extern void Rwr_Precompute();
+    extern int  Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerbose );
 
     pNtk = Abc_FrameReadNet(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    fPrecompute = 0;
-    fUseZeros   = 0;
-    fVerbose    = 0;
+    fUpdateLevel = 0;
+    fPrecompute  = 0;
+    fUseZeros    = 0;
+    fVerbose     = 0;
     util_getopt_reset();
-    while ( ( c = util_getopt( argc, argv, "xzvh" ) ) != EOF )
+    while ( ( c = util_getopt( argc, argv, "lxzvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'l':
+            fUpdateLevel ^= 1;
+            break;
         case 'x':
             fPrecompute ^= 1;
             break;
@@ -1731,7 +1736,7 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // modify the current network
-    if ( !Abc_NtkRewrite( pNtk, fUseZeros, fVerbose ) )
+    if ( !Abc_NtkRewrite( pNtk, fUpdateLevel, fUseZeros, fVerbose ) )
     {
         fprintf( pErr, "Rewriting has failed.\n" );
         return 1;
@@ -1739,8 +1744,9 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: rewrite [-zvh]\n" );
+    fprintf( pErr, "usage: rewrite [-lzvh]\n" );
     fprintf( pErr, "\t         performs technology-independent rewriting of the AIG\n" );
+    fprintf( pErr, "\t-l     : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" );
     fprintf( pErr, "\t-z     : toggle using zero-cost replacements [default = %s]\n", fUseZeros? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
@@ -1765,10 +1771,11 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     int nNodeSizeMax;
     int nConeSizeMax;
+    bool fUpdateLevel;
     bool fUseZeros;
     bool fUseDcs;
     bool fVerbose;
-    extern int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool fUseZeros, bool fUseDcs, bool fVerbose );
+    extern int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool fUpdateLevel, bool fUseZeros, bool fUseDcs, bool fVerbose );
 
     pNtk = Abc_FrameReadNet(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -1777,11 +1784,12 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     nNodeSizeMax = 10;
     nConeSizeMax = 16;
+    fUpdateLevel =  0;
     fUseZeros    =  0;
     fUseDcs      =  0;
     fVerbose     =  0;
     util_getopt_reset();
-    while ( ( c = util_getopt( argc, argv, "NCzdvh" ) ) != EOF )
+    while ( ( c = util_getopt( argc, argv, "NClzdvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -1807,6 +1815,9 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nConeSizeMax < 0 ) 
                 goto usage;
             break;
+        case 'l':
+            fUpdateLevel ^= 1;
+            break;
         case 'z':
             fUseZeros ^= 1;
             break;
@@ -1846,7 +1857,7 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // modify the current network
-    if ( !Abc_NtkRefactor( pNtk, nNodeSizeMax, nConeSizeMax, fUseZeros, fUseDcs, fVerbose ) )
+    if ( !Abc_NtkRefactor( pNtk, nNodeSizeMax, nConeSizeMax, fUpdateLevel, fUseZeros, fUseDcs, fVerbose ) )
     {
         fprintf( pErr, "Refactoring has failed.\n" );
         return 1;
@@ -1854,10 +1865,11 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: refactor [-N num] [-C num] [-zdvh]\n" );
+    fprintf( pErr, "usage: refactor [-N num] [-C num] [-lzdvh]\n" );
     fprintf( pErr, "\t         performs technology-independent refactoring of the AIG\n" );
     fprintf( pErr, "\t-N num : the max support of the collapsed node [default = %d]\n", nNodeSizeMax );  
     fprintf( pErr, "\t-C num : the max support of the containing cone [default = %d]\n", nConeSizeMax );  
+    fprintf( pErr, "\t-l     : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" );
     fprintf( pErr, "\t-z     : toggle using zero-cost replacements [default = %s]\n", fUseZeros? "yes": "no" );
     fprintf( pErr, "\t-d     : toggle using don't-cares [default = %s]\n", fUseDcs? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
@@ -2291,7 +2303,9 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
     int c;
+    int RetValue;
     int fVerbose;
+    int nSeconds;
 
     pNtk = Abc_FrameReadNet(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -2299,11 +2313,23 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // set defaults
     fVerbose = 0;
+    nSeconds = 20;
     util_getopt_reset();
-    while ( ( c = util_getopt( argc, argv, "vh" ) ) != EOF )
+    while ( ( c = util_getopt( argc, argv, "Tvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'T':
+            if ( util_optind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-T\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nSeconds = atoi(argv[util_optind]);
+            util_optind++;
+            if ( nSeconds < 0 ) 
+                goto usage;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -2323,7 +2349,7 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     {
         fprintf( stdout, "Currently can only solve the miter for combinational circuits.\n" );
         return 0;
-    }
+    } 
     if ( !Abc_NtkIsLogic(pNtk) )
     {
         fprintf( stdout, "This command can only be applied to logic network (run \"renode -c\").\n" );
@@ -2334,15 +2360,19 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( Abc_NtkIsSopLogic(pNtk) )
         Abc_NtkSopToBdd(pNtk);
 
-    if ( Abc_NtkMiterSat( pNtk, fVerbose ) )
-        printf( "The miter is satisfiable.\n" );
+    RetValue = Abc_NtkMiterSat( pNtk, nSeconds, fVerbose );
+    if ( RetValue == -1 )
+        printf( "The miter is UNDECIDED (SAT solver timed out).\n" );
+    else if ( RetValue == 0 )
+        printf( "The miter is SATISFIABLE.\n" );
     else
-        printf( "The miter is unsatisfiable.\n" );
+        printf( "The miter is UNSATISFIABLE.\n" );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: sat [-vh]\n" );
+    fprintf( pErr, "usage: sat [-T num] [-vh]\n" );
     fprintf( pErr, "\t         solves the miter\n" );
+    fprintf( pErr, "\t-T num : approximate runtime limit in seconds [default = %d]\n", nSeconds );
     fprintf( pErr, "\t-v     : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );  
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
@@ -2863,6 +2893,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // set defaults
     fAllNodes = 0;
+    memset( pParams, 0, sizeof(Fraig_Params_t) );
     pParams->nPatsRand  = 2048; // the number of words of random simulation info
     pParams->nPatsDyna  = 2048; // the number of words of dynamic simulation info
     pParams->nBTLimit   = 99;   // the max number of backtracks to perform
@@ -2879,7 +2910,6 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     {
         switch ( c )
         {
-
         case 'R':
             if ( util_optind >= argc )
             {
@@ -3913,9 +3943,10 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     int fSat;
     int fVerbose;
+    int nSeconds;
 
-    extern void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 );
-    extern void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fVerbose );
+    extern void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds );
+    extern void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fVerbose );
 
 
     pNtk = Abc_FrameReadNet(pAbc);
@@ -3923,13 +3954,25 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    fSat     = 0;
-    fVerbose = 0;
+    fSat     =  0;
+    fVerbose =  0;
+    nSeconds = 20;
     util_getopt_reset();
-    while ( ( c = util_getopt( argc, argv, "svh" ) ) != EOF )
+    while ( ( c = util_getopt( argc, argv, "Tsvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'T':
+            if ( util_optind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-T\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nSeconds = atoi(argv[util_optind]);
+            util_optind++;
+            if ( nSeconds < 0 ) 
+                goto usage;
+            break;
         case 's':
             fSat ^= 1;
             break;
@@ -3948,24 +3991,25 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // perform equivalence checking
     if ( fSat )
-        Abc_NtkCecSat( pNtk1, pNtk2 );
+        Abc_NtkCecSat( pNtk1, pNtk2, nSeconds );
     else
-        Abc_NtkCecFraig( pNtk1, pNtk2, fVerbose );
+        Abc_NtkCecFraig( pNtk1, pNtk2, nSeconds, fVerbose );
 
     if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
     if ( fDelete2 ) Abc_NtkDelete( pNtk2 );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: cec [-svh] <file1> <file2>\n" );
-    fprintf( pErr, "\t        performs combinational equivalence checking\n" );
-    fprintf( pErr, "\t-s    : toggle \"SAT only\" and \"FRAIG + SAT\" [default = %s]\n", fSat? "SAT only": "FRAIG + SAT" );
-    fprintf( pErr, "\t-v    : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
-    fprintf( pErr, "\t-h    : print the command usage\n");
-    fprintf( pErr, "\tfile1 : (optional) the file with the first network\n");
-    fprintf( pErr, "\tfile2 : (optional) the file with the second network\n");
-    fprintf( pErr, "\t        if no files are given, uses the current network and its spec\n");
-    fprintf( pErr, "\t        if one file is given, uses the current network and the file\n");
+    fprintf( pErr, "usage: cec [-T num] [-svh] <file1> <file2>\n" );
+    fprintf( pErr, "\t         performs combinational equivalence checking\n" );
+    fprintf( pErr, "\t-T num : approximate runtime limit in seconds [default = %d]\n", nSeconds );
+    fprintf( pErr, "\t-s     : toggle \"SAT only\" and \"FRAIG + SAT\" [default = %s]\n", fSat? "SAT only": "FRAIG + SAT" );
+    fprintf( pErr, "\t-v     : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    fprintf( pErr, "\tfile1  : (optional) the file with the first network\n");
+    fprintf( pErr, "\tfile2  : (optional) the file with the second network\n");
+    fprintf( pErr, "\t         if no files are given, uses the current network and its spec\n");
+    fprintf( pErr, "\t         if one file is given, uses the current network and the file\n");
     return 1;
 }
 
@@ -3989,10 +4033,12 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
     int nArgcNew;
     int c;
     int fSat;
+    int fVerbose;
     int nFrames;
+    int nSeconds;
 
-    extern void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames );
-    extern void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames );
+    extern void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFrames );
+    extern void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFrames, int fVerbose );
 
 
     pNtk = Abc_FrameReadNet(pAbc);
@@ -4000,10 +4046,12 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    nFrames = 3;
-    fSat    = 0;
+    fSat     =  0;
+    fVerbose =  0;
+    nFrames  =  3;
+    nSeconds = 20;
     util_getopt_reset();
-    while ( ( c = util_getopt( argc, argv, "Fsh" ) ) != EOF )
+    while ( ( c = util_getopt( argc, argv, "FTsvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -4018,6 +4066,20 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nFrames < 0 ) 
                 goto usage;
             break;
+        case 'T':
+            if ( util_optind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-T\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nSeconds = atoi(argv[util_optind]);
+            util_optind++;
+            if ( nSeconds < 0 ) 
+                goto usage;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
         case 's':
             fSat ^= 1;
             break;
@@ -4033,20 +4095,22 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // perform equivalence checking
     if ( fSat )
-        Abc_NtkSecSat( pNtk1, pNtk2, nFrames );
+        Abc_NtkSecSat( pNtk1, pNtk2, nSeconds, nFrames );
     else
-        Abc_NtkSecFraig( pNtk1, pNtk2, nFrames );
+        Abc_NtkSecFraig( pNtk1, pNtk2, nSeconds, nFrames, fVerbose );
 
     if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
     if ( fDelete2 ) Abc_NtkDelete( pNtk2 );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: sec [-sh] [-F num] <file1> <file2>\n" );
+    fprintf( pErr, "usage: sec [-F num] [-T num] [-svh] <file1> <file2>\n" );
     fprintf( pErr, "\t         performs bounded sequential equivalence checking\n" );
     fprintf( pErr, "\t-s     : toggle \"SAT only\" and \"FRAIG + SAT\" [default = %s]\n", fSat? "SAT only": "FRAIG + SAT" );
+    fprintf( pErr, "\t-v     : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     fprintf( pErr, "\t-F num : the number of time frames to use [default = %d]\n", nFrames );
+    fprintf( pErr, "\t-T num : approximate runtime limit in seconds [default = %d]\n", nSeconds );
     fprintf( pErr, "\tfile1  : (optional) the file with the first network\n");
     fprintf( pErr, "\tfile2  : (optional) the file with the second network\n");
     fprintf( pErr, "\t         if no files are given, uses the current network and its spec\n");
diff --git a/src/base/abci/abcBalance.c b/src/base/abci/abcBalance.c
index 40701e41..5e0f81a1 100644
--- a/src/base/abci/abcBalance.c
+++ b/src/base/abci/abcBalance.c
@@ -25,8 +25,8 @@
 ////////////////////////////////////////////////////////////////////////
  
 static void        Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplicate );
-static Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, Vec_Vec_t * vStorage, bool fDuplicate );
-static Vec_Ptr_t * Abc_NodeBalanceCone( Abc_Obj_t * pNode, Vec_Vec_t * vSuper, int fDuplicate );
+static Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, Vec_Vec_t * vStorage, int Level, bool fDuplicate );
+static Vec_Ptr_t * Abc_NodeBalanceCone( Abc_Obj_t * pNode, Vec_Vec_t * vSuper, int Level, int fDuplicate );
 static int         Abc_NodeBalanceCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, bool fFirst, bool fDuplicate );
 
 ////////////////////////////////////////////////////////////////////////
@@ -86,7 +86,7 @@ void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplica
     // set the level of PIs of AIG according to the arrival times of the old network
     Abc_NtkSetNodeLevelsArrival( pNtk );
     // allocate temporary storage for supergates
-    vStorage = Vec_VecStart( Abc_AigGetLevelNum(pNtk) + 1 );
+    vStorage = Vec_VecStart( 10 );
     // perform balancing of POs
     pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
     Abc_NtkForEachCo( pNtk, pNode, i )
@@ -94,7 +94,7 @@ void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplica
         Extra_ProgressBarUpdate( pProgress, i, NULL );
         // strash the driver node
         pDriver = Abc_ObjFanin0(pNode);
-        Abc_NodeBalance_rec( pNtkAig, pDriver, vStorage, fDuplicate );
+        Abc_NodeBalance_rec( pNtkAig, pDriver, vStorage, 0, fDuplicate );
     }
     Extra_ProgressBarStop( pProgress );
     Vec_VecFree( vStorage );
@@ -111,7 +111,7 @@ void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplica
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_Vec_t * vStorage, bool fDuplicate )
+Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_Vec_t * vStorage, int Level, bool fDuplicate )
 {
     Abc_Aig_t * pMan = pNtkNew->pManFunc;
     Abc_Obj_t * pNodeNew, * pNode1, * pNode2;
@@ -123,7 +123,7 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_
         return pNodeOld->pCopy;
     assert( Abc_ObjIsNode(pNodeOld) );
     // get the implication supergate
-    vSuper = Abc_NodeBalanceCone( pNodeOld, vStorage, fDuplicate );
+    vSuper = Abc_NodeBalanceCone( pNodeOld, vStorage, Level, fDuplicate );
     if ( vSuper->nSize == 0 )
     { // it means that the supergate contains two nodes in the opposite polarity
         pNodeOld->pCopy = Abc_ObjNot(Abc_AigConst1(pMan));
@@ -132,9 +132,11 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_
     // for each old node, derive the new well-balanced node
     for ( i = 0; i < vSuper->nSize; i++ )
     {
-        pNodeNew = Abc_NodeBalance_rec( pNtkNew, Abc_ObjRegular(vSuper->pArray[i]), vStorage, fDuplicate );
+        pNodeNew = Abc_NodeBalance_rec( pNtkNew, Abc_ObjRegular(vSuper->pArray[i]), vStorage, Level + 1, fDuplicate );
         vSuper->pArray[i] = Abc_ObjNotCond( pNodeNew, Abc_ObjIsComplement(vSuper->pArray[i]) );
     }
+    if ( vSuper->nSize < 2 )
+        printf( "BUG!\n" );
     // sort the new nodes by level in the decreasing order
     Vec_PtrSort( vSuper, Abc_NodeCompareLevelsDecrease );
     // balance the nodes
@@ -149,6 +151,7 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_
     assert( pNodeOld->pCopy == NULL );
     // mark the old node with the new node
     pNodeOld->pCopy = vSuper->pArray[0];
+    vSuper->nSize = 0;
     return pNodeOld->pCopy;
 }
 
@@ -165,17 +168,25 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Abc_NodeBalanceCone( Abc_Obj_t * pNode, Vec_Vec_t * vStorage, int fDuplicate )
+Vec_Ptr_t * Abc_NodeBalanceCone( Abc_Obj_t * pNode, Vec_Vec_t * vStorage, int Level, int fDuplicate )
 {
     Vec_Ptr_t * vNodes;
     int RetValue, i;
     assert( !Abc_ObjIsComplement(pNode) );
-    vNodes = Vec_VecEntry( vStorage, pNode->Level );
+    // extend the storage
+    if ( Vec_VecSize( vStorage ) <= Level )
+        Vec_VecPush( vStorage, Level, 0 );
+    // get the temporary array of nodes
+    vNodes = Vec_VecEntry( vStorage, Level );
     Vec_PtrClear( vNodes );
+    // collect the nodes in the implication supergate
     RetValue = Abc_NodeBalanceCone_rec( pNode, vNodes, 1, fDuplicate );
-    assert( vNodes->nSize > 0 );
+    assert( vNodes->nSize > 1 );
+    // unmark the visited nodes
     for ( i = 0; i < vNodes->nSize; i++ )
         Abc_ObjRegular((Abc_Obj_t *)vNodes->pArray[i])->fMarkB = 0;
+    // if we found the node and its complement in the same implication supergate, 
+    // return empty set of nodes (meaning that we should use constant-0 node)
     if ( RetValue == -1 )
         vNodes->nSize = 0;
     return vNodes;
diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c
index e82065fc..3f860585 100644
--- a/src/base/abci/abcFraig.c
+++ b/src/base/abci/abcFraig.c
@@ -26,7 +26,6 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-extern Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fAllNodes );
 static Abc_Ntk_t *   Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );
 static Abc_Obj_t *   Abc_NodeFromFraig_rec( Abc_Ntk_t * pNtkNew, Fraig_Node_t * pNodeFraig );
 
@@ -83,13 +82,14 @@ Abc_Ntk_t * Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes )
   SeeAlso     []
 
 ***********************************************************************/
-Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fAllNodes )
+void * Abc_NtkToFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes )
 {
     Fraig_Man_t * pMan;
     ProgressBar * pProgress;
     Fraig_Node_t * pNodeFraig;
     Vec_Ptr_t * vNodes;
     Abc_Obj_t * pNode, * pConst1, * pReset;
+    int fInternal = ((Fraig_Params_t *)pParams)->fInternal;
     int i;
 
     assert( Abc_NtkIsStrash(pNtk) );
@@ -106,11 +106,11 @@ Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fA
 
     // perform strashing
     vNodes = Abc_AigDfs( pNtk, fAllNodes, 0 );
-    if ( !pParams->fInternal )
+    if ( !fInternal )
         pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
     Vec_PtrForEachEntry( vNodes, pNode, i )
     {
-        if ( !pParams->fInternal )
+        if ( !fInternal )
             Extra_ProgressBarUpdate( pProgress, i, NULL );
         if ( pNode == pConst1 )
             pNodeFraig = Fraig_ManReadConst1(pMan);
@@ -123,7 +123,7 @@ Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fA
         assert( pNode->pCopy == NULL );
         pNode->pCopy = (Abc_Obj_t *)pNodeFraig;
     }
-    if ( !pParams->fInternal )
+    if ( !fInternal )
         Extra_ProgressBarStop( pProgress );
     Vec_PtrFree( vNodes );
 
diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c
index 68dccd18..b6755a04 100644
--- a/src/base/abci/abcMiter.c
+++ b/src/base/abci/abcMiter.c
@@ -372,8 +372,8 @@ Abc_Ntk_t * Abc_NtkMiterForCofactors( Abc_Ntk_t * pNtk, int Out, int In1, int In
 
   Synopsis    [Checks the status of the miter.]
 
-  Description [Return 1 if the miter is sat for at least one output.
-  Return 0 if the miter is unsat for all its outputs. Returns -1 if the
+  Description [Return 0 if the miter is sat for at least one output.
+  Return 1 if the miter is unsat for all its outputs. Returns -1 if the
   miter is undecided for some outputs.]
                
   SideEffects []
@@ -396,15 +396,15 @@ int Abc_NtkMiterIsConstant( Abc_Ntk_t * pMiter )
             {
                 // if the miter is constant 1, return immediately
                 printf( "MITER IS CONSTANT 1!\n" );
-                return 1;
+                return 0;
             }
         }
         // if the miter is undecided (or satisfiable), return immediately
         else 
             return -1;
     }
-    // return 0, meaning all outputs are constant zero
-    return 0;
+    // return 1, meaning all outputs are constant zero
+    return 1;
 }
 
 /**Function*************************************************************
diff --git a/src/base/abci/abcRefactor.c b/src/base/abci/abcRefactor.c
index 92d497fc..3d9534c8 100644
--- a/src/base/abci/abcRefactor.c
+++ b/src/base/abci/abcRefactor.c
@@ -58,7 +58,7 @@ struct Abc_ManRef_t_
 static void           Abc_NtkManRefPrintStats( Abc_ManRef_t * p );
 static Abc_ManRef_t * Abc_NtkManRefStart( int nNodeSizeMax, int nConeSizeMax, bool fUseDcs, bool fVerbose );
 static void           Abc_NtkManRefStop( Abc_ManRef_t * p );
-static Dec_Graph_t *  Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, bool fUseZeros, bool fUseDcs, bool fVerbose );
+static Dec_Graph_t *  Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, bool fUpdateLevel, bool fUseZeros, bool fUseDcs, bool fVerbose );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
@@ -80,7 +80,7 @@ static Dec_Graph_t *  Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool fUseZeros, bool fUseDcs, bool fVerbose )
+int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool fUpdateLevel, bool fUseZeros, bool fUseDcs, bool fVerbose )
 {
     ProgressBar * pProgress;
     Abc_ManRef_t * pManRef;
@@ -98,7 +98,9 @@ int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool
     pManCut = Abc_NtkManCutStart( nNodeSizeMax, nConeSizeMax, 2, 1000 );
     pManRef = Abc_NtkManRefStart( nNodeSizeMax, nConeSizeMax, fUseDcs, fVerbose );
     pManRef->vLeaves   = Abc_NtkManCutReadCutLarge( pManCut );
-    Abc_NtkStartReverseLevels( pNtk );
+    // compute the reverse levels if level update is requested
+    if ( fUpdateLevel )
+        Abc_NtkStartReverseLevels( pNtk );
 
     // resynthesize each node once
     nNodes = Abc_NtkObjNumMax(pNtk);
@@ -121,13 +123,13 @@ clk = clock();
 pManRef->timeCut += clock() - clk;
         // evaluate this cut
 clk = clock();
-        pFForm = Abc_NodeRefactor( pManRef, pNode, vFanins, fUseZeros, fUseDcs, fVerbose );
+        pFForm = Abc_NodeRefactor( pManRef, pNode, vFanins, fUpdateLevel, fUseZeros, fUseDcs, fVerbose );
 pManRef->timeRes += clock() - clk;
         if ( pFForm == NULL )
             continue;
         // acceptable replacement found, update the graph
 clk = clock();
-        Dec_GraphUpdateNetwork( pNode, pFForm, pManRef->nLastGain );
+        Dec_GraphUpdateNetwork( pNode, pFForm, fUpdateLevel, pManRef->nLastGain );
 pManRef->timeNtk += clock() - clk;
         Dec_GraphFree( pFForm );
     }
@@ -140,7 +142,13 @@ pManRef->timeTotal = clock() - clkStart;
     // delete the managers
     Abc_NtkManCutStop( pManCut );
     Abc_NtkManRefStop( pManRef );
-    Abc_NtkStopReverseLevels( pNtk );
+    // put the nodes into the DFS order and reassign their IDs
+    Abc_NtkReassignIds( pNtk );
+    // fix the levels
+    if ( fUpdateLevel )
+        Abc_NtkStopReverseLevels( pNtk );
+    else
+        Abc_NtkGetLevelNum( pNtk );
     // check
     if ( !Abc_NtkCheck( pNtk ) )
     {
@@ -161,7 +169,7 @@ pManRef->timeTotal = clock() - clkStart;
   SeeAlso     []
 
 ***********************************************************************/
-Dec_Graph_t * Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, bool fUseZeros, bool fUseDcs, bool fVerbose )
+Dec_Graph_t * Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, bool fUpdateLevel, bool fUseZeros, bool fUseDcs, bool fVerbose )
 {
     int fVeryVerbose = 0;
     Abc_Obj_t * pFanin;
@@ -169,6 +177,9 @@ Dec_Graph_t * Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec_Ptr_t *
     DdNode * bNodeFunc;
     int nNodesSaved, nNodesAdded, i, clk;
     char * pSop;
+    int Required;
+
+    Required = fUpdateLevel? Abc_NodeReadRequiredLevel(pNode) : ABC_INFINITY;
 
     p->nNodesConsidered++;
 
@@ -239,7 +250,7 @@ p->timeFact += clock() - clk;
 
     // detect how many new nodes will be added (while taking into account reused nodes)
 clk = clock();
-    nNodesAdded = Dec_GraphToNetworkCount( pNode, pFForm, nNodesSaved, Abc_NodeReadRequiredLevel(pNode) );
+    nNodesAdded = Dec_GraphToNetworkCount( pNode, pFForm, nNodesSaved, Required );
 p->timeEval += clock() - clk;
     // quit if there is no improvement
     if ( nNodesAdded == -1 || nNodesAdded == nNodesSaved && !fUseZeros )
diff --git a/src/base/abci/abcRenode.c b/src/base/abci/abcRenode.c
index 165777f8..ad91134e 100644
--- a/src/base/abci/abcRenode.c
+++ b/src/base/abci/abcRenode.c
@@ -486,7 +486,7 @@ void Abc_NtkRenodeSetBoundsCnf( Abc_Ntk_t * pNtk )
             Abc_ObjFanin1(pNode)->fMarkA == 0 )
             nMuxes++;
     }
-    printf( "The number of MUXes detected = %d (%5.2f %% of logic).\n", nMuxes, 300.0*nMuxes/Abc_NtkNodeNum(pNtk) );
+//    printf( "The number of MUXes detected = %d (%5.2f %% of logic).\n", nMuxes, 300.0*nMuxes/Abc_NtkNodeNum(pNtk) );
 } 
  
 /**Function*************************************************************
diff --git a/src/base/abci/abcRewrite.c b/src/base/abci/abcRewrite.c
index ea221296..81d97028 100644
--- a/src/base/abci/abcRewrite.c
+++ b/src/base/abci/abcRewrite.c
@@ -50,7 +50,7 @@ static void        Abc_NodePrintCuts( Abc_Obj_t * pNode );
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUseZeros, int fVerbose )
+int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerbose )
 {
     int fDrop = 0;
     ProgressBar * pProgress;
@@ -67,7 +67,9 @@ int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUseZeros, int fVerbose )
     pManRwr = Rwr_ManStart( 0 );
     if ( pManRwr == NULL )
         return 0;
-    Abc_NtkStartReverseLevels( pNtk );
+    // compute the reverse levels if level update is requested
+    if ( fUpdateLevel )
+        Abc_NtkStartReverseLevels( pNtk );
     // start the cut manager
 clk = clock();
     pManCut = Abc_NtkStartCutManForRewrite( pNtk, fDrop );
@@ -90,14 +92,16 @@ Rwr_ManAddTimeCuts( pManRwr, clock() - clk );
         if ( Abc_ObjFanoutNum(pNode) > 1000 )
             continue;
         // for each cut, try to resynthesize it
-        nGain = Rwr_NodeRewrite( pManRwr, pManCut, pNode, fUseZeros );
+        nGain = Rwr_NodeRewrite( pManRwr, pManCut, pNode, fUpdateLevel, fUseZeros );
         if ( nGain > 0 || nGain == 0 && fUseZeros )
         {
             Dec_Graph_t * pGraph = Rwr_ManReadDecs(pManRwr);
             int fCompl           = Rwr_ManReadCompl(pManRwr);
             // complement the FF if needed
             if ( fCompl ) Dec_GraphComplement( pGraph );
-            Dec_GraphUpdateNetwork( pNode, pGraph, nGain );
+clk = clock();
+            Dec_GraphUpdateNetwork( pNode, pGraph, fUpdateLevel, nGain );
+Rwr_ManAddTimeUpdate( pManRwr, clock() - clk );
             if ( fCompl ) Dec_GraphComplement( pGraph );
         }
     }
@@ -110,7 +114,13 @@ Rwr_ManAddTimeTotal( pManRwr, clock() - clkStart );
     Rwr_ManStop( pManRwr );
     Cut_ManStop( pManCut );
     pNtk->pManCut = NULL;
-    Abc_NtkStopReverseLevels( pNtk );
+    // put the nodes into the DFS order and reassign their IDs
+    Abc_NtkReassignIds( pNtk );
+    // fix the levels
+    if ( fUpdateLevel )
+        Abc_NtkStopReverseLevels( pNtk );
+    else
+        Abc_NtkGetLevelNum( pNtk );
     // check
     if ( !Abc_NtkCheck( pNtk ) )
     {
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index 4fb059e5..b335086f 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -35,18 +35,18 @@ static void Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t *
 
   Synopsis    [Attempts to solve the miter using an internal SAT solver.]
 
-  Description [Returns 1 if the miter is SAT.]
+  Description [Returns -1 if timed out; 0 if SAT; 1 if UNSAT.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-bool Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int fVerbose )
+int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose )
 {
     solver * pSat;
     lbool   status;
-    int clk;
+    int RetValue, clk;
 
     assert( Abc_NtkIsBddLogic(pNtk) );
     assert( Abc_NtkLatchNum(pNtk) == 0 );
@@ -57,20 +57,18 @@ bool Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int fVerbose )
     // load clauses into the solver
     clk = clock();
     pSat = Abc_NtkMiterSatCreate( pNtk );
-//    printf( "Created SAT problem with %d variable and %d clauses.   ", 
-//        solver_nvars(pSat), solver_nclauses(pSat) );
+//    printf( "Created SAT problem with %d variable and %d clauses. ", solver_nvars(pSat), solver_nclauses(pSat) );
 //    PRT( "Time", clock() - clk );
 
     // simplify the problem
     clk = clock();
     status = solver_simplify(pSat);
-//    printf( "Simplified the problem to %d variables and %d clauses. ", 
-//        solver_nvars(pSat), solver_nclauses(pSat) );
+//    printf( "Simplified the problem to %d variables and %d clauses. ", solver_nvars(pSat), solver_nclauses(pSat) );
 //    PRT( "Time", clock() - clk );
     if ( status == l_False )
     {
         solver_delete( pSat );
-        printf( "The problem is UNSAT after simplification.\n" );
+        printf( "The problem is UNSATISFIABLE after simplification.\n" );
         return 0;
     }
 
@@ -78,17 +76,38 @@ bool Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int fVerbose )
     clk = clock();
     if ( fVerbose )
         pSat->verbosity = 1;
-    status = solver_solve( pSat, NULL, NULL );
-//    if ( fVerbose )
-//    {
-    printf( "The problem is %5s. ", (status == l_True)? "SAT" : "UNSAT" );
-    PRT( "SAT solver time", clock() - clk );
-//    }
+    status = solver_solve( pSat, NULL, NULL, nSeconds );
+    if ( status == l_Undef )
+    {
+//        printf( "The problem timed out.\n" );
+        RetValue = -1;
+    }
+    else if ( status == l_True )
+    {
+//        printf( "The problem is SATISFIABLE.\n" );
+        RetValue = 0;
+    }
+    else if ( status == l_False )
+    {
+//        printf( "The problem is UNSATISFIABLE.\n" );
+        RetValue = 1;
+    }
+    else
+        assert( 0 );
+//    PRT( "SAT solver time", clock() - clk );
+
+    // if the problem is SAT, get the counterexample
+    if ( status == l_True )
+    {
+        Vec_Int_t * vCiIds = Abc_NtkGetCiIds( pNtk );
+        pNtk->pModel = solver_get_model( pSat, vCiIds->pArray, vCiIds->nSize );
+        Vec_IntFree( vCiIds );
+    }
     // free the solver
     solver_delete( pSat );
-    return status == l_True;
+    return RetValue;
 }
-
+ 
 /**Function*************************************************************
 
   Synopsis    [Sets up the SAT solver.]
diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c
index 7000ecad..fa840937 100644
--- a/src/base/abci/abcSweep.c
+++ b/src/base/abci/abcSweep.c
@@ -25,8 +25,6 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-extern Fraig_Man_t *  Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fAllNodes );
-
 static stmm_table *   Abc_NtkFraigEquiv( Fraig_Man_t * p, Abc_Ntk_t * pNtk, int fUseInv, bool fVerbose );
 static void           Abc_NtkFraigTransform( Abc_Ntk_t * pNtk, stmm_table * tEquiv, int fUseInv, bool fVerbose );
 static void           Abc_NtkFraigMergeClassMapped( Abc_Ntk_t * pNtk, Abc_Obj_t * pChain, int fVerbose, int fUseInv );
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index 55d6cf7d..2d5493ea 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -25,6 +25,10 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
  
+static int * Abc_NtkVerifyGetCleanModel( Abc_Ntk_t * pNtk );
+static int * Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel );
+static void  Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
@@ -40,7 +44,7 @@
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
+void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds )
 {
     Abc_Ntk_t * pMiter;
     Abc_Ntk_t * pCnf;
@@ -54,13 +58,17 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
         return;
     }
     RetValue = Abc_NtkMiterIsConstant( pMiter );
-    if ( RetValue == 1 )
+    if ( RetValue == 0 )
     {
         Abc_NtkDelete( pMiter );
         printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
+        // report the error
+        pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter );
+        Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel );
+        FREE( pMiter->pModel );
         return;
     }
-    if ( RetValue == 0 )
+    if ( RetValue == 1 )
     {
         Abc_NtkDelete( pMiter );
         printf( "Networks are equivalent after structural hashing.\n" );
@@ -77,10 +85,16 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
     }
 
     // solve the CNF using the SAT solver
-    if ( Abc_NtkMiterSat( pCnf, 0 ) )
+    RetValue = Abc_NtkMiterSat( pCnf, nSeconds, 0 );
+    if ( RetValue == -1 )
+        printf( "Networks are undecided (SAT solver timed out).\n" );
+    else if ( RetValue == 0 )
         printf( "Networks are NOT EQUIVALENT after SAT.\n" );
     else
         printf( "Networks are equivalent after SAT.\n" );
+    if ( pCnf->pModel )
+        Abc_NtkVerifyReportError( pNtk1, pNtk2, pCnf->pModel );
+    FREE( pCnf->pModel );
     Abc_NtkDelete( pCnf );
 }
 
@@ -96,11 +110,11 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fVerbose )
+void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fVerbose )
 {
     Fraig_Params_t Params;
+    Fraig_Man_t * pMan;
     Abc_Ntk_t * pMiter;
-    Abc_Ntk_t * pFraig;
     int RetValue;
 
     // get the miter of the two networks
@@ -111,13 +125,17 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fVerbose )
         return;
     }
     RetValue = Abc_NtkMiterIsConstant( pMiter );
-    if ( RetValue == 1 )
+    if ( RetValue == 0 )
     {
         Abc_NtkDelete( pMiter );
         printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
+        // report the error
+        pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter );
+        Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel );
+        FREE( pMiter->pModel );
         return;
     }
-    if ( RetValue == 0 )
+    if ( RetValue == 1 )
     {
         Abc_NtkDelete( pMiter );
         printf( "Networks are equivalent after structural hashing.\n" );
@@ -127,21 +145,27 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fVerbose )
     // convert the miter into a FRAIG
     Fraig_ParamsSetDefault( &Params );
     Params.fVerbose = fVerbose;
-    pFraig = Abc_NtkFraig( pMiter, &Params, 0 );
-    Abc_NtkDelete( pMiter );
-    if ( pFraig == NULL )
-    {
-        printf( "Fraiging has failed.\n" );
-        return;
-    }
-    RetValue = Abc_NtkMiterIsConstant( pFraig );
-    Abc_NtkDelete( pFraig );
-    if ( RetValue == 0 )
-    {
+    Params.nSeconds = nSeconds;
+    pMan = Abc_NtkToFraig( pMiter, &Params, 0 ); 
+    Fraig_ManProveMiter( pMan );
+
+    // analyze the result
+    RetValue = Fraig_ManCheckMiter( pMan );
+    // report the result
+    if ( RetValue == -1 )
+        printf( "Networks are undecided (SAT solver timed out on the final miter).\n" );
+    else if ( RetValue == 1 )
         printf( "Networks are equivalent after fraiging.\n" );
-        return;
+    else if ( RetValue == 0 )
+    {
+        printf( "Networks are NOT EQUIVALENT after fraiging.\n" );
+        Abc_NtkVerifyReportError( pNtk1, pNtk2, Fraig_ManReadModel(pMan) );
     }
-    printf( "Networks are NOT EQUIVALENT after fraiging.\n" );
+    else assert( 0 );
+    // delete the fraig manager
+    Fraig_ManFree( pMan );
+    // delete the miter
+    Abc_NtkDelete( pMiter );
 }
 
 /**Function*************************************************************
@@ -155,7 +179,7 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames )
+void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFrames )
 {
     Abc_Ntk_t * pMiter;
     Abc_Ntk_t * pFrames;
@@ -170,13 +194,13 @@ void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames )
         return;
     }
     RetValue = Abc_NtkMiterIsConstant( pMiter );
-    if ( RetValue == 1 )
+    if ( RetValue == 0 )
     {
         Abc_NtkDelete( pMiter );
         printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
         return;
     }
-    if ( RetValue == 0 )
+    if ( RetValue == 1 )
     {
         Abc_NtkDelete( pMiter );
         printf( "Networks are equivalent after structural hashing.\n" );
@@ -192,13 +216,13 @@ void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames )
         return;
     }
     RetValue = Abc_NtkMiterIsConstant( pFrames );
-    if ( RetValue == 1 )
+    if ( RetValue == 0 )
     {
         Abc_NtkDelete( pFrames );
         printf( "Networks are NOT EQUIVALENT after framing.\n" );
         return;
     }
-    if ( RetValue == 0 )
+    if ( RetValue == 1 )
     {
         Abc_NtkDelete( pFrames );
         printf( "Networks are equivalent after framing.\n" );
@@ -215,7 +239,10 @@ void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames )
     }
 
     // solve the CNF using the SAT solver
-    if ( Abc_NtkMiterSat( pCnf, 0 ) )
+    RetValue = Abc_NtkMiterSat( pCnf, nSeconds, 0 );
+    if ( RetValue == -1 )
+        printf( "Networks are undecided (SAT solver timed out).\n" );
+    else if ( RetValue == 0 )
         printf( "Networks are NOT EQUIVALENT after SAT.\n" );
     else
         printf( "Networks are equivalent after SAT.\n" );
@@ -233,11 +260,11 @@ void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames )
+void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFrames, int fVerbose )
 {
     Fraig_Params_t Params;
+    Fraig_Man_t * pMan;
     Abc_Ntk_t * pMiter;
-    Abc_Ntk_t * pFraig;
     Abc_Ntk_t * pFrames;
     int RetValue;
 
@@ -249,13 +276,13 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames )
         return;
     }
     RetValue = Abc_NtkMiterIsConstant( pMiter );
-    if ( RetValue == 1 )
+    if ( RetValue == 0 )
     {
         Abc_NtkDelete( pMiter );
         printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
         return;
     }
-    if ( RetValue == 0 )
+    if ( RetValue == 1 )
     {
         Abc_NtkDelete( pMiter );
         printf( "Networks are equivalent after structural hashing.\n" );
@@ -271,13 +298,13 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames )
         return;
     }
     RetValue = Abc_NtkMiterIsConstant( pFrames );
-    if ( RetValue == 1 )
+    if ( RetValue == 0 )
     {
         Abc_NtkDelete( pFrames );
         printf( "Networks are NOT EQUIVALENT after framing.\n" );
         return;
     }
-    if ( RetValue == 0 )
+    if ( RetValue == 1 )
     {
         Abc_NtkDelete( pFrames );
         printf( "Networks are equivalent after framing.\n" );
@@ -286,23 +313,164 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames )
 
     // convert the miter into a FRAIG
     Fraig_ParamsSetDefault( &Params );
-    pFraig = Abc_NtkFraig( pFrames, &Params, 0 );
-    Abc_NtkDelete( pFrames );
-    if ( pFraig == NULL )
+    Params.fVerbose = fVerbose;
+    Params.nSeconds = nSeconds;
+    pMan = Abc_NtkToFraig( pFrames, &Params, 0 ); 
+    Fraig_ManProveMiter( pMan );
+
+    // analyze the result
+    RetValue = Fraig_ManCheckMiter( pMan );
+    // report the result
+    if ( RetValue == -1 )
+        printf( "Networks are undecided (SAT solver timed out on the final miter).\n" );
+    else if ( RetValue == 1 )
+        printf( "Networks are equivalent after fraiging.\n" );
+    else if ( RetValue == 0 )
     {
-        printf( "Fraiging has failed.\n" );
-        return;
+        printf( "Networks are NOT EQUIVALENT after fraiging.\n" );
+//        Abc_NtkVerifyReportError( pNtk1, pNtk2, Fraig_ManReadModel(pMan) );
     }
-    RetValue = Abc_NtkMiterIsConstant( pFraig );
-    Abc_NtkDelete( pFraig );
-    if ( RetValue == 0 )
+    else assert( 0 );
+    // delete the fraig manager
+    Fraig_ManFree( pMan );
+    // delete the miter
+    Abc_NtkDelete( pFrames );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reports mismatch between the two networks.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel )
+{
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pNode;
+    int * pValues1, * pValues2;
+    int nMisses, nPrinted, i, iNode = -1;
+
+    assert( Abc_NtkCiNum(pNtk1) == Abc_NtkCiNum(pNtk2) );
+    assert( Abc_NtkCoNum(pNtk1) == Abc_NtkCoNum(pNtk2) );
+    // get the CO values under this model
+    pValues1 = Abc_NtkVerifySimulatePattern( pNtk1, pModel );
+    pValues2 = Abc_NtkVerifySimulatePattern( pNtk2, pModel );
+    // count the mismatches
+    nMisses = 0;
+    for ( i = 0; i < Abc_NtkCoNum(pNtk1); i++ )
+        nMisses += (int)( pValues1[i] != pValues2[i] );
+    printf( "Verification failed for %d outputs: ", nMisses );
+    // print the first 3 outputs
+    nPrinted = 0;
+    for ( i = 0; i < Abc_NtkCoNum(pNtk1); i++ )
+        if ( pValues1[i] != pValues2[i] )
+        {
+            if ( iNode == -1 )
+                iNode = i;
+            printf( " %s", Abc_ObjName(Abc_NtkCo(pNtk1,i)) );
+            if ( ++nPrinted == 3 )
+                break;
+        }
+    if ( nPrinted != nMisses )
+        printf( " ..." );
+    printf( "\n" );
+    // report mismatch for the first output
+    if ( iNode >= 0 )
     {
-        printf( "Networks are equivalent after fraiging.\n" );
-        return;
+        printf( "Output %s: Value in Network1 = %d. Value in Network2 = %d.\n", 
+            Abc_ObjName(Abc_NtkCo(pNtk1,iNode)), pValues1[iNode], pValues2[iNode] );
+        printf( "Input pattern: " );
+        // collect PIs in the cone
+        pNode = Abc_NtkCo(pNtk1,iNode);
+        vNodes = Abc_NtkNodeSupport( pNtk1, &pNode, 1 );
+        // set the PI numbers
+        Abc_NtkForEachCi( pNtk1, pNode, i )
+            pNode->pCopy = (void*)i;
+        // print the model
+        Vec_PtrForEachEntry( vNodes, pNode, i )
+        {
+            assert( Abc_ObjIsCi(pNode) );
+            printf( " %s=%d", Abc_ObjName(pNode), pModel[(int)pNode->pCopy] );
+        }
+        printf( "\n" );
+        Vec_PtrFree( vNodes );
     }
-    printf( "Networks are NOT EQUIVALENT after fraiging.\n" );
+    free( pValues1 );
+    free( pValues2 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns a dummy pattern full of zeros.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int * Abc_NtkVerifyGetCleanModel( Abc_Ntk_t * pNtk )
+{
+    int * pModel = ALLOC( int, Abc_NtkCiNum(pNtk) );
+    memset( pModel, 0, sizeof(int) * Abc_NtkCiNum(pNtk) );
+    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;
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///