Version abc90408

22 files changed, 283 insertions, 60 deletions

diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c
index 289c422d..a3188901 100644
--- a/src/base/abc/abcAig.c
+++ b/src/base/abc/abcAig.c
@@ -163,7 +163,7 @@ void Abc_AigFree( Abc_Aig_t * pMan )
 {
     assert( Vec_PtrSize( pMan->vStackReplaceOld ) == 0 );
     assert( Vec_PtrSize( pMan->vStackReplaceNew ) == 0 );
-    // ABC_FREE the table
+    // free the table
     if ( pMan->vAddedCells )
         Vec_PtrFree( pMan->vAddedCells );
     if ( pMan->vUpdatedNets )
diff --git a/src/base/abc/abcLatch.c b/src/base/abc/abcLatch.c
index aef44b11..d870a610 100644
--- a/src/base/abc/abcLatch.c
+++ b/src/base/abc/abcLatch.c
@@ -371,6 +371,116 @@ printf( "Converted %d one-hot registers.\n", Vec_IntSize(vNumbers) );
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Converts registers with DC values into additional PIs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkConvertOnehot( Abc_Ntk_t * pNtk )
+{
+    Vec_Ptr_t * vNodes;
+    Abc_Ntk_t * pNtkNew;
+    Abc_Obj_t * pObj, * pFanin, * pObjNew, * pObjLiNew, * pObjLoNew;
+    int i, k, nFlops, nStates, iState, pfCompl[32];
+    assert( Abc_NtkIsLogic(pNtk) );
+    nFlops = Abc_NtkLatchNum(pNtk);
+    if ( nFlops == 0 )
+        return Abc_NtkDup( pNtk );
+    if ( nFlops > 16 )
+    {
+        printf( "Cannot reencode %d flops because it will lead to 2^%d states.\n", nFlops, nFlops );
+        return NULL;
+    }
+    // check if there are latches with DC values
+    iState = 0;
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+    {
+        if ( Abc_LatchIsInitDc(pObj) )
+        {
+            printf( "Cannot process logic network with don't-care init values. Run \"zero\".\n" );
+            return NULL;
+        }
+        if ( Abc_LatchIsInit1(pObj) )
+            iState |= (1 << i);
+    }
+    // transfer logic to SOPs
+    Abc_NtkToSop( pNtk, 0 );
+    // create new network
+    pNtkNew = Abc_NtkStartFromNoLatches( pNtk, pNtk->ntkType, pNtk->ntkFunc );
+    nStates = (1 << nFlops);
+    for ( i = 0; i < nStates; i++ )
+    {
+        pObjNew   = Abc_NtkCreateLatch( pNtkNew );
+        pObjLiNew = Abc_NtkCreateBi( pNtkNew );
+        pObjLoNew = Abc_NtkCreateBo( pNtkNew );
+        Abc_ObjAddFanin( pObjNew, pObjLiNew );
+        Abc_ObjAddFanin( pObjLoNew, pObjNew );
+        if ( i == iState )
+            Abc_LatchSetInit1( pObjNew );
+        else
+            Abc_LatchSetInit0( pObjNew );
+    }
+    Abc_NtkAddDummyBoxNames( pNtkNew );
+    assert( Abc_NtkLatchNum(pNtkNew) == nStates );
+    assert( Abc_NtkPiNum(pNtkNew) == Abc_NtkPiNum(pNtk) );
+    assert( Abc_NtkPoNum(pNtkNew) == Abc_NtkPoNum(pNtk) );
+    assert( Abc_NtkCiNum(pNtkNew) == Abc_NtkPiNum(pNtkNew) + nStates );
+    assert( Abc_NtkCoNum(pNtkNew) == Abc_NtkPoNum(pNtkNew) + nStates );
+    assert( Abc_NtkCiNum(pNtk) == Abc_NtkPiNum(pNtk) + nFlops );
+    assert( Abc_NtkCoNum(pNtk) == Abc_NtkPoNum(pNtk) + nFlops );
+    // create hot-to-log transformers
+    for ( i = 0; i < nFlops; i++ ) 
+    {
+        pObjNew = Abc_NtkCreateNode( pNtkNew );
+        for ( k = 0; k < nStates; k++ )
+            if ( (k >> i) & 1 )
+                Abc_ObjAddFanin( pObjNew, Abc_NtkCi(pNtkNew, Abc_NtkPiNum(pNtkNew)+k) );
+        assert( Abc_ObjFaninNum(pObjNew) == nStates/2 );
+        pObjNew->pData = Abc_SopCreateOr( pNtkNew->pManFunc, nStates/2, NULL );
+        // save the new flop
+        pObj = Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i );
+        pObj->pCopy = pObjNew;
+    }
+    // duplicate the nodes
+    vNodes = Abc_NtkDfs( pNtk, 0 );
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+    {
+        pObj->pCopy = Abc_NtkDupObj( pNtkNew, pObj, 1 );
+        Abc_ObjForEachFanin( pObj, pFanin, k )
+            Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
+    }
+    Vec_PtrFree( vNodes );
+    // connect the POs
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Abc_ObjAddFanin( pObj->pCopy, Abc_ObjNotCond(Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj)) );
+    // write entries into the nodes
+    Abc_NtkForEachCo( pNtk, pObj, i )
+        pObj->pCopy = Abc_ObjNotCond(Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj));
+    // create log-to-hot transformers
+    for ( k = 0; k < nStates; k++ )
+    {
+        pObjNew = Abc_NtkCreateNode( pNtkNew );
+        for ( i = 0; i < nFlops; i++ )
+        {
+            pObj = Abc_NtkCo( pNtk, Abc_NtkPoNum(pNtk) + i );
+            Abc_ObjAddFanin( pObjNew, Abc_ObjRegular(pObj->pCopy) );
+            pfCompl[i] = Abc_ObjIsComplement(pObj->pCopy) ^ !((k >> i) & 1);
+        }
+        pObjNew->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, nFlops, pfCompl );
+        // connect it to the flop input
+        Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, Abc_NtkPoNum(pNtkNew)+k), pObjNew );
+    }
+    if ( !Abc_NtkCheck( pNtkNew ) )
+        fprintf( stdout, "Abc_NtkConvertOnehot(): Network check has failed.\n" );
+    return pNtkNew;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index 639319d1..d6ab7ea1 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -935,10 +935,10 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
 //    int LargePiece = (4 << ABC_NUM_STEPS);
     if ( pNtk == NULL )
         return;
-    // ABC_FREE the HAIG
+    // free the HAIG
 //    if ( pNtk->pHaig )
 //        Abc_NtkHaigStop( pNtk );
-    // ABC_FREE EXDC Ntk
+    // free EXDC Ntk
     if ( pNtk->pExdc )
         Abc_NtkDelete( pNtk->pExdc );
     if ( pNtk->pExcare )
@@ -952,7 +952,7 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
     // make sure all the marks are clean
     Abc_NtkForEachObj( pNtk, pObj, i )
     {
-        // ABC_FREE large fanout arrays
+        // free large fanout arrays
 //        if ( pNtk->pMmObj && pObj->vFanouts.nCap * 4 > LargePiece )
 //            ABC_FREE( pObj->vFanouts.pArray );
         // these flags should be always zero
@@ -961,7 +961,7 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
         assert( pObj->fMarkB == 0 );
         assert( pObj->fMarkC == 0 );
     }
-    // ABC_FREE the nodes
+    // free the nodes
     if ( pNtk->pMmStep == NULL )
     {
         Abc_NtkForEachObj( pNtk, pObj, i )
@@ -976,7 +976,7 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
             ABC_FREE( pObj );
     }
         
-    // ABC_FREE the arrays
+    // free the arrays
     Vec_PtrFree( pNtk->vPios );
     Vec_PtrFree( pNtk->vPis );
     Vec_PtrFree( pNtk->vPos );
@@ -992,14 +992,14 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
     TotalMemory += pNtk->pMmObj? Extra_MmFixedReadMemUsage(pNtk->pMmObj)  : 0;
     TotalMemory += pNtk->pMmStep? Extra_MmStepReadMemUsage(pNtk->pMmStep) : 0;
 //    fprintf( stdout, "The total memory allocated internally by the network = %0.2f Mb.\n", ((double)TotalMemory)/(1<<20) );
-    // ABC_FREE the storage 
+    // free the storage 
     if ( pNtk->pMmObj )
         Extra_MmFixedStop( pNtk->pMmObj );
     if ( pNtk->pMmStep )
         Extra_MmStepStop ( pNtk->pMmStep );
     // name manager
     Nm_ManFree( pNtk->pManName );
-    // ABC_FREE the timing manager
+    // free the timing manager
     if ( pNtk->pManTime )
         Abc_ManTimeStop( pNtk->pManTime );
     // start the functionality manager
@@ -1015,7 +1015,7 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
         pNtk->pManFunc = NULL;
     else if ( !Abc_NtkHasBlackbox(pNtk) )
         assert( 0 );
-    // ABC_FREE the hierarchy
+    // free the hierarchy
     if ( pNtk->pDesign )
     {
         Abc_LibFree( pNtk->pDesign, pNtk );
@@ -1023,7 +1023,7 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
     }
 //    if ( pNtk->pBlackBoxes ) 
 //        Vec_IntFree( pNtk->pBlackBoxes );
-    // ABC_FREE node attributes
+    // free node attributes
     Vec_PtrForEachEntry( pNtk->vAttrs, pAttrMan, i )
         if ( pAttrMan )
         {
diff --git a/src/base/abc/abcObj.c b/src/base/abc/abcObj.c
index 4b18aa36..e4484ec5 100644
--- a/src/base/abc/abcObj.c
+++ b/src/base/abc/abcObj.c
@@ -71,9 +71,9 @@ void Abc_ObjRecycle( Abc_Obj_t * pObj )
 {
     Abc_Ntk_t * pNtk = pObj->pNtk;
 //    int LargePiece = (4 << ABC_NUM_STEPS);
-    // ABC_FREE large fanout arrays
+    // free large fanout arrays
 //    if ( pNtk->pMmStep && pObj->vFanouts.nCap * 4 > LargePiece )
-//        ABC_FREE( pObj->vFanouts.pArray );
+//        free( pObj->vFanouts.pArray );
     if ( pNtk->pMmStep == NULL )
     {
         ABC_FREE( pObj->vFanouts.pArray );
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index cdb9b465..8ebb00a3 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -1770,7 +1770,7 @@ void Abc_NtkCompareCones( Abc_Ntk_t * pNtk )
         printf( "%4d CO %5d :  Supp = %5d.  Lev = %3d.  Cone = %5d.  Rev = %5d.  COs = %3d (%3d).\n",
             Iter, pPerms[i], Vec_PtrSize(vSupp), Abc_ObjLevel(Abc_ObjFanin0(pObj)), Vec_PtrSize(vNodes), Counter, CounterCos, CounterCosNew );
 
-        // ABC_FREE arrays
+        // free arrays
         Vec_PtrFree( vSupp );
         Vec_PtrFree( vNodes );
         Vec_PtrFree( vReverse );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index ef7969be..c48b7e95 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -27,7 +27,7 @@
 #include "if.h"
 #include "res.h"
 #include "lpk.h"
-#include "aig.h"
+#include "giaAig.h"
 #include "dar.h"
 #include "mfs.h"
 #include "mfx.h"
@@ -39,7 +39,6 @@
 #include "ssw.h"
 #include "cgt.h"
 #include "amap.h"
-#include "gia.h"
 #include "cec.h"
 
 ////////////////////////////////////////////////////////////////////////
@@ -194,6 +193,7 @@ static int Abc_CommandScut           ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandInit           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandZero           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandUndc           ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandOneHot         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPipe           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSeq            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandUnseq          ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -513,6 +513,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Sequential",   "init",          Abc_CommandInit,             1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "zero",          Abc_CommandZero,             1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "undc",          Abc_CommandUndc,             1 );
+    Cmd_CommandAdd( pAbc, "Sequential",   "onehot",        Abc_CommandOneHot,           1 );
 //    Cmd_CommandAdd( pAbc, "Sequential",   "pipe",          Abc_CommandPipe,             1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "retime",        Abc_CommandRetime,           1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "dretime",       Abc_CommandDRetime,          1 );
@@ -598,7 +599,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "AIG",          "&psig",         Abc_CommandAbc9PSig,         0 );
     Cmd_CommandAdd( pAbc, "AIG",          "&status",       Abc_CommandAbc9Status,       0 );
     Cmd_CommandAdd( pAbc, "AIG",          "&show",         Abc_CommandAbc9Show,         0 );
-    Cmd_CommandAdd( pAbc, "AIG",          "&hash",         Abc_CommandAbc9Hash,         0 );
+    Cmd_CommandAdd( pAbc, "AIG",          "&st",           Abc_CommandAbc9Hash,         0 );
     Cmd_CommandAdd( pAbc, "AIG",          "&topand",       Abc_CommandAbc9Topand,       0 );
     Cmd_CommandAdd( pAbc, "AIG",          "&cof",          Abc_CommandAbc9Cof,          0 );
     Cmd_CommandAdd( pAbc, "AIG",          "&trim",         Abc_CommandAbc9Trim,         0 );
@@ -11945,7 +11946,7 @@ usage:
     fprintf( pErr, "\t-E float : sets epsilon used for tie-breaking [default = %f]\n", pPars->fEpsilon );  
     fprintf( pErr, "\t-m       : toggles using MUX matching [default = %s]\n", pPars->fUseMuxes? "yes": "no" );
     fprintf( pErr, "\t-x       : toggles using XOR matching [default = %s]\n", pPars->fUseXors? "yes": "no" );
-    fprintf( pErr, "\t-i       : toggles assuming inverters are ABC_FREE [default = %s]\n", pPars->fFreeInvs? "yes": "no" );
+    fprintf( pErr, "\t-i       : toggles assuming inverters are free [default = %s]\n", pPars->fFreeInvs? "yes": "no" );
     fprintf( pErr, "\t-s       : toggles sweep after mapping [default = %s]\n", fSweep? "yes": "no" );
     fprintf( pErr, "\t-v       : toggles verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h       : print the command usage\n");
@@ -13094,7 +13095,74 @@ int Abc_CommandUndc( Abc_Frame_t * pAbc, int argc, char ** argv )
 
 usage:
     fprintf( pErr, "usage: undc [-h]\n" );
-    fprintf( pErr, "\t        converts latches with DC init values into ABC_FREE PIs\n" );
+    fprintf( pErr, "\t        converts latches with DC init values into free PIs\n" );
+    fprintf( pErr, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandOneHot( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c;
+    extern Abc_Ntk_t * Abc_NtkConvertOnehot( Abc_Ntk_t * pNtk );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( Abc_NtkIsComb(pNtk) )
+    {
+        fprintf( pErr, "The current network is combinational.\n" );
+        return 0;
+    }
+    if ( !Abc_NtkIsLogic(pNtk) )
+    {
+        fprintf( pErr, "This command works only for logic networks.\n" );
+        return 0;
+    }
+    // get the new network
+    pNtkRes = Abc_NtkConvertOnehot( pNtk );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Converting to one-hot encoding has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: onehot [-h]\n" );
+    fprintf( pErr, "\t        converts natural encoding into one-hot encoding\n" );
     fprintf( pErr, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -15030,7 +15098,7 @@ int Abc_CommandSim( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    fNew       =  1;
+    fNew       =  0;
     fComb      =  0;
     nFrames    = 32;
     nWords     =  8;
@@ -18381,22 +18449,28 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
     int nConfMax;
     int fDynamic;
     int fExtend;
+    int fSkipProof;
+    int nFramesBmc;
+    int nConfMaxBmc;
     int fVerbose;
     int c;
-    extern Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    nFramesMax =    10;
-    nConfMax   = 10000;
-    fDynamic   =     1;
-    fExtend    =     0;
-    fVerbose   =     0;
+    nFramesMax  =    10;
+    nConfMax    = 10000;
+    fDynamic    =     1;
+    fExtend     =     0;
+    fSkipProof  =     0;
+    nFramesBmc  =  2000;
+    nConfMaxBmc =  5000;
+    fVerbose    =     0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FCdevh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FCGDdesvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -18422,12 +18496,37 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nConfMax < 0 ) 
                 goto usage;
             break;
+        case 'G':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-G\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nFramesBmc = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nFramesBmc < 0 ) 
+                goto usage;
+            break;
+        case 'D':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-D\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nConfMaxBmc = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nConfMaxBmc < 0 ) 
+                goto usage;
+            break;
         case 'd':
             fDynamic ^= 1;
             break;
         case 'e':
             fExtend ^= 1;
             break;
+        case 's':
+            fSkipProof ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -18454,7 +18553,7 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // modify the current network
-    pNtkRes = Abc_NtkDarPBAbstraction( pNtk, nFramesMax, nConfMax, fDynamic, fExtend, fVerbose );
+    pNtkRes = Abc_NtkDarPBAbstraction( pNtk, nFramesMax, nConfMax, fDynamic, fExtend, fSkipProof, nFramesBmc, nConfMaxBmc, fVerbose );
     if ( pNtkRes == NULL )
     {
         if ( pNtk->pSeqModel == NULL )
@@ -18465,12 +18564,16 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
     return 0;
 usage:
-    fprintf( pErr, "usage: abs [-FC num] [-devh]\n" );
-    fprintf( pErr, "\t         proof-based abstraction from UNSAT core of the BMC instance\n" );
-    fprintf( pErr, "\t-F num : the max number of timeframes [default = %d]\n", nFramesMax );
-    fprintf( pErr, "\t-C num : the max number of conflicts by SAT solver [default = %d]\n", nConfMax );
+    fprintf( pErr, "usage: abs [-FCGD num] [-desvh]\n" );
+    fprintf( pErr, "\t         proof-based abstraction (PBA) using UNSAT core of BMC\n" );
+    fprintf( pErr, "\t         followed by counter-example-based abstraction\n" );
+    fprintf( pErr, "\t-F num : the max number of timeframes for PBA [default = %d]\n", nFramesMax );
+    fprintf( pErr, "\t-C num : the max number of conflicts by SAT solver for PBA [default = %d]\n", nConfMax );
+    fprintf( pErr, "\t-G num : the max number of timeframes for BMC [default = %d]\n", nFramesBmc );
+    fprintf( pErr, "\t-D num : the max number of conflicts by SAT solver for BMC [default = %d]\n", nConfMaxBmc );
     fprintf( pErr, "\t-d     : toggle dynamic unrolling of timeframes [default = %s]\n", fDynamic? "yes": "no" );
     fprintf( pErr, "\t-e     : toggle extending abstraction using COI of flops [default = %s]\n", fExtend? "yes": "no" );
+    fprintf( pErr, "\t-s     : toggle skipping proof-based abstraction [default = %s]\n", fSkipProof? "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;
@@ -22128,11 +22231,15 @@ int Abc_CommandAbc9Hash( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Gia_Man_t * pTemp;
     int c;
+    int fAddStrash = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "ah" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'a':
+            fAddStrash ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -22144,13 +22251,14 @@ int Abc_CommandAbc9Hash( Abc_Frame_t * pAbc, int argc, char ** argv )
         printf( "Abc_CommandAbc9Hash(): There is no AIG.\n" );
         return 1;
     } 
-    pAbc->pAig = Gia_ManRehash( pTemp = pAbc->pAig );
+    pAbc->pAig = Gia_ManRehash( pTemp = pAbc->pAig, fAddStrash );
     Gia_ManStop( pTemp );
     return 0;
 
 usage:
-    fprintf( stdout, "usage: &hash [-h]\n" );
+    fprintf( stdout, "usage: &st [-ah]\n" );
     fprintf( stdout, "\t        performs structural hashing\n" );
+    fprintf( stdout, "\t-a    : toggle additional hashing [default = %s]\n", fAddStrash? "yes": "no" );
     fprintf( stdout, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -22186,7 +22294,7 @@ int Abc_CommandAbc9Topand( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( pAbc->pAig == NULL )
     {
-        printf( "Abc_CommandAbc9Hash(): There is no AIG.\n" );
+        printf( "Abc_CommandAbc9Topand(): There is no AIG.\n" );
         return 1;
     } 
     if ( Gia_ManRegNum(pAbc->pAig) > 0 )
diff --git a/src/base/abci/abcBmc.c b/src/base/abci/abcBmc.c
index d2c5a12c..1512c76f 100644
--- a/src/base/abci/abcBmc.c
+++ b/src/base/abci/abcBmc.c
@@ -64,7 +64,7 @@ printf( "Fraig has %6d nodes.\n", Ivy_ManNodeNum(pFraig) );
     // report the classes
 //    if ( fVerbose )
 //        Abc_NtkBmcReport( pMan, pFrames, pFraig, vMapping, nFrames );
-    // ABC_FREE stuff
+    // free stuff
     Vec_PtrFree( vMapping );
     Ivy_ManStop( pFraig );
     Ivy_ManStop( pFrames );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 91046340..840068d6 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -19,7 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
-#include "aig.h"
+#include "giaAig.h"
 #include "saig.h"
 #include "dar.h"
 #include "cnf.h"
@@ -2299,7 +2299,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
             ABC_FREE( pNtk->pSeqModel );
             pNtk->pSeqModel = pCex;
             RetValue = 1;
-        }
+        } 
         else
         {
             RetValue = 0;
@@ -2375,7 +2375,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
         pGia = Gia_ManFromAig( pMan );
         if ( Gia_ManSimSimulate( pGia, pPars ) )
         { 
-            if ( (pCex = pMan->pSeqModel) )
+            if ( (pCex = (Fra_Cex_t *)pGia->pCexSeq) )
             {
                 printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ", 
                     nFrames, nWords, pCex->iPo, pCex->iFrame );
@@ -2404,8 +2404,13 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
         {
             pCex = Fra_SmlGetCounterExample( pSml );
             if ( pCex )
+            {
                 printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ", 
                     nFrames, nWords, pCex->iPo, pCex->iFrame );
+                status = Ssw_SmlRunCounterExample( pMan, (Ssw_Cex_t *)pCex );
+                if ( status == 0 )
+                    printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
+            }
             ABC_FREE( pNtk->pModel );
             ABC_FREE( pNtk->pSeqModel );
             pNtk->pSeqModel = pCex;
@@ -2557,7 +2562,7 @@ ABC_PRT( "Time", clock() - clkTotal );
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fVerbose )
+Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int fVerbose )
 {
     Abc_Ntk_t * pNtkAig;
     Aig_Man_t * pMan, * pTemp;
@@ -2567,7 +2572,7 @@ Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConf
         return NULL;
 
     Aig_ManSetRegNum( pMan, pMan->nRegs );
-    pMan = Saig_ManProofAbstraction( pTemp = pMan, nFramesMax, nConfMax, fDynamic, fExtend, 0, fVerbose );
+    pMan = Saig_ManProofAbstraction( pTemp = pMan, nFramesMax, nConfMax, fDynamic, fExtend, fSkipProof, nFramesBmc, nConfMaxBmc, fVerbose );
     if ( pTemp->pSeqModel )
     {
         ABC_FREE( pNtk->pModel );
@@ -3380,7 +3385,7 @@ Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk )
         return NULL;
 /*
     Aig_ManSetRegNum( pMan, pMan->nRegs );
-    pMan = Saig_ManProofAbstraction( pTemp = pMan, 5, 10000, 0, 0, 0, 1 );
+    pMan = Saig_ManProofAbstraction( pTemp = pMan, 5, 10000, 0, 0, 0, -1, -1, 1 );
     Aig_ManStop( pTemp );
     if ( pMan == NULL )
         return NULL;
diff --git a/src/base/abci/abcFxu.c b/src/base/abci/abcFxu.c
index 1596e774..6109870e 100644
--- a/src/base/abci/abcFxu.c
+++ b/src/base/abci/abcFxu.c
@@ -177,12 +177,12 @@ void Abc_NtkFxuCollectInfo( Abc_Ntk_t * pNtk, Fxu_Data_t * p )
 void Abc_NtkFxuFreeInfo( Fxu_Data_t * p )
 {
     int i;
-    // ABC_FREE the arrays of new fanins
+    // free the arrays of new fanins
     if ( p->vFaninsNew )
         for ( i = 0; i < p->vFaninsNew->nSize; i++ )
             if ( p->vFaninsNew->pArray[i] )
                 Vec_IntFree( p->vFaninsNew->pArray[i] );
-    // ABC_FREE the arrays
+    // free the arrays
     if ( p->vSops      ) Vec_PtrFree( p->vSops      );
     if ( p->vSopsNew   ) Vec_PtrFree( p->vSopsNew   );
     if ( p->vFanins    ) Vec_PtrFree( p->vFanins    );
diff --git a/src/base/abci/abcHaig.c b/src/base/abci/abcHaig.c
index 569275f2..3f3fefcd 100644
--- a/src/base/abci/abcHaig.c
+++ b/src/base/abci/abcHaig.c
@@ -691,7 +691,7 @@ Abc_Ntk_t * Abc_NtkHaigUse( Abc_Ntk_t * pNtk )
     pNtkAig = Abc_NtkHaigRecreateAig( pNtk, pMan );
     Hop_ManStop( pMan );
 
-    // ABC_FREE HAIG
+    // free HAIG
     return pNtkAig;
 }
 
diff --git a/src/base/abci/abcMv.c b/src/base/abci/abcMv.c
index dacd16b2..8ea3697f 100644
--- a/src/base/abci/abcMv.c
+++ b/src/base/abci/abcMv.c
@@ -349,7 +349,7 @@ void Abc_MvDecompose( Mv_Man_t * p )
             printf( "%d ", Vec_PtrSize(vCofs) );
             Vec_PtrFree( vCofs );
 
-            // ABC_FREE the cofactors
+            // free the cofactors
             for ( v1 = 0; v1 < 4; v1++ )
             for ( v2 = 0; v2 < 4; v2++ )
                 Cudd_RecursiveDeref( p->dd, bCofs[v1 * 4 + v2] );
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index e65ce11a..d47dfe1f 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -64,7 +64,7 @@ int Abc_NtkCompareAndSaveBest( Abc_Ntk_t * pNtk )
         int    nPis;   // the number of primary inputs
         int    nPos;   // the number of primary outputs
     } ParsNew, ParsBest = { 0 };
-    // ABC_FREE storage for the name
+    // free storage for the name
     if ( pNtk == NULL )
     {
         ABC_FREE( ParsBest.pName );
diff --git a/src/base/abci/abcReach.c b/src/base/abci/abcReach.c
index 3834c00d..e25be81a 100644
--- a/src/base/abci/abcReach.c
+++ b/src/base/abci/abcReach.c
@@ -102,7 +102,7 @@ DdNode ** Abc_NtkCreatePartitions( DdManager * dd, Abc_Ntk_t * pNtk, int fReorde
         bVar  = Cudd_bddIthVar( dd, Abc_NtkCiNum(pNtk) + i );
         pbParts[i] = Cudd_bddXnor( dd, bVar, Abc_ObjGlobalBdd(Abc_ObjFanin0(pNode)) );  Cudd_Ref( pbParts[i] );
     }
-    // ABC_FREE the global BDDs
+    // free the global BDDs
     Abc_NtkFreeGlobalBdds( pNtk, 0 );
 
     // reorder and disable reordering
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index 3cee19ca..5e14116c 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -117,7 +117,7 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsL
         pNtk->pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
         Vec_IntFree( vCiIds );
     }
-    // ABC_FREE the sat_solver
+    // free the sat_solver
     if ( fVerbose )
         Sat_SolverPrintStats( stdout, pSat );
 
diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c
index d1f4d4f7..dfb8137c 100644
--- a/src/base/abci/abcSweep.c
+++ b/src/base/abci/abcSweep.c
@@ -111,7 +111,7 @@ bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose,
     Abc_NtkFraigTransform( pNtk, tEquiv, fUseInv, fVerbose );
     stmm_free_table( tEquiv );
 
-    // ABC_FREE the manager
+    // free the manager
     Fraig_ManFree( pMan );
     Abc_NtkDelete( pNtkAig );
 
diff --git a/src/base/abci/abcUnreach.c b/src/base/abci/abcUnreach.c
index 196ff643..251d3953 100644
--- a/src/base/abci/abcUnreach.c
+++ b/src/base/abci/abcUnreach.c
@@ -143,7 +143,7 @@ DdNode * Abc_NtkTransitionRelation( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbo
         Cudd_RecursiveDeref( dd, bTemp ); 
         Cudd_RecursiveDeref( dd, bProd ); 
     }
-    // ABC_FREE the global BDDs
+    // free the global BDDs
 //    Abc_NtkFreeGlobalBdds( pNtk );
     Abc_NtkFreeGlobalBdds( pNtk, 0 );
 
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index 60197d29..424c26ec 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -799,7 +799,7 @@ void Abc_NtkGetSeqPoSupp( Abc_Ntk_t * pNtk, int iFrame, int iNumPo )
         for ( k = 0; k <= iFrame; k++ )
             if ( Abc_NtkPi(pFrames, k*Abc_NtkPiNum(pNtk) + i)->pCopy )
                 pObj->pCopy = (void *)1;
-    // ABC_FREE stuff
+    // free stuff
     Vec_PtrFree( vSupp );
     Abc_NtkDelete( pFrames );
 }
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 20f412e0..46d61583 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -1140,7 +1140,7 @@ int IoCommandReadVerLib( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     printf( "The library contains %d gates.\n", st_count(pLibrary->tModules) );
-    // ABC_FREE old library
+    // free old library
     if ( Abc_FrameReadLibVer() )
         Abc_LibFree( Abc_FrameReadLibVer(), NULL );
     // read new library
diff --git a/src/base/io/ioReadAiger.c b/src/base/io/ioReadAiger.c
index c26e4cd5..85475204 100644
--- a/src/base/io/ioReadAiger.c
+++ b/src/base/io/ioReadAiger.c
@@ -327,7 +327,7 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
                 i++;
     }
     else // modified AIGER
-    {
+    { 
         vLits = Io_WriteDecodeLiterals( &pCur, nLatches + nOutputs );
     }
 
diff --git a/src/base/io/ioReadBlifMv.c b/src/base/io/ioReadBlifMv.c
index 34ea4294..eea601a8 100644
--- a/src/base/io/ioReadBlifMv.c
+++ b/src/base/io/ioReadBlifMv.c
@@ -160,7 +160,7 @@ Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck )
     pDesignName  = Extra_FileNameGeneric( pFileName );
     p->pDesign   = Abc_LibCreate( pDesignName );
     ABC_FREE( pDesignName );
-    // ABC_FREE the HOP manager
+    // free the HOP manager
     Hop_ManStop( p->pDesign->pManFunc );
     p->pDesign->pManFunc = NULL;
     // prepare the file for parsing
diff --git a/src/base/io/ioWriteCnf.c b/src/base/io/ioWriteCnf.c
index 7d03e545..3df189d1 100644
--- a/src/base/io/ioWriteCnf.c
+++ b/src/base/io/ioWriteCnf.c
@@ -78,7 +78,7 @@ int Io_WriteCnf( Abc_Ntk_t * pNtk, char * pFileName, int fAllPrimes )
     s_pNtk = pNtk;
     Sat_SolverWriteDimacs( pSat, pFileName, 0, 0, 1 );
     s_pNtk = NULL;
-    // ABC_FREE the solver
+    // free the solver
     sat_solver_delete( pSat );
     return 1;
 }
diff --git a/src/base/ver/verCore.c b/src/base/ver/verCore.c
index c318545b..42d6349a 100644
--- a/src/base/ver/verCore.c
+++ b/src/base/ver/verCore.c
@@ -274,7 +274,7 @@ void Ver_ParsePrintErrorMessage( Ver_Man_t * p )
     else // print the error message with the line number
         fprintf( p->Output, "%s (line %d): %s\n", 
             p->pFileName, Ver_StreamGetLineNumber(p->pReader), p->sError );
-    // ABC_FREE the data
+    // free the data
     Ver_ParseFreeData( p );
 }
 
@@ -2104,7 +2104,7 @@ int Ver_ParseConnectBox( Ver_Man_t * pMan, Abc_Obj_t * pBox )
             i--;
         }
 
-        // ABC_FREE the bundling
+        // free the bundling
         Vec_PtrForEachEntry( vBundles, pBundle, k )
             Ver_ParseFreeBundle( pBundle );
         Vec_PtrFree( vBundles );
@@ -2227,7 +2227,7 @@ int Ver_ParseConnectBox( Ver_Man_t * pMan, Abc_Obj_t * pBox )
         i--;
     }
 
-    // ABC_FREE the bundling
+    // free the bundling
     Vec_PtrForEachEntry( vBundles, pBundle, k )
         Ver_ParseFreeBundle( pBundle );
     Vec_PtrFree( vBundles );
@@ -2626,7 +2626,7 @@ int Ver_ParseDriveInputs( Ver_Man_t * pMan, Vec_Ptr_t * vUndefs )
                 Vec_PtrWriteEntry( (Vec_Ptr_t *)pBox->pCopy, j, NULL );
             }
 
-            // ABC_FREE the bundles
+            // free the bundles
             Vec_PtrFree( (Vec_Ptr_t *)pBox->pCopy );
             pBox->pCopy = NULL;
         }