Version abc90329

9 files changed, 449 insertions, 114 deletions

diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c
index 758bc1e2..df46fc06 100644
--- a/src/base/abc/abcFunc.c
+++ b/src/base/abc/abcFunc.c
@@ -595,6 +595,7 @@ Hop_Obj_t * Abc_ConvertSopToAigInternal( Hop_Man_t * pMan, char * pSop )
     Hop_Obj_t * pAnd, * pSum;
     int i, Value, nFanins;
     char * pCube;
+    int fExor = Abc_SopIsExorType(pSop);
     // get the number of variables
     nFanins = Abc_SopGetVarNum(pSop);
     // go through the cubes of the node's SOP
@@ -611,7 +612,10 @@ Hop_Obj_t * Abc_ConvertSopToAigInternal( Hop_Man_t * pMan, char * pSop )
                 pAnd = Hop_And( pMan, pAnd, Hop_Not(Hop_IthVar(pMan,i)) );
         }
         // add to the sum of cubes
-        pSum = Hop_Or( pMan, pSum, pAnd );
+        if ( fExor )
+            pSum = Hop_Exor( pMan, pSum, pAnd );
+        else
+            pSum = Hop_Or( pMan, pSum, pAnd );
     }
     // decide whether to complement the result
     if ( Abc_SopIsComplement(pSop) )
@@ -637,11 +641,8 @@ Hop_Obj_t * Abc_ConvertSopToAig( Hop_Man_t * pMan, char * pSop )
     // consider the constant node
     if ( Abc_SopGetVarNum(pSop) == 0 )
         return Hop_NotCond( Hop_ManConst1(pMan), Abc_SopIsConst0(pSop) );
-    // consider the special case of EXOR function
-    if ( Abc_SopIsExorType(pSop) )
-        return Hop_NotCond( Hop_CreateExor(pMan, Abc_SopGetVarNum(pSop)), Abc_SopIsComplement(pSop) );
     // decide when to use factoring
-    if ( fUseFactor && Abc_SopGetVarNum(pSop) > 2 && Abc_SopGetCubeNum(pSop) > 1 )
+    if ( fUseFactor && Abc_SopGetVarNum(pSop) > 2 && Abc_SopGetCubeNum(pSop) > 1 && !Abc_SopIsExorType(pSop) )
         return Dec_GraphFactorSop( pMan, pSop );
     return Abc_ConvertSopToAigInternal( pMan, pSop );
 }
diff --git a/src/base/abc/abcLib.c b/src/base/abc/abcLib.c
index 850e59e0..138dc9a1 100644
--- a/src/base/abc/abcLib.c
+++ b/src/base/abc/abcLib.c
@@ -82,6 +82,8 @@ void Abc_LibFree( Abc_Lib_t * pLib, Abc_Ntk_t * pNtkSave )
                 continue;
 //            pNtk->pManFunc = NULL;
             pNtk->pDesign = NULL;
+            if ( pNtk->pManFunc == pNtkSave->pManFunc )
+                pNtk->pManFunc = NULL;
             Abc_NtkDelete( pNtk );
         }
         Vec_PtrFree( pLib->vModules );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index cf574ecb..876266af 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -128,7 +128,7 @@ static int Abc_CommandCareSet        ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandCut            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandEspresso       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandGen            ( Abc_Frame_t * pAbc, int argc, char ** argv );
-//static int Abc_CommandXyz            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandCover          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDouble         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandInter          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTest           ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -297,6 +297,9 @@ static int Abc_CommandAbc9Retime     ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandAbc9Enable     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Miter      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Scl        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Lcorr      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Scorr      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Choice     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Sat        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Fraig      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Srm        ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -448,7 +451,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Various",      "cut",           Abc_CommandCut,              0 );
     Cmd_CommandAdd( pAbc, "Various",      "espresso",      Abc_CommandEspresso,         1 );
     Cmd_CommandAdd( pAbc, "Various",      "gen",           Abc_CommandGen,              0 );
-//    Cmd_CommandAdd( pAbc, "Various",      "xyz",           Abc_CommandXyz,              1 );
+    Cmd_CommandAdd( pAbc, "Various",      "cover",         Abc_CommandCover,            1 );
     Cmd_CommandAdd( pAbc, "Various",      "double",        Abc_CommandDouble,           1 );
     Cmd_CommandAdd( pAbc, "Various",      "inter",         Abc_CommandInter,            1 );
     Cmd_CommandAdd( pAbc, "Various",      "test",          Abc_CommandTest,             0 );
@@ -610,6 +613,9 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "AIG",          "&enable",       Abc_CommandAbc9Enable,       0 );
     Cmd_CommandAdd( pAbc, "AIG",          "&miter",        Abc_CommandAbc9Miter,        0 );
     Cmd_CommandAdd( pAbc, "AIG",          "&scl",          Abc_CommandAbc9Scl,          0 );
+    Cmd_CommandAdd( pAbc, "AIG",          "&lcorr",        Abc_CommandAbc9Lcorr,        0 );
+    Cmd_CommandAdd( pAbc, "AIG",          "&scorr",        Abc_CommandAbc9Scorr,        0 );
+    Cmd_CommandAdd( pAbc, "AIG",          "&choice",       Abc_CommandAbc9Choice,       0 );
     Cmd_CommandAdd( pAbc, "AIG",          "&sat",          Abc_CommandAbc9Sat,          0 );
     Cmd_CommandAdd( pAbc, "AIG",          "&fraig",        Abc_CommandAbc9Fraig,        0 );
     Cmd_CommandAdd( pAbc, "AIG",          "&srm",          Abc_CommandAbc9Srm,          0 );
@@ -7575,7 +7581,7 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: cut [-K num] [-M num] [-tfdxyzamjvh]\n" );
+    fprintf( pErr, "usage: cut [-K num] [-M num] [-tfdcovamjvh]\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 );
@@ -7785,6 +7791,7 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fMesh;
     int fFpga;
     int fOneHot;
+    int fRandom;
     int fVerbose;
     char * FileName;
     extern void Abc_GenAdder( char * pFileName, int nVars );
@@ -7792,7 +7799,7 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern void Abc_GenMesh( char * pFileName, int nVars );
     extern void Abc_GenFpga( char * pFileName, int nLutSize, int nLuts, int nVars );
     extern void Abc_GenOneHot( char * pFileName, int nVars );
-
+    extern void Abc_GenRandom( char * pFileName, int nPis );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -7805,9 +7812,10 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
     fMesh = 0;
     fFpga = 0;
     fOneHot = 0;
+    fRandom = 0;
     fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Nasmftvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Nasmftrvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -7837,6 +7845,9 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 't':
             fOneHot ^= 1;
             break;
+        case 'r':
+            fRandom ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -7866,12 +7877,14 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
 //        Abc_GenFpga( FileName, 3, 2, 5 );
     else if ( fOneHot )
         Abc_GenOneHot( FileName, nVars );
+    else if ( fRandom )
+        Abc_GenRandom( FileName, nVars );
     else
         printf( "Type of circuit is not specified.\n" );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: gen [-N num] [-asmftvh] <file>\n" );
+    fprintf( pErr, "usage: gen [-N num] [-asmftrvh] <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     : generate ripple-carry adder [default = %s]\n", fAdder? "yes": "no" );  
@@ -7879,13 +7892,13 @@ usage:
     fprintf( pErr, "\t-m     : generate a mesh [default = %s]\n", fMesh? "yes": "no" );  
     fprintf( pErr, "\t-f     : generate a LUT FPGA structure [default = %s]\n", fFpga? "yes": "no" );  
     fprintf( pErr, "\t-t     : generate one-hotness conditions [default = %s]\n", fOneHot? "yes": "no" );  
+    fprintf( pErr, "\t-r     : generate random single-output function [default = %s]\n", fRandom? "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");
     return 1;
 }
 
-
 /**Function*************************************************************
 
   Synopsis    []
@@ -7897,79 +7910,52 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandCover( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
-    Abc_Ntk_t * pNtk, * pNtkRes;//, * pNtkTemp;
+    Abc_Ntk_t * pNtk, * pNtkRes;
     int c;
-    int nLutMax;
-    int nPlaMax;
-    int RankCost;
-    int fFastMode;
-    int fRewriting;
-    int fSynthesis;
     int fVerbose;
-//    extern Abc_Ntk_t * Abc_NtkXyz( Abc_Ntk_t * pNtk, int nPlaMax, bool fEsop, bool fSop, bool fInvs, bool fVerbose );
-    extern void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int RankCost, int fFastMode, int fRewriting, int fSynthesis, int fVerbose );
+    int fUseSop;
+    int fUseEsop;
+    int fUseInvs;
+    int nFaninMax;
+    extern Abc_Ntk_t * Abc_NtkSopEsopCover( Abc_Ntk_t * pNtk, int nFaninMax, bool fUseEsop, bool fUseSop, bool fUseInvs, bool fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    nLutMax    = 8;
-    nPlaMax    = 128;
-    RankCost   = 96000;
-    fFastMode  = 1;
-    fRewriting = 0;
-    fSynthesis = 0;
-    fVerbose   = 0;
+    fUseSop   =  1;
+    fUseEsop  =  0;
+    fVerbose  =  0;
+    fUseInvs  =  1;
+    nFaninMax =  8;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "LPRfrsvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Nsxivh" ) ) != EOF )
     {
         switch ( c )
         {
-        case 'L':
-            if ( globalUtilOptind >= argc )
-            {
-                fprintf( pErr, "Command line switch \"-L\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            nLutMax = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( nLutMax < 0 ) 
-                goto usage;
-            break;
-        case 'P':
-            if ( globalUtilOptind >= argc )
-            {
-                fprintf( pErr, "Command line switch \"-P\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            nPlaMax = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( nPlaMax < 0 ) 
-                goto usage;
-            break;
-        case 'R':
+        case 'N':
             if ( globalUtilOptind >= argc )
             {
-                fprintf( pErr, "Command line switch \"-R\" should be followed by an integer.\n" );
+                fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
                 goto usage;
             }
-            RankCost = atoi(argv[globalUtilOptind]);
+            nFaninMax = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( RankCost < 0 ) 
+            if ( nFaninMax < 0 ) 
                 goto usage;
             break;
-        case 'f':
-            fFastMode ^= 1;
+        case 's':
+            fUseSop ^= 1;
             break;
-        case 'r':
-            fRewriting ^= 1;
+        case 'x':
+            fUseEsop ^= 1;
             break;
-        case 's':
-            fSynthesis ^= 1;
+        case 'i':
+            fUseInvs ^= 1;
             break;
         case 'v':
             fVerbose ^= 1;
@@ -7991,26 +7977,9 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Only works for strashed networks.\n" );
         return 1;
     }
-/*
-    if ( nLutMax < 2 || nLutMax > 12 || nPlaMax < 8 || nPlaMax > 128  )
-    {
-        fprintf( pErr, "Incorrect LUT/PLA parameters.\n" );
-        return 1;
-    }
-*/
+
     // run the command
-//    pNtkRes = Abc_NtkXyz( pNtk, nPlaMax, 1, 0, fInvs, fVerbose );
-/*
-    if ( !Abc_NtkIsStrash(pNtk) )
-    {
-        pNtkTemp = Abc_NtkStrash( pNtk, 0, 1, 0 );
-        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;
+    pNtkRes = Abc_NtkSopEsopCover( pNtk, nFaninMax, fUseEsop, fUseSop, fUseInvs, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Command has failed.\n" );
@@ -8021,20 +7990,17 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: xyz [-L num] [-P num] [-R num] [-frsvh]\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-r     : toggle using one pass of AIG rewriting [default = %s]\n", fRewriting? "yes": "no" );
-    fprintf( pErr, "\t-s     : toggle using synthesis by AIG rewriting [default = %s]\n", fSynthesis? "yes": "no" );
+    fprintf( pErr, "usage: cover [-N num] [-sxvh]\n" );
+    fprintf( pErr, "\t         decomposition into a network of SOP/ESOP PLAs\n" );
+    fprintf( pErr, "\t-N num : maximum number of inputs [default = %d]\n", nFaninMax );
+    fprintf( pErr, "\t-s     : toggle the use of SOPs [default = %s]\n", fUseSop? "yes": "no" );
+    fprintf( pErr, "\t-x     : toggle the use of ESOPs [default = %s]\n", fUseEsop? "yes": "no" );
+//    fprintf( pErr, "\t-i     : toggle the use of interters [default = %s]\n", fUseInvs? "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;
 }
 
-
 /**Function*************************************************************
 
   Synopsis    []
@@ -21930,11 +21896,15 @@ usage:
 int Abc_CommandAbc9Ps( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     int c;
+    int fSwitch = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "ph" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'p':
+            fSwitch ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -21946,12 +21916,13 @@ int Abc_CommandAbc9Ps( Abc_Frame_t * pAbc, int argc, char ** argv )
         printf( "Abc_CommandAbc9Ps(): There is no AIG.\n" );
         return 1;
     } 
-    Gia_ManPrintStats( pAbc->pAig );
+    Gia_ManPrintStats( pAbc->pAig, fSwitch );
     return 0;
 
 usage:
-    fprintf( stdout, "usage: &ps [-h]\n" );
+    fprintf( stdout, "usage: &ps [-ph]\n" );
     fprintf( stdout, "\t        prints stats of the current AIG\n" );
+    fprintf( stdout, "\t-p    : toggle printing switching activity [default = %s]\n", fSwitch? "yes": "no" );
     fprintf( stdout, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -22393,11 +22364,23 @@ int Abc_CommandAbc9Dfs( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Gia_Man_t * pTemp;
     int c;
+    int fNormal  = 0;
+    int fReverse = 0;
+    int fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "nrvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'n':
+            fNormal ^= 1;
+            break;
+        case 'r':
+            fReverse ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -22409,13 +22392,33 @@ int Abc_CommandAbc9Dfs( Abc_Frame_t * pAbc, int argc, char ** argv )
         printf( "Abc_CommandAbc9Dfs(): There is no AIG.\n" );
         return 1;
     } 
-    pAbc->pAig = Gia_ManDupDfs( pTemp = pAbc->pAig );
+    if ( fNormal )
+    {
+        pAbc->pAig = Gia_ManDupOrderAiger( pTemp = pAbc->pAig );
+        if ( fVerbose )
+            printf( "AIG objects are reordered as follows: CIs, ANDs, COs.\n" );
+    }
+    else if ( fReverse )
+    {
+        pAbc->pAig = Gia_ManDupOrderDfsReverse( pTemp = pAbc->pAig );
+        if ( fVerbose )
+            printf( "AIG objects are reordered in the reserve DFS order.\n" );
+    }
+    else 
+    {
+        pAbc->pAig = Gia_ManDupOrderDfs( pTemp = pAbc->pAig );
+        if ( fVerbose )
+            printf( "AIG objects are reordered in the DFS order.\n" );
+    }
     Gia_ManStop( pTemp );
     return 0;
 
 usage:
-    fprintf( stdout, "usage: &dfs [-h]\n" );
+    fprintf( stdout, "usage: &dfs [-nrvh]\n" );
     fprintf( stdout, "\t        orders objects in the DFS order\n" );
+    fprintf( stdout, "\t-n    : toggle using normalized ordering [default = %s]\n", fNormal? "yes": "no" );
+    fprintf( stdout, "\t-r    : toggle using reverse DFS ordering [default = %s]\n", fReverse? "yes": "no" );
+    fprintf( stdout, "\t-v    : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( stdout, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -23218,14 +23221,258 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc9Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Cec_ParCor_t Pars, * pPars = &Pars;
+    Gia_Man_t * pTemp;
+    int c;
+    Cec_ManCorSetDefaultParams( pPars );
+    pPars->fLatchCorr = 1;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FCfrcvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nFrames = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nFrames < 0 ) 
+                goto usage;
+            break;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nBTLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nBTLimit < 0 ) 
+                goto usage;
+            break;
+        case 'f':
+            pPars->fFirstStop ^= 1;
+            break;
+        case 'r':
+            pPars->fUseRings ^= 1;
+            break;
+        case 'c':
+            pPars->fUseCSat ^= 1;
+            break;
+        case 'v':
+            pPars->fVerbose ^= 1;
+            break;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pAig == NULL )
+    {
+        printf( "Abc_CommandAbc9Lcorr(): There is no AIG.\n" );
+        return 1;
+    } 
+    pAbc->pAig = Cec_ManLSCorrespondence( pTemp = pAbc->pAig, pPars );
+    if ( pAbc->pAig == NULL )
+    {
+        pAbc->pAig = pTemp;
+        printf( "Abc_CommandAbc9Lcorr(): Command has failed.\n" );
+    }
+    else 
+        Gia_ManStop( pTemp );
+    return 0;
+
+usage:
+    fprintf( stdout, "usage: &lcorr [-FC num] [-frcvh]\n" );
+    fprintf( stdout, "\t         performs latch correpondence computation\n" );
+    fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
+    fprintf( stdout, "\t-F num : the number of timeframes in inductive case [default = %d]\n", pPars->nFrames );
+    fprintf( stdout, "\t-f     : toggle quitting when one PO is asserted [default = %s]\n", pPars->fFirstStop? "yes": "no" );
+    fprintf( stdout, "\t-r     : toggle using implication rings for equivalence classes [default = %s]\n", pPars->fUseRings? "yes": "no" );
+    fprintf( stdout, "\t-c     : toggle using circuit-based SAT solver [default = %s]\n", pPars->fUseCSat? "yes": "no" );
+    fprintf( stdout, "\t-v     : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
+    fprintf( stdout, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Cec_ParCor_t Pars, * pPars = &Pars;
+    Gia_Man_t * pTemp;
+    int c;
+    Cec_ManCorSetDefaultParams( pPars );
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FCfrcvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nFrames = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nFrames < 0 ) 
+                goto usage;
+            break;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nBTLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nBTLimit < 0 ) 
+                goto usage;
+            break;
+        case 'f':
+            pPars->fFirstStop ^= 1;
+            break;
+        case 'r':
+            pPars->fUseRings ^= 1;
+            break;
+        case 'c':
+            pPars->fUseCSat ^= 1;
+            break;
+        case 'v':
+            pPars->fVerbose ^= 1;
+            break;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pAig == NULL )
+    {
+        printf( "Abc_CommandAbc9Scorr(): There is no AIG.\n" );
+        return 1;
+    } 
+    pAbc->pAig = Cec_ManLSCorrespondence( pTemp = pAbc->pAig, pPars );
+    if ( pAbc->pAig == NULL )
+    {
+        pAbc->pAig = pTemp;
+        printf( "Abc_CommandAbc9Scorr(): Command has failed.\n" );
+    }
+    else 
+        Gia_ManStop( pTemp );
+    return 0;
+
+usage:
+    fprintf( stdout, "usage: &scorr [-FC num] [-frcvh]\n" );
+    fprintf( stdout, "\t         performs signal correpondence computation\n" );
+    fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
+    fprintf( stdout, "\t-F num : the number of timeframes in inductive case [default = %d]\n", pPars->nFrames );
+    fprintf( stdout, "\t-f     : toggle quitting when one PO is asserted [default = %s]\n", pPars->fFirstStop? "yes": "no" );
+    fprintf( stdout, "\t-r     : toggle using implication rings for equivalence classes [default = %s]\n", pPars->fUseRings? "yes": "no" );
+    fprintf( stdout, "\t-c     : toggle using circuit-based SAT solver [default = %s]\n", pPars->fUseCSat? "yes": "no" );
+    fprintf( stdout, "\t-v     : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
+    fprintf( stdout, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9Choice( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Cec_ParChc_t Pars, * pPars = &Pars;
+    Gia_Man_t * pTemp;
+    int c;
+    Cec_ManChcSetDefaultParams( pPars );
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Cvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nBTLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nBTLimit < 0 ) 
+                goto usage;
+            break;
+        case 'v':
+            pPars->fVerbose ^= 1;
+            break;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pAig == NULL )
+    {
+        printf( "Abc_CommandAbc9Choice(): There is no AIG.\n" );
+        return 1;
+    } 
+    printf("The command is not yet ready.\n" );
+    return 0;
+    pAbc->pAig = Cec_ManChoiceComputation( pTemp = pAbc->pAig, pPars );
+    if ( pAbc->pAig == NULL )
+    {
+        pAbc->pAig = pTemp;
+        printf( "Abc_CommandAbc9Choice(): Command has failed.\n" );
+    }
+    else 
+        Gia_ManStop( pTemp );
+    return 0;
+
+usage:
+    fprintf( stdout, "usage: &choice [-C num] [-vh]\n" );
+    fprintf( stdout, "\t         performs computation of structural choices\n" );
+    fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
+    fprintf( stdout, "\t-v     : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
+    fprintf( stdout, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Cec_ParSat_t ParsSat, * pPars = &ParsSat;
     Gia_Man_t * pTemp;
     int c;
+    int fCSat = 0;
     Cec_ManSatSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "CSNmfvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CSNmfcvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -23268,6 +23515,9 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'f':
             pPars->fFirstStop ^= 1;
             break;
+        case 'c':
+            fCSat ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -23280,18 +23530,30 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
         printf( "Abc_CommandAbc9Sat(): There is no AIG.\n" );
         return 1;
     } 
-    pAbc->pAig = Cec_ManSatSolving( pTemp = pAbc->pAig, pPars );
-    Gia_ManStop( pTemp );
+    if ( fCSat )
+    {
+        Vec_Int_t * vCounters;
+        Vec_Str_t * vStatus;
+        vCounters = Cbs_ManSolveMiter( pAbc->pAig, 10*pPars->nBTLimit, &vStatus );
+        Vec_IntFree( vCounters );
+        Vec_StrFree( vStatus );
+    }
+    else
+    {
+        pAbc->pAig = Cec_ManSatSolving( pTemp = pAbc->pAig, pPars );
+        Gia_ManStop( pTemp );
+    }
     return 0;
 
 usage:
-    fprintf( stdout, "usage: &sat [-CSN <num>] [-mfvh]\n" );
+    fprintf( stdout, "usage: &sat [-CSN <num>] [-mfcvh]\n" );
     fprintf( stdout, "\t         performs SAT solving for the combinational outputs\n" );
     fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
     fprintf( stdout, "\t-S num : the min number of variables to recycle the solver [default = %d]\n", pPars->nSatVarMax );
     fprintf( stdout, "\t-N num : the min number of calls to recycle the solver [default = %d]\n", pPars->nCallsRecycle );
     fprintf( stdout, "\t-m     : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "yes": "no" );
     fprintf( stdout, "\t-f     : toggle quitting when one PO is asserted [default = %s]\n", pPars->fFirstStop? "yes": "no" );
+    fprintf( stdout, "\t-c     : toggle using circuit-based SAT solver [default = %s]\n", fCSat? "yes": "no" );
     fprintf( stdout, "\t-v     : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
     fprintf( stdout, "\t-h     : print the command usage\n");
     return 1;
@@ -23545,7 +23807,11 @@ int Abc_CommandAbc9Reduce( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( pAbc->pAig == NULL )
         pAbc->pAig = pTemp;
     else
+    {
         Gia_ManStop( pTemp );
+        pAbc->pAig = Gia_ManSeqStructSweep( pTemp = pAbc->pAig, 1, 1, 0 );
+        Gia_ManStop( pTemp );
+    }
     return 0;
 
 usage:
diff --git a/src/base/abci/abcGen.c b/src/base/abci/abcGen.c
index e40c21d6..f6111dfd 100644
--- a/src/base/abci/abcGen.c
+++ b/src/base/abci/abcGen.c
@@ -599,6 +599,56 @@ void Abc_GenOneHotIntervals( char * pFileName, int nPis, int nRegs, Vec_Ptr_t *
     fclose( pFile );
 }
 
+#include "aig.h"
+
+/**Function*************************************************************
+
+  Synopsis    [Generates structure of L K-LUTs implementing an N-var function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_GenRandom( char * pFileName, int nPis )
+{
+    FILE * pFile;
+    unsigned * pTruth;
+    int i, b, w, nWords = Aig_TruthWordNum( nPis );
+    int nDigitsIn;
+    Aig_ManRandom( 1 );
+    pTruth = ABC_ALLOC( unsigned, nWords );
+    for ( w = 0; w < nWords; w++ )
+        pTruth[w] = Aig_ManRandom( 0 );
+    pFile = fopen( pFileName, "w" );
+    fprintf( pFile, "# Random function with %d inputs generated by ABC on %s\n", nPis, Extra_TimeStamp() );
+    fprintf( pFile, ".model rand%d\n", nPis );
+    fprintf( pFile, ".inputs" );
+    nDigitsIn = Extra_Base10Log( nPis );
+    for ( i = 0; i < nPis; i++ )
+        fprintf( pFile, " i%0*d", nDigitsIn, i );
+    fprintf( pFile, "\n" );
+    fprintf( pFile, ".outputs f\n" );
+    fprintf( pFile, ".names" );
+    nDigitsIn = Extra_Base10Log( nPis );
+    for ( i = 0; i < nPis; i++ )
+        fprintf( pFile, " i%0*d", nDigitsIn, i );
+    fprintf( pFile, " f\n" );
+    for ( i = 0; i < (1<<nPis); i++ )
+        if ( Aig_InfoHasBit(pTruth, i) )
+        {
+            for ( b = nPis-1; b >= 0; b-- )
+                fprintf( pFile, "%d", (i>>b)&1 );
+            fprintf( pFile, " 1\n" );
+        }
+    fprintf( pFile, ".end\n" ); 
+    fprintf( pFile, "\n" ); 
+    fclose( pFile );
+    ABC_FREE( pTruth );
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
index c7fa5a1e..9e0347d5 100644
--- a/src/base/abci/abcIvy.c
+++ b/src/base/abci/abcIvy.c
@@ -946,12 +946,8 @@ Ivy_Obj_t * Abc_NodeStrashAig( Ivy_Man_t * pMan, Abc_Obj_t * pNode )
     if ( Abc_NodeIsConst(pNode) )
         return Ivy_NotCond( Ivy_ManConst1(pMan), Abc_SopIsConst0(pSop) );
 
-    // consider the special case of EXOR function
-    if ( Abc_SopIsExorType(pSop) )
-        return Abc_NodeStrashAigExorAig( pMan, pNode, pSop );
-
     // decide when to use factoring
-    if ( fUseFactor && Abc_ObjFaninNum(pNode) > 2 && Abc_SopGetCubeNum(pSop) > 1 )
+    if ( fUseFactor && Abc_ObjFaninNum(pNode) > 2 && Abc_SopGetCubeNum(pSop) > 1 && !Abc_SopIsExorType(pSop) )
         return Abc_NodeStrashAigFactorAig( pMan, pNode, pSop );
     return Abc_NodeStrashAigSopAig( pMan, pNode, pSop );
 }
@@ -973,6 +969,7 @@ Ivy_Obj_t * Abc_NodeStrashAigSopAig( Ivy_Man_t * pMan, Abc_Obj_t * pNode, char *
     Ivy_Obj_t * pAnd, * pSum;
     char * pCube;
     int i, nFanins;
+    int fExor = Abc_SopIsExorType(pSop);
 
     // get the number of node's fanins
     nFanins = Abc_ObjFaninNum( pNode );
@@ -991,7 +988,10 @@ Ivy_Obj_t * Abc_NodeStrashAigSopAig( Ivy_Man_t * pMan, Abc_Obj_t * pNode, char *
                 pAnd = Ivy_And( pMan, pAnd, Ivy_Not((Ivy_Obj_t *)pFanin->pCopy) );
         }
         // add to the sum of cubes
-        pSum = Ivy_Or( pMan, pSum, pAnd );
+        if ( fExor )
+            pSum = Ivy_Exor( pMan, pSum, pAnd );
+        else
+            pSum = Ivy_Or( pMan, pSum, pAnd );
     }
     // decide whether to complement the result
     if ( Abc_SopIsComplement(pSop) )
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index b869f067..e65ce11a 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -135,8 +135,10 @@ float Abc_NtkMfsTotalSwitching( Abc_Ntk_t * pNtk )
     Abc_NtkForEachObj( pNtk, pObjAbc, i )
     {
         if ( (pObjAbc2 = Abc_ObjRegular(pObjAbc->pTemp)) && (pObjAig = Aig_Regular(pObjAbc2->pTemp)) )
+        {
             Result += Abc_ObjFanoutNum(pObjAbc) * pSwitching[pObjAig->Id];
-//            Result += pSwitching[pObjAig->Id];
+//            printf( "%d = %.2f\n", i, Abc_ObjFanoutNum(pObjAbc) * pSwitching[pObjAig->Id] );
+        }
     }
     Vec_IntFree( vSwitching );
     Aig_ManStop( pAig );
diff --git a/src/base/io/io.c b/src/base/io/io.c
index e8af161e..20f412e0 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -1849,6 +1849,7 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
 
     if ( argc != globalUtilOptind + 1 )
     {
+        printf( "File name is missing on the command line.\n" );
         goto usage;
     }
     // get the input file name
diff --git a/src/base/io/ioReadBlifMv.c b/src/base/io/ioReadBlifMv.c
index 95ea4fe5..34ea4294 100644
--- a/src/base/io/ioReadBlifMv.c
+++ b/src/base/io/ioReadBlifMv.c
@@ -1615,7 +1615,7 @@ static char * Io_MvParseTableBlif( Io_MvMod_t * p, char * pTable, int nFanins )
 {
     Vec_Ptr_t * vTokens = p->pMan->vTokens;
     Vec_Str_t * vFunc = p->pMan->vFunc;
-    char * pProduct, * pOutput;
+    char * pProduct, * pOutput, c;
     int i, Polarity = -1;
 
     p->pMan->nTablesRead++;
@@ -1626,7 +1626,8 @@ static char * Io_MvParseTableBlif( Io_MvMod_t * p, char * pTable, int nFanins )
     if ( Vec_PtrSize(vTokens) == 1 )
     {
         pOutput = Vec_PtrEntry( vTokens, 0 );
-        if ( ((pOutput[0] - '0') & 0x8E) || pOutput[1] )
+        c = pOutput[0];
+        if ( (c!='0'&&c!='1'&&c!='x'&&c!='n') || pOutput[1] )
         {
             sprintf( p->pMan->sError, "Line %d: Constant table has wrong output value \"%s\".", Io_MvGetLine(p->pMan, pOutput), pOutput );
             return NULL;
@@ -1650,14 +1651,15 @@ static char * Io_MvParseTableBlif( Io_MvMod_t * p, char * pTable, int nFanins )
             sprintf( p->pMan->sError, "Line %d: Cube \"%s\" has size different from the fanin count (%d).", Io_MvGetLine(p->pMan, pProduct), pProduct, nFanins );
             return NULL;
         }
-        if ( ((pOutput[0] - '0') & 0x8E) || pOutput[1] )
+        c = pOutput[0];
+        if ( (c!='0'&&c!='1'&&c!='x'&&c!='n') || pOutput[1] )
         {
             sprintf( p->pMan->sError, "Line %d: Output value \"%s\" is incorrect.", Io_MvGetLine(p->pMan, pProduct), pOutput );
             return NULL;
         }
         if ( Polarity == -1 )
-            Polarity = pOutput[0] - '0';
-        else if ( Polarity != pOutput[0] - '0' )
+            Polarity = (c=='1' || c=='x');
+        else if ( Polarity != (c=='1' || c=='x') )
         {
             sprintf( p->pMan->sError, "Line %d: Output value \"%s\" differs from the value in the first line of the table (%d).", Io_MvGetLine(p->pMan, pProduct), pOutput, Polarity );
             return NULL;
diff --git a/src/base/ver/verCore.c b/src/base/ver/verCore.c
index aa213010..c318545b 100644
--- a/src/base/ver/verCore.c
+++ b/src/base/ver/verCore.c
@@ -2042,6 +2042,11 @@ int Ver_ParseConnectBox( Ver_Man_t * pMan, Abc_Obj_t * pBox )
     assert( !Ver_ObjIsConnected(pBox) );
     assert( Ver_NtkIsDefined(pNtkBox) );
     assert( !Abc_NtkHasBlackbox(pNtkBox) || Abc_NtkBoxNum(pNtkBox) == 1 );
+
+    if ( !strcmp(pNtkBox->pName,"add_4u_4u") )
+    {
+        int s = 0;
+    }
 /*
     // clean the PI/PO nets
     Abc_NtkForEachPi( pNtkBox, pTerm, i )
@@ -2134,7 +2139,7 @@ int Ver_ParseConnectBox( Ver_Man_t * pMan, Abc_Obj_t * pBox )
                 if ( Length > 0 )
                 {
                     Vec_PtrForEachEntry( vBundles, pBundle, j )
-                        if ( !strncmp(pBundle->pNameFormal, pNameFormal, Length) )
+                        if ( !strncmp(pBundle->pNameFormal, pNameFormal, Length) && (int)strlen(pBundle->pNameFormal) == Length )
                             break;
                     if ( j == Vec_PtrSize(vBundles) )
                         pBundle = NULL;
@@ -2185,7 +2190,7 @@ int Ver_ParseConnectBox( Ver_Man_t * pMan, Abc_Obj_t * pBox )
                 if ( Length > 0 )
                 {
                     Vec_PtrForEachEntry( vBundles, pBundle, j )
-                        if ( !strncmp(pBundle->pNameFormal, pNameFormal, Length) )
+                        if ( !strncmp(pBundle->pNameFormal, pNameFormal, Length) && (int)strlen(pBundle->pNameFormal) == Length ) 
                             break;
                     if ( j == Vec_PtrSize(vBundles) )
                         pBundle = NULL;
@@ -2193,8 +2198,14 @@ int Ver_ParseConnectBox( Ver_Man_t * pMan, Abc_Obj_t * pBox )
             }
             if ( pBundle == NULL )
             {
+                char Buffer[1000];
 //                printf( "Warning: The formal output %s is not driven when instantiating network %s in box %s.", 
 //                    pNameFormal, pNtkBox->pName, Abc_ObjName(pBox) );
+                pTermNew = Abc_NtkCreateBo( pNtk );
+                sprintf( Buffer, "_temp_net%d", Abc_ObjId(pTermNew) );
+                pNetAct = Abc_NtkFindOrCreateNet( pNtk, Buffer );
+                Abc_ObjAddFanin( pTermNew, pBox );
+                Abc_ObjAddFanin( pNetAct, pTermNew );
                 continue;
             }
         }