Version abc70302

10 files changed, 703 insertions, 38 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index dc185302..fbe81f48 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -85,8 +85,8 @@ static int Abc_CommandReorder        ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandOrder          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandMuxes          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandExtSeqDcs      ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandOneOutput      ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandOneNode        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandCone      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandNode        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandShortNames     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandExdcFree       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandExdcGet        ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -113,6 +113,7 @@ static int Abc_CommandIProve         ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandHaig           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandMini           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandBmc            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandQbf            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandFraig          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandFraigTrust     ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -227,8 +228,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Various",      "order",         Abc_CommandOrder,            0 );
     Cmd_CommandAdd( pAbc, "Various",      "muxes",         Abc_CommandMuxes,            1 );
     Cmd_CommandAdd( pAbc, "Various",      "ext_seq_dcs",   Abc_CommandExtSeqDcs,        0 );
-    Cmd_CommandAdd( pAbc, "Various",      "cone",          Abc_CommandOneOutput,        1 );
-    Cmd_CommandAdd( pAbc, "Various",      "node",          Abc_CommandOneNode,          1 );
+    Cmd_CommandAdd( pAbc, "Various",      "cone",          Abc_CommandCone,        1 );
+    Cmd_CommandAdd( pAbc, "Various",      "node",          Abc_CommandNode,          1 );
     Cmd_CommandAdd( pAbc, "Various",      "short_names",   Abc_CommandShortNames,       0 );
     Cmd_CommandAdd( pAbc, "Various",      "exdc_free",     Abc_CommandExdcFree,         1 );
     Cmd_CommandAdd( pAbc, "Various",      "exdc_get",      Abc_CommandExdcGet,          1 );
@@ -255,6 +256,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "New AIG",      "haig",          Abc_CommandHaig,             1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "mini",          Abc_CommandMini,             1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "bmc",           Abc_CommandBmc,              0 );
+    Cmd_CommandAdd( pAbc, "New AIG",      "qbf",           Abc_CommandQbf,              0 );
 
     Cmd_CommandAdd( pAbc, "Fraiging",     "fraig",         Abc_CommandFraig,            1 );
     Cmd_CommandAdd( pAbc, "Fraiging",     "fraig_trust",   Abc_CommandFraigTrust,       1 );
@@ -3585,7 +3587,7 @@ int Abc_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
 
     // compute the miter
-    pNtkRes = Abc_NtkMiter( pNtk1, pNtk2, fComb );
+    pNtkRes = Abc_NtkMiter( pNtk1, pNtk2, fComb, 10 );
     if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
     if ( fDelete2 ) Abc_NtkDelete( pNtk2 );
 
@@ -4486,7 +4488,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_CommandOneOutput( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandCone( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
@@ -4615,7 +4617,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_CommandOneNode( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandNode( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
@@ -5284,10 +5286,12 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
     int nVars;
     int fAdder;
     int fSorter;
+    int fMesh;
     int fVerbose;
     char * FileName;
     extern void Abc_GenAdder( char * pFileName, int nVars );
     extern void Abc_GenSorter( char * pFileName, int nVars );
+    extern void Abc_GenMesh( char * pFileName, int nVars );
 
 
     pNtk = Abc_FrameReadNtk(pAbc);
@@ -5300,7 +5304,7 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
     fSorter = 0;
     fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Nasvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Nasmvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -5321,6 +5325,9 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 's':
             fSorter ^= 1;
             break;
+        case 'm':
+            fMesh ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -5342,16 +5349,19 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_GenAdder( FileName, nVars );
     else if ( fSorter )
         Abc_GenSorter( FileName, nVars );
+    else if ( fMesh )
+        Abc_GenMesh( FileName, nVars );
     else
         printf( "Type of circuit is not specified.\n" );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: gen [-N] [-asvh] <file>\n" );
+    fprintf( pErr, "usage: gen [-N] [-asmvh] <file>\n" );
     fprintf( pErr, "\t         generates simple circuits\n" );
     fprintf( pErr, "\t-N num : the number of variables [default = %d]\n", nVars );  
-    fprintf( pErr, "\t-a     : toggle ripple-carry adder [default = %s]\n", fAdder? "yes": "no" );  
-    fprintf( pErr, "\t-s     : toggle simple sorter [default = %s]\n", fSorter? "yes": "no" );  
+    fprintf( pErr, "\t-a     : generate ripple-carry adder [default = %s]\n", fAdder? "yes": "no" );  
+    fprintf( pErr, "\t-s     : generate a sorter [default = %s]\n", fSorter? "yes": "no" );  
+    fprintf( pErr, "\t-m     : generate a mesh [default = %s]\n", fMesh? "yes": "no" );  
     fprintf( pErr, "\t-v     : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );  
     fprintf( pErr, "\t-h     : print the command usage\n");
     fprintf( pErr, "\t<file> : output file name\n");
@@ -5730,8 +5740,8 @@ int Abc_CommandQuaVar( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
-    int c, iVar, fVerbose, RetValue;
-    extern int Abc_NtkQuantify( Abc_Ntk_t * pNtk, int iVar, int fVerbose );
+    int c, iVar, fUniv, fVerbose, RetValue;
+    extern int Abc_NtkQuantify( Abc_Ntk_t * pNtk, int fUniv, int iVar, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -5739,9 +5749,10 @@ int Abc_CommandQuaVar( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // set defaults
     iVar = 0;
+    fUniv = 0;
     fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Ivh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Iuvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -5756,6 +5767,9 @@ int Abc_CommandQuaVar( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( iVar < 0 ) 
                 goto usage;
             break;
+        case 'u':
+            fUniv ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -5778,7 +5792,7 @@ int Abc_CommandQuaVar( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // get the strashed network
     pNtkRes = Abc_NtkStrash( pNtk, 0, 1 );
-    RetValue = Abc_NtkQuantify( pNtkRes, iVar, fVerbose );
+    RetValue = Abc_NtkQuantify( pNtkRes, fUniv, iVar, fVerbose );
     // clean temporary storage for the cofactors
     Abc_NtkCleanData( pNtkRes );
     Abc_AigCleanup( pNtkRes->pManFunc );
@@ -5793,9 +5807,10 @@ int Abc_CommandQuaVar( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: qvar [-I num] [-vh]\n" );
+    fprintf( pErr, "usage: qvar [-I num] [-uvh]\n" );
     fprintf( pErr, "\t         quantifies one variable using the AIG\n" );
     fprintf( pErr, "\t-I num : the zero-based index of a variable to quantify [default = %d]\n", iVar );
+    fprintf( pErr, "\t-u     : toggle universal quantification [default = %s]\n", fUniv? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
@@ -6824,6 +6839,98 @@ usage:
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
 }
+ 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandQbf( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+    int nPars;
+    int fVerbose;
+
+    extern void Abc_NtkQbf( Abc_Ntk_t * pNtk, int nPars, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    nPars    = -1;
+    fVerbose =  1;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Pvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'P':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-P\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nPars = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nPars < 0 ) 
+                goto usage;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsComb(pNtk) )
+    {
+        fprintf( pErr, "Works only for combinational networks.\n" );
+        return 1;
+    }
+    if ( Abc_NtkPoNum(pNtk) != 1 )
+    {
+        fprintf( pErr, "The miter should have one primary output.\n" );
+        return 1;
+    }
+    if ( !(nPars > 0 && nPars < Abc_NtkPiNum(pNtk)) )
+    {
+        fprintf( pErr, "The number of paramter variables is invalid (should be > 0 and < PI num).\n" );
+        return 1;
+    }
+    if ( Abc_NtkIsStrash(pNtk) )
+        Abc_NtkQbf( pNtk, nPars, fVerbose );
+    else
+    {
+        pNtk = Abc_NtkStrash( pNtk, 0, 1 );
+        Abc_NtkQbf( pNtk, nPars, fVerbose );
+        Abc_NtkDelete( pNtk );
+    }
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: qbf [-P num] [-vh]\n" );
+    fprintf( pErr, "\t         solves a quantified boolean formula problem EpVxM(p,x)\n" );
+    fprintf( pErr, "\t-P num : number of paramters (should be the first PIs) [default = %d]\n", nPars );
+    fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
 
 
 /**Function*************************************************************
@@ -9447,6 +9554,7 @@ usage:
 ***********************************************************************/
 int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
+    char Buffer[16];
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtk1, * pNtk2;
     int fDelete1, fDelete2;
@@ -9456,11 +9564,13 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fSat;
     int fVerbose;
     int nSeconds;
+    int nPartSize;
     int nConfLimit;
     int nInsLimit;
 
     extern void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nInsLimit );
     extern void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fVerbose );
+    extern void Abc_NtkCecFraigPart( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nPartSize, int fVerbose );
 
 
     pNtk = Abc_FrameReadNtk(pAbc);
@@ -9471,10 +9581,11 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
     fSat     =  0;
     fVerbose =  0;
     nSeconds = 20;
+    nPartSize  = 0;
     nConfLimit = 10000;   
     nInsLimit  = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "TCIsvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "TCIPsvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -9511,6 +9622,17 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nInsLimit < 0 ) 
                 goto usage;
             break;
+        case 'P':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-P\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nPartSize = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nPartSize < 0 ) 
+                goto usage;
+            break;
         case 's':
             fSat ^= 1;
             break;
@@ -9528,7 +9650,9 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
 
     // perform equivalence checking
-    if ( fSat )
+    if ( nPartSize )
+        Abc_NtkCecFraigPart( pNtk1, pNtk2, nSeconds, nPartSize, fVerbose );
+    else if ( fSat )
         Abc_NtkCecSat( pNtk1, pNtk2, nConfLimit, nInsLimit );
     else
         Abc_NtkCecFraig( pNtk1, pNtk2, nSeconds, fVerbose );
@@ -9538,11 +9662,16 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: cec [-T num] [-C num] [-I num] [-svh] <file1> <file2>\n" );
+    if ( nPartSize == 0 )
+        strcpy( Buffer, "unused" );
+    else
+        sprintf( Buffer, "%d", nPartSize );
+    fprintf( pErr, "usage: cec [-T num] [-C num] [-I num] [-P 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-C num : limit on the number of conflicts [default = %d]\n",    nConfLimit );
     fprintf( pErr, "\t-I num : limit on the number of clause inspections [default = %d]\n", nInsLimit );
+    fprintf( pErr, "\t-P num : partition size for multi-output networks [default = %s]\n", Buffer );
     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");
diff --git a/src/base/abci/abcGen.c b/src/base/abci/abcGen.c
index 626e5e1e..5d74bda5 100644
--- a/src/base/abci/abcGen.c
+++ b/src/base/abci/abcGen.c
@@ -254,6 +254,112 @@ void Abc_WriteFullAdder( FILE * pFile )
     fprintf( pFile, "\n" ); 
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_WriteCell( FILE * pFile )
+{
+    fprintf( pFile, ".model cell\n" );
+    fprintf( pFile, ".inputs px1 px2 py1 py2 x y\n" ); 
+    fprintf( pFile, ".outputs fx fy\n" ); 
+    fprintf( pFile, ".names x y a\n" ); 
+    fprintf( pFile, "11 1\n" ); 
+    fprintf( pFile, ".names px1 a x nx\n" ); 
+    fprintf( pFile, "11- 1\n" ); 
+    fprintf( pFile, "0-1 1\n" ); 
+    fprintf( pFile, ".names py1 a y ny\n" ); 
+    fprintf( pFile, "11- 1\n" ); 
+    fprintf( pFile, "0-1 1\n" ); 
+    fprintf( pFile, ".names px2 nx fx\n" ); 
+    fprintf( pFile, "10 1\n" ); 
+    fprintf( pFile, "01 1\n" ); 
+    fprintf( pFile, ".names py2 ny fy\n" ); 
+    fprintf( pFile, "10 1\n" ); 
+    fprintf( pFile, "01 1\n" ); 
+    fprintf( pFile, ".end\n" ); 
+    fprintf( pFile, "\n" ); 
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_GenMesh( char * pFileName, int nVars )
+{
+    FILE * pFile;
+    int i, k;
+
+    assert( nVars > 0 );
+
+    pFile = fopen( pFileName, "w" );
+    fprintf( pFile, "# %dx%d mesh generated by ABC on %s\n", nVars, nVars, Extra_TimeStamp() );
+    fprintf( pFile, ".model mesh%d\n", nVars );
+
+    for ( i = 0; i < nVars; i++ )
+        for ( k = 0; k < nVars; k++ )
+        {
+            fprintf( pFile, ".inputs" );
+            fprintf( pFile, " p%d%dx1", i, k );
+            fprintf( pFile, " p%d%dx2", i, k );
+            fprintf( pFile, " p%d%dy1", i, k );
+            fprintf( pFile, " p%d%dy2", i, k );
+            fprintf( pFile, "\n" );
+        }
+    fprintf( pFile, ".inputs" );
+    for ( i = 0; i < nVars; i++ )
+        fprintf( pFile, " v%02d v%02d", 2*i, 2*i+1 );
+    fprintf( pFile, "\n" );
+
+    fprintf( pFile, ".outputs" );
+    fprintf( pFile, " fx00" );
+    fprintf( pFile, "\n" );
+
+    for ( i = 0; i < nVars; i++ ) // horizontal
+        for ( k = 0; k < nVars; k++ ) // vertical
+        {
+            fprintf( pFile, ".subckt cell" );
+            fprintf( pFile, " px1=p%d%dx1", i, k );
+            fprintf( pFile, " px2=p%d%dx2", i, k );
+            fprintf( pFile, " py1=p%d%dy1", i, k );
+            fprintf( pFile, " py2=p%d%dy2", i, k );
+            if ( k == nVars - 1 )
+                fprintf( pFile, " x=v%02d", i );
+            else
+                fprintf( pFile, " x=fx%d%d", i, k+1 );
+            if ( i == nVars - 1 )
+                fprintf( pFile, " y=v%02d", nVars+k );
+            else
+                fprintf( pFile, " y=fy%d%d", i+1, k );
+            // outputs
+            fprintf( pFile, " fx=fx%d%d", i, k );
+            fprintf( pFile, " fy=fy%d%d", i, k );
+            fprintf( pFile, "\n" );
+        }
+    fprintf( pFile, ".end\n" ); 
+    fprintf( pFile, "\n" );
+    fprintf( pFile, "\n" );
+
+    Abc_WriteCell( pFile );
+    fclose( pFile );
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c
index cbd330da..0088d72b 100644
--- a/src/base/abci/abcMiter.c
+++ b/src/base/abci/abcMiter.c
@@ -24,10 +24,10 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb );
+static Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int nPartSize );
 static void        Abc_NtkMiterPrepare( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb );
 static void        Abc_NtkMiterAddOne( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter );
-static void        Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb );
+static void        Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb, int nPartSize );
 static void        Abc_NtkAddFrame( Abc_Ntk_t * pNetNew, Abc_Ntk_t * pNet, int iFrame );
 
 // to be exported 
@@ -50,7 +50,7 @@ static void        Abc_NtkAddFrame2( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, i
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
+Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int nPartSize )
 {
     Abc_Ntk_t * pTemp = NULL;
     int fRemove1, fRemove2;
@@ -63,7 +63,7 @@ Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
     fRemove1 = (!Abc_NtkIsStrash(pNtk1)) && (pNtk1 = Abc_NtkStrash(pNtk1, 0, 0));
     fRemove2 = (!Abc_NtkIsStrash(pNtk2)) && (pNtk2 = Abc_NtkStrash(pNtk2, 0, 0));
     if ( pNtk1 && pNtk2 )
-        pTemp = Abc_NtkMiterInt( pNtk1, pNtk2, fComb );
+        pTemp = Abc_NtkMiterInt( pNtk1, pNtk2, fComb, nPartSize );
     if ( fRemove1 )  Abc_NtkDelete( pNtk1 );
     if ( fRemove2 )  Abc_NtkDelete( pNtk2 );
     return pTemp;
@@ -80,7 +80,7 @@ Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
+Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int nPartSize )
 {
     char Buffer[1000];
     Abc_Ntk_t * pNtkMiter;
@@ -97,7 +97,7 @@ Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
     Abc_NtkMiterPrepare( pNtk1, pNtk2, pNtkMiter, fComb );
     Abc_NtkMiterAddOne( pNtk1, pNtkMiter );
     Abc_NtkMiterAddOne( pNtk2, pNtkMiter );
-    Abc_NtkMiterFinalize( pNtk1, pNtk2, pNtkMiter, fComb );
+    Abc_NtkMiterFinalize( pNtk1, pNtk2, pNtkMiter, fComb, nPartSize );
 
     // make sure that everything is okay
     if ( !Abc_NtkCheck( pNtkMiter ) )
@@ -243,7 +243,7 @@ void Abc_NtkMiterAddCone( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter, Abc_Obj_t * p
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb )
+void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb, int nPartSize )
 {
     Vec_Ptr_t * vPairs;
     Abc_Obj_t * pMiter, * pNode;
@@ -276,9 +276,46 @@ void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNt
             Abc_ObjAddFanin( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjChild0Copy(Abc_ObjFanin0(pNode)) );
     }
     // add the miter
-    pMiter = Abc_AigMiter( pNtkMiter->pManFunc, vPairs );
-    Abc_ObjAddFanin( Abc_NtkPo(pNtkMiter,0), pMiter );
-    Vec_PtrFree( vPairs );
+    if ( nPartSize == 0 )
+    {
+        pMiter = Abc_AigMiter( pNtkMiter->pManFunc, vPairs );
+        Abc_ObjAddFanin( Abc_NtkPo(pNtkMiter,0), pMiter );
+        Vec_PtrFree( vPairs );
+    }
+    else
+    {
+        char Buffer[10];
+        Vec_Ptr_t * vPairsPart;
+        int nParts, i, k, iCur;
+        assert( Vec_PtrSize(vPairs) == 2 * Abc_NtkCoNum(pNtk1) );
+        // create partitions
+        nParts = Abc_NtkCoNum(pNtk1) / nPartSize + (int)((Abc_NtkCoNum(pNtk1) % nPartSize) > 0);
+        vPairsPart = Vec_PtrAlloc( nPartSize );
+        for ( i = 0; i < nParts; i++ )
+        {
+            Vec_PtrClear( vPairsPart );
+            for ( k = 0; k < nPartSize; k++ )
+            {
+                iCur = i * nPartSize + k;
+                if ( iCur >= Abc_NtkCoNum(pNtk1) )
+                    break;
+                Vec_PtrPush( vPairsPart, Vec_PtrEntry(vPairs, 2*iCur  ) );
+                Vec_PtrPush( vPairsPart, Vec_PtrEntry(vPairs, 2*iCur+1) );
+            }
+            pMiter = Abc_AigMiter( pNtkMiter->pManFunc, vPairsPart );
+            if ( i == 0 )
+                Abc_ObjAddFanin( Abc_NtkPo(pNtkMiter,0), pMiter );
+            else
+            {
+                sprintf( Buffer, "%d", i );
+                pNode = Abc_NtkCreatePo( pNtkMiter );
+                Abc_ObjAssignName( pNode, "miter", Buffer );
+                Abc_ObjAddFanin( pNode, pMiter );
+            }
+        }
+        Vec_PtrFree( vPairsPart );
+        Vec_PtrFree( vPairs );
+    }
 }
 
 
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index 0a917bbb..33f336de 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -52,6 +52,10 @@ int s_MappingMem = 0;
 void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
 {
     int Num;
+
+//    if ( Abc_NtkIsStrash(pNtk) )
+//        Abc_AigCountNext( pNtk->pManFunc );
+
     fprintf( pFile, "%-13s:",       pNtk->pName );
     if ( Abc_NtkAssertNum(pNtk) )
         fprintf( pFile, " i/o/a = %4d/%4d/%4d", Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk), Abc_NtkAssertNum(pNtk) );
diff --git a/src/base/abci/abcQbf.c b/src/base/abci/abcQbf.c
new file mode 100644
index 00000000..6d4e480b
--- /dev/null
+++ b/src/base/abci/abcQbf.c
@@ -0,0 +1,260 @@
+/**CFile****************************************************************
+
+  FileName    [abcQbf.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Implementation of a simple QBF solver.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcQbf.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+/*
+   Implementation of a simple QBF solver along the lines of
+   A. Solar-Lezama, L. Tancau, R. Bodik, V. Saraswat, and S. Seshia, 
+   "Combinatorial sketching for finite programs", 12th International 
+   Conference on Architectural Support for Programming Languages and 
+   Operating Systems (ASPLOS 2006), San Jose, CA, October 2006.
+*/
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void Abc_NtkModelToVector( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues );
+static void Abc_NtkVectorClearPars( Vec_Int_t * vPiValues, int nPars );
+static void Abc_NtkVectorClearVars( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues, int nPars );
+static void Abc_NtkVectorPrintPars( Vec_Int_t * vPiValues, int nPars );
+static void Abc_NtkVectorPrintVars( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues, int nPars );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Solve the QBF problem EpAx[M(p,x)].]
+
+  Description [Variables p go first, followed by variable x.
+  The number of parameters is nPars. The miter is in pNtk.
+  The miter expresses EQUALITY of the implementation and spec.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkQbf( Abc_Ntk_t * pNtk, int nPars, int fVerbose )
+{
+    Abc_Ntk_t * pNtkVer, * pNtkSyn, * pNtkSyn2, * pNtkTemp;
+    Vec_Int_t * vPiValues;
+    int clkTotal = clock(), clkS, clkV;
+    int nIters, nIterMax = 500, nInputs, RetValue, fFound = 0;
+
+    assert( Abc_NtkIsStrash(pNtk) );
+    assert( Abc_NtkIsComb(pNtk) );
+    assert( Abc_NtkPoNum(pNtk) == 1 );
+    assert( nPars > 0 && nPars < Abc_NtkPiNum(pNtk) );
+    assert( Abc_NtkPiNum(pNtk)-nPars < 32 );
+    nInputs = Abc_NtkPiNum(pNtk) - nPars;
+
+    // initialize the synthesized network with 0000-combination
+    vPiValues = Vec_IntStart( Abc_NtkPiNum(pNtk) );
+    Abc_NtkVectorClearPars( vPiValues, nPars );
+    pNtkSyn = Abc_NtkMiterCofactor( pNtk, vPiValues );
+    if ( fVerbose )
+    {
+        printf( "Iter %2d : ", 0 );
+        printf( "AIG = %6d  ", Abc_NtkNodeNum(pNtkSyn) );
+        Abc_NtkVectorPrintVars( pNtk, vPiValues, nPars );
+        printf( "\n" );
+    }
+
+    // iteratively solve
+    for ( nIters = 0; nIters < nIterMax; nIters++ )
+    {
+        // solve the synthesis instance
+clkS = clock();
+        RetValue = Abc_NtkMiterSat( pNtkSyn, 0, 0, 0, NULL, NULL );
+clkS = clock() - clkS;
+        if ( RetValue == 0 )
+            Abc_NtkModelToVector( pNtkSyn, vPiValues );
+        if ( RetValue == 1 )
+        {
+            break;
+        }
+        if ( RetValue == -1 )
+        {
+            printf( "Synthesis timed out.\n" );
+            break;
+        }
+        // there is a counter-example
+
+        // construct the verification instance
+        Abc_NtkVectorClearVars( pNtk, vPiValues, nPars );
+        pNtkVer = Abc_NtkMiterCofactor( pNtk, vPiValues );
+        // complement the output
+        Abc_ObjXorFaninC( Abc_NtkPo(pNtkVer,0), 0 );
+
+        // solve the verification instance
+clkV = clock();
+        RetValue = Abc_NtkMiterSat( pNtkVer, 0, 0, 0, NULL, NULL );
+clkV = clock() - clkV;
+        if ( RetValue == 0 )
+            Abc_NtkModelToVector( pNtkVer, vPiValues );
+        Abc_NtkDelete( pNtkVer );
+        if ( RetValue == 1 )
+        {
+            fFound = 1;
+            break;
+        }
+        if ( RetValue == -1 )
+        {
+            printf( "Verification timed out.\n" );
+            break;
+        }
+        // there is a counter-example
+
+        // create a new synthesis network
+        Abc_NtkVectorClearPars( vPiValues, nPars );
+        pNtkSyn2 = Abc_NtkMiterCofactor( pNtk, vPiValues );
+        // add to the synthesis instance
+        pNtkSyn = Abc_NtkMiterAnd( pNtkTemp = pNtkSyn, pNtkSyn2, 0, 0 );
+        Abc_NtkDelete( pNtkSyn2 );
+        Abc_NtkDelete( pNtkTemp );
+
+        if ( fVerbose )
+        {
+            printf( "Iter %2d : ", nIters+1 );
+            printf( "AIG = %6d  ", Abc_NtkNodeNum(pNtkSyn) );
+            Abc_NtkVectorPrintVars( pNtk, vPiValues, nPars );
+            printf( "  " );
+            PRTn( "Syn", clkS );
+            PRT( "Ver", clkV );
+        }
+    }
+    Abc_NtkDelete( pNtkSyn );
+    // report the results
+    if ( fFound )
+    {
+        printf( "Parameters: " );
+        Abc_NtkVectorPrintPars( vPiValues, nPars );
+        printf( "\n" );
+        printf( "Solved after %d interations.  ", nIters );
+    }
+    else if ( nIters == nIterMax )
+        printf( "Unsolved after %d interations.  ", nIters );
+    else 
+        printf( "Implementation does not exist.  " );
+    PRT( "Total runtime", clock() - clkTotal );
+    Vec_IntFree( vPiValues );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Translates model into the vector of values.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkModelToVector( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues )
+{
+    int * pModel, i;
+    pModel = pNtk->pModel;
+    for ( i = 0; i < Abc_NtkPiNum(pNtk); i++ )
+        Vec_IntWriteEntry( vPiValues, i, pModel[i] );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Clears parameters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkVectorClearPars( Vec_Int_t * vPiValues, int nPars )
+{
+    int i;
+    for ( i = 0; i < nPars; i++ )
+        Vec_IntWriteEntry( vPiValues, i, -1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Clears variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkVectorClearVars( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues, int nPars )
+{
+    int i;
+    for ( i = nPars; i < Abc_NtkPiNum(pNtk); i++ )
+        Vec_IntWriteEntry( vPiValues, i, -1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Clears variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkVectorPrintPars( Vec_Int_t * vPiValues, int nPars )
+{
+    int i;
+    for ( i = 0; i < nPars; i++ )
+        printf( "%d", Vec_IntEntry(vPiValues,i) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Clears variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkVectorPrintVars( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues, int nPars )
+{
+    int i;
+    for ( i = nPars; i < Abc_NtkPiNum(pNtk); i++ )
+        printf( "%d", Vec_IntEntry(vPiValues,i) );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcQuant.c b/src/base/abci/abcQuant.c
index 8591663e..0f2bd72f 100644
--- a/src/base/abci/abcQuant.c
+++ b/src/base/abci/abcQuant.c
@@ -72,7 +72,7 @@ void Abc_NtkSynthesize( Abc_Ntk_t ** ppNtk, int fMoreEffort )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkQuantify( Abc_Ntk_t * pNtk, int iVar, int fVerbose )
+int Abc_NtkQuantify( Abc_Ntk_t * pNtk, int fUniv, int iVar, int fVerbose )
 {
     Vec_Ptr_t * vNodes;
     Abc_Obj_t * pObj, * pNext, * pFanin;
@@ -112,7 +112,10 @@ int Abc_NtkQuantify( Abc_Ntk_t * pNtk, int iVar, int fVerbose )
             continue;
         pFanin = Abc_ObjFanin0(pObj);
         // get the result of quantification
-        pNext = Abc_AigOr( pNtk->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild0Data(pObj) );
+        if ( fUniv )
+            pNext = Abc_AigAnd( pNtk->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild0Data(pObj) );
+        else
+            pNext = Abc_AigOr( pNtk->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild0Data(pObj) );
         pNext = Abc_ObjNotCond( pNext, Abc_ObjFaninC0(pObj) );
         if ( Abc_ObjRegular(pNext) == pFanin )
             continue;
@@ -197,7 +200,7 @@ Abc_Ntk_t * Abc_NtkTransRel( Abc_Ntk_t * pNtk, int fInputs, int fVerbose )
         for ( i = Abc_NtkPiNum(pNtkNew) - 1; i >= 2*nLatches; i-- )
 //        for ( i = 2*nLatches; i < Abc_NtkPiNum(pNtkNew); i++ )
         {
-            Abc_NtkQuantify( pNtkNew, i, fVerbose );
+            Abc_NtkQuantify( pNtkNew, 0, i, fVerbose );
 //            if ( fSynthesis && (i % 3 == 2) )
             if ( fSynthesis  )
             {
@@ -339,7 +342,7 @@ Abc_Ntk_t * Abc_NtkReachability( Abc_Ntk_t * pNtkRel, int nIters, int fVerbose )
         // quantify the current state variables
         for ( v = 0; v < nVars; v++ )
         {
-            Abc_NtkQuantify( pNtkNext, v, fVerbose );
+            Abc_NtkQuantify( pNtkNext, 0, v, fVerbose );
             if ( fSynthesis && (v % 3 == 2) )
             {
                 Abc_NtkCleanData( pNtkNext );
diff --git a/src/base/abci/abcRr.c b/src/base/abci/abcRr.c
index b9fab415..92adc718 100644
--- a/src/base/abci/abcRr.c
+++ b/src/base/abci/abcRr.c
@@ -354,7 +354,7 @@ int Abc_NtkRRProve( Abc_RRMan_t * p )
     Abc_NtkRRUpdate( pWndCopy, p->pNode->pCopy->pCopy, p->pFanin->pCopy->pCopy, p->pFanout? p->pFanout->pCopy->pCopy : NULL );
     if ( !Abc_NtkIsDfsOrdered(pWndCopy) )
         Abc_NtkReassignIds(pWndCopy);
-    p->pMiter = Abc_NtkMiter( p->pWnd, pWndCopy, 1 );
+    p->pMiter = Abc_NtkMiter( p->pWnd, pWndCopy, 1, 0 );
     Abc_NtkDelete( pWndCopy );
 clk = clock();
     RetValue  = Abc_NtkMiterProve( &p->pMiter, p->pParams );
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index c891772f..05bd021d 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -52,7 +52,7 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI
     int RetValue;
 
     // get the miter of the two networks
-    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1 );
+    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, 0 );
     if ( pMiter == NULL )
     {
         printf( "Miter computation has failed.\n" );
@@ -120,7 +120,7 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV
     int RetValue;
 
     // get the miter of the two networks
-    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1 );
+    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, 0 );
     if ( pMiter == NULL )
     {
         printf( "Miter computation has failed.\n" );
@@ -198,6 +198,108 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV
 
 /**Function*************************************************************
 
+  Synopsis    [Verifies sequential equivalence by fraiging followed by SAT.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkCecFraigPart( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nPartSize, int fVerbose )
+{
+    extern int Cmd_CommandExecute( void * pAbc, char * sCommand );
+    extern void * Abc_FrameGetGlobalFrame();
+
+    Prove_Params_t Params, * pParams = &Params;
+    Abc_Ntk_t * pMiter, * pMiterPart;
+    Abc_Obj_t * pObj;
+    int i, RetValue, Status, nOutputs;
+
+    // solve the CNF using the SAT solver
+    Prove_ParamsSetDefault( pParams );
+    pParams->nItersMax = 5;
+    //    pParams->fVerbose = 1;
+
+    assert( nPartSize > 0 );
+
+    // get the miter of the two networks
+    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, nPartSize );
+    if ( pMiter == NULL )
+    {
+        printf( "Miter computation has failed.\n" );
+        return;
+    }
+    RetValue = Abc_NtkMiterIsConstant( pMiter );
+    if ( RetValue == 0 )
+    {
+        printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
+        // report the error
+        pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, 1 );
+        Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel );
+        FREE( pMiter->pModel );
+        Abc_NtkDelete( pMiter );
+        return;
+    }
+    if ( RetValue == 1 )
+    {
+        printf( "Networks are equivalent after structural hashing.\n" );
+        Abc_NtkDelete( pMiter );
+        return;
+    }
+
+    Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "unset progressbar" );
+
+    // solve the problem iteratively for each output of the miter
+    Status = 1;
+    nOutputs = 0;
+    Abc_NtkForEachPo( pMiter, pObj, i )
+    {
+        // get the cone of this output
+        pMiterPart = Abc_NtkCreateCone( pMiter, Abc_ObjFanin0(pObj), Abc_ObjName(pObj), 0 );
+        if ( Abc_ObjFaninC0(pObj) )
+            Abc_ObjXorFaninC( Abc_NtkPo(pMiterPart,0), 0 );
+        // solve the cone
+    //    RetValue = Abc_NtkMiterProve( &pMiterPart, pParams );
+        RetValue = Abc_NtkIvyProve( &pMiterPart, pParams );
+        if ( RetValue == -1 )
+        {
+            printf( "Networks are undecided (resource limits is reached).\r" );
+            Status = -1;
+        }
+        else if ( RetValue == 0 )
+        {
+            int * pSimInfo = Abc_NtkVerifySimulatePattern( pMiterPart, pMiterPart->pModel );
+            if ( pSimInfo[0] != 1 )
+                printf( "ERROR in Abc_NtkMiterProve(): Generated counter-example is invalid.\n" );
+            else
+                printf( "Networks are NOT EQUIVALENT.                 \n" );
+            free( pSimInfo );
+            Status = 0;
+            break;
+        }
+        else
+        {
+            printf( "Finished part %d (out of %d)\r", i+1, Abc_NtkPoNum(pMiter) );
+            nOutputs += nPartSize;
+        }
+//        if ( pMiter->pModel )
+//            Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel );
+        Abc_NtkDelete( pMiterPart );
+    }
+
+    Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "set progressbar" );
+
+    if ( Status == 1 )
+        printf( "Networks are equivalent.                         \n" );
+    else if ( Status == -1 )
+        printf( "Timed out after verifying %d outputs (out of %d).\n", nOutputs, Abc_NtkCoNum(pNtk1) );
+    Abc_NtkDelete( pMiter );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Verifies sequential equivalence by brute-force SAT.]
 
   Description []
@@ -216,7 +318,7 @@ void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI
     int RetValue;
 
     // get the miter of the two networks
-    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0 );
+    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0 );
     if ( pMiter == NULL )
     {
         printf( "Miter computation has failed.\n" );
@@ -298,7 +400,7 @@ int Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFr
     int RetValue;
 
     // get the miter of the two networks
-    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0 );
+    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0 );
     if ( pMiter == NULL )
     {
         printf( "Miter computation has failed.\n" );
diff --git a/src/base/abci/abc_new.h b/src/base/abci/abc_new.h
new file mode 100644
index 00000000..3460bb38
--- /dev/null
+++ b/src/base/abci/abc_new.h
@@ -0,0 +1,23 @@
+struct Abc_Obj_t_ // 6 words
+{
+    Abc_Obj_t *       pCopy;         // the copy of this object
+    Abc_Ntk_t *       pNtk;          // the host network
+    int               Id;            // the object ID
+    int               TravId;        // the traversal ID 
+    int               nRefs;         // the number of fanouts
+    unsigned          Type    :  4;  // the object type
+    unsigned          fMarkA  :  1;  // the multipurpose mark
+    unsigned          fMarkB  :  1;  // the multipurpose mark
+    unsigned          fPhase  :  1;  // the flag to mark the phase of equivalent node
+    unsigned          fPersist:  1;  // marks the persistant AIG node
+    unsigned          nFanins : 24;  // the level of the node
+    Abc_Obj_t *       Fanins[0];     // the array of fanins
+};
+
+struct Abc_Pin_t_ // 4 words
+{
+    Abc_Pin_t *       pNext;
+    Abc_Pin_t *       pPrev;
+    Abc_Obj_t *       pFanin;
+    Abc_Obj_t *       pFanout;
+};
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index 016ada60..3bec3840 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -30,6 +30,7 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcPlace.c \
     src/base/abci/abcPrint.c \
     src/base/abci/abcProve.c \
+    src/base/abci/abcQbf.c \
     src/base/abci/abcQuant.c \
     src/base/abci/abcReconv.c \
     src/base/abci/abcRefactor.c \