Version abc90313

6 files changed, 375 insertions, 46 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index b7fe6316..2869352c 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -661,6 +661,7 @@ extern ABC_DLL Abc_Ntk_t *        Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames,
 /*=== abcNames.c ====================================================*/
 extern ABC_DLL char *             Abc_ObjName( Abc_Obj_t * pNode );
 extern ABC_DLL char *             Abc_ObjAssignName( Abc_Obj_t * pObj, char * pName, char * pSuffix );
+extern ABC_DLL char *             Abc_ObjNamePrefix( Abc_Obj_t * pObj, char * pPrefix );
 extern ABC_DLL char *             Abc_ObjNameSuffix( Abc_Obj_t * pObj, char * pSuffix );
 extern ABC_DLL char *             Abc_ObjNameDummy( char * pPrefix, int Num, int nDigits );
 extern ABC_DLL void               Abc_NtkTrasferNames( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
diff --git a/src/base/abc/abcHie.c b/src/base/abc/abcHie.c
index 19bdc47e..2addf289 100644
--- a/src/base/abc/abcHie.c
+++ b/src/base/abc/abcHie.c
@@ -40,9 +40,9 @@
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkFlattenLogicHierarchy_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, int * pCounter )
+void Abc_NtkFlattenLogicHierarchy2_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, int * pCounter )
 {
-    char Suffix[1000] = {0};
+    char Suffix[2000] = {0};
     Abc_Ntk_t * pNtkModel;
     Abc_Obj_t * pObj, * pTerm, * pNet, * pFanin;
     int i, k;
@@ -70,7 +70,7 @@ void Abc_NtkFlattenLogicHierarchy_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, in
 
     (*pCounter)++;
 
-    // create the prefix, which will be appended to the internal names
+    // create the suffix, which will be appended to the internal names
     if ( *pCounter )
         sprintf( Suffix, "_%s_%d", Abc_NtkName(pNtk), *pCounter );
 
@@ -98,7 +98,18 @@ void Abc_NtkFlattenLogicHierarchy_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, in
     Abc_NtkForEachPi( pNtk, pTerm, i )
         Abc_NodeSetTravIdCurrent( pTerm );
     Abc_NtkForEachPo( pNtk, pTerm, i )
+    {
         Abc_NodeSetTravIdCurrent( pTerm );
+        // if the netlist has net names beginning with "abc_property_"
+        // these names will be addes as primary outputs of the network
+        pNet = Abc_ObjFanin0(pTerm);
+        if ( strncmp( Abc_ObjName(pNet), "abc_property", 12 ) )
+            continue;
+        Abc_ObjAddFanin( Abc_NtkCreatePo(pNet->pCopy->pNtk), pNet->pCopy );
+        if ( Nm_ManFindNameById(pNet->pCopy->pNtk->pManName, pNet->pCopy->Id) )
+            Nm_ManDeleteIdName(pNet->pCopy->pNtk->pManName, pNet->pCopy->Id);
+        Abc_ObjAssignName( pNet->pCopy, Abc_ObjName(pNet), Suffix );
+    }
     Abc_NtkForEachBox( pNtk, pObj, i )
     {
         if ( Abc_ObjIsLatch(pObj) )
@@ -144,7 +155,7 @@ void Abc_NtkFlattenLogicHierarchy_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, in
         Abc_ObjForEachFanout( pObj, pTerm, k )
             Abc_ObjFanin0( Abc_NtkPo(pNtkModel, k) )->pCopy = Abc_ObjFanout0(pTerm)->pCopy;
         // call recursively
-        Abc_NtkFlattenLogicHierarchy_rec( pNtkNew, pNtkModel, pCounter );
+        Abc_NtkFlattenLogicHierarchy2_rec( pNtkNew, pNtkModel, pCounter );
     }
 
     // if it is a BLIF-MV netlist transfer the values of all nets
@@ -168,7 +179,7 @@ void Abc_NtkFlattenLogicHierarchy_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, in
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkFlattenLogicHierarchy( Abc_Ntk_t * pNtk )
+Abc_Ntk_t * Abc_NtkFlattenLogicHierarchy2( Abc_Ntk_t * pNtk )
 {
     Abc_Ntk_t * pNtkNew; 
     Abc_Obj_t * pTerm, * pNet;
@@ -203,7 +214,7 @@ Abc_Ntk_t * Abc_NtkFlattenLogicHierarchy( Abc_Ntk_t * pNtk )
 
     // recursively flatten hierarchy, create internal logic, add new PI/PO names if there are black boxes
     Counter = -1;
-    Abc_NtkFlattenLogicHierarchy_rec( pNtkNew, pNtk, &Counter );
+    Abc_NtkFlattenLogicHierarchy2_rec( pNtkNew, pNtk, &Counter );
     printf( "Hierarchy reader flattened %d instances of logic boxes and left %d black boxes.\n", 
         Counter, Abc_NtkBlackboxNum(pNtkNew) );
 
@@ -217,6 +228,241 @@ Abc_Ntk_t * Abc_NtkFlattenLogicHierarchy( Abc_Ntk_t * pNtk )
             pTerm->pData = ((Abc_Ntk_t *)pTerm->pData)->pCopy;
     }
 
+    // we may have added property outputs
+    Abc_NtkOrderCisCos( pNtkNew );
+
+    // copy the timing information
+//    Abc_ManTimeDup( pNtk, pNtkNew );
+    // duplicate EXDC 
+    if ( pNtk->pExdc )
+        printf( "EXDC is not transformed.\n" );
+    if ( !Abc_NtkCheck( pNtkNew ) )
+    {
+        fprintf( stdout, "Abc_NtkFlattenLogicHierarchy2(): Network check has failed.\n" );
+        Abc_NtkDelete( pNtkNew );
+        return NULL;
+    }
+    return pNtkNew;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively flattens logic hierarchy of the netlist.]
+
+  Description [When this procedure is called, the PI/PO nets of the old 
+  netlist point to the corresponding nets of the flattened netlist.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkFlattenLogicHierarchy_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, int * pCounter, Vec_Str_t * vPref )
+{
+    Abc_Ntk_t * pNtkModel;
+    Abc_Obj_t * pObj, * pTerm, * pNet, * pFanin;
+    int i, k, Length;
+
+    // process the blackbox
+    if ( Abc_NtkHasBlackbox(pNtk) )
+    {
+        // duplicate the blackbox
+        assert( Abc_NtkBoxNum(pNtk) == 1 );
+        pObj = Abc_NtkBox( pNtk, 0 );
+        Abc_NtkDupBox( pNtkNew, pObj, 1 );
+        pObj->pCopy->pData = pNtk;
+
+        // connect blackbox fanins to the PI nets
+        assert( Abc_ObjFaninNum(pObj->pCopy) == Abc_NtkPiNum(pNtk) );
+        Abc_NtkForEachPi( pNtk, pTerm, i )
+            Abc_ObjAddFanin( Abc_ObjFanin(pObj->pCopy,i), Abc_ObjFanout0(pTerm)->pCopy );
+
+        // connect blackbox fanouts to the PO nets
+        assert( Abc_ObjFanoutNum(pObj->pCopy) == Abc_NtkPoNum(pNtk) );
+        Abc_NtkForEachPo( pNtk, pTerm, i )
+            Abc_ObjAddFanin( Abc_ObjFanin0(pTerm)->pCopy, Abc_ObjFanout(pObj->pCopy,i) );
+        return;
+    }
+
+    (*pCounter)++;
+
+    // create the suffix, which will be appended to the internal names
+    if ( *pCounter )
+    {
+        char Buffer[20];
+        sprintf( Buffer, "(%d)", *pCounter );
+        Vec_StrAppend( vPref, Buffer );
+    }
+    Vec_StrPush( vPref, '|' );
+    Vec_StrPush( vPref, 0 );
+
+    // duplicate nets of all boxes, including latches
+    Abc_NtkForEachBox( pNtk, pObj, i )
+    {
+        Abc_ObjForEachFanin( pObj, pTerm, k )
+        {
+            pNet = Abc_ObjFanin0(pTerm);
+            if ( pNet->pCopy )
+                continue;
+            pNet->pCopy = Abc_NtkFindOrCreateNet( pNtkNew, Abc_ObjNamePrefix(pNet, Vec_StrArray(vPref)) );
+        }
+        Abc_ObjForEachFanout( pObj, pTerm, k )
+        {
+            pNet = Abc_ObjFanout0(pTerm);
+            if ( pNet->pCopy )
+                continue;
+            pNet->pCopy = Abc_NtkFindOrCreateNet( pNtkNew, Abc_ObjNamePrefix(pNet, Vec_StrArray(vPref)) );
+        }
+    }
+
+    // mark objects that will not be used
+    Abc_NtkIncrementTravId( pNtk );
+    Abc_NtkForEachPi( pNtk, pTerm, i )
+        Abc_NodeSetTravIdCurrent( pTerm );
+    Abc_NtkForEachPo( pNtk, pTerm, i )
+    {
+        Abc_NodeSetTravIdCurrent( pTerm );
+        // if the netlist has net names beginning with "abc_property_"
+        // these names will be addes as primary outputs of the network
+        pNet = Abc_ObjFanin0(pTerm);
+        if ( strncmp( Abc_ObjName(pNet), "abc_property", 12 ) )
+            continue;
+        Abc_ObjAddFanin( Abc_NtkCreatePo(pNet->pCopy->pNtk), pNet->pCopy );
+        if ( Nm_ManFindNameById(pNet->pCopy->pNtk->pManName, pNet->pCopy->Id) )
+            Nm_ManDeleteIdName(pNet->pCopy->pNtk->pManName, pNet->pCopy->Id);
+        Abc_ObjAssignName( pNet->pCopy, Vec_StrArray(vPref), Abc_ObjName(pNet) );
+    }
+    Abc_NtkForEachBox( pNtk, pObj, i )
+    {
+        if ( Abc_ObjIsLatch(pObj) )
+            continue;
+        Abc_NodeSetTravIdCurrent( pObj );
+        Abc_ObjForEachFanin( pObj, pTerm, k )
+            Abc_NodeSetTravIdCurrent( pTerm );
+        Abc_ObjForEachFanout( pObj, pTerm, k )
+            Abc_NodeSetTravIdCurrent( pTerm );
+    }
+
+    // duplicate objects that do not have prototypes yet
+    Abc_NtkForEachObj( pNtk, pObj, i )
+    {
+        if ( Abc_NodeIsTravIdCurrent(pObj) )
+            continue;
+        if ( pObj->pCopy )
+            continue;
+        Abc_NtkDupObj( pNtkNew, pObj, 0 );
+    }
+
+    // connect objects
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        if ( !Abc_NodeIsTravIdCurrent(pObj) )
+            Abc_ObjForEachFanin( pObj, pFanin, k )
+                if ( !Abc_NodeIsTravIdCurrent(pFanin) )
+                    Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
+
+    // call recursively
+    Vec_StrPop( vPref );
+    Length = Vec_StrSize( vPref );
+    Abc_NtkForEachBox( pNtk, pObj, i )
+    {
+        if ( Abc_ObjIsLatch(pObj) )
+            continue;
+        pNtkModel = pObj->pData;
+        // check the match between the number of actual and formal parameters
+        assert( Abc_ObjFaninNum(pObj) == Abc_NtkPiNum(pNtkModel) );
+        assert( Abc_ObjFanoutNum(pObj) == Abc_NtkPoNum(pNtkModel) );
+        // clean the node copy fields
+        Abc_NtkCleanCopy( pNtkModel );
+        // map PIs/POs
+        Abc_ObjForEachFanin( pObj, pTerm, k )
+            Abc_ObjFanout0( Abc_NtkPi(pNtkModel, k) )->pCopy = Abc_ObjFanin0(pTerm)->pCopy;
+        Abc_ObjForEachFanout( pObj, pTerm, k )
+            Abc_ObjFanin0( Abc_NtkPo(pNtkModel, k) )->pCopy = Abc_ObjFanout0(pTerm)->pCopy;
+        // create name
+        Vec_StrShrink( vPref, Length );
+        Vec_StrAppend( vPref, Abc_NtkName(pNtkModel) );
+        // call recursively
+        Abc_NtkFlattenLogicHierarchy_rec( pNtkNew, pNtkModel, pCounter, vPref );
+    }
+
+    // if it is a BLIF-MV netlist transfer the values of all nets
+    if ( Abc_NtkHasBlifMv(pNtk) && Abc_NtkMvVar(pNtk) )
+    {
+        if ( Abc_NtkMvVar( pNtkNew ) == NULL )
+            Abc_NtkStartMvVars( pNtkNew );
+        Abc_NtkForEachNet( pNtk, pObj, i )
+            Abc_NtkSetMvVarValues( pObj->pCopy, Abc_ObjMvVarNum(pObj) );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Flattens the logic hierarchy of the netlist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkFlattenLogicHierarchy( Abc_Ntk_t * pNtk )
+{
+    extern Abc_Lib_t * Abc_LibDupBlackboxes( Abc_Lib_t * pLib, Abc_Ntk_t * pNtkSave );
+    Vec_Str_t * vPref;
+    Abc_Ntk_t * pNtkNew; 
+    Abc_Obj_t * pTerm, * pNet;
+    int i, Counter = -1;
+
+    assert( Abc_NtkIsNetlist(pNtk) );
+    // start the network
+    pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
+    // duplicate the name and the spec
+    pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
+    pNtkNew->pSpec = Extra_UtilStrsav(pNtk->pSpec);
+
+    // clean the node copy fields
+    Abc_NtkCleanCopy( pNtk );
+
+    // duplicate PIs/POs and their nets
+    Abc_NtkForEachPi( pNtk, pTerm, i )
+    {
+        Abc_NtkDupObj( pNtkNew, pTerm, 0 );
+        pNet = Abc_ObjFanout0( pTerm );
+        pNet->pCopy = Abc_NtkFindOrCreateNet( pNtkNew, Abc_ObjName(pNet) );
+        Abc_ObjAddFanin( pNet->pCopy, pTerm->pCopy );
+    }
+    Abc_NtkForEachPo( pNtk, pTerm, i )
+    {
+        Abc_NtkDupObj( pNtkNew, pTerm, 0 );
+        pNet = Abc_ObjFanin0( pTerm );
+        pNet->pCopy = Abc_NtkFindOrCreateNet( pNtkNew, Abc_ObjName(pNet) );
+        Abc_ObjAddFanin( pTerm->pCopy, pNet->pCopy );
+    }
+
+    // recursively flatten hierarchy, create internal logic, add new PI/PO names if there are black boxes
+    vPref = Vec_StrAlloc( 1000 );
+    Vec_StrAppend( vPref, Abc_NtkName(pNtk) );
+    Abc_NtkFlattenLogicHierarchy_rec( pNtkNew, pNtk, &Counter, vPref );
+    printf( "Hierarchy reader flattened %d instances of logic boxes and left %d black boxes.\n", 
+        Counter, Abc_NtkBlackboxNum(pNtkNew) );
+    Vec_StrFree( vPref );
+
+    if ( pNtk->pDesign )
+    {
+        // pass on the design
+        assert( Vec_PtrEntry(pNtk->pDesign->vTops, 0) == pNtk );
+        pNtkNew->pDesign = Abc_LibDupBlackboxes( pNtk->pDesign, pNtkNew );
+        // update the pointers
+        Abc_NtkForEachBlackbox( pNtkNew, pTerm, i )
+            pTerm->pData = ((Abc_Ntk_t *)pTerm->pData)->pCopy;
+    }
+
+    // we may have added property outputs
+    Abc_NtkOrderCisCos( pNtkNew );
+
     // copy the timing information
 //    Abc_ManTimeDup( pNtk, pNtkNew );
     // duplicate EXDC 
@@ -231,6 +477,7 @@ Abc_Ntk_t * Abc_NtkFlattenLogicHierarchy( Abc_Ntk_t * pNtk )
     return pNtkNew;
 }
 
+
 /**Function*************************************************************
 
   Synopsis    [Extracts blackboxes by making them into additional PIs/POs.]
diff --git a/src/base/abc/abcNames.c b/src/base/abc/abcNames.c
index 90fcd191..e07b47c1 100644
--- a/src/base/abc/abcNames.c
+++ b/src/base/abc/abcNames.c
@@ -70,9 +70,27 @@ char * Abc_ObjAssignName( Abc_Obj_t * pObj, char * pName, char * pSuffix )
 
 /**Function*************************************************************
 
-  Synopsis    [Gets the long name of the node.]
+  Synopsis    [Appends name to the prefix]
 
-  Description [This name is the output net's name.]
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Abc_ObjNamePrefix( Abc_Obj_t * pObj, char * pPrefix )
+{
+    static char Buffer[2000];
+    sprintf( Buffer, "%s%s", pPrefix, Abc_ObjName(pObj) );
+    return Buffer;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Appends suffic to the name.]
+
+  Description []
                
   SideEffects []
 
@@ -81,7 +99,7 @@ char * Abc_ObjAssignName( Abc_Obj_t * pObj, char * pName, char * pSuffix )
 ***********************************************************************/
 char * Abc_ObjNameSuffix( Abc_Obj_t * pObj, char * pSuffix )
 {
-    static char Buffer[500];
+    static char Buffer[2000];
     sprintf( Buffer, "%s%s", Abc_ObjName(pObj), pSuffix );
     return Buffer;
 }
@@ -99,7 +117,7 @@ char * Abc_ObjNameSuffix( Abc_Obj_t * pObj, char * pSuffix )
 ***********************************************************************/
 char * Abc_ObjNameDummy( char * pPrefix, int Num, int nDigits )
 {
-    static char Buffer[100];
+    static char Buffer[2000];
     sprintf( Buffer, "%s%0*d", pPrefix, nDigits, Num );
     return Buffer;
 }
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 3045eb93..b5e23856 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -17580,9 +17580,10 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
     int nNodeDelta;
     int fRewrite;
     int fNewAlgo;
+    int nCofFanLit;
     int fVerbose;
 
-    extern int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nNodeDelta, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int fVerbose );
+    extern int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nNodeDelta, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int nCofFanLit, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -17596,9 +17597,10 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
     nNodeDelta  =     1000;
     fRewrite    =        0;
     fNewAlgo    =        1;
+    nCofFanLit  =        0;
     fVerbose    =        0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FNCGDrvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FNCGDLrvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -17657,6 +17659,17 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nNodeDelta < 0 ) 
                 goto usage;
             break;
+        case 'L':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-L\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nCofFanLit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nCofFanLit < 0 ) 
+                goto usage;
+            break;
         case 'r':
             fRewrite ^= 1;
             break;
@@ -17687,19 +17700,20 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( stdout, "Does not work for combinational networks.\n" );
         return 0;
     }
-    Abc_NtkDarBmc( pNtk, nFrames, nSizeMax, nNodeDelta, nBTLimit, nBTLimitAll, fRewrite, fNewAlgo, fVerbose );
+    Abc_NtkDarBmc( pNtk, nFrames, nSizeMax, nNodeDelta, nBTLimit, nBTLimitAll, fRewrite, fNewAlgo, nCofFanLit, fVerbose );
     pAbc->pCex = pNtk->pSeqModel; // temporary ???
     return 0;
 
 usage:
 //    fprintf( pErr, "usage: bmc [-FNCGD num] [-ravh]\n" );
-    fprintf( pErr, "usage: bmc [-FNC num] [-rvh]\n" );
+    fprintf( pErr, "usage: bmc [-FNCL num] [-rcvh]\n" );
     fprintf( pErr, "\t         performs bounded model checking with static unrolling\n" );
     fprintf( pErr, "\t-F num : the number of time frames [default = %d]\n", nFrames );
     fprintf( pErr, "\t-N num : the max number of nodes in the frames [default = %d]\n", nSizeMax );
     fprintf( pErr, "\t-C num : the max number of conflicts at a node [default = %d]\n", nBTLimit );
 //    fprintf( pErr, "\t-G num : the max number of conflicts globally [default = %d]\n", nBTLimitAll );
 //    fprintf( pErr, "\t-D num : the delta in the number of nodes [default = %d]\n", nNodeDelta );
+    fprintf( pErr, "\t-L num : the limit on fanout count of resets/enables to cofactor [default = %d]\n", nCofFanLit? "yes": "no" );
     fprintf( pErr, "\t-r     : toggle the use of rewriting [default = %s]\n", fRewrite? "yes": "no" );
 //    fprintf( pErr, "\t-a     : toggle SAT sweeping and SAT solving [default = %s]\n", fNewAlgo? "SAT solving": "SAT sweeping" );
     fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
@@ -17732,7 +17746,7 @@ int Abc_CommandBmc2( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fNewAlgo;
     int fVerbose;
 
-    extern int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nNodeDelta, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int fVerbose );
+    extern int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nNodeDelta, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int nCofFanLit, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -17837,7 +17851,7 @@ int Abc_CommandBmc2( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( stdout, "Does not work for combinational networks.\n" );
         return 0;
     }
-    Abc_NtkDarBmc( pNtk, nFrames, nSizeMax, nNodeDelta, nBTLimit, nBTLimitAll, fRewrite, fNewAlgo, fVerbose );
+    Abc_NtkDarBmc( pNtk, nFrames, nSizeMax, nNodeDelta, nBTLimit, nBTLimitAll, fRewrite, fNewAlgo, 0, fVerbose );
     pAbc->pCex = pNtk->pSeqModel; // temporary ???
     return 0;
 
@@ -22007,7 +22021,7 @@ usage:
 int Abc_CommandAbc9PSig( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     int c;
-    int fSetReset = 0;
+    int fSetReset = 1;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "rh" ) ) != EOF )
     {
@@ -22032,7 +22046,7 @@ int Abc_CommandAbc9PSig( Abc_Frame_t * pAbc, int argc, char ** argv )
         printf( "Abc_CommandAbc9PSigs(): Works only for sequential circuits.\n" );
         return 1;
     } 
-    Gia_ManDetectSeqSignals( pAbc->pAig, fSetReset );
+    Gia_ManDetectSeqSignals( pAbc->pAig, fSetReset, 1 );
     return 0;
 
 usage:
@@ -22233,9 +22247,10 @@ usage:
 int Abc_CommandAbc9Cof( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Gia_Man_t * pTemp;
-    int c, iVar = 0, nLimFan = 0;
+    int c, fVerbose = 0;
+    int iVar = 0, nLimFan = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "VLh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "VLvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -22255,12 +22270,15 @@ int Abc_CommandAbc9Cof( Abc_Frame_t * pAbc, int argc, char ** argv )
             {
                 fprintf( stdout, "Command line switch \"-L\" should be followed by an integer.\n" );
                 goto usage;
-            }
+            } 
             nLimFan = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
             if ( nLimFan < 0 ) 
                 goto usage;
             break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -22272,7 +22290,21 @@ int Abc_CommandAbc9Cof( Abc_Frame_t * pAbc, int argc, char ** argv )
         printf( "Abc_CommandAbc9Cof(): There is no AIG.\n" );
         return 1;
     } 
-    pAbc->pAig = Gia_ManDupCofactored( pTemp = pAbc->pAig, iVar, nLimFan );
+    if ( nLimFan )
+    {
+        printf( "Cofactoring all variables whose fanout count is higher than %d.\n", nLimFan );
+        pAbc->pAig = Gia_ManDupCofAll( pTemp = pAbc->pAig, nLimFan, fVerbose );
+    }
+    else if ( iVar )
+    {
+        printf( "Cofactoring one variable with object ID %d.\n", iVar );
+        pAbc->pAig = Gia_ManDupCof( pTemp = pAbc->pAig, iVar );
+    }
+    else
+    {
+        printf( "One of the paramters, -V <num> or -L <num>, should be set on the command line.\n" );
+        goto usage;
+    }
     if ( pAbc->pAig == NULL )
     {
         pAbc->pAig = pTemp;
@@ -22283,10 +22315,11 @@ int Abc_CommandAbc9Cof( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( stdout, "usage: &cof [-VL num] [-h]\n" );
-    fprintf( stdout, "\t         performs cofactoring w.r.t. a variable\n" );
-    fprintf( stdout, "\t-V num : the zero-based ID of the variable to cofactor [default = %d]\n", iVar );
-    fprintf( stdout, "\t-L num : cofactor w.r.t. variables whose fanout is higher [default = %d]\n", nLimFan );
+    fprintf( stdout, "usage: &cof [-VL num] [-vh]\n" );
+    fprintf( stdout, "\t         performs cofactoring w.r.t. variable(s)\n" );
+    fprintf( stdout, "\t-V num : the zero-based ID of one variable to cofactor [default = %d]\n", iVar );
+    fprintf( stdout, "\t-L num : cofactor vars with fanout count higher than this [default = %d]\n", nLimFan );
+    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;
 }
@@ -22825,9 +22858,10 @@ int Abc_CommandAbc9Frames( Abc_Frame_t * pAbc, int argc, char ** argv )
     Gia_Man_t * pTemp;
     Gia_ParFra_t Pars, * pPars = &Pars;
     int c;
+    int nCofFanLit = 0;
     Gia_ManFraSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Fivh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FLivh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -22842,6 +22876,17 @@ int Abc_CommandAbc9Frames( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nFrames < 0 ) 
                 goto usage;
             break;
+        case 'L':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-L\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nCofFanLit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nCofFanLit < 0 ) 
+                goto usage;
+            break;
         case 'i':
             pPars->fInit ^= 1;
             break;
@@ -22859,14 +22904,18 @@ int Abc_CommandAbc9Frames( Abc_Frame_t * pAbc, int argc, char ** argv )
         printf( "Abc_CommandAbc9Times(): There is no AIG.\n" );
         return 1;
     } 
-    pAbc->pAig = Gia_ManFrames( pTemp = pAbc->pAig, pPars );
+    if ( nCofFanLit )
+        pAbc->pAig = Gia_ManUnrollAndCofactor( pTemp = pAbc->pAig, pPars->nFrames, nCofFanLit, pPars->fVerbose );
+    else
+        pAbc->pAig = Gia_ManFrames( pTemp = pAbc->pAig, pPars );
     Gia_ManStop( pTemp );
     return 0;
 
 usage:
-    fprintf( stdout, "usage: &frames [-F <num>] [-ivh]\n" );
+    fprintf( stdout, "usage: &frames [-FL <num>] [-ivh]\n" );
     fprintf( stdout, "\t         unrolls the design for several timeframes\n" );
     fprintf( stdout, "\t-F num : the number of frames to unroll [default = %d]\n", pPars->nFrames );
+    fprintf( stdout, "\t-L num : the limit on fanout count of resets/enables to cofactor [default = %d]\n", nCofFanLit? "yes": "no" );
     fprintf( stdout, "\t-i     : toggle initializing registers [default = %s]\n", pPars->fInit? "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");
@@ -22929,7 +22978,7 @@ int Abc_CommandAbc9Miter( Abc_Frame_t * pAbc, int argc, char ** argv )
         }
         pAbc->pAig = Gia_ManTransformMiter( pAux = pAbc->pAig );
         Gia_ManStop( pAux );
-        printf( "Abc_CommandAbc9Miter(): Miter is transformed by merging POs pair-wise.\n" );
+        printf( "The miter (current AIG) is transformed by XORing POs pair-wise.\n" );
         return 0;
     }
 
@@ -23286,7 +23335,7 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    char * pFileName = "gia_srm.aig";
+    char * pFileName = "gsrm.aig";
     Gia_Man_t * pTemp;
     int c, fVerbose = 0;
     int fDualOut = 0;
@@ -23314,11 +23363,14 @@ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv )
     } 
 //    pAbc->pAig = Gia_ManSpecReduce( pTemp = pAbc->pAig, fDualOut );
 //    Gia_ManStop( pTemp );
-    pTemp = Gia_ManSpecReduce( pAbc->pAig, fDualOut );
-    Gia_WriteAiger( pTemp, "gia_srm.aig", 0, 0 );
-    printf( "Speculatively reduced model was written into file \"%s\".\n", pFileName );
-    Gia_ManPrintStatsShort( pTemp );
-    Gia_ManStop( pTemp );
+    pTemp = Gia_ManSpecReduce( pAbc->pAig, fDualOut, fVerbose );
+    if ( pTemp )
+    {
+        Gia_WriteAiger( pTemp, pFileName, 0, 0 );
+        printf( "Speculatively reduced model was written into file \"%s\".\n", pFileName );
+        Gia_ManPrintStatsShort( pTemp );
+        Gia_ManStop( pTemp );
+    }
     return 0;
 
 usage:
@@ -23346,14 +23398,18 @@ int Abc_CommandAbc9Reduce( Abc_Frame_t * pAbc, int argc, char ** argv )
     Gia_Man_t * pTemp;
     int c, fVerbose = 0;
     int fUseAll = 0;
+    int fDualOut = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "avh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "advh" ) ) != EOF )
     {
         switch ( c )
         {
         case 'a':
             fUseAll ^= 1;
             break;
+        case 'd':
+            fDualOut ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -23368,14 +23424,18 @@ int Abc_CommandAbc9Reduce( Abc_Frame_t * pAbc, int argc, char ** argv )
         printf( "Abc_CommandAbc9Reduce(): There is no AIG.\n" );
         return 1;
     } 
-    pAbc->pAig = Gia_ManEquivReduce( pTemp = pAbc->pAig, fUseAll );
-    Gia_ManStop( pTemp );
+    pAbc->pAig = Gia_ManEquivReduce( pTemp = pAbc->pAig, fUseAll, fDualOut, fVerbose );
+    if ( pAbc->pAig == NULL )
+        pAbc->pAig = pTemp;
+    else
+        Gia_ManStop( pTemp );
     return 0;
 
 usage:
-    fprintf( stdout, "usage: &reduce [-avh]\n" );
+    fprintf( stdout, "usage: &reduce [-advh]\n" );
     fprintf( stdout, "\t         reduces the circuit using equivalence classes\n" );
-    fprintf( stdout, "\t-a     : toggle creating dual output miter [default = %s]\n", fUseAll? "yes": "no" );
+    fprintf( stdout, "\t-a     : toggle merging all equivalences [default = %s]\n", fUseAll? "yes": "no" );
+    fprintf( stdout, "\t-d     : toggle using dual-output merging [default = %s]\n", fDualOut? "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;
@@ -23922,6 +23982,9 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    Gia_ManTestDistance( pAbc->pAig );
 //    Gia_SatSolveTest( pAbc->pAig );
 //    For_ManExperiment( pAbc->pAig, 20, 1, 1 );
+//    Gia_ManUnrollSpecial( pAbc->pAig, 5, 100, 1 );
+    pAbc->pAig = Gia_ManDupSelf( pTemp = pAbc->pAig );
+    Gia_ManStop( pTemp );
     return 0;
 
 usage:
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index ca33667f..91046340 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1538,7 +1538,7 @@ Abc_Ntk_t * Abc_NtkDarLcorrNew( Abc_Ntk_t * pNtk, int nVarsMax, int nConfMax, in
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nNodeDelta, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int fVerbose )
+int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nNodeDelta, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int nCofFanLit, int fVerbose )
 {
     Aig_Man_t * pMan;
     int status, RetValue = -1, clk = clock();
@@ -1554,7 +1554,7 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nNodeDelta,
     if ( fNewAlgo )
     {
         int iFrame;
-        RetValue = Saig_ManBmcSimple( pMan, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, &iFrame );
+        RetValue = Saig_ManBmcSimple( pMan, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, &iFrame, nCofFanLit );
         ABC_FREE( pNtk->pModel );
         ABC_FREE( pNtk->pSeqModel );
         pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
@@ -1751,7 +1751,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar )
     }
     if ( pSecPar->fTryBmc )
     {
-        RetValue = Abc_NtkDarBmc( pNtk, 20, 100000, -1, 2000, -1, 0, 1, 0 );
+        RetValue = Abc_NtkDarBmc( pNtk, 20, 100000, -1, 2000, -1, 0, 1, 0, 0 );
         if ( RetValue == 0 )
         {
             printf( "Networks are not equivalent.\n" );
diff --git a/src/base/main/mainMC.c b/src/base/main/mainMC.c
index dcabaf36..7761d428 100644
--- a/src/base/main/mainMC.c
+++ b/src/base/main/mainMC.c
@@ -91,7 +91,7 @@ int main( int argc, char * argv[] )
     {
         // perform BMC
         if ( pAig->nRegs != 0 )
-            RetValue = Saig_ManBmcSimple( pAig, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, NULL );
+            RetValue = Saig_ManBmcSimple( pAig, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, NULL, 0 );
 
         // perform full-blown SEC
         if ( RetValue != 0 )
@@ -120,7 +120,7 @@ int main( int argc, char * argv[] )
         int nSizeMax = 500000;
         int nBTLimit = 10000000;
         int fRewrite = 0;
-        RetValue = Saig_ManBmcSimple( pAig, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, &Depth );
+        RetValue = Saig_ManBmcSimple( pAig, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, &Depth, 0 );
         if ( RetValue != 0 )
             RetValue = -1;
     }