Version abc80511_2

10 files changed, 240 insertions, 58 deletions

diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index 7311d414..f7ad40dd 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -104,6 +104,7 @@ struct Fra_Ssw_t_
     int              fUse1Hot;          // use one-hotness constraints
     int              fVerbose;          // enable verbose output 
     int              nIters;            // the number of iterations performed
+    float            TimeLimit;         // the runtime budget for this call
 };
 
 // FRAIG equivalence classes
@@ -312,7 +313,7 @@ extern Aig_Man_t *         Fra_FraigInduction( Aig_Man_t * p, Fra_Ssw_t * pPars
 /*=== fraIndVer.c =====================================================*/
 extern int                 Fra_InvariantVerify( Aig_Man_t * p, int nFrames, Vec_Int_t * vClauses, Vec_Int_t * vLits );
 /*=== fraLcr.c ========================================================*/
-extern Aig_Man_t *         Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int * pnIter );
+extern Aig_Man_t *         Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int * pnIter, float TimeLimit );
 /*=== fraMan.c ========================================================*/
 extern void                Fra_ParamsDefault( Fra_Par_t * pParams );
 extern void                Fra_ParamsDefaultSeq( Fra_Par_t * pParams );
@@ -328,7 +329,7 @@ extern int                 Fra_NodesAreImp( Fra_Man_t * p, Aig_Obj_t * pOld, Aig
 extern int                 Fra_NodesAreClause( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR );
 extern int                 Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew );
 /*=== fraSec.c ========================================================*/
-extern int                 Fra_FraigSec( Aig_Man_t * p, int nFrames, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose );
+extern int                 Fra_FraigSec( Aig_Man_t * p, int nFrames, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose, int TimeLimit );
 /*=== fraSim.c ========================================================*/
 extern int                 Fra_SmlNodeHash( Aig_Obj_t * pObj, int nTableSize );
 extern int                 Fra_SmlNodeIsConst( Aig_Obj_t * pObj );
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index b29fa946..99b62856 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -336,9 +336,10 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, Fra_Ssw_t * pParams )
     Fra_Par_t Pars, * pPars = &Pars; 
     Aig_Obj_t * pObj;
     Cnf_Dat_t * pCnf;
-    Aig_Man_t * pManAigNew;
+    Aig_Man_t * pManAigNew = NULL;
     int nNodesBeg, nRegsBeg;
     int nIter, i, clk = clock(), clk2;
+    int TimeToStop = (pParams->TimeLimit == 0.0)? 0 : clock() + (int)(pParams->TimeLimit * CLOCKS_PER_SEC);
 
     if ( Aig_ManNodeNum(pManAig) == 0 )
     {
@@ -419,6 +420,12 @@ PRT( "Time", clock() - clk );
     if ( pPars->fUseImps )
         p->pCla->vImps = Fra_ImpDerive( p, 5000000, pPars->nMaxImps, pPars->fLatchCorr );
 
+    if ( pParams->TimeLimit != 0.0 && clock() > TimeToStop )
+    {
+        printf( "Fra_FraigInduction(): Runtime limit exceeded.\n" );
+        goto finish;
+    }
+
     // perform BMC (for the min number of frames)
     Fra_BmcPerform( p, pPars->nFramesP, pPars->nFramesK+1 ); // +1 is needed to prevent non-refinement
 //Fra_ClassesPrint( p->pCla, 1 );
@@ -442,6 +449,13 @@ PRT( "Time", clock() - clk );
         int nLitsOld = Fra_ClassesCountLits(p->pCla);
         int nImpsOld = p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0;
         int nHotsOld = p->vOneHots? Fra_OneHotCount(p, p->vOneHots) : 0;
+
+        if ( pParams->TimeLimit != 0.0 && clock() > TimeToStop )
+        {
+            printf( "Fra_FraigInduction(): Runtime limit exceeded.\n" );
+            goto finish;
+        }
+
         // mark the classes as non-refined
         p->pCla->fRefinement = 0;
         // derive non-init K-timeframes while implementing e-classes
@@ -592,6 +606,7 @@ p->timeTotal = clock() - clk;
     p->nNodesEnd = Aig_ManNodeNum(pManAigNew);
     p->nRegsEnd  = Aig_ManRegNum(pManAigNew);
     // free the manager
+finish:
     Fra_ManStop( p );
     // check the output
 //    if ( Aig_ManPoNum(pManAigNew) - Aig_ManRegNum(pManAigNew) == 1 )
diff --git a/src/aig/fra/fraLcr.c b/src/aig/fra/fraLcr.c
index 145bafae..0f5cc207 100644
--- a/src/aig/fra/fraLcr.c
+++ b/src/aig/fra/fraLcr.c
@@ -526,7 +526,7 @@ void Fra_ClassNodesUnmark( Fra_Lcr_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int * pnIter )
+Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int * pnIter, float TimeLimit )
 {
     int nPartSize    = 200;
     int fReprSelect  = 0;
@@ -536,6 +536,7 @@ Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nC
     Aig_Man_t * pAigPart, * pAigNew = NULL;
     Vec_Int_t * vPart;
     int i, nIter, timeSim, clk = clock(), clk2, clk3;
+    int TimeToStop = (TimeLimit == 0.0)? 0 : clock() + (int)(TimeLimit * CLOCKS_PER_SEC);
     if ( Aig_ManNodeNum(pAig) == 0 )
     {
         if ( pnIter ) *pnIter = 0;
@@ -609,6 +610,15 @@ p->timePart += clock() - clk2;
         Vec_PtrClear( p->vFraigs );
         Vec_PtrForEachEntry( p->vParts, vPart, i )
         {
+            if ( TimeLimit != 0.0 && clock() > TimeToStop )
+            {
+                Vec_PtrForEachEntry( p->vFraigs, pAigPart, i )
+                    Aig_ManStop( pAigPart );
+                Aig_ManCleanMarkA( pAig );
+                Aig_ManCleanMarkB( pAig );
+                printf( "Fra_FraigLatchCorrespondence(): Runtime limit exceeded.\n" );
+                goto finish;
+            }
 clk2 = clock();
             pAigPart = Fra_LcrCreatePart( p, vPart );
 p->timeTrav += clock() - clk2;
@@ -649,7 +659,6 @@ clk2 = clock();
 p->timePart += clock() - clk2;
         }
     }
-    free( pTemp );
     p->nIters = nIter;
 
     // move the classes into representatives and reduce AIG
@@ -667,6 +676,8 @@ p->timeTotal = clock() - clk;
     p->nLitsEnd  = Fra_ClassesCountLits( p->pCla );
     p->nNodesEnd = Aig_ManNodeNum(pAigNew);
     p->nRegsEnd  = Aig_ManRegNum(pAigNew);
+finish:
+    free( pTemp );
     Lcr_ManFree( p );
     if ( pnIter ) *pnIter = nIter;
     return pAigNew;
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 9a500680..5146344c 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -40,13 +40,14 @@
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose )
+int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose, int TimeLimit )
 {
     Fra_Ssw_t Pars, * pPars = &Pars;
     Fra_Sml_t * pSml;
     Aig_Man_t * pNew, * pTemp;
     int nFrames, RetValue, nIter, clk, clkTotal = clock();
     int fLatchCorr = 0;
+    float TimeLeft = 0.0;
 
     // try the miter before solving
     pNew = Aig_ManDup( p );
@@ -119,7 +120,24 @@ clk = clock();
     pNew = Aig_ManDupOrdered( pTemp = pNew );
 //    pNew = Aig_ManDupDfs( pTemp = pNew );
     Aig_ManStop( pTemp );
-    pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 100000, 1, fVeryVerbose, &nIter );
+    if ( TimeLimit )
+    {
+        TimeLeft = (float)TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
+        TimeLeft = AIG_MAX( TimeLeft, 0.0 );
+        if ( TimeLeft == 0.0 )
+        {
+            printf( "Runtime limit exceeded.\n" );
+            RetValue = -1;
+            goto finish;
+        }
+    }
+    pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 100000, 1, fVeryVerbose, &nIter, TimeLeft );
+    if ( pNew == NULL )
+    {
+        pNew = pTemp;
+        RetValue = -1;
+        goto finish;
+    }
     p->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
     Aig_ManStop( pTemp );
     if ( pNew == NULL )
@@ -138,6 +156,18 @@ PRT( "Time", clock() - clk );
     }
     }
 
+    if ( TimeLimit )
+    {
+        TimeLeft = (float)TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
+        TimeLeft = AIG_MAX( TimeLeft, 0.0 );
+        if ( TimeLeft == 0.0 )
+        {
+            printf( "Runtime limit exceeded.\n" );
+            RetValue = -1;
+            goto finish;
+        }
+    }
+
     // perform fraiging
     if ( fFraiging )
     {
@@ -159,6 +189,18 @@ PRT( "Time", clock() - clk );
     if ( RetValue >= 0 )
         goto finish;
 
+    if ( TimeLimit )
+    {
+        TimeLeft = (float)TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
+        TimeLeft = AIG_MAX( TimeLeft, 0.0 );
+        if ( TimeLeft == 0.0 )
+        {
+            printf( "Runtime limit exceeded.\n" );
+            RetValue = -1;
+            goto finish;
+        }
+    }
+
     // perform min-area retiming
     if ( fRetimeRegs && pNew->nRegs )
     {
@@ -184,9 +226,28 @@ PRT( "Time", clock() - clk );
     if ( RetValue == -1 )
     for ( nFrames = 1; nFrames <= nFramesMax; nFrames *= 2 )
     {
+        if ( TimeLimit )
+        {
+            TimeLeft = (float)TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
+            TimeLeft = AIG_MAX( TimeLeft, 0.0 );
+            if ( TimeLeft == 0.0 )
+            {
+                printf( "Runtime limit exceeded.\n" );
+                RetValue = -1;
+                goto finish;
+            }
+        }
+
 clk = clock();
         pPars->nFramesK = nFrames;
+        pPars->TimeLimit = TimeLeft;
         pNew = Fra_FraigInduction( pTemp = pNew, pPars );
+        if ( pNew == NULL )
+        {
+            pNew = pTemp;
+            RetValue = -1;
+            goto finish;
+        }
         Aig_ManStop( pTemp );
         RetValue = Fra_FraigMiterStatus( pNew );
         if ( fVerbose )
@@ -264,11 +325,33 @@ PRT( "Time", clock() - clkTotal );
     // get the miter status
     RetValue = Fra_FraigMiterStatus( pNew );
 
+    // try interplation
+clk = clock();
+    if ( RetValue == -1 && Aig_ManRegNum(pNew) > 0 )
+    {
+        extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int fRewrite, int fTransLoop, int fVerbose, int * pDepth );
+        int Depth;
+        pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); 
+        pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); 
+        RetValue = Saig_Interpolate( pNew, 10000, 0, 1, 0, &Depth );
+        if ( fVerbose )
+        {
+        if ( RetValue == 1 )
+            printf( "Property proved using interpolation.  " );
+        else if ( RetValue == 0 )
+            printf( "Property DISPROVED with cex at depth %d using interpolation.  ", Depth );
+        else if ( RetValue == -1 )
+            printf( "Property UNDECIDED after interpolation.  " );
+        else
+            assert( 0 ); 
+PRT( "Time", clock() - clk );
+        }
+    }
+
     // try reachability analysis
-    if ( RetValue == -1 && Aig_ManRegNum(pNew) < 200 )
+    if ( RetValue == -1 && Aig_ManRegNum(pNew) < 200 && Aig_ManRegNum(pNew) > 0 )
     {
         extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose );
-        assert( Aig_ManRegNum(pNew) > 0 );
         pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); 
         pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); 
         RetValue = Aig_ManVerifyUsingBdds( pNew, 100000, 1000, 1, 1, 0 );
diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c
index a723c981..1b135212 100644
--- a/src/aig/ntl/ntlFraig.c
+++ b/src/aig/ntl/ntlFraig.c
@@ -347,7 +347,7 @@ Ntl_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, int nConfMax, int fVerbose )
 
     // perform SCL for the given design
     pAigCol->nRegs = Ntl_ModelLatchNum(Ntl_ManRootModel(p));
-    pTemp = Fra_FraigLatchCorrespondence( pAigCol, 0, nConfMax, 0, fVerbose, NULL );
+    pTemp = Fra_FraigLatchCorrespondence( pAigCol, 0, nConfMax, 0, fVerbose, NULL, 0 );
     Aig_ManStop( pTemp );
 
     // finalize the transformation
diff --git a/src/aig/saig/saigInter.c b/src/aig/saig/saigInter.c
index ffd32206..c3bb0875 100644
--- a/src/aig/saig/saigInter.c
+++ b/src/aig/saig/saigInter.c
@@ -519,8 +519,6 @@ int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int fRewrite, int fTrans
         p->pAigTrans = Saig_ManTransformed( pAig );
     else
         p->pAigTrans = Saig_ManDuplicated( pAig );
-//    p->pAigTrans = Dar_ManRwsat( pAigTemp = p->pAigTrans, 1, 0 );
-//    Aig_ManStop( pAigTemp );
     // derive CNF for the transformed AIG
 clk = clock();
     p->pCnfAig = Cnf_Derive( p->pAigTrans, Aig_ManRegNum(p->pAigTrans) ); 
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 87c040ad..f914b9c4 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -9166,6 +9166,12 @@ int Abc_CommandIProve( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
+    if ( Abc_NtkLatchNum(pNtk) > 0 )
+    {
+        fprintf( pErr, "The network has registers. Use \"dprove\".\n" );
+        return 1;
+    }
+
     clk = clock();
 
     if ( Abc_NtkIsStrash(pNtk) )
@@ -13923,7 +13929,7 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    nFrames        = 16;
+    nFrames        =  2;
     fPhaseAbstract =  1;
     fRetimeFirst   =  1;
     fRetimeRegs    =  1;
@@ -14020,6 +14026,8 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
+    int fTryComb;
+    int fTryBmc;
     int nFrames;
     int fPhaseAbstract;
     int fRetimeFirst;
@@ -14027,31 +14035,55 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fFraiging;
     int fVerbose;
     int fVeryVerbose;
+    int TimeLimit;
     int c;
 
-    extern int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose );
+    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 );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    nFrames        =  8; 
-    fPhaseAbstract =  1;
-    fRetimeFirst   =  1;
-    fRetimeRegs    =  1;
-    fFraiging      =  1;
-    fVerbose       =  0;
-    fVeryVerbose   =  0;
+    fTryComb       =   1;
+    fTryBmc        =   1;
+    nFrames        =   2; 
+    fPhaseAbstract =   1;
+    fRetimeFirst   =   1;
+    fRetimeRegs    =   1;
+    fFraiging      =   1;
+    fVerbose       =   0;
+    fVeryVerbose   =   0;
+    TimeLimit      = 300;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Farmfwvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "cbTFarmfwvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'c':
+            fTryComb ^= 1;
+            break;
+        case 'b':
+            fTryBmc ^= 1;
+            break;
+        case 'T':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-T\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            TimeLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( TimeLimit < 0 ) 
+                goto usage;
+            break;
         case 'F':
             if ( globalUtilOptind >= argc )
             {
-                fprintf( pErr, "Command line switch \"-K\" should be followed by an integer.\n" );
+                fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
                 goto usage;
             }
             nFrames = atoi(argv[globalUtilOptind]);
@@ -14095,13 +14127,16 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // perform verification
-    Abc_NtkDarProve( pNtk, nFrames, fPhaseAbstract, fRetimeFirst, fRetimeRegs, fFraiging, fVerbose, fVeryVerbose );
+    Abc_NtkDarProve( pNtk, fTryComb, fTryBmc, nFrames, fPhaseAbstract, fRetimeFirst, fRetimeRegs, fFraiging, fVerbose, fVeryVerbose, TimeLimit );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: dprove [-F num] [-armfwvh]\n" );
+    fprintf( pErr, "usage: dprove [-F num] [-T num] [-carmfwvh]\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" );
@@ -14742,7 +14777,7 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
     nBTLimit   = 20000;
     fRewrite   = 0;
     fTransLoop = 1;
-    fVerbose   = 1;
+    fVerbose   = 0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "Crtvh" ) ) != EOF )
     {
@@ -17530,11 +17565,11 @@ int Abc_CommandAbc8DSec( Abc_Frame_t * pAbc, int argc, char ** argv )
     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 );
+    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 Aig_Man_t * Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 );
 
     // set defaults
-    nFrames        =  8;
+    nFrames        =  2;
     fPhaseAbstract =  0;
     fRetimeFirst   =  0;
     fRetimeRegs    =  0;
@@ -17591,7 +17626,7 @@ 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 );
+    Fra_FraigSec( pAig, nFrames, fPhaseAbstract, fRetimeFirst, fRetimeRegs, fFraiging, fVerbose, fVeryVerbose, 0 );
     Aig_ManStop( pAig );
     return 0;
 
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index d4771989..75995a60 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1115,7 +1115,7 @@ PRT( "Time", clock() - clkTotal );
 Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, Fra_Ssw_t * pPars )
 {
     Fraig_Params_t Params;
-    Abc_Ntk_t * pNtkAig, * pNtkFraig;
+    Abc_Ntk_t * pNtkAig = NULL, * pNtkFraig;
     Aig_Man_t * pMan, * pTemp;
     int clk = clock();
 
@@ -1140,20 +1140,23 @@ PRT( "Initial fraiging time", clock() - clk );
     if ( pMan == NULL )
         return NULL;
 
+//    pPars->TimeLimit = 5.0;
     pMan = Fra_FraigInduction( pTemp = pMan, pPars );
     Aig_ManStop( pTemp );
-
-    if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
-        pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
-    else
+    if ( pMan )
     {
-        Abc_Obj_t * pObj;
-        int i;
-        pNtkAig = Abc_NtkFromDar( pNtk, pMan );
-        Abc_NtkForEachLatch( pNtkAig, pObj, i )
-            Abc_LatchSetInit0( pObj );
+        if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
+            pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
+        else
+        {
+            Abc_Obj_t * pObj;
+            int i;
+            pNtkAig = Abc_NtkFromDar( pNtk, pMan );
+            Abc_NtkForEachLatch( pNtkAig, pObj, i )
+                Abc_LatchSetInit0( pObj );
+        }
+        Aig_ManStop( pMan );
     }
-    Aig_ManStop( pMan );
     return pNtkAig;
 }
 
@@ -1161,7 +1164,7 @@ PRT( "Initial fraiging time", clock() - clk );
 
   Synopsis    [Computes latch correspondence.]
 
-  Description []
+  Description [] 
                
   SideEffects []
 
@@ -1171,23 +1174,26 @@ PRT( "Initial fraiging time", clock() - clk );
 Abc_Ntk_t * Abc_NtkDarLcorr( Abc_Ntk_t * pNtk, int nFramesP, int nConfMax, int fVerbose )
 {
     Aig_Man_t * pMan, * pTemp;
-    Abc_Ntk_t * pNtkAig;
+    Abc_Ntk_t * pNtkAig = NULL;
     pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( pMan == NULL )
         return NULL;
-    pMan = Fra_FraigLatchCorrespondence( pTemp = pMan, nFramesP, nConfMax, 0, fVerbose, NULL );
+    pMan = Fra_FraigLatchCorrespondence( pTemp = pMan, nFramesP, nConfMax, 0, fVerbose, NULL, 0.0 );
     Aig_ManStop( pTemp );
-    if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
-        pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
-    else
+    if ( pMan )
     {
-        Abc_Obj_t * pObj;
-        int i;
-        pNtkAig = Abc_NtkFromDar( pNtk, pMan );
-        Abc_NtkForEachLatch( pNtkAig, pObj, i )
-            Abc_LatchSetInit0( pObj );
+        if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
+            pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
+        else
+        {
+            Abc_Obj_t * pObj;
+            int i;
+            pNtkAig = Abc_NtkFromDar( pNtk, pMan );
+            Abc_NtkForEachLatch( pNtkAig, pObj, i )
+                Abc_LatchSetInit0( pObj );
+        }
+        Aig_ManStop( pMan );
     }
-    Aig_ManStop( pMan );
     return pNtkAig;
 }
 
@@ -1205,13 +1211,13 @@ Abc_Ntk_t * Abc_NtkDarLcorr( Abc_Ntk_t * pNtk, int nFramesP, int nConfMax, int f
 int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nBTLimit, int fRewrite, int fNewAlgo, int fVerbose )
 {
     Aig_Man_t * pMan;
-    int RetValue, clk = clock();
+    int RetValue = -1, clk = clock();
     // derive the AIG manager
     pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( pMan == NULL )
     {
         printf( "Converting miter into AIG has failed.\n" );
-        return -1;
+        return RetValue;
     }
     assert( pMan->nRegs > 0 );
     pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan);
@@ -1221,6 +1227,7 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nBTLimit, int fRewrite, in
     {
         int iFrame;
         RetValue = Saig_ManBmcSimple( pMan, nFrames, nBTLimit, fRewrite, fVerbose, &iFrame );
+        pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
         if ( RetValue == 1 )
             printf( "No output was asserted in %d frames. ", nFrames );
         else if ( RetValue == -1 )
@@ -1239,13 +1246,17 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nBTLimit, int fRewrite, in
         {
             Fra_Cex_t * pCex = pNtk->pSeqModel;
             printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump the trace). ", pCex->iPo, pCex->iFrame );
+            RetValue = 0;
         }
         else
+        {
             printf( "No output was asserted in %d frames. ", nFrames );
+            RetValue = 1;
+        }
     }
 PRT( "Time", clock() - clk );
     Aig_ManStop( pMan );
-    return 1;
+    return RetValue;
 }
 
 /**Function*************************************************************
@@ -1298,10 +1309,38 @@ PRT( "Time", clock() - clk );
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose )
+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 )
 {
     Aig_Man_t * pMan;
     int RetValue;
+    if ( fTryComb )
+    {
+        Prove_Params_t Params, * pParams = &Params;
+        Abc_Ntk_t * pNtkComb;
+        int RetValue, clk = clock();
+        // create combinational network
+        pNtkComb = Abc_NtkDup( pNtk );
+        Abc_NtkMakeComb( pNtkComb, 1 );
+        // solve it using combinational equivalence checking
+        Prove_ParamsSetDefault( pParams );
+        RetValue = Abc_NtkIvyProve( &pNtkComb, pParams );
+        // transfer model if given
+        pNtk->pModel = pNtkComb->pModel; pNtkComb->pModel = NULL;
+        Abc_NtkDelete( pNtkComb );
+        // return the result, if solved
+        if ( RetValue == 1 )
+        {
+            printf( "Networks are equivalent after CEC.   " );
+            PRT( "Time", clock() - clk );
+            return RetValue;
+        }
+    }
+    if ( fTryBmc )
+    {
+        RetValue = Abc_NtkDarBmc( pNtk, 10, 1000, 0, 1, 0 );
+        if ( RetValue == 0 )
+            return RetValue;
+    }
     // derive the AIG manager
     pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( pMan == NULL )
@@ -1311,7 +1350,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fPhaseAbstract, int fRet
     }
     assert( pMan->nRegs > 0 );
     // perform verification
-    RetValue = Fra_FraigSec( pMan, nFrames, fPhaseAbstract, fRetimeFirst, fRetimeRegs, fFraiging, fVerbose, fVeryVerbose );
+    RetValue = Fra_FraigSec( pMan, nFrames, fPhaseAbstract, fRetimeFirst, fRetimeRegs, fFraiging, fVerbose, fVeryVerbose, TimeLimit );
     pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
     if ( pNtk->pSeqModel )
     {
@@ -1405,7 +1444,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 );
+    RetValue = Fra_FraigSec( pMan, nFrames, fPhaseAbstract, fRetimeFirst, fRetimeRegs, fFraiging, fVerbose, fVeryVerbose, 0 );
     Aig_ManStop( pMan );
     return RetValue;
 }
diff --git a/src/map/pcm/module.make b/src/map/pcm/module.make
new file mode 100644
index 00000000..e69de29b
--- /dev/null
+++ b/src/map/pcm/module.make
diff --git a/src/map/ply/module.make b/src/map/ply/module.make
new file mode 100644
index 00000000..e69de29b
--- /dev/null
+++ b/src/map/ply/module.make