Version abc60803

11 files changed, 359 insertions, 53 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index f89253f3..03f5a66f 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -640,6 +640,7 @@ extern char *             Abc_SopCreateMux( Extra_MmFlex_t * pMan );
 extern char *             Abc_SopCreateInv( Extra_MmFlex_t * pMan );
 extern char *             Abc_SopCreateBuf( Extra_MmFlex_t * pMan );
 extern char *             Abc_SopCreateFromTruth( Extra_MmFlex_t * pMan, int nVars, unsigned * pTruth );
+extern char *             Abc_SopCreateFromIsop( Extra_MmFlex_t * pMan, int nVars, Vec_Int_t * vCover );
 extern int                Abc_SopGetCubeNum( char * pSop );
 extern int                Abc_SopGetLitNum( char * pSop );
 extern int                Abc_SopGetVarNum( char * pSop );
diff --git a/src/base/abc/abcRefs.c b/src/base/abc/abcRefs.c
index 91f37e8f..ea076e47 100644
--- a/src/base/abc/abcRefs.c
+++ b/src/base/abc/abcRefs.c
@@ -357,6 +357,32 @@ int Abc_NodeMffsInside( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vIns
     return Count1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Collects the internal nodes of the MFFC limited by cut.]
+
+  Description []
+               
+  SideEffects [Increments the trav ID and marks visited nodes.]
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NodeMffsInsideCollect( Abc_Obj_t * pNode )
+{
+    Vec_Ptr_t * vInside;
+    int Count1, Count2;
+    // dereference the node
+    Count1 = Abc_NodeDeref_rec( pNode );
+    // collect the nodes inside the MFFC
+    vInside = Vec_PtrAlloc( 10 );
+    Abc_NodeMffsConeSupp( pNode, vInside, NULL );
+    // reference it back
+    Count2 = Abc_NodeRef_rec( pNode );
+    assert( Count1 == Count2 );
+    return vInside;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abcSop.c b/src/base/abc/abcSop.c
index a893f3e2..db0803c1 100644
--- a/src/base/abc/abcSop.c
+++ b/src/base/abc/abcSop.c
@@ -401,6 +401,44 @@ char * Abc_SopCreateFromTruth( Extra_MmFlex_t * pMan, int nVars, unsigned * pTru
 
 /**Function*************************************************************
 
+  Synopsis    [Creates the cover from the ISOP computed from TT.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Abc_SopCreateFromIsop( Extra_MmFlex_t * pMan, int nVars, Vec_Int_t * vCover )
+{
+    char * pSop, * pCube;
+    int i, k, Entry, Literal;
+    assert( Vec_IntSize(vCover) > 0 );
+    if ( Vec_IntSize(vCover) == 0 )
+        return NULL;
+    // start the cover
+    pSop = Abc_SopStart( pMan, Vec_IntSize(vCover), nVars );
+    // create cubes
+    Vec_IntForEachEntry( vCover, Entry, i )
+    {
+        pCube = pSop + i * (nVars + 3);
+        for ( k = 0; k < nVars; k++ )
+        {
+            Literal = 3 & (Entry >> (k << 1));
+            if ( Literal == 1 )
+                pCube[k] = '1';
+            else if ( Literal == 2 )
+                pCube[k] = '0';
+            else if ( Literal != 0 )
+                assert( 0 );
+        }
+    }
+    return pSop;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Reads the number of cubes in the cover.]
 
   Description []
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index eb98c722..7bee7f40 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -91,6 +91,7 @@ static int Abc_CommandTest           ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandIStrash        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandICut           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandIRewrite       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandIRewriteSeq    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandIResyn         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandFraig          ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -207,6 +208,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "New AIG",      "istrash",       Abc_CommandIStrash,          1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "icut",          Abc_CommandICut,             0 );
     Cmd_CommandAdd( pAbc, "New AIG",      "irw",           Abc_CommandIRewrite,         1 );
+    Cmd_CommandAdd( pAbc, "New AIG",      "irws",          Abc_CommandIRewriteSeq,      1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "iresyn",        Abc_CommandIResyn,           1 );
 
     Cmd_CommandAdd( pAbc, "Fraiging",     "fraig",         Abc_CommandFraig,            1 );
@@ -4086,9 +4088,10 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
     pParams->fGlobal   = 0;     // compute global cuts
     pParams->fLocal    = 0;     // compute local cuts
     pParams->fFancy    = 0;     // compute something fancy
+    pParams->fMap      = 0;     // compute mapping delay
     pParams->fVerbose  = 0;     // the verbosiness flag
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "KMtfdxyglzvoh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "KMtfdxyglzmvoh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -4138,6 +4141,9 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'z':
             pParams->fFancy ^= 1;
             break;
+        case 'm':
+            pParams->fMap ^= 1;
+            break;
         case 'v':
             pParams->fVerbose ^= 1;
             break;
@@ -4175,7 +4181,6 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( fOracle )
         pParams->fRecord = 1;
     pCutMan = Abc_NtkCuts( pNtk, pParams );
-    Cut_ManPrintStats( pCutMan );
     if ( fOracle )
         pCutOracle = Cut_OracleStart( pCutMan );
     Cut_ManStop( pCutMan );
@@ -4187,7 +4192,7 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: cut [-K num] [-M num] [-tfdxyzvh]\n" );
+    fprintf( pErr, "usage: cut [-K num] [-M num] [-tfdxyzmvh]\n" );
     fprintf( pErr, "\t         computes k-feasible cuts for the AIG\n" );
     fprintf( pErr, "\t-K num : max number of leaves (%d <= num <= %d) [default = %d]\n",   CUT_SIZE_MIN, CUT_SIZE_MAX, pParams->nVarsMax );
     fprintf( pErr, "\t-M num : max number of cuts stored at a node [default = %d]\n",      pParams->nKeepMax );
@@ -4199,6 +4204,7 @@ usage:
     fprintf( pErr, "\t-g     : toggle computing only global cuts [default = %s]\n",        pParams->fGlobal?  "yes": "no" );
     fprintf( pErr, "\t-l     : toggle computing only local cuts [default = %s]\n",         pParams->fLocal?   "yes": "no" );
     fprintf( pErr, "\t-z     : toggle fancy computations [default = %s]\n",                pParams->fFancy?   "yes": "no" );
+    fprintf( pErr, "\t-m     : toggle delay-oriented FPGA mapping [default = %s]\n",       pParams->fMap?     "yes": "no" );
     fprintf( pErr, "\t-v     : toggle printing verbose information [default = %s]\n",      pParams->fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
@@ -4293,7 +4299,6 @@ int Abc_CommandScut( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     pCutMan = Abc_NtkSeqCuts( pNtk, pParams );
-    Cut_ManPrintStats( pCutMan );
     Cut_ManStop( pCutMan );
     return 0;
 
@@ -4480,27 +4485,31 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     int nLutMax;
     int nPlaMax;
+    int RankCost;
+    int fFastMode;
     int fVerbose;
 //    extern Abc_Ntk_t * Abc_NtkXyz( Abc_Ntk_t * pNtk, int nPlaMax, bool fUseEsop, bool fUseSop, bool fUseInvs, bool fVerbose );
-    extern void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int fVerbose );
+    extern void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int RankCost, int fFastMode, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    nLutMax = 8;
-    nPlaMax = 128;
-    fVerbose = 0;
+    nLutMax   = 8;
+    nPlaMax   = 128;
+    RankCost  = 96000;
+    fFastMode = 0;
+    fVerbose  = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "LPvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "LPRfvh" ) ) != EOF )
     {
         switch ( c )
         {
         case 'L':
             if ( globalUtilOptind >= argc )
             {
-                fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
+                fprintf( pErr, "Command line switch \"-L\" should be followed by an integer.\n" );
                 goto usage;
             }
             nLutMax = atoi(argv[globalUtilOptind]);
@@ -4511,7 +4520,7 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'P':
             if ( globalUtilOptind >= argc )
             {
-                fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
+                fprintf( pErr, "Command line switch \"-P\" should be followed by an integer.\n" );
                 goto usage;
             }
             nPlaMax = atoi(argv[globalUtilOptind]);
@@ -4519,6 +4528,20 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nPlaMax < 0 ) 
                 goto usage;
             break;
+        case 'R':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-R\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            RankCost = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( RankCost < 0 ) 
+                goto usage;
+            break;
+        case 'f':
+            fFastMode ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -4548,7 +4571,7 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // run the command
 //    pNtkRes = Abc_NtkXyz( pNtk, nPlaMax, 1, 0, fUseInvs, fVerbose );
-    pNtkRes = Abc_NtkPlayer( pNtk, nLutMax, nPlaMax, fVerbose );
+    pNtkRes = Abc_NtkPlayer( pNtk, nLutMax, nPlaMax, RankCost, fFastMode, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Command has failed.\n" );
@@ -4559,10 +4582,12 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: xyz [-L num] [-P num] [-vh]\n" );
+    fprintf( pErr, "usage: xyz [-L num] [-P num] [-R num] [-fvh]\n" );
     fprintf( pErr, "\t         specilized LUT/PLA decomposition\n" );
     fprintf( pErr, "\t-L num : maximum number of LUT inputs (2<=num<=8) [default = %d]\n", nLutMax );
     fprintf( pErr, "\t-P num : maximum number of PLA inputs/cubes (8<=num<=128) [default = %d]\n", nPlaMax );
+    fprintf( pErr, "\t-R num : maximum are of one decomposition rank [default = %d]\n", RankCost );
+    fprintf( pErr, "\t-f     : toggle using fast LUT mapping mode [default = %s]\n", fFastMode? "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;
@@ -4744,7 +4769,7 @@ int Abc_CommandIStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Command has failed.\n" );
-        return 1;
+        return 0;
     }
     // replace the current network
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
@@ -4886,7 +4911,7 @@ int Abc_CommandIRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Command has failed.\n" );
-        return 1;
+        return 0;
     }
     // replace the current network
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
@@ -4913,6 +4938,83 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandIRewriteSeq( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c, fUpdateLevel, fUseZeroCost, fVerbose;
+    extern Abc_Ntk_t * Abc_NtkIvyRewriteSeq( Abc_Ntk_t * pNtk, int fUseZeroCost, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fUpdateLevel = 1;
+    fUseZeroCost = 0;
+    fVerbose     = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "lzvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'l':
+            fUpdateLevel ^= 1;
+            break;
+        case 'z':
+            fUseZeroCost ^= 1;
+            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_NtkIsSeq(pNtk) )
+    {
+        fprintf( pErr, "Only works for non-sequential networks.\n" );
+        return 1;
+    }
+
+    pNtkRes = Abc_NtkIvyRewriteSeq( pNtk, fUseZeroCost, fVerbose );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Command has failed.\n" );
+        return 0;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: irws [-zvh]\n" );
+    fprintf( pErr, "\t         perform sequential AIG rewriting\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", fUseZeroCost? "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;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandIResyn( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
@@ -4959,7 +5061,7 @@ int Abc_CommandIResyn( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Command has failed.\n" );
-        return 1;
+        return 0;
     }
     // replace the current network
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
@@ -5915,11 +6017,12 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     int fRecovery;
     int fSwitching;
+    int fLatchPaths;
     int fVerbose;
     int nLutSize;
     float DelayTarget;
 
-    extern Abc_Ntk_t * Abc_NtkFpga( Abc_Ntk_t * pNtk, float DelayTarget, int fRecovery, int fSwitching, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkFpga( Abc_Ntk_t * pNtk, float DelayTarget, int fRecovery, int fSwitching, int fLatchPaths, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -5928,11 +6031,12 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     fRecovery   = 1;
     fSwitching  = 0;
+    fLatchPaths = 0;
     fVerbose    = 0;
     DelayTarget =-1;
     nLutSize    =-1;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "apvhDK" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "aplvhDK" ) ) != EOF )
     {
         switch ( c )
         {
@@ -5942,6 +6046,9 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'p':
             fSwitching ^= 1;
             break;
+        case 'l':
+            fLatchPaths ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -5989,7 +6096,13 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
     // create the new LUT library
     if ( nLutSize >= 3 && nLutSize <= 6 )
         Fpga_SetSimpleLutLib( nLutSize );
-
+/*
+    else
+    {
+        fprintf( pErr, "Cannot perform FPGA mapping with LUT size %d.\n", nLutSize );
+        return 1;
+    }
+*/
     if ( !Abc_NtkIsStrash(pNtk) )
     {
         // strash and balance the network
@@ -6008,7 +6121,7 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
         }
         fprintf( pOut, "The network was strashed and balanced before FPGA mapping.\n" );
         // get the new network
-        pNtkRes = Abc_NtkFpga( pNtk, DelayTarget, fRecovery, fSwitching, fVerbose );
+        pNtkRes = Abc_NtkFpga( pNtk, DelayTarget, fRecovery, fSwitching, fLatchPaths, fVerbose );
         if ( pNtkRes == NULL )
         {
             Abc_NtkDelete( pNtk );
@@ -6020,7 +6133,7 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
     else
     {
         // get the new network
-        pNtkRes = Abc_NtkFpga( pNtk, DelayTarget, fRecovery, fSwitching, fVerbose );
+        pNtkRes = Abc_NtkFpga( pNtk, DelayTarget, fRecovery, fSwitching, fLatchPaths, fVerbose );
         if ( pNtkRes == NULL )
         {
             fprintf( pErr, "FPGA mapping has failed.\n" );
@@ -6040,10 +6153,11 @@ usage:
         sprintf( LutSize, "library" );
     else
         sprintf( LutSize, "%d", nLutSize );
-    fprintf( pErr, "usage: fpga [-D float] [-K num] [-apvh]\n" );
+    fprintf( pErr, "usage: fpga [-D float] [-K num] [-aplvh]\n" );
     fprintf( pErr, "\t           performs FPGA mapping of the current network\n" );
     fprintf( pErr, "\t-a       : toggles area recovery [default = %s]\n", fRecovery? "yes": "no" );
     fprintf( pErr, "\t-p       : optimizes power by minimizing switching activity [default = %s]\n", fSwitching? "yes": "no" );
+    fprintf( pErr, "\t-l       : optimizes latch paths for delay, other paths for area [default = %s]\n", fLatchPaths? "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 [default = %s]%s\n", LutSize, (nLutSize == -1 ? " (type \"print_lut\")" : "") );
     fprintf( pErr, "\t-v       : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
diff --git a/src/base/abci/abcCut.c b/src/base/abci/abcCut.c
index 00045bf4..c7c164b9 100644
--- a/src/base/abci/abcCut.c
+++ b/src/base/abci/abcCut.c
@@ -32,6 +32,7 @@ static void Abc_NtkPrintCuts_( void * p, Abc_Ntk_t * pNtk, int fSeq );
 extern int nTotal, nGood, nEqual;
 
 static Vec_Int_t * Abc_NtkGetNodeAttributes( Abc_Ntk_t * pNtk );
+static int Abc_NtkComputeArea( Abc_Ntk_t * pNtk, Cut_Man_t * p );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -117,7 +118,9 @@ Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
     Extra_ProgressBarStop( pProgress );
     Vec_PtrFree( vNodes );
     Vec_IntFree( vChoices );
-PRT( "Total", clock() - clk );
+    Cut_ManPrintStats( p );
+PRT( "TOTAL ", clock() - clk );
+    printf( "Area = %d.\n", Abc_NtkComputeArea( pNtk, p ) );
 //Abc_NtkPrintCuts( p, pNtk, 0 );
 //    Cut_ManPrintStatsToFile( p, pNtk->pSpec, clock() - clk );
 
@@ -279,7 +282,8 @@ Cut_Man_t * Abc_NtkSeqCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
         pObj->fMarkC = 0;
 if ( pParams->fVerbose )
 {
-PRT( "Total", clock() - clk );
+    Cut_ManPrintStats( p );
+PRT( "TOTAL ", clock() - clk );
 printf( "Converged after %d iterations.\n", nIters );
 }
 //Abc_NtkPrintCuts( p, pNtk, 1 );
@@ -288,6 +292,27 @@ printf( "Converged after %d iterations.\n", nIters );
 
 /**Function*************************************************************
 
+  Synopsis    [Computes area.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkComputeArea( Abc_Ntk_t * pNtk, Cut_Man_t * p )
+{
+    Abc_Obj_t * pObj;
+    int Counter, i;
+    Counter = 0;
+    Abc_NtkForEachCo( pNtk, pObj, i )
+        Counter += Cut_ManMappingArea_rec( p, Abc_ObjFaninId0(pObj) );
+    return Counter;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Computes the cuts for the network.]
 
   Description []
@@ -479,21 +504,51 @@ void Abc_NtkPrintCuts_( void * p, Abc_Ntk_t * pNtk, int fSeq )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Abc_NtkGetNodeAttributes2( Abc_Ntk_t * pNtk ) 
+Vec_Int_t * Abc_NtkGetNodeAttributes( Abc_Ntk_t * pNtk ) 
 {
     Vec_Int_t * vAttrs;
-    Abc_Obj_t * pObj;
-    int i;
+//    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pObj;//, * pTemp;
+    int i;//, k;
+    int nNodesTotal = 0, nMffcsTotal = 0;
+    extern Vec_Ptr_t * Abc_NodeMffsInsideCollect( Abc_Obj_t * pNode );
 
     vAttrs = Vec_IntStart( Abc_NtkObjNumMax(pNtk) + 1 );
 //    Abc_NtkForEachCi( pNtk, pObj, i )
 //        Vec_IntWriteEntry( vAttrs, pObj->Id, 1 );
+
     Abc_NtkForEachObj( pNtk, pObj, i )
     {
+        if ( Abc_ObjIsNode(pObj) )
+            nNodesTotal++;
+        if ( Abc_ObjIsCo(pObj) && Abc_ObjIsNode(Abc_ObjFanin0(pObj)) )
+            nMffcsTotal += Abc_NodeMffcSize( Abc_ObjFanin0(pObj) );
 //        if ( Abc_ObjIsNode(pObj) && (rand() % 4 == 0) )
-        if ( Abc_ObjIsNode(pObj) && Abc_ObjFanoutNum(pObj) > 1 && !Abc_NodeIsMuxControlType(pObj) && (rand() % 3 == 0) )
-            Vec_IntWriteEntry( vAttrs, pObj->Id, 1 );
+//        if ( Abc_ObjIsNode(pObj) && Abc_ObjFanoutNum(pObj) > 1 && !Abc_NodeIsMuxControlType(pObj) && (rand() % 3 == 0) )
+        if ( Abc_ObjIsNode(pObj) && Abc_ObjFanoutNum(pObj) > 1 && !Abc_NodeIsMuxControlType(pObj) )
+        {
+            int nMffc = Abc_NodeMffcSize(pObj);
+            nMffcsTotal += Abc_NodeMffcSize(pObj);
+//            printf( "%d ", nMffc );
+
+            if ( nMffc > 2 || Abc_ObjFanoutNum(pObj) > 8 )
+                Vec_IntWriteEntry( vAttrs, pObj->Id, 1 );
+        }
     }
+/*
+    Abc_NtkForEachObj( pNtk, pObj, i )
+    {
+        if ( Vec_IntEntry( vAttrs, pObj->Id ) )
+        {
+            vNodes = Abc_NodeMffsInsideCollect( pObj );
+            Vec_PtrForEachEntry( vNodes, pTemp, k )
+                if ( pTemp != pObj )
+                    Vec_IntWriteEntry( vAttrs, pTemp->Id, 0 );
+            Vec_PtrFree( vNodes );
+        }
+    }
+*/
+    printf( "Total nodes = %d. Total MFFC nodes = %d.\n", nNodesTotal, nMffcsTotal );
     return vAttrs; 
 }
 
@@ -533,7 +588,7 @@ int Abc_NtkSubDagSize_rec( Abc_Obj_t * pObj, Vec_Int_t * vAttrs )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Abc_NtkGetNodeAttributes( Abc_Ntk_t * pNtk ) 
+Vec_Int_t * Abc_NtkGetNodeAttributes2( Abc_Ntk_t * pNtk ) 
 {
     Vec_Int_t * vAttrs;
     Abc_Obj_t * pObj;
diff --git a/src/base/abci/abcFpga.c b/src/base/abci/abcFpga.c
index 8ae0287c..a59ef2af 100644
--- a/src/base/abci/abcFpga.c
+++ b/src/base/abci/abcFpga.c
@@ -25,7 +25,7 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static Fpga_Man_t * Abc_NtkToFpga( Abc_Ntk_t * pNtk, int fRecovery, float * pSwitching, int fVerbose );
+static Fpga_Man_t * Abc_NtkToFpga( Abc_Ntk_t * pNtk, int fRecovery, float * pSwitching, int fLatchPaths, int fVerbose );
 static Abc_Ntk_t *  Abc_NtkFromFpga( Fpga_Man_t * pMan, Abc_Ntk_t * pNtk );
 static Abc_Obj_t *  Abc_NodeFromFpga_rec( Abc_Ntk_t * pNtkNew, Fpga_Node_t * pNodeFpga );
  
@@ -44,7 +44,7 @@ static Abc_Obj_t *  Abc_NodeFromFpga_rec( Abc_Ntk_t * pNtkNew, Fpga_Node_t * pNo
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkFpga( Abc_Ntk_t * pNtk, float DelayTarget, int fRecovery, int fSwitching, int fVerbose )
+Abc_Ntk_t * Abc_NtkFpga( Abc_Ntk_t * pNtk, float DelayTarget, int fRecovery, int fSwitching, int fLatchPaths, int fVerbose )
 {
     int fShowSwitching = 1;
     Abc_Ntk_t * pNtkNew;
@@ -68,11 +68,13 @@ Abc_Ntk_t * Abc_NtkFpga( Abc_Ntk_t * pNtk, float DelayTarget, int fRecovery, int
     }
 
     // perform FPGA mapping
-    pMan = Abc_NtkToFpga( pNtk, fRecovery, pSwitching, fVerbose );    
+    pMan = Abc_NtkToFpga( pNtk, fRecovery, pSwitching, fLatchPaths, fVerbose );    
     if ( pSwitching ) Vec_IntFree( vSwitching );
     if ( pMan == NULL )
         return NULL;
     Fpga_ManSetSwitching( pMan, fSwitching );
+    Fpga_ManSetLatchPaths( pMan, fLatchPaths );
+    Fpga_ManSetLatchNum( pMan, Abc_NtkLatchNum(pNtk) );
     Fpga_ManSetDelayTarget( pMan, DelayTarget );
     if ( !Fpga_Mapping( pMan ) )
     {
@@ -113,13 +115,14 @@ Abc_Ntk_t * Abc_NtkFpga( Abc_Ntk_t * pNtk, float DelayTarget, int fRecovery, int
   SeeAlso     []
 
 ***********************************************************************/
-Fpga_Man_t * Abc_NtkToFpga( Abc_Ntk_t * pNtk, int fRecovery, float * pSwitching, int fVerbose )
+Fpga_Man_t * Abc_NtkToFpga( Abc_Ntk_t * pNtk, int fRecovery, float * pSwitching, int fLatchPaths, int fVerbose )
 {
     Fpga_Man_t * pMan;
     ProgressBar * pProgress;
     Fpga_Node_t * pNodeFpga;
     Vec_Ptr_t * vNodes;
     Abc_Obj_t * pNode, * pFanin, * pPrev;
+    float * pfArrivals;
     int i;
 
     assert( Abc_NtkIsStrash(pNtk) );
@@ -130,7 +133,13 @@ Fpga_Man_t * Abc_NtkToFpga( Abc_Ntk_t * pNtk, int fRecovery, float * pSwitching,
         return NULL;
     Fpga_ManSetAreaRecovery( pMan, fRecovery );
     Fpga_ManSetOutputNames( pMan, Abc_NtkCollectCioNames(pNtk, 1) );
-    Fpga_ManSetInputArrivals( pMan, Abc_NtkGetCiArrivalFloats(pNtk) );
+    pfArrivals = Abc_NtkGetCiArrivalFloats(pNtk);
+    if ( fLatchPaths )
+    {
+        for ( i = 0; i < Abc_NtkPiNum(pNtk); i++ )
+            pfArrivals[i] = -FPGA_FLOAT_LARGE;
+    }
+    Fpga_ManSetInputArrivals( pMan, pfArrivals );
 
     // create PIs and remember them in the old nodes
     Abc_NtkCleanCopy( pNtk );
diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c
index 49b24be8..46f2cdf0 100644
--- a/src/base/abci/abcFraig.c
+++ b/src/base/abci/abcFraig.c
@@ -63,8 +63,8 @@ Abc_Ntk_t * Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes, int f
     // perform fraiging
     pMan = Abc_NtkToFraig( pNtk, pParams, fAllNodes, fExdc ); 
     // add algebraic choices
-    if ( pPars->fChoicing )
-        Fraig_ManAddChoices( pMan, 0, 6 );
+//    if ( pPars->fChoicing )
+//        Fraig_ManAddChoices( pMan, 0, 6 );
     // prove the miter if asked to
     if ( pPars->fTryProve )
         Fraig_ManProveMiter( pMan );
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
index 1ef84c20..a3ffcf4e 100644
--- a/src/base/abci/abcIvy.c
+++ b/src/base/abci/abcIvy.c
@@ -50,7 +50,7 @@ static inline Abc_Obj_t *  Abc_EdgeToNode( Abc_Ntk_t * p, Abc_Edge_t Edge )    {
 static inline Abc_Obj_t *  Abc_ObjFanin0Ivy( Abc_Ntk_t * p, Ivy_Obj_t * pObj ) { return Abc_ObjNotCond( Abc_EdgeToNode(p, Ivy_ObjFanin0(pObj)->TravId), Ivy_ObjFaninC0(pObj) ); }
 static inline Abc_Obj_t *  Abc_ObjFanin1Ivy( Abc_Ntk_t * p, Ivy_Obj_t * pObj ) { return Abc_ObjNotCond( Abc_EdgeToNode(p, Ivy_ObjFanin1(pObj)->TravId), Ivy_ObjFaninC1(pObj) ); }
 
-static int * Abc_NtkCollectLatchValues( Abc_Ntk_t * pNtk );
+static int * Abc_NtkCollectLatchValues( Abc_Ntk_t * pNtk, int fUseDcs );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -67,7 +67,7 @@ static int * Abc_NtkCollectLatchValues( Abc_Ntk_t * pNtk );
   SeeAlso     []
 
 ***********************************************************************/
-Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq )
+Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq, int fUseDc )
 {
     Ivy_Man_t * pMan;
     int fCleanup = 1;
@@ -101,7 +101,7 @@ Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq )
     if ( fSeq )
     {
         int nLatches = Abc_NtkLatchNum(pNtk);
-        int * pInit = Abc_NtkCollectLatchValues( pNtk );
+        int * pInit = Abc_NtkCollectLatchValues( pNtk, fUseDc );
         Ivy_ManMakeSeq( pMan, nLatches, pInit );
         FREE( pInit );
 //        Ivy_ManPrintStats( pMan );
@@ -160,7 +160,7 @@ Abc_Ntk_t * Abc_NtkIvyStrash( Abc_Ntk_t * pNtk )
 {
     Abc_Ntk_t * pNtkAig;
     Ivy_Man_t * pMan;
-    pMan = Abc_NtkIvyBefore( pNtk, 1 );
+    pMan = Abc_NtkIvyBefore( pNtk, 1, 0 );
     if ( pMan == NULL )
         return NULL;
     pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1 );
@@ -183,7 +183,7 @@ void Abc_NtkIvyCuts( Abc_Ntk_t * pNtk, int nInputs )
 {
     extern void Ivy_CutComputeAll( Ivy_Man_t * p, int nInputs );
     Ivy_Man_t * pMan;
-    pMan = Abc_NtkIvyBefore( pNtk, 1 );
+    pMan = Abc_NtkIvyBefore( pNtk, 1, 0 );
     if ( pMan == NULL )
         return;
     Ivy_CutComputeAll( pMan, nInputs );
@@ -205,7 +205,7 @@ Abc_Ntk_t * Abc_NtkIvyRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeroC
 {
     Abc_Ntk_t * pNtkAig;
     Ivy_Man_t * pMan;
-    pMan = Abc_NtkIvyBefore( pNtk, 0 );
+    pMan = Abc_NtkIvyBefore( pNtk, 0, 0 );
     if ( pMan == NULL )
         return NULL;
     Ivy_ManRewritePre( pMan, fUpdateLevel, fUseZeroCost, fVerbose );
@@ -225,11 +225,35 @@ Abc_Ntk_t * Abc_NtkIvyRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeroC
   SeeAlso     []
 
 ***********************************************************************/
+Abc_Ntk_t * Abc_NtkIvyRewriteSeq( Abc_Ntk_t * pNtk, int fUseZeroCost, int fVerbose )
+{
+    Abc_Ntk_t * pNtkAig;
+    Ivy_Man_t * pMan;
+    pMan = Abc_NtkIvyBefore( pNtk, 1, 1 );
+    if ( pMan == NULL )
+        return NULL;
+    Ivy_ManRewriteSeq( pMan, fUseZeroCost, fVerbose );
+    pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1 );
+    Ivy_ManStop( pMan );
+    return pNtkAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Abc_Ntk_t * Abc_NtkIvyResyn( Abc_Ntk_t * pNtk, int fUpdateLevel, int fVerbose )
 {
     Abc_Ntk_t * pNtkAig;
     Ivy_Man_t * pMan, * pTemp;
-    pMan = Abc_NtkIvyBefore( pNtk, 0 );
+    pMan = Abc_NtkIvyBefore( pNtk, 0, 0 );
     if ( pMan == NULL )
         return NULL;
     pMan = Ivy_ManResyn( pTemp = pMan, fUpdateLevel, fVerbose );
@@ -253,11 +277,11 @@ Abc_Ntk_t * Abc_NtkIvyResyn( Abc_Ntk_t * pNtk, int fUpdateLevel, int fVerbose )
 Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk )
 {
     Abc_Ntk_t * pNtkAig;
-    Ivy_Man_t * pMan, * pTemp;
+    Ivy_Man_t * pMan;//, * pTemp;
     int fCleanup = 1;
     int nNodes;
     int nLatches = Abc_NtkLatchNum(pNtk);
-    int * pInit = Abc_NtkCollectLatchValues( pNtk );
+    int * pInit = Abc_NtkCollectLatchValues( pNtk, 0 );
 
     assert( !Abc_NtkIsNetlist(pNtk) );
     assert( !Abc_NtkIsSeq(pNtk) );
@@ -304,7 +328,7 @@ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk )
 //    pMan = Ivy_ManResyn( pTemp = pMan, 1, 0 );
 //    Ivy_ManStop( pTemp );
 
-    Ivy_ManTestCutsAll( pMan );
+//    Ivy_ManTestCutsAll( pMan );
 
 //    Ivy_ManPrintStats( pMan );
 
@@ -319,6 +343,10 @@ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk )
 
 //    Ivy_ManRequiredLevels( pMan );
 
+    Pla_ManFastLutMap( pMan, 8 );
+    Ivy_ManStop( pMan );
+    return NULL;
+/*
     // convert from the AIG manager
     pNtkAig = Abc_NtkFromAig( pNtk, pMan );
 //    pNtkAig = Abc_NtkFromAigSeq( pNtk, pMan );
@@ -341,6 +369,7 @@ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk )
 
     FREE( pInit );
     return pNtkAig;
+*/
 }
 
 
@@ -717,14 +746,14 @@ Ivy_Obj_t * Abc_NodeStrashAigFactorAig( Ivy_Man_t * pMan, Abc_Obj_t * pRoot, cha
   SeeAlso     []
 
 ***********************************************************************/
-int * Abc_NtkCollectLatchValues( Abc_Ntk_t * pNtk )
+int * Abc_NtkCollectLatchValues( Abc_Ntk_t * pNtk, int fUseDcs )
 {
     Abc_Obj_t * pLatch;
     int * pArray, i;
     pArray = ALLOC( int, Abc_NtkLatchNum(pNtk) );
     Abc_NtkForEachLatch( pNtk, pLatch, i )
     {
-        if ( Abc_LatchIsInitDc(pLatch) )
+        if ( fUseDcs || Abc_LatchIsInitDc(pLatch) )
             pArray[i] = IVY_INIT_DC;
         else if ( Abc_LatchIsInit1(pLatch) )
             pArray[i] = IVY_INIT_1;
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index 0124d7bf..cb32def5 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -300,6 +300,7 @@ void Abc_NtkPrintFanio( FILE * pFile, Abc_Ntk_t * pNtk )
             nFanouts = Abc_ObjFanoutNum( Abc_ObjFanout0(pNode) );
         else
             nFanouts = Abc_ObjFanoutNum(pNode);
+//            nFanouts = Abc_NodeMffcSize(pNode);
         if ( nFanins > vFanins->nSize || nFanouts > vFanouts->nSize )
         {
             nOldSize = vFanins->nSize;
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index b21278f7..f447516f 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -396,6 +396,26 @@ void Abc_NtkCollectSupergate( Abc_Obj_t * pNode, int fStopAtMux, Vec_Ptr_t * vNo
 
 /**Function*************************************************************
 
+  Synopsis    [Computes the factor of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkNodeFactor( Abc_Obj_t * pObj, int nLevelMax )
+{
+//  nLevelMax = ((nLevelMax)/2)*3;
+    assert( pObj->Level <= nLevelMax );
+//    return (int)(100000000.0 * pow(0.999, nLevelMax - pObj->Level));
+    return (int)(100000000.0 * (1 + 0.01 * pObj->Level));
+//    return (int)(100000000.0 / ((nLevelMax)/2)*3 - pObj->Level);
+}
+
+/**Function*************************************************************
+
   Synopsis    [Sets up the SAT solver.]
 
   Description []
@@ -409,11 +429,13 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront )
 {
     Abc_Obj_t * pNode, * pFanin, * pNodeC, * pNodeT, * pNodeE;
     Vec_Ptr_t * vNodes, * vSuper;
+//    Vec_Int_t * vLevels;
     Vec_Int_t * vVars, * vFanio;
     Vec_Vec_t * vCircuit;
     int i, k, fUseMuxes = 1;
     int clk1 = clock(), clk;
     int fOrderCiVarsFirst = 0;
+    int nLevelsMax = Abc_AigGetLevelNum(pNtk);
 
     assert( Abc_NtkIsStrash(pNtk) );
 
@@ -422,9 +444,9 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront )
         pNode->pCopy = NULL;
 
     // start the data structures
-    vNodes = Vec_PtrAlloc( 1000 );   // the nodes corresponding to vars in the solver
-    vSuper = Vec_PtrAlloc( 100 );    // the nodes belonging to the given implication supergate
-    vVars  = Vec_IntAlloc( 100 );    // the temporary array for variables in the clause
+    vNodes  = Vec_PtrAlloc( 1000 );   // the nodes corresponding to vars in the solver
+    vSuper  = Vec_PtrAlloc( 100 );    // the nodes belonging to the given implication supergate
+    vVars   = Vec_IntAlloc( 100 );    // the temporary array for variables in the clause
     if ( fJFront )
         vCircuit = Vec_VecAlloc( 1000 );
 //        vCircuit = Vec_VecStart( 184 );
@@ -565,7 +587,16 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront )
 //        Asat_JManStop( pSat );
 //    PRT( "Total", clock() - clk1 );
     }
-
+/*
+    // create factors
+    vLevels = Vec_IntStart( Vec_PtrSize(vNodes) );   // the reverse levels of the nodes
+    Abc_NtkForEachObj( pNtk, pNode, i )
+        if ( pNode->fMarkA )
+            Vec_IntWriteEntry( vLevels, (int)pNode->pCopy, Abc_NtkNodeFactor(pNode, nLevelsMax) );
+    assert( Vec_PtrSize(vNodes) == Vec_IntSize(vLevels) );
+    Asat_SolverSetFactors( pSat, Vec_IntReleaseArray(vLevels) );
+    Vec_IntFree( vLevels );
+*/
     // delete
     Vec_IntFree( vVars );
     Vec_PtrFree( vNodes );
diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c
index 39aebc83..ecf77f70 100644
--- a/src/base/main/mainFrame.c
+++ b/src/base/main/mainFrame.c
@@ -136,9 +136,11 @@ void Abc_FrameDeallocate( Abc_Frame_t * p )
 {
     extern void Rwt_ManGlobalStop();
     extern void undefine_cube_size();
+    extern void Ivy_TruthManStop();
 //    Abc_HManStop();
     undefine_cube_size();
     Rwt_ManGlobalStop();
+    Ivy_TruthManStop();
     if ( p->pManDec ) Dec_ManStop( p->pManDec );
     if ( p->dd )      Extra_StopManager( p->dd );
     Abc_FrameDeleteAllNetworks( p );