Version abc80515

7 files changed, 195 insertions, 171 deletions

diff --git a/src/base/abc/1.txt b/src/base/abc/1.txt
deleted file mode 100644
index c0765c2b..00000000
--- a/src/base/abc/1.txt
+++ /dev/null
@@ -1,21 +0,0 @@
-Comparing files abcDfs.c and C:\_PROJECTS\AARON\FRETIME\SRC\BASE\ABC\ABCDFS.C
-***** abcDfs.c
-        return pNode->Level;
-    assert( Abc_ObjIsNode( pNode ) );
-    // if this node is already visited, return
-***** C:\_PROJECTS\AARON\FRETIME\SRC\BASE\ABC\ABCDFS.C
-        return pNode->Level;
-    assert( Abc_ObjIsNode( pNode ) || pNode->Type == ABC_OBJ_CONST1);
-    // if this node is already visited, return
-*****
-
-***** abcDfs.c
-        return pNode->Level;
-    assert( Abc_ObjIsNode( pNode ) );
-    // if this node is already visited, return
-***** C:\_PROJECTS\AARON\FRETIME\SRC\BASE\ABC\ABCDFS.C
-        return pNode->Level;
-    assert( Abc_ObjIsNode( pNode ) || pNode->Type == ABC_OBJ_CONST1);
-    // if this node is already visited, return
-*****
-
diff --git a/src/base/abc/abcBlifMv.c b/src/base/abc/abcBlifMv.c
index 428fc6af..f945696e 100644
--- a/src/base/abc/abcBlifMv.c
+++ b/src/base/abc/abcBlifMv.c
@@ -135,6 +135,7 @@ static inline int Abc_StringGetNumber( char ** ppStr )
 ***********************************************************************/
 int Abc_NodeStrashBlifMv( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj )
 {
+    int fAddFreeVars = 1;
     char * pSop;
     Abc_Obj_t ** pValues, ** pValuesF, ** pValuesF2;
     Abc_Obj_t * pTemp, * pTemp2, * pFanin, * pFanin2, * pNet;
@@ -168,7 +169,17 @@ int Abc_NodeStrashBlifMv( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj )
         else
             Index = Abc_StringGetNumber( &pSop );
         assert( Index < nValues );
-        pValues[Index] = Abc_AigConst1(pNtkNew);
+        ////////////////////////////////////////////
+        // adding free variables for binary ND-constants
+        if ( fAddFreeVars && nValues == 2 && *pSop == '-' )
+        {
+            pValues[1] = Abc_NtkCreatePi(pNtkNew);
+            pValues[0] = Abc_ObjNot( pValues[1] );
+            Abc_ObjAssignName( pValues[1], "free_var_", Abc_ObjName(pValues[1]) );
+        }
+        else
+            pValues[Index] = Abc_AigConst1(pNtkNew);
+        ////////////////////////////////////////////
         // save the values in the fanout net
         pNet->pCopy = (Abc_Obj_t *)pValues;
         return 1;
@@ -414,7 +425,10 @@ Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk )
             for ( v = 0; v < nValues; v++ )
             {
                 pValues[v] = Abc_NtkCreatePi( pNtkNew );
-                Abc_NtkConvertAssignName( pValues[v], pNet, v );
+                if ( nValuesMax == 2 )
+                    Abc_ObjAssignName( pValues[v], Abc_ObjName(pNet), NULL );
+                else
+                    Abc_NtkConvertAssignName( pValues[v], pNet, v );
             }
             // save the values in the fanout net
             pNet->pCopy = (Abc_Obj_t *)pValues;
@@ -432,7 +446,10 @@ Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk )
             for ( v = 0; v < nValues; v++ )
             {
                 pValues[v] = Abc_NtkCreateBo( pNtkNew );
-                Abc_NtkConvertAssignName( pValues[v], pNet, v );
+                if ( nValuesMax == 2 )
+                    Abc_ObjAssignName( pValues[v], Abc_ObjName(pNet), NULL );
+                else
+                    Abc_NtkConvertAssignName( pValues[v], pNet, v );
                 nCount1++;
             }
             // save the values in the fanout net
@@ -455,7 +472,10 @@ Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk )
             for ( k = 0; k < nBits; k++ )
             {
                 pBits[k] = Abc_NtkCreatePi( pNtkNew );
-                Abc_NtkConvertAssignName( pBits[k], pNet, k );
+                if ( nValuesMax == 2 )
+                    Abc_ObjAssignName( pBits[k], Abc_ObjName(pNet), NULL );
+                else
+                    Abc_NtkConvertAssignName( pBits[k], pNet, k );
             }
             // encode the values
             for ( v = 0; v < nValues; v++ )
@@ -484,7 +504,10 @@ Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk )
             for ( k = 0; k < nBits; k++ )
             {
                 pBits[k] = Abc_NtkCreateBo( pNtkNew );
-                Abc_NtkConvertAssignName( pBits[k], pNet, k );
+                if ( nValuesMax == 2 )
+                    Abc_ObjAssignName( pBits[k], Abc_ObjName(pNet), NULL );
+                else
+                    Abc_NtkConvertAssignName( pBits[k], pNet, k );
                 nCount1++;
             }
             // encode the values
@@ -522,16 +545,19 @@ Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk )
                 continue;
             pNet = Abc_ObjFanin0(pObj);
             // skip marked nets
-            if ( Abc_NodeIsTravIdCurrent(pNet) )
-                continue;
-            Abc_NodeSetTravIdCurrent( pNet );
+//            if ( Abc_NodeIsTravIdCurrent(pNet) )
+//                continue;
+//            Abc_NodeSetTravIdCurrent( pNet );
             nValues = Abc_ObjMvVarNum(pNet);
             pValues = (Abc_Obj_t **)pNet->pCopy;
             for ( v = 0; v < nValues; v++ )
             {
                 pTemp = Abc_NtkCreatePo( pNtkNew );
                 Abc_ObjAddFanin( pTemp, pValues[v] );
-                Abc_NtkConvertAssignName( pTemp, pNet, v );
+                if ( nValuesMax == 2 )
+                    Abc_ObjAssignName( pTemp, Abc_ObjName(pNet), NULL );
+                else
+                    Abc_NtkConvertAssignName( pTemp, pNet, v );
             }
         }
         Abc_NtkForEachCo( pNtk, pObj, i )
@@ -540,21 +566,24 @@ Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk )
                 continue;
             pNet = Abc_ObjFanin0(pObj);
             // skip marked nets
-            if ( Abc_NodeIsTravIdCurrent(pNet) )
-                continue;
-            Abc_NodeSetTravIdCurrent( pNet );
+//            if ( Abc_NodeIsTravIdCurrent(pNet) )
+//                continue;
+//            Abc_NodeSetTravIdCurrent( pNet );
             nValues = Abc_ObjMvVarNum(pNet);
             pValues = (Abc_Obj_t **)pNet->pCopy;
             for ( v = 0; v < nValues; v++ )
             {
                 pTemp = Abc_NtkCreateBi( pNtkNew );
                 Abc_ObjAddFanin( pTemp, pValues[v] );
-                Abc_NtkConvertAssignName( pTemp, pNet, v );
+                if ( nValuesMax == 2 )
+                    Abc_ObjAssignName( pTemp, Abc_ObjName(pNet), NULL );
+                else
+                    Abc_NtkConvertAssignName( pTemp, pNet, v );
                 nCount2++;
             }
         }
     }
-    else
+    else // if ( fPositional == 0 )
     {
         Abc_NtkForEachCo( pNtk, pObj, i )
         {
@@ -562,9 +591,9 @@ Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk )
                 continue;
             pNet = Abc_ObjFanin0(pObj);
             // skip marked nets
-            if ( Abc_NodeIsTravIdCurrent(pNet) )
-                continue;
-            Abc_NodeSetTravIdCurrent( pNet );
+//            if ( Abc_NodeIsTravIdCurrent(pNet) )
+//                continue;
+//            Abc_NodeSetTravIdCurrent( pNet );
             nValues = Abc_ObjMvVarNum(pNet);
             pValues = (Abc_Obj_t **)pNet->pCopy;
             nBits = Extra_Base2Log( nValues );
@@ -576,7 +605,10 @@ Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk )
                         pBit = Abc_AigOr( pNtkNew->pManFunc, pBit, pValues[v] );
                 pTemp = Abc_NtkCreatePo( pNtkNew );
                 Abc_ObjAddFanin( pTemp, pBit );
-                Abc_NtkConvertAssignName( pTemp, pNet, k );
+                if ( nValuesMax == 2 )
+                    Abc_ObjAssignName( pTemp, Abc_ObjName(pNet), NULL );
+                else
+                    Abc_NtkConvertAssignName( pTemp, pNet, k );
             }
         }
         Abc_NtkForEachCo( pNtk, pObj, i )
@@ -585,9 +617,9 @@ Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk )
                 continue;
             pNet = Abc_ObjFanin0(pObj);
             // skip marked nets
-            if ( Abc_NodeIsTravIdCurrent(pNet) )
-                continue;
-            Abc_NodeSetTravIdCurrent( pNet );
+//            if ( Abc_NodeIsTravIdCurrent(pNet) )
+//                continue;
+//            Abc_NodeSetTravIdCurrent( pNet );
             nValues = Abc_ObjMvVarNum(pNet);
             pValues = (Abc_Obj_t **)pNet->pCopy;
             nBits = Extra_Base2Log( nValues );
@@ -599,7 +631,10 @@ Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk )
                         pBit = Abc_AigOr( pNtkNew->pManFunc, pBit, pValues[v] );
                 pTemp = Abc_NtkCreateBi( pNtkNew );
                 Abc_ObjAddFanin( pTemp, pBit );
-                Abc_NtkConvertAssignName( pTemp, pNet, k );
+                if ( nValuesMax == 2 )
+                    Abc_ObjAssignName( pTemp, Abc_ObjName(pNet), NULL );
+                else
+                    Abc_NtkConvertAssignName( pTemp, pNet, k );
                 nCount2++;
             }
         }
@@ -607,8 +642,32 @@ Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk )
 
     if ( Abc_NtkLatchNum(pNtk) )
     {
+        Vec_Ptr_t * vTemp;
         Abc_Obj_t * pLatch, * pObjLi, * pObjLo;
         int i;
+        // move free vars to the front among the PIs
+        vTemp = Vec_PtrAlloc( Vec_PtrSize(pNtkNew->vPis) );
+        Abc_NtkForEachPi( pNtkNew, pObj, i )
+            if ( strncmp( Abc_ObjName(pObj), "free_var_", 9 ) == 0 )
+                Vec_PtrPush( vTemp, pObj );
+        Abc_NtkForEachPi( pNtkNew, pObj, i )
+            if ( strncmp( Abc_ObjName(pObj), "free_var_", 9 ) != 0 )
+                Vec_PtrPush( vTemp, pObj );
+        assert( Vec_PtrSize(vTemp) == Vec_PtrSize(pNtkNew->vPis) );
+        Vec_PtrFree( pNtkNew->vPis );
+        pNtkNew->vPis = vTemp;
+        // move free vars to the front among the CIs
+        vTemp = Vec_PtrAlloc( Vec_PtrSize(pNtkNew->vCis) );
+        Abc_NtkForEachCi( pNtkNew, pObj, i )
+            if ( strncmp( Abc_ObjName(pObj), "free_var_", 9 ) == 0 )
+                Vec_PtrPush( vTemp, pObj );
+        Abc_NtkForEachCi( pNtkNew, pObj, i )
+            if ( strncmp( Abc_ObjName(pObj), "free_var_", 9 ) != 0 )
+                Vec_PtrPush( vTemp, pObj );
+        assert( Vec_PtrSize(vTemp) == Vec_PtrSize(pNtkNew->vCis) );
+        Vec_PtrFree( pNtkNew->vCis );
+        pNtkNew->vCis = vTemp;
+        // create registers
         assert( nCount1 == nCount2 );
         for ( i = 0; i < nCount1; i++ )
         {
diff --git a/src/base/abc/abcBlifMv.zip b/src/base/abc/abcBlifMv.zip
new file mode 100644
index 00000000..4a4d080a
--- /dev/null
+++ b/src/base/abc/abcBlifMv.zip
diff --git a/src/base/abc/abcFanio.c b/src/base/abc/abcFanio.c
index c8536695..9f60b0bc 100644
--- a/src/base/abc/abcFanio.c
+++ b/src/base/abc/abcFanio.c
@@ -92,6 +92,10 @@ void Abc_ObjAddFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin )
     {
         int x = 0; 
     }
+    if ( pObj->Id == 1960 )
+    {
+        int x = 0;
+    }
 //    printf( "Adding fanin of %s ", Abc_ObjName(pObj) );
 //    printf( "to be %s\n", Abc_ObjName(pFanin) );
 }
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 151e9ddc..0437f8a9 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -13915,34 +13915,24 @@ usage:
 ***********************************************************************/
 int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
+    Fra_Sec_t SecPar, * pSecPar = &SecPar;
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtk1, * pNtk2;
     int fDelete1, fDelete2;
     char ** pArgvNew;
     int nArgcNew;
-    int nFrames;
-    int fPhaseAbstract;
-    int fRetimeFirst;
-    int fRetimeRegs;
-    int fFraiging;
-    int fVerbose;
-    int fVeryVerbose;
     int c;
 
-    extern int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose );
+    extern void Fra_SecSetDefaultParams( Fra_Sec_t * p );
+    extern int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Fra_Sec_t * p );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    nFrames        =  2;
-    fPhaseAbstract =  1;
-    fRetimeFirst   =  1;
-    fRetimeRegs    =  1;
-    fFraiging      =  1;
-    fVerbose       =  0;
-    fVeryVerbose   =  0;
+    Fra_SecSetDefaultParams( pSecPar );
+    pSecPar->TimeLimit = 300;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "Farmfwvh" ) ) != EOF )
     {
@@ -13954,28 +13944,28 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
                 fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
                 goto usage;
             }
-            nFrames = atoi(argv[globalUtilOptind]);
+            pSecPar->nFramesMax = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( nFrames < 0 ) 
+            if ( pSecPar->nFramesMax < 0 ) 
                 goto usage;
             break;
         case 'a':
-            fPhaseAbstract ^= 1;
+            pSecPar->fPhaseAbstract ^= 1;
             break;
         case 'r':
-            fRetimeFirst ^= 1;
+            pSecPar->fRetimeFirst ^= 1;
             break;
         case 'm':
-            fRetimeRegs ^= 1;
+            pSecPar->fRetimeRegs ^= 1;
             break;
         case 'f':
-            fFraiging ^= 1;
+            pSecPar->fFraiging ^= 1;
             break;
         case 'w':
-            fVeryVerbose ^= 1;
+            pSecPar->fVeryVerbose ^= 1;
             break;
         case 'v':
-            fVerbose ^= 1;
+            pSecPar->fVerbose ^= 1;
             break;
         default:
             goto usage;
@@ -13994,7 +13984,7 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // perform verification
-    Abc_NtkDarSec( pNtk1, pNtk2, nFrames, fPhaseAbstract, fRetimeFirst, fRetimeRegs, fFraiging, fVerbose, fVeryVerbose );
+    Abc_NtkDarSec( pNtk1, pNtk2, pSecPar );
 
     if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
     if ( fDelete2 ) Abc_NtkDelete( pNtk2 );
@@ -14003,13 +13993,13 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
 usage:
     fprintf( pErr, "usage: dsec [-F num] [-armfwvh] <file1> <file2>\n" );
     fprintf( pErr, "\t         performs inductive sequential equivalence checking\n" );
-    fprintf( pErr, "\t-F num : the limit on the depth of induction [default = %d]\n", nFrames );
-    fprintf( pErr, "\t-a     : toggles the use of phase abstraction [default = %s]\n", fPhaseAbstract? "yes": "no" );
-    fprintf( pErr, "\t-r     : toggles forward retiming at the beginning [default = %s]\n", fRetimeFirst? "yes": "no" );
-    fprintf( pErr, "\t-m     : toggles min-register retiming [default = %s]\n", fRetimeRegs? "yes": "no" );
-    fprintf( pErr, "\t-f     : toggles the internal use of fraiging [default = %s]\n", fFraiging? "yes": "no" );
-    fprintf( pErr, "\t-v     : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
-    fprintf( pErr, "\t-w     : toggles additional verbose output [default = %s]\n", fVeryVerbose? "yes": "no" );
+    fprintf( pErr, "\t-F num : the limit on the depth of induction [default = %d]\n", pSecPar->nFramesMax );
+    fprintf( pErr, "\t-a     : toggles the use of phase abstraction [default = %s]\n", pSecPar->fPhaseAbstract? "yes": "no" );
+    fprintf( pErr, "\t-r     : toggles forward retiming at the beginning [default = %s]\n", pSecPar->fRetimeFirst? "yes": "no" );
+    fprintf( pErr, "\t-m     : toggles min-register retiming [default = %s]\n", pSecPar->fRetimeRegs? "yes": "no" );
+    fprintf( pErr, "\t-f     : toggles the internal use of fraiging [default = %s]\n", pSecPar->fFraiging? "yes": "no" );
+    fprintf( pErr, "\t-v     : toggles verbose output [default = %s]\n", pSecPar->fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-w     : toggles additional verbose output [default = %s]\n", pSecPar->fVeryVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     fprintf( pErr, "\tfile1  : (optional) the file with the first network\n");
     fprintf( pErr, "\tfile2  : (optional) the file with the second network\n");
@@ -14031,50 +14021,31 @@ usage:
 ***********************************************************************/
 int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
+    Fra_Sec_t SecPar, * pSecPar = &SecPar;
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
-    int fTryComb;
-    int fTryBmc;
-    int nFrames;
-    int fPhaseAbstract;
-    int fRetimeFirst;
-    int fRetimeRegs;
-    int fFraiging;
-    int fVerbose;
-    int fVeryVerbose;
-    int TimeLimit;
     int c;
 
-    extern int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int fTryComb, int fTryBmc, 
-                                int nFrames, int fPhaseAbstract, int fRetimeFirst, 
-                                int fRetimeRegs, int fFraiging, int fVerbose, 
-                                int fVeryVerbose, int TimeLimit );
+    extern void Fra_SecSetDefaultParams( Fra_Sec_t * p );
+    extern int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    fTryComb       =   1;
-    fTryBmc        =   1;
-    nFrames        =   2; 
-    fPhaseAbstract =   1;
-    fRetimeFirst   =   1;
-    fRetimeRegs    =   1;
-    fFraiging      =   1;
-    fVerbose       =   0;
-    fVeryVerbose   =   0;
-    TimeLimit      = 300;
+    Fra_SecSetDefaultParams( pSecPar );
+    pSecPar->TimeLimit = 300;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "cbTFarmfwvh" ) ) != EOF )
     {
         switch ( c )
         {
         case 'c':
-            fTryComb ^= 1;
+            pSecPar->fTryComb ^= 1;
             break;
         case 'b':
-            fTryBmc ^= 1;
+            pSecPar->fTryBmc ^= 1;
             break;
         case 'T':
             if ( globalUtilOptind >= argc )
@@ -14082,9 +14053,9 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
                 fprintf( pErr, "Command line switch \"-T\" should be followed by an integer.\n" );
                 goto usage;
             }
-            TimeLimit = atoi(argv[globalUtilOptind]);
+            pSecPar->TimeLimit = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( TimeLimit < 0 ) 
+            if ( pSecPar->TimeLimit < 0 ) 
                 goto usage;
             break;
         case 'F':
@@ -14093,40 +14064,34 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
                 fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
                 goto usage;
             }
-            nFrames = atoi(argv[globalUtilOptind]);
+            pSecPar->nFramesMax = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( nFrames < 0 ) 
+            if ( pSecPar->nFramesMax < 0 ) 
                 goto usage;
             break;
         case 'a':
-            fPhaseAbstract ^= 1;
+            pSecPar->fPhaseAbstract ^= 1;
             break;
         case 'r':
-            fRetimeFirst ^= 1;
+            pSecPar->fRetimeFirst ^= 1;
             break;
         case 'm':
-            fRetimeRegs ^= 1;
+            pSecPar->fRetimeRegs ^= 1;
             break;
         case 'f':
-            fFraiging ^= 1;
+            pSecPar->fFraiging ^= 1;
             break;
         case 'w':
-            fVeryVerbose ^= 1;
+            pSecPar->fVeryVerbose ^= 1;
             break;
         case 'v':
-            fVerbose ^= 1;
+            pSecPar->fVerbose ^= 1;
             break;
         default:
             goto usage;
         }
     }
 
-    if ( Abc_NtkLatchNum(pNtk) == 0 )
-    {
-        printf( "The network has no latches. Running combinational command \"iprove\".\n" );
-        Cmd_CommandExecute( pAbc, "orpos; st; iprove" );
-        return 0;
-    }
     if ( !Abc_NtkIsStrash(pNtk) )
     {
         printf( "This command works only for structrally hashed networks. Run \"st\".\n" );
@@ -14134,22 +14099,22 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // perform verification
-    Abc_NtkDarProve( pNtk, fTryComb, fTryBmc, nFrames, fPhaseAbstract, fRetimeFirst, fRetimeRegs, fFraiging, fVerbose, fVeryVerbose, TimeLimit );
+    Abc_NtkDarProve( pNtk, pSecPar );
     return 0;
 
 usage:
     fprintf( pErr, "usage: dprove [-F num] [-T num] [-cbarmfwvh]\n" );
     fprintf( pErr, "\t         performs SEC on the sequential miter\n" );
-    fprintf( pErr, "\t-F num : the limit on the depth of induction [default = %d]\n", nFrames );
-    fprintf( pErr, "\t-T num : the approximate runtime limit (in seconds) [default = %d]\n", TimeLimit );
-    fprintf( pErr, "\t-c     : toggles using CEC before attempting SEC [default = %s]\n", fTryComb? "yes": "no" );
-    fprintf( pErr, "\t-b     : toggles using BMC before attempting SEC [default = %s]\n", fTryBmc? "yes": "no" );
-    fprintf( pErr, "\t-a     : toggles the use of phase abstraction [default = %s]\n", fPhaseAbstract? "yes": "no" );
-    fprintf( pErr, "\t-r     : toggles forward retiming at the beginning [default = %s]\n", fRetimeFirst? "yes": "no" );
-    fprintf( pErr, "\t-m     : toggles min-register retiming [default = %s]\n", fRetimeRegs? "yes": "no" );
-    fprintf( pErr, "\t-f     : toggles the internal use of fraiging [default = %s]\n", fFraiging? "yes": "no" );
-    fprintf( pErr, "\t-v     : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
-    fprintf( pErr, "\t-w     : toggles additional verbose output [default = %s]\n", fVeryVerbose? "yes": "no" );
+    fprintf( pErr, "\t-F num : the limit on the depth of induction [default = %d]\n", pSecPar->nFramesMax );
+    fprintf( pErr, "\t-T num : the approximate runtime limit (in seconds) [default = %d]\n", pSecPar->TimeLimit );
+    fprintf( pErr, "\t-c     : toggles using CEC before attempting SEC [default = %s]\n", pSecPar->fTryComb? "yes": "no" );
+    fprintf( pErr, "\t-b     : toggles using BMC before attempting SEC [default = %s]\n", pSecPar->fTryBmc? "yes": "no" );
+    fprintf( pErr, "\t-a     : toggles the use of phase abstraction [default = %s]\n", pSecPar->fPhaseAbstract? "yes": "no" );
+    fprintf( pErr, "\t-r     : toggles forward retiming at the beginning [default = %s]\n", pSecPar->fRetimeFirst? "yes": "no" );
+    fprintf( pErr, "\t-m     : toggles min-register retiming [default = %s]\n", pSecPar->fRetimeRegs? "yes": "no" );
+    fprintf( pErr, "\t-f     : toggles the internal use of fraiging [default = %s]\n", pSecPar->fFraiging? "yes": "no" );
+    fprintf( pErr, "\t-v     : toggles verbose output [default = %s]\n", pSecPar->fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-w     : toggles additional verbose output [default = %s]\n", pSecPar->fVeryVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
 }
@@ -17575,29 +17540,22 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc8DSec( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
+    Fra_Sec_t SecPar, * pSecPar = &SecPar;
     Aig_Man_t * pAig;
     char ** pArgvNew;
     int nArgcNew;
-    int nFrames;
-    int fPhaseAbstract;
-    int fRetimeFirst;
-    int fRetimeRegs;
-    int fFraiging;
-    int fVerbose;
-    int fVeryVerbose;
     int c;
 
-    extern int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose, int TimeLimit );
+    extern void Fra_SecSetDefaultParams( Fra_Sec_t * pSecPar );
+    extern int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pSecPar );
     extern Aig_Man_t * Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 );
 
     // set defaults
-    nFrames        =  2;
-    fPhaseAbstract =  0;
-    fRetimeFirst   =  0;
-    fRetimeRegs    =  0;
-    fFraiging      =  1;
-    fVerbose       =  0;
-    fVeryVerbose   =  0;
+    Fra_SecSetDefaultParams( pSecPar );
+    pSecPar->nFramesMax     = 2;
+    pSecPar->fPhaseAbstract = 0;
+    pSecPar->fRetimeFirst   = 0;
+    pSecPar->fRetimeRegs    = 0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "Farmfwvh" ) ) != EOF )
     {
@@ -17609,28 +17567,28 @@ int Abc_CommandAbc8DSec( Abc_Frame_t * pAbc, int argc, char ** argv )
                 fprintf( stdout, "Command line switch \"-F\" should be followed by an integer.\n" );
                 goto usage;
             }
-            nFrames = atoi(argv[globalUtilOptind]);
+            pSecPar->nFramesMax = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( nFrames < 0 ) 
+            if ( pSecPar->nFramesMax < 0 ) 
                 goto usage;
             break;
         case 'a':
-            fPhaseAbstract ^= 1;
+            pSecPar->fPhaseAbstract ^= 1;
             break;
         case 'r':
-            fRetimeFirst ^= 1;
+            pSecPar->fRetimeFirst ^= 1;
             break;
         case 'm':
-            fRetimeRegs ^= 1;
+            pSecPar->fRetimeRegs ^= 1;
             break;
         case 'f':
-            fFraiging ^= 1;
+            pSecPar->fFraiging ^= 1;
             break;
         case 'w':
-            fVeryVerbose ^= 1;
+            pSecPar->fVeryVerbose ^= 1;
             break;
         case 'v':
-            fVerbose ^= 1;
+            pSecPar->fVerbose ^= 1;
             break;
         default:
             goto usage;
@@ -17648,20 +17606,20 @@ int Abc_CommandAbc8DSec( Abc_Frame_t * pAbc, int argc, char ** argv )
     pAig = Ntl_ManPrepareSec( pArgvNew[0], pArgvNew[1] );
     if ( pAig == NULL )
         return 0;
-    Fra_FraigSec( pAig, nFrames, fPhaseAbstract, fRetimeFirst, fRetimeRegs, fFraiging, fVerbose, fVeryVerbose, 0 );
+    Fra_FraigSec( pAig, pSecPar );
     Aig_ManStop( pAig );
     return 0;
 
 usage:
     fprintf( stdout, "usage: *dsec [-F num] [-armfwvh] <file1> <file2>\n" );
     fprintf( stdout, "\t         performs sequential equivalence checking for two designs\n" );
-    fprintf( stdout, "\t-F num : the limit on the depth of induction [default = %d]\n", nFrames );
-    fprintf( stdout, "\t-a     : toggles the use of phase abstraction [default = %s]\n", fPhaseAbstract? "yes": "no" );
-    fprintf( stdout, "\t-r     : toggles forward retiming at the beginning [default = %s]\n", fRetimeFirst? "yes": "no" );
-    fprintf( stdout, "\t-m     : toggles min-register retiming [default = %s]\n", fRetimeRegs? "yes": "no" );
-    fprintf( stdout, "\t-f     : toggles the internal use of fraiging [default = %s]\n", fFraiging? "yes": "no" );
-    fprintf( stdout, "\t-v     : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
-    fprintf( stdout, "\t-w     : toggles additional verbose output [default = %s]\n", fVeryVerbose? "yes": "no" );
+    fprintf( stdout, "\t-F num : the limit on the depth of induction [default = %d]\n", pSecPar->nFramesMax );
+    fprintf( stdout, "\t-a     : toggles the use of phase abstraction [default = %s]\n", pSecPar->fPhaseAbstract? "yes": "no" );
+    fprintf( stdout, "\t-r     : toggles forward retiming at the beginning [default = %s]\n", pSecPar->fRetimeFirst? "yes": "no" );
+    fprintf( stdout, "\t-m     : toggles min-register retiming [default = %s]\n", pSecPar->fRetimeRegs? "yes": "no" );
+    fprintf( stdout, "\t-f     : toggles the internal use of fraiging [default = %s]\n", pSecPar->fFraiging? "yes": "no" );
+    fprintf( stdout, "\t-v     : toggles verbose output [default = %s]\n", pSecPar->fVerbose? "yes": "no" );
+    fprintf( stdout, "\t-w     : toggles additional verbose output [default = %s]\n", pSecPar->fVeryVerbose? "yes": "no" );
     fprintf( stdout, "\t-h     : print the command usage\n");
     fprintf( stdout, "\tfile1  : the file with the first design\n");
     fprintf( stdout, "\tfile2  : the file with the second design\n");
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 13683e4f..7b7617e6 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1229,7 +1229,7 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nBTLimit, in
         RetValue = Saig_ManBmcSimple( pMan, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, &iFrame );
         pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
         if ( RetValue == 1 )
-            printf( "No output was asserted in %d frames. ", nFrames );
+            printf( "No output was asserted in %d frames. ", iFrame );
         else if ( RetValue == -1 )
             printf( "No output was asserted in %d frames. Reached conflict limit (%d). ", iFrame, nBTLimit );
         else // if ( RetValue == 0 )
@@ -1309,15 +1309,17 @@ PRT( "Time", clock() - clk );
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int fTryComb, int fTryBmc, int nFrames, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose, int TimeLimit )
+int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar )
 {
     Aig_Man_t * pMan;
-    int RetValue;
-    if ( fTryComb )
+    int RetValue, clkTotal = clock();
+    if ( pSecPar->fTryComb || Abc_NtkLatchNum(pNtk) == 0 )
     {
         Prove_Params_t Params, * pParams = &Params;
         Abc_Ntk_t * pNtkComb;
         int RetValue, clk = clock();
+        if ( Abc_NtkLatchNum(pNtk) == 0 )
+            printf( "The network has no latches. Running CEC.\n" );
         // create combinational network
         pNtkComb = Abc_NtkDup( pNtk );
         Abc_NtkMakeComb( pNtkComb, 1 );
@@ -1332,14 +1334,27 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int fTryComb, int fTryBmc, int nFrames, i
         {
             printf( "Networks are equivalent after CEC.   " );
             PRT( "Time", clock() - clk );
+            if ( pSecPar->fReportSolution )
+            {
+            printf( "SOLUTION: PASS       " );
+            PRT( "Time", clock() - clkTotal );
+            }
             return RetValue;
         }
     }
-    if ( fTryBmc )
+    if ( pSecPar->fTryBmc )
     {
-        RetValue = Abc_NtkDarBmc( pNtk, 20, 100000, 1000, 0, 1, 0 );
+        RetValue = Abc_NtkDarBmc( pNtk, 20, 100000, 2000, 0, 1, 0 );
         if ( RetValue == 0 )
+        {
+            printf( "Networks are not equivalent.\n" );
+            if ( pSecPar->fReportSolution )
+            {
+            printf( "SOLUTION: FAIL       " );
+            PRT( "Time", clock() - clkTotal );
+            }
             return RetValue;
+        }
     }
     // derive the AIG manager
     pMan = Abc_NtkToDar( pNtk, 0, 1 );
@@ -1350,7 +1365,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int fTryComb, int fTryBmc, int nFrames, i
     }
     assert( pMan->nRegs > 0 );
     // perform verification
-    RetValue = Fra_FraigSec( pMan, nFrames, fPhaseAbstract, fRetimeFirst, fRetimeRegs, fFraiging, fVerbose, fVeryVerbose, TimeLimit );
+    RetValue = Fra_FraigSec( pMan, pSecPar );
     pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
     if ( pNtk->pSeqModel )
     {
@@ -1372,7 +1387,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int fTryComb, int fTryBmc, int nFrames, i
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose )
+int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Fra_Sec_t * pSecPar )
 {
 //    Fraig_Params_t Params;
     Aig_Man_t * pMan;
@@ -1392,8 +1407,8 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fPhase
         extern void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames );
         printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
         // report the error
-        pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, nFrames );
-        Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pMiter->pModel, nFrames );
+        pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, pSecPar->nFramesMax );
+        Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pMiter->pModel, pSecPar->nFramesMax );
         FREE( pMiter->pModel );
         Abc_NtkDelete( pMiter );
         return 0;
@@ -1444,7 +1459,7 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fPhase
     assert( pMan->nRegs > 0 );
 
     // perform verification
-    RetValue = Fra_FraigSec( pMan, nFrames, fPhaseAbstract, fRetimeFirst, fRetimeRegs, fFraiging, fVerbose, fVeryVerbose, 0 );
+    RetValue = Fra_FraigSec( pMan, pSecPar );
     Aig_ManStop( pMan );
     return RetValue;
 }
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 6efa8b67..7538e31c 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -683,7 +683,7 @@ int IoCommandReadInit( Abc_Frame_t * pAbc, int argc, char ** argv )
                 goto usage;
         }
     }
-    if ( argc != globalUtilOptind + 1 )
+    if ( argc != globalUtilOptind && argc != globalUtilOptind + 1 )
         goto usage;
 
     if ( pNtk == NULL )
@@ -692,7 +692,16 @@ int IoCommandReadInit( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     // get the input file name
-    pFileName = argv[globalUtilOptind];
+    if ( argc == globalUtilOptind + 1 )
+        pFileName = argv[globalUtilOptind];
+    else if ( pNtk->pSpec )
+        pFileName = Extra_FileNameGenericAppend( pNtk->pSpec, ".init" );
+    else
+    {
+        printf( "File name should be given on the command line.\n" );
+        return 1;
+    }
+
     // read the file using the corresponding file reader
     pNtk = Abc_NtkDup( pNtk );
     Io_ReadBenchInit( pNtk, pFileName );