Version abc61007

12 files changed, 526 insertions, 84 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 2427146c..b25ca2f7 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -117,6 +117,7 @@ static int Abc_CommandSuperChoice    ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandSuperChoiceLut ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandFpga           ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFpgaFast       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPga            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandScut           ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -246,6 +247,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "SC mapping",   "scl",           Abc_CommandSuperChoiceLut,   1 );
 
     Cmd_CommandAdd( pAbc, "FPGA mapping", "fpga",          Abc_CommandFpga,             1 );
+    Cmd_CommandAdd( pAbc, "FPGA mapping", "ffpga",         Abc_CommandFpgaFast,         1 );
     Cmd_CommandAdd( pAbc, "FPGA mapping", "pga",           Abc_CommandPga,              1 );
 
     Cmd_CommandAdd( pAbc, "Sequential",   "scut",          Abc_CommandScut,             0 );
@@ -4007,6 +4009,7 @@ int Abc_CommandOneOutput( Abc_Frame_t * pAbc, int argc, char ** argv )
         goto usage;
     }
 
+    pNodeCo = NULL;
     if ( argc == globalUtilOptind + 1 )
     {
         pNode = Abc_NtkFindNode( pNtk, argv[globalUtilOptind] );
@@ -4827,7 +4830,7 @@ usage:
 int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
-    Abc_Ntk_t * pNtk, * pNtkRes;
+    Abc_Ntk_t * pNtk, * pNtkRes;//, * pNtkTemp;
     int c;
     int nLutMax;
     int nPlaMax;
@@ -4844,13 +4847,13 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    nLutMax    = 6;
+    nLutMax    = 8;
     nPlaMax    = 128;
     RankCost   = 96000;
     fFastMode  = 1;
     fRewriting = 0;
     fSynthesis = 0;
-    fVerbose   = 1;
+    fVerbose   = 0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "LPRfrsvh" ) ) != EOF )
     {
@@ -4927,8 +4930,17 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
 */
     // run the command
 //    pNtkRes = Abc_NtkXyz( pNtk, nPlaMax, 1, 0, fInvs, fVerbose );
-    pNtkRes = Abc_NtkPlayer( pNtk, nLutMax, nPlaMax, RankCost, fFastMode, fRewriting, fSynthesis, fVerbose );
-//    pNtkRes = NULL;
+/*
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        pNtkTemp = Abc_NtkStrash( pNtk, 0, 1 );
+        pNtkRes = Abc_NtkPlayer( pNtkTemp, nLutMax, nPlaMax, RankCost, fFastMode, fRewriting, fSynthesis, fVerbose );
+        Abc_NtkDelete( pNtkTemp );
+    }
+    else
+        pNtkRes = Abc_NtkPlayer( pNtk, nLutMax, nPlaMax, RankCost, fFastMode, fRewriting, fSynthesis, fVerbose );
+*/
+    pNtkRes = NULL;
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Command has failed.\n" );
@@ -5537,10 +5549,10 @@ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
-    int c, fUpdateLevel, fVerbose;
+    int c, fProve, fVerbose;
     int nConfLimit;
 
-    extern Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fProve, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -5548,10 +5560,10 @@ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // set defaults
     nConfLimit   = 100;   
-    fUpdateLevel = 1;
+    fProve       = 0;
     fVerbose     = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Clzvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Cpvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -5566,8 +5578,8 @@ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nConfLimit < 0 ) 
                 goto usage;
             break;
-        case 'l':
-            fUpdateLevel ^= 1;
+        case 'p':
+            fProve ^= 1;
             break;
         case 'v':
             fVerbose ^= 1;
@@ -5589,7 +5601,7 @@ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    pNtkRes = Abc_NtkIvyFraig( pNtk, nConfLimit, fVerbose );
+    pNtkRes = Abc_NtkIvyFraig( pNtk, nConfLimit, fProve, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Command has failed.\n" );
@@ -5600,10 +5612,10 @@ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: ifraig [-C num] [-vh]\n" );
+    fprintf( pErr, "usage: ifraig [-C num] [-pvh]\n" );
     fprintf( pErr, "\t         performs fraiging using a new method\n" );
-    fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n",    nConfLimit );
-//    fprintf( pErr, "\t-l     : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" );
+    fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit );
+    fprintf( pErr, "\t-p     : toggle proving miter outputs [default = %s]\n", fProve? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
@@ -5622,29 +5634,31 @@ usage:
 ***********************************************************************/
 int Abc_CommandIProve( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
+    Prove_Params_t Params, * pParams = &Params;
     FILE * pOut, * pErr;
-    Abc_Ntk_t * pNtk, * pNtkRes;
-    int c, fUpdateLevel, fVerbose;
+    Abc_Ntk_t * pNtk, * pNtkTemp;
+    int c, clk, RetValue;
 
-    extern Abc_Ntk_t * Abc_NtkIvyProve( Abc_Ntk_t * pNtk );
+    extern int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    fUpdateLevel = 1;
-    fVerbose     = 0;
+    Prove_ParamsSetDefault( pParams );
+    pParams->fUseRewriting = 1;
+    pParams->fVerbose      = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "lzvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "rvh" ) ) != EOF )
     {
         switch ( c )
         {
-        case 'l':
-            fUpdateLevel ^= 1;
+        case 'r':
+            pParams->fUseRewriting ^= 1;
             break;
         case 'v':
-            fVerbose ^= 1;
+            pParams->fVerbose ^= 1;
             break;
         case 'h':
             goto usage;
@@ -5663,21 +5677,43 @@ int Abc_CommandIProve( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    pNtkRes = Abc_NtkIvyProve( pNtk );
-    if ( pNtkRes == NULL )
+
+    clk = clock();
+
+    if ( Abc_NtkIsStrash(pNtk) )
+        pNtkTemp = Abc_NtkDup( pNtk );
+    else
+        pNtkTemp = Abc_NtkStrash( pNtk, 0, 0 );
+
+    RetValue = Abc_NtkIvyProve( &pNtkTemp, pParams );
+
+    // verify that the pattern is correct
+    if ( RetValue == 0 )
     {
-        fprintf( pErr, "Command has failed.\n" );
-        return 0;
+        int * pSimInfo = Abc_NtkVerifySimulatePattern( pNtk, pNtkTemp->pModel );
+        if ( pSimInfo[0] != 1 )
+            printf( "ERROR in Abc_NtkMiterProve(): Generated counter-example is invalid.\n" );
+        free( pSimInfo );
     }
+ 
+    if ( RetValue == -1 ) 
+        printf( "UNDECIDED      " );
+    else if ( RetValue == 0 )
+        printf( "SATISFIABLE    " );
+    else
+        printf( "UNSATISFIABLE  " );
+    //printf( "\n" );
+
+    PRT( "Time", clock() - clk );
     // replace the current network
-    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkTemp );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: iprove [-h]\n" );
+    fprintf( pErr, "usage: iprove [-rvh]\n" );
     fprintf( pErr, "\t         performs CEC using a new method\n" );
-//    fprintf( pErr, "\t-l     : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" );
-//    fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-r     : toggle AIG rewriting [default = %s]\n", pParams->fUseRewriting? "yes": "no" );
+    fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", pParams->fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
 }
@@ -6932,6 +6968,147 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandFpgaFast( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    char Buffer[100];
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c;
+    int fRecovery;
+    int fVerbose;
+    int nLutSize;
+    float DelayTarget;
+
+    extern Abc_Ntk_t * Abc_NtkFpgaFast( Abc_Ntk_t * pNtk, int nLutSize, int fRecovery, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fRecovery   = 1;
+    fVerbose    = 0;
+    DelayTarget =-1;
+    nLutSize    = 8;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "avhDK" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'a':
+            fRecovery ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        case 'D':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-D\" should be followed by a floating point number.\n" );
+                goto usage;
+            }
+            DelayTarget = (float)atof(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( DelayTarget <= 0.0 ) 
+                goto usage;
+            break;
+        case 'K':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-K\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nLutSize = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nLutSize < 0 ) 
+                goto usage;
+            break;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    if ( Abc_NtkIsSeq(pNtk) )
+    {
+        fprintf( pErr, "Cannot FPGA map a sequential AIG.\n" );
+        return 1;
+    }
+
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        // strash and balance the network
+        pNtk = Abc_NtkStrash( pNtk, 0, 0 );
+        if ( pNtk == NULL )
+        {
+            fprintf( pErr, "Strashing before FPGA mapping has failed.\n" );
+            return 1;
+        }
+        pNtk = Abc_NtkBalance( pNtkRes = pNtk, 0, 0, 1 );
+        Abc_NtkDelete( pNtkRes );
+        if ( pNtk == NULL )
+        {
+            fprintf( pErr, "Balancing before FPGA mapping has failed.\n" );
+            return 1;
+        }
+        fprintf( pOut, "The network was strashed and balanced before FPGA mapping.\n" );
+        // get the new network
+        pNtkRes = Abc_NtkFpgaFast( pNtk, nLutSize, fRecovery, fVerbose );
+        if ( pNtkRes == NULL )
+        {
+            Abc_NtkDelete( pNtk );
+            fprintf( pErr, "FPGA mapping has failed.\n" );
+            return 1;
+        }
+        Abc_NtkDelete( pNtk );
+    }
+    else
+    {
+        // get the new network
+        pNtkRes = Abc_NtkFpgaFast( pNtk, nLutSize, fRecovery, fVerbose );
+        if ( pNtkRes == NULL )
+        {
+            fprintf( pErr, "FPGA mapping has failed.\n" );
+            return 1;
+        }
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    if ( DelayTarget == -1 ) 
+        sprintf( Buffer, "not used" );
+    else
+        sprintf( Buffer, "%.2f", DelayTarget );
+    fprintf( pErr, "usage: ffpga [-K num] [-avh]\n" );
+    fprintf( pErr, "\t           performs fast FPGA mapping of the current network\n" );
+    fprintf( pErr, "\t-a       : toggles area recovery [default = %s]\n", fRecovery? "yes": "no" );
+//    fprintf( pErr, "\t-D float : sets the required time for the mapping [default = %s]\n", Buffer );  
+    fprintf( pErr, "\t-K num   : the number of LUT inputs (2 < num < 32) [default = %d]\n", nLutSize );
+    fprintf( pErr, "\t-v       : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h       : prints the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandPga( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
diff --git a/src/base/abci/abcDsd.c b/src/base/abci/abcDsd.c
index cd8f9047..6708217c 100644
--- a/src/base/abci/abcDsd.c
+++ b/src/base/abci/abcDsd.c
@@ -172,7 +172,7 @@ void Abc_NtkDsdConstruct( Dsd_Manager_t * pManDsd, Abc_Ntk_t * pNtk, Abc_Ntk_t *
     int i, nNodesDsd;
 
     // save the CI nodes in the DSD nodes
-    Dsd_NodeSetMark( Dsd_ManagerReadConst1(pManDsd), (int)Abc_AigConst1(pNtkNew) );
+    Dsd_NodeSetMark( Dsd_ManagerReadConst1(pManDsd), (int)Abc_NodeCreateConst1(pNtkNew) );
     Abc_NtkForEachCi( pNtk, pNode, i )
     {
         pNodeDsd = Dsd_ManagerReadInput( pManDsd, i );
diff --git a/src/base/abci/abcExtract.c b/src/base/abci/abcExtract.c
new file mode 100644
index 00000000..52ea03a3
--- /dev/null
+++ b/src/base/abci/abcExtract.c
@@ -0,0 +1,51 @@
+/**CFile****************************************************************
+
+  FileName    [abcMvCost.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Calculating the cost of one MV block.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcMvCost.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_MvCostTest( Abc_Ntk_t * pNtk )
+{
+
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcFpgaFast.c b/src/base/abci/abcFpgaFast.c
index 2d5813c7..b307273f 100644
--- a/src/base/abci/abcFpgaFast.c
+++ b/src/base/abci/abcFpgaFast.c
@@ -19,11 +19,20 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "ivy.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+extern Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq, int fUseDc );
+
+static Abc_Ntk_t * Ivy_ManFpgaToAbc( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan );
+static Abc_Obj_t * Ivy_ManToAbcFast_rec( Abc_Ntk_t * pNtkNew, Ivy_Man_t * pMan, Ivy_Obj_t * pObjIvy, Vec_Int_t * vNodes );
+
+static inline void        Abc_ObjSetIvy2Abc( Ivy_Man_t * p, int IvyId, Abc_Obj_t * pObjAbc ) {  assert(Vec_PtrEntry(p->pCopy, IvyId) == NULL); assert(!Abc_ObjIsComplement(pObjAbc)); Vec_PtrWriteEntry( p->pCopy, IvyId, pObjAbc );  }
+static inline Abc_Obj_t * Abc_ObjGetIvy2Abc( Ivy_Man_t * p, int IvyId )                      {  return Vec_PtrEntry( p->pCopy, IvyId );         }
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -43,25 +52,20 @@
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkFpgaFast( Abc_Ntk_t * pNtk, int nLutSize, int fVerbose )
+Abc_Ntk_t * Abc_NtkFpgaFast( Abc_Ntk_t * pNtk, int nLutSize, int fRecovery, int fVerbose )
 {
+    Ivy_Man_t * pMan;
     Abc_Ntk_t * pNtkNew;
-    Abc_Obj_t * pObj;
-    int i;
-
     // make sure the network is an AIG
     assert( Abc_NtkIsStrash(pNtk) );
-
-    // iterate over the nodes in the network
-    Abc_NtkForEachNode( pNtk, pObj, i )
-    {
-    }
-
-    // create the new network after mapping
-    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD );
-
-    // here we need to create nodes of the new network
-    
+    // convert the network into the AIG
+    pMan = Abc_NtkIvyBefore( pNtk, 0, 0 );
+    // perform fast FPGA mapping
+    Ivy_FastMapPerform( pMan, nLutSize, fRecovery, fVerbose );
+    // convert back into the ABC network
+    pNtkNew = Ivy_ManFpgaToAbc( pNtk, pMan );
+    Ivy_FastMapStop( pMan );
+    Ivy_ManStop( pMan );  
     // make sure that the final network passes the test
     if ( pNtkNew != NULL && !Abc_NtkCheck( pNtkNew ) )
     {
@@ -72,6 +76,113 @@ Abc_Ntk_t * Abc_NtkFpgaFast( Abc_Ntk_t * pNtk, int nLutSize, int fVerbose )
     return pNtkNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Constructs the ABC network after mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Ivy_ManFpgaToAbc( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan )
+{
+    Abc_Ntk_t * pNtkNew;
+    Abc_Obj_t * pObjAbc, * pObj;
+    Ivy_Obj_t * pObjIvy;
+    Vec_Int_t * vNodes;
+    int i;
+    // start mapping from Ivy into Abc
+    pMan->pCopy = Vec_PtrStart( Ivy_ManObjIdMax(pMan) + 1 );
+    // start the new ABC network
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_AIG );
+    // transfer the pointers to the basic nodes
+    Abc_ObjSetIvy2Abc( pMan, Ivy_ManConst1(pMan)->Id, Abc_NodeCreateConst1(pNtkNew) );
+    Abc_NtkForEachCi( pNtkNew, pObjAbc, i )
+        Abc_ObjSetIvy2Abc( pMan, Ivy_ManPi(pMan, i)->Id, pObjAbc ); 
+    // recursively construct the network
+    vNodes = Vec_IntAlloc( 100 );
+    Ivy_ManForEachPo( pMan, pObjIvy, i )
+    {
+        // get the new ABC node corresponding to the old fanin of the PO in IVY
+        pObjAbc = Ivy_ManToAbcFast_rec( pNtkNew, pMan, Ivy_ObjFanin0(pObjIvy), vNodes );
+        // consider the case of complemented fanin of the PO
+        if ( Ivy_ObjFaninC0(pObjIvy) ) // complement
+        {
+            if ( Abc_ObjIsCi(pObjAbc) )
+                pObjAbc = Abc_NodeCreateInv( pNtkNew, pObjAbc );
+            else
+            {
+                // clone the node
+                pObj = Abc_NtkCloneObj( pObjAbc );
+                // set complemented functions
+                pObj->pData = Aig_Not( pObjAbc->pData );
+                // return the new node
+                pObjAbc = pObj;
+            }
+        }
+        Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), pObjAbc );
+    }
+    Vec_IntFree( vNodes );
+    Vec_PtrFree( pMan->pCopy ); 
+    pMan->pCopy = NULL;
+    // remove dangling nodes
+    Abc_NtkCleanup( pNtkNew, 0 );
+    // fix CIs feeding directly into COs
+    Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively construct the new node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Ivy_ManToAbcFast_rec( Abc_Ntk_t * pNtkNew, Ivy_Man_t * pMan, Ivy_Obj_t * pObjIvy, Vec_Int_t * vNodes )
+{
+    Vec_Int_t Supp, * vSupp = &Supp;
+    Abc_Obj_t * pObjAbc, * pFaninAbc;
+    Ivy_Obj_t * pNodeIvy;
+    int i, Entry;
+    // skip the node if it is a constant or already processed
+    pObjAbc = Abc_ObjGetIvy2Abc( pMan, pObjIvy->Id );
+    if ( pObjAbc )
+        return pObjAbc;
+    assert( Ivy_ObjIsAnd(pObjIvy) || Ivy_ObjIsExor(pObjIvy) );
+    // get the support of K-LUT
+    Ivy_FastMapReadSupp( pMan, pObjIvy, vSupp );
+    // create new ABC node and its fanins
+    pObjAbc = Abc_NtkCreateNode( pNtkNew );
+    Vec_IntForEachEntry( vSupp, Entry, i )
+    {
+        pFaninAbc = Ivy_ManToAbcFast_rec( pNtkNew, pMan, Ivy_ManObj(pMan, Entry), vNodes );
+        Abc_ObjAddFanin( pObjAbc, pFaninAbc );
+    }
+    // collect the nodes used in the cut
+    Ivy_ManCollectCut( pMan, pObjIvy, vSupp, vNodes );
+    // create the local function
+    Ivy_ManForEachNodeVec( pMan, vNodes, pNodeIvy, i )
+    {
+        if ( i < Vec_IntSize(vSupp) )
+            pNodeIvy->pEquiv = (Ivy_Obj_t *)Aig_IthVar( pNtkNew->pManFunc, i );
+        else
+            pNodeIvy->pEquiv = (Ivy_Obj_t *)Aig_And( pNtkNew->pManFunc, (Aig_Obj_t *)Ivy_ObjChild0Equiv(pNodeIvy), (Aig_Obj_t *)Ivy_ObjChild1Equiv(pNodeIvy) );
+    }
+    // set the local function
+    pObjAbc->pData = (Abc_Obj_t *)pObjIvy->pEquiv;
+    // set the node
+    Abc_ObjSetIvy2Abc( pMan, pObjIvy->Id, pObjAbc ); 
+    return pObjAbc;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
index 320c76dd..82e03119 100644
--- a/src/base/abci/abcIvy.c
+++ b/src/base/abci/abcIvy.c
@@ -21,6 +21,7 @@
 #include "abc.h"
 #include "dec.h"
 #include "ivy.h"
+#include "fraig.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -81,7 +82,7 @@ Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq, int fUseDc )
             return NULL;
         }
     }
-    if ( Abc_NtkCountSelfFeedLatches(pNtk) )
+    if ( fSeq && Abc_NtkCountSelfFeedLatches(pNtk) )
     {
         printf( "Warning: The network has %d self-feeding latches. Quitting.\n", Abc_NtkCountSelfFeedLatches(pNtk) );
         return NULL;
@@ -368,7 +369,7 @@ Abc_Ntk_t * Abc_NtkIvySat( Abc_Ntk_t * pNtk, int nConfLimit, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fVerbose )
+Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fProve, int fVerbose )
 {
     Ivy_FraigParams_t Params, * pParams = &Params; 
     Abc_Ntk_t * pNtkAig;
@@ -379,6 +380,7 @@ Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fVerbose )
     Ivy_FraigParamsDefault( pParams );
     pParams->nBTLimitNode = nConfLimit;
     pParams->fVerbose = fVerbose;
+    pParams->fProve = fProve;
     pMan = Ivy_FraigPerform( pTemp = pMan, pParams );
     Ivy_ManStop( pTemp );
     pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 );
@@ -394,23 +396,76 @@ Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fVerbose )
                
   SideEffects []
 
-  SeeAlso     []
+  SeeAlso     [] 
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkIvyProve( Abc_Ntk_t * pNtk )
+int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars )
 {
-    Ivy_FraigParams_t Params, * pParams = &Params; 
-    Abc_Ntk_t * pNtkAig;
-    Ivy_Man_t * pMan, * pTemp;
+    Prove_Params_t * pParams = pPars;
+    Abc_Ntk_t * pNtk = *ppNtk, * pNtkTemp;
+    Ivy_Man_t * pMan;
+    int RetValue;
+    assert( Abc_NtkIsStrash(pNtk) || Abc_NtkIsLogic(pNtk) );
+    // experiment with various parameters settings
+//    pParams->fUseBdds = 1;
+//    pParams->fBddReorder = 1;
+//    pParams->nTotalBacktrackLimit = 10000;
+
+    // strash the network if it is not strashed already
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        pNtk = Abc_NtkStrash( pNtkTemp = pNtk, 0, 1 );
+        Abc_NtkDelete( pNtkTemp );
+    }
+
+    // if SAT only, solve without iteration
+    RetValue = Abc_NtkMiterSat( pNtk, 2*(sint64)pParams->nMiteringLimitStart, (sint64)0, 0, 0, NULL, NULL );
+    if ( RetValue >= 0 )
+        return RetValue;
+
+    // apply AIG rewriting
+    if ( pParams->fUseRewriting && Abc_NtkNodeNum(pNtk) > 500 )
+    {
+        pParams->fUseRewriting = 0;
+        Abc_NtkRewrite( pNtk, 0, 0, 0 );
+        pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );          
+        Abc_NtkDelete( pNtkTemp );
+        Abc_NtkRewrite( pNtk, 0, 0, 0 );
+        Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
+    }
+
+    // convert ABC network into IVY network
     pMan = Abc_NtkIvyBefore( pNtk, 0, 0 );
-    if ( pMan == NULL )
-        return NULL;
-    Ivy_FraigParamsDefault( pParams );
-    pMan = Ivy_FraigProve( pTemp = pMan, pParams );
-    Ivy_ManStop( pTemp );
-    pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 );
+    // solve the CEC problem
+    RetValue = Ivy_FraigProve( &pMan, pParams );
+    // convert IVY network into ABC network    
+    pNtk = Abc_NtkIvyAfter( pNtkTemp = pNtk, pMan, 0, 0 );
+    Abc_NtkDelete( pNtkTemp );
+    // transfer model if given
+    pNtk->pModel = pMan->pData; pMan->pData = NULL;
     Ivy_ManStop( pMan );
-    return pNtkAig;
+
+    // try to prove it using brute force SAT
+    if ( RetValue < 0 && pParams->fUseBdds )
+    {
+        if ( pParams->fVerbose )
+        {
+            printf( "Attempting BDDs with node limit %d ...\n", pParams->nBddSizeLimit );
+            fflush( stdout );
+        }
+        pNtk = Abc_NtkCollapse( pNtkTemp = pNtk, pParams->nBddSizeLimit, 0, pParams->fBddReorder, 0 );
+        if ( pNtk )   
+        {
+            Abc_NtkDelete( pNtkTemp );
+            RetValue = ( (Abc_NtkNodeNum(pNtk) == 1) && (Abc_ObjFanin0(Abc_NtkPo(pNtk,0))->pData == Cudd_ReadLogicZero(pNtk->pManFunc)) );
+        }
+        else 
+            pNtk = pNtkTemp;
+    }
+
+    // return the result
+    *ppNtk = pNtk;
+    return RetValue;
 }
 
 /**Function*************************************************************
diff --git a/src/base/abci/abcMini.c b/src/base/abci/abcMini.c
index 037f058a..014eafd3 100644
--- a/src/base/abci/abcMini.c
+++ b/src/base/abci/abcMini.c
@@ -59,6 +59,7 @@ Abc_Ntk_t * Abc_NtkMiniBalance( Abc_Ntk_t * pNtk )
     }
     // perform balance
     Aig_ManPrintStats( pMan );
+//    Aig_ManDumpBlif( pMan, "aig_temp.blif" );
     pMan = Aig_ManBalance( pTemp = pMan, 1 );
     Aig_ManStop( pTemp );
     Aig_ManPrintStats( pMan );
diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c
index 9a88db99..9b67ab13 100644
--- a/src/base/abci/abcNtbdd.c
+++ b/src/base/abci/abcNtbdd.c
@@ -189,7 +189,6 @@ Abc_Obj_t * Abc_NodeBddToMuxes( Abc_Obj_t * pNodeOld, Abc_Ntk_t * pNtkNew )
     // create the table mapping BDD nodes into the ABC nodes
     tBdd2Node = st_init_table( st_ptrcmp, st_ptrhash );
     // add the constant and the elementary vars
-    st_insert( tBdd2Node, (char *)b1, (char *)Abc_AigConst1(pNtkNew) );
     Abc_ObjForEachFanin( pNodeOld, pFaninOld, i )
         st_insert( tBdd2Node, (char *)Cudd_bddIthVar(dd, i), (char *)pFaninOld->pCopy );
     // create the new nodes recursively
@@ -215,6 +214,8 @@ Abc_Obj_t * Abc_NodeBddToMuxes_rec( DdManager * dd, DdNode * bFunc, Abc_Ntk_t *
 {
     Abc_Obj_t * pNodeNew, * pNodeNew0, * pNodeNew1, * pNodeNewC;
     assert( !Cudd_IsComplement(bFunc) );
+    if ( bFunc == b1 )
+        return Abc_NodeCreateConst1(pNtkNew);
     if ( st_lookup( tBdd2Node, (char *)bFunc, (char **)&pNodeNew ) )
         return pNodeNew;
     // solve for the children nodes
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index c7e2acc0..afc635e9 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -144,7 +144,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
     }
 */
 
-
+/*
     // print the statistic into a file
     {
         FILE * pTable;
@@ -157,7 +157,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
         fprintf( pTable, "\n" );
         fclose( pTable );
     }
-
+*/
 
 /*
     // print the statistic into a file
diff --git a/src/base/abci/abcProve.c b/src/base/abci/abcProve.c
index f3c1a825..c9e5bfd7 100644
--- a/src/base/abci/abcProve.c
+++ b/src/base/abci/abcProve.c
@@ -314,6 +314,29 @@ void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, int clk, int fVerbose
     PRT( pString, clock() - clk );
 }
 
+  
+/**Function*************************************************************
+
+  Synopsis    [Implements resynthesis for CEC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkMiterRwsat( Abc_Ntk_t * pNtk )
+{
+    Abc_Ntk_t * pNtkTemp;
+    Abc_NtkRewrite( pNtk, 0, 0, 0 );
+    pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );  Abc_NtkDelete( pNtkTemp );
+    Abc_NtkRewrite( pNtk, 0, 0, 0 );
+    Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
+    return pNtk;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index 3e0d6ba0..8d5dd2a7 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -56,8 +56,8 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int
     assert( Abc_NtkIsStrash(pNtk) );
     assert( Abc_NtkLatchNum(pNtk) == 0 );
 
-    if ( Abc_NtkPoNum(pNtk) > 1 )
-        fprintf( stdout, "Warning: The miter has %d outputs. SAT will try to prove all of them.\n", Abc_NtkPoNum(pNtk) );
+//    if ( Abc_NtkPoNum(pNtk) > 1 )
+//        fprintf( stdout, "Warning: The miter has %d outputs. SAT will try to prove all of them.\n", Abc_NtkPoNum(pNtk) );
 
     // load clauses into the solver
     clk = clock();
@@ -180,6 +180,29 @@ int Abc_NtkClauseTriv( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars )
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_NtkClauseTop( solver * pSat, Vec_Ptr_t * vNodes, Vec_Int_t * vVars )
+{
+    Abc_Obj_t * pNode;
+    int i;
+//printf( "Adding triv %d.         %d\n", Abc_ObjRegular(pNode)->Id, (int)pSat->solver_stats.clauses );
+    vVars->nSize = 0;
+    Vec_PtrForEachEntry( vNodes, pNode, i )
+        Vec_IntPush( vVars, toLitCond( (int)Abc_ObjRegular(pNode)->pCopy, Abc_ObjIsComplement(pNode) ) );
+//    Vec_IntPush( vVars, toLitCond( (int)Abc_ObjRegular(pNode)->Id, Abc_ObjIsComplement(pNode) ) );
+    return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    [Adds trivial clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_NtkClauseAnd( solver * pSat, Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, Vec_Int_t * vVars )
 {
     int fComp1, Var, Var1, i;
@@ -467,8 +490,8 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront )
         Vec_PtrPush( vNodes, pNode );
     }
 */
-
     // collect the nodes that need clauses and top-level assignments
+    Vec_PtrClear( vSuper );
     Abc_NtkForEachCo( pNtk, pNode, i )
     {
         // get the fanin
@@ -481,9 +504,11 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront )
             Vec_PtrPush( vNodes, pFanin );
         }
         // add the trivial clause
-        if ( !Abc_NtkClauseTriv( pSat, Abc_ObjChild0(pNode), vVars ) )
-            goto Quits;
+        Vec_PtrPush( vSuper, Abc_ObjChild0(pNode) );
     }
+    if ( !Abc_NtkClauseTop( pSat, vSuper, vVars ) )
+        goto Quits;
+
 
     // add the clauses
     Vec_PtrForEachEntry( vNodes, pNode, i )
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index 1fddc8cb..622b4103 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -174,7 +174,8 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV
     // solve the CNF using the SAT solver
     Prove_ParamsSetDefault( pParams );
     pParams->nItersMax = 5;
-    RetValue = Abc_NtkMiterProve( &pMiter, pParams );
+//    RetValue = Abc_NtkMiterProve( &pMiter, pParams );
+    RetValue = Abc_NtkIvyProve( &pMiter, pParams );
     if ( RetValue == -1 )
         printf( "Networks are undecided (resource limits is reached).\n" );
     else if ( RetValue == 0 )
@@ -399,12 +400,11 @@ int * Abc_NtkVerifyGetCleanModel( Abc_Ntk_t * pNtk, int nFrames )
                
   SideEffects []
 
-  SeeAlso     []
+  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;
@@ -416,22 +416,16 @@ int * Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel )
     // increment the trav ID
     Abc_NtkIncrementTravId( pNtk );
     // set the CI values
+    Abc_AigConst1(pNtk)->pCopy = (void *)1;
     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 )
+    Abc_NtkForEachNode( pNtk, 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);
-        }
+        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 )
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index dba9e6fd..bb2ae1a0 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -7,12 +7,16 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcCut.c \
     src/base/abci/abcDsd.c \
     src/base/abci/abcEspresso.c \
+    src/base/abci/abcExtract.c \
     src/base/abci/abcFpga.c \
+    src/base/abci/abcFpgaFast.c \
     src/base/abci/abcFraig.c \
         src/base/abci/abcFxu.c \
         src/base/abci/abcGen.c \
+        src/base/abci/abcIvy.c \
     src/base/abci/abcLut.c \
     src/base/abci/abcMap.c \
+    src/base/abci/abcMini.c \
     src/base/abci/abcMiter.c \
     src/base/abci/abcNtbdd.c \
     src/base/abci/abcOrder.c \