Changes to support sequential verification with reduction without speculation.

5 files changed, 243 insertions, 421 deletions

diff --git a/src/aig/cec/cecSeq.c b/src/aig/cec/cecSeq.c
index c255d50e..269c42c0 100644
--- a/src/aig/cec/cecSeq.c
+++ b/src/aig/cec/cecSeq.c
@@ -393,7 +393,7 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars )
         // write equivalence classes
         Gia_WriteAiger( pAig, "gore.aig", 0, 0 );
         // reduce the model
-        pReduce = Gia_ManSpecReduce( pAig, 0, 0, 0 );
+        pReduce = Gia_ManSpecReduce( pAig, 0, 0, 1, 0 );
         if ( pReduce )
         {
             pReduce = Gia_ManSeqStructSweep( pAux = pReduce, 1, 1, 0 );
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index b2f039a7..c4d41459 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -659,7 +659,7 @@ extern void                Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose
 extern Gia_Man_t *         Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fVerbose );
 extern Gia_Man_t *         Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs );
 extern int                 Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose );
-extern Gia_Man_t *         Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int fVerbose );
+extern Gia_Man_t *         Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int fReduce, int fVerbose );
 extern Gia_Man_t *         Gia_ManSpecReduceInit( Gia_Man_t * p, Abc_Cex_t * pInit, int nFrames, int fDualOut );
 extern Gia_Man_t *         Gia_ManSpecReduceInitFrames( Gia_Man_t * p, Abc_Cex_t * pInit, int nFramesMax, int * pnFrames, int fDualOut, int nMinOutputs );
 extern void                Gia_ManEquivTransform( Gia_Man_t * p, int fVerbose );
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index 581383ea..170830ee 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -748,7 +748,7 @@ int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int fDualOut )
+static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int fDualOut, int fSpeculate )
 {
     Gia_Obj_t * pRepr;
     unsigned iLitNew;
@@ -761,7 +761,8 @@ static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t
     iLitNew = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
     if ( pObj->Value != iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) )
         Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, pObj->Value, iLitNew) );
-    pObj->Value = iLitNew;
+    if ( fSpeculate )
+        pObj->Value = iLitNew;
 }
 
 /**Function*************************************************************
@@ -798,15 +799,15 @@ int Gia_ManHasNoEquivs( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int fDualOut )
+void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int fDualOut, int fSpeculate )
 {
     if ( ~pObj->Value )
         return;
     assert( Gia_ObjIsAnd(pObj) );
-    Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut );
-    Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits, fDualOut );
+    Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut, fSpeculate );
+    Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits, fDualOut, fSpeculate );
     pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
-    Gia_ManSpecBuild( pNew, p, pObj, vXorLits, fDualOut );
+    Gia_ManSpecBuild( pNew, p, pObj, vXorLits, fDualOut, fSpeculate );
 }
 
 /**Function*************************************************************
@@ -820,7 +821,7 @@ void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, V
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int fVerbose )
+Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int fSpeculate, int fVerbose )
 {
     Gia_Man_t * pNew, * pTemp;
     Gia_Obj_t * pObj;
@@ -862,9 +863,9 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int
     Gia_ManForEachCi( p, pObj, i )
         pObj->Value = Gia_ManAppendCi(pNew);
     Gia_ManForEachRo( p, pObj, i )
-        Gia_ManSpecBuild( pNew, p, pObj, vXorLits, fDualOut );
+        Gia_ManSpecBuild( pNew, p, pObj, vXorLits, fDualOut, fSpeculate );
     Gia_ManForEachCo( p, pObj, i )
-        Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut );
+        Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut, fSpeculate );
     if ( !fSynthesis )
     {
         Gia_ManForEachPo( p, pObj, i )
@@ -1127,6 +1128,62 @@ void Gia_ManEquivTransform( Gia_Man_t * p, int fVerbose )
 
 /**Function*************************************************************
 
+  Synopsis    [Marks proved equivalences.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManEquivMark( Gia_Man_t * p, char * pFileName, int fVerbose )
+{
+    Gia_Man_t * pMiter;
+    Gia_Obj_t * pObj;
+    int i, nLits = 0;
+    int nLitsAll, Counter = 0;
+    nLitsAll = Gia_ManEquivCountLitsAll( p );
+    if ( nLitsAll == 0 )
+    {
+        printf( "Gia_ManEquivMark(): Current AIG does not have equivalences.\n" );
+        return;
+    }
+    // read AIGER file
+    pMiter = Gia_ReadAiger( pFileName, 0 );
+    if ( pMiter == NULL )
+    {
+        printf( "Gia_ManEquivMark(): Input file %s could not be read.\n", pFileName );
+        return;
+    }
+    if ( Gia_ManPoNum(pMiter) != Gia_ManPoNum(p) + nLitsAll )
+    {
+        printf( "Gia_ManEquivMark(): The number of POs is not correct: MiterPONum(%d) != AIGPONum(%d) + AIGEquivNum(%d).\n", 
+            Gia_ManPoNum(pMiter), Gia_ManPoNum(p), nLitsAll );
+        Gia_ManStop( pMiter );
+        return;
+    }
+    // mark corresponding POs as solved
+    nLits = 0;
+    for ( i = 0; i < Gia_ManObjNum(p); i++ )
+    {
+        if ( Gia_ObjRepr(p, i) == GIA_VOID )
+            continue;
+        pObj = Gia_ManPo( pMiter, Gia_ManPoNum(p) + nLits++ );
+        if ( Gia_ObjFaninLit0p(pMiter, pObj) == 0 ) // const 0 - proven
+        {
+            Gia_ObjSetProved(p, i);
+            Counter++;
+        }
+    }
+    if ( fVerbose )
+        printf( "Set %d equivalences as proved.\n", Counter );
+    assert( nLits == nLitsAll );
+    Gia_ManStop( pMiter );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Transforms equiv classes by setting a good representative.]
 
   Description []
@@ -1534,7 +1591,7 @@ int Gia_CommandSpecI( Gia_Man_t * pGia, int nFramesInit, int nBTLimitInit, int f
             printf( "Gia_CommandSpecI: There are only trivial equiv candidates left (PO drivers). Quitting.\n" );
             break;
         }
-        pSrm = Gia_ManSpecReduce( pGia, 0, 0, 0 ); 
+        pSrm = Gia_ManSpecReduce( pGia, 0, 0, 1, 0 ); 
         // bmc2 -F 100 -C 25000
         {
             Abc_Cex_t * pCex;
@@ -1571,7 +1628,7 @@ int Gia_CommandSpecI( Gia_Man_t * pGia, int nFramesInit, int nBTLimitInit, int f
         // write equivalence classes
         Gia_WriteAiger( pGia, "gore.aig", 0, 0 );
         // reduce the model
-        pReduce = Gia_ManSpecReduce( pGia, 0, 0, 0 );
+        pReduce = Gia_ManSpecReduce( pGia, 0, 0, 1, 0 );
         if ( pReduce )
         {
             pReduce = Gia_ManSeqStructSweep( pAux = pReduce, 1, 1, 0 );
diff --git a/src/aig/ivy/ivyFraig.c b/src/aig/ivy/ivyFraig.c
index 7310d4cb..87209ca3 100644
--- a/src/aig/ivy/ivyFraig.c
+++ b/src/aig/ivy/ivyFraig.c
@@ -200,6 +200,7 @@ static void          Ivy_FraigMiterPrint( Ivy_Man_t * pNtk, char * pString, int
 static int *         Ivy_FraigCreateModel( Ivy_FraigMan_t * p );
 
 static int Ivy_FraigNodesAreEquivBdd( Ivy_Obj_t * pObj1, Ivy_Obj_t * pObj2 );
+static int Ivy_FraigCheckCone( Ivy_FraigMan_t * pGlo, Ivy_Man_t * p, Ivy_Obj_t * pObj1, Ivy_Obj_t * pObj2, int nConfLimit );
 
 static ABC_INT64_T s_nBTLimitGlobal = 0;
 static ABC_INT64_T s_nInsLimitGlobal = 0;
@@ -593,10 +594,10 @@ Ivy_FraigMan_t * Ivy_FraigStart( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParam
     }
     assert( k == Ivy_ManObjNum(pManAig) );
     // allocate storage for sim pattern
-    p->nPatWords = Ivy_BitWordNum( Ivy_ManPiNum(pManAig) );
-    p->pPatWords = ABC_ALLOC( unsigned, p->nPatWords ); 
+    p->nPatWords  = Ivy_BitWordNum( Ivy_ManPiNum(pManAig) );
+    p->pPatWords  = ABC_ALLOC( unsigned, p->nPatWords ); 
     p->pPatScores = ABC_ALLOC( int, 32 * p->nSimWords ); 
-    p->vPiVars   = Vec_PtrAlloc( 100 );
+    p->vPiVars    = Vec_PtrAlloc( 100 );
     // set random number generator
     srand( 0xABCABC );
     return p;
@@ -1992,6 +1993,7 @@ p->nClassesEnd = p->lClasses.nItems;
         if ( Ivy_ObjFaninVec(pObj) )
             Vec_PtrFree( Ivy_ObjFaninVec(pObj) );
         pObj->pNextFan0 = pObj->pNextFan1 = NULL;
+        pObj->pEquiv = NULL;
     }
     // remove dangling nodes 
     Ivy_ManCleanup( p->pManFraig );
@@ -2154,6 +2156,14 @@ p->timeSatSat += clock() - clk;
     else // if ( RetValue1 == l_Undef )
     {
 p->timeSatFail += clock() - clk;
+/*
+        if ( nBTLimit > 1000 )
+        {
+            RetValue = Ivy_FraigCheckCone( p, p->pManFraig, pOld, pNew, nBTLimit );
+            if ( RetValue != -1 )
+                return RetValue;
+        }
+*/
         // mark the node as the failed node
         if ( pOld != p->pManFraig->pConst1 ) 
             pOld->fFailTfo = 1;
@@ -2197,6 +2207,14 @@ p->timeSatSat += clock() - clk;
     else // if ( RetValue1 == l_Undef )
     {
 p->timeSatFail += clock() - clk;
+/*
+        if ( nBTLimit > 1000 )
+        {
+            RetValue = Ivy_FraigCheckCone( p, p->pManFraig, pOld, pNew, nBTLimit );
+            if ( RetValue != -1 )
+                return RetValue;
+        }
+*/
         // mark the node as the failed node
         pOld->fFailTfo = 1;
         pNew->fFailTfo = 1;
@@ -2286,6 +2304,14 @@ p->timeSatSat += clock() - clk;
     else // if ( RetValue1 == l_Undef )
     {
 p->timeSatFail += clock() - clk;
+/*
+        if ( p->pParams->nBTLimitMiter > 1000 )
+        {
+            RetValue = Ivy_FraigCheckCone( p, p->pManFraig, p->pManFraig->pConst1, pNew, p->pParams->nBTLimitMiter );
+            if ( RetValue != -1 )
+                return RetValue;
+        }
+*/
         // mark the node as the failed node
         pNew->fFailTfo = 1;
         p->nSatFailsReal++;
@@ -2773,6 +2799,150 @@ int Ivy_FraigNodesAreEquivBdd( Ivy_Obj_t * pObj1, Ivy_Obj_t * pObj2 )
     return RetValue;
 }
 
+ABC_NAMESPACE_IMPL_END
+
+#include "aig.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+/**Function*************************************************************
+
+  Synopsis    [Computes truth table of the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigExtractCone_rec( Ivy_Man_t * p, Ivy_Obj_t * pNode, Vec_Int_t * vLeaves, Vec_Int_t * vNodes )
+{
+    if ( pNode->fMarkB )
+        return;
+    pNode->fMarkB = 1;
+    if ( Ivy_ObjIsPi(pNode) )
+    {
+        Vec_IntPush( vLeaves, pNode->Id );
+        return;
+    }
+    assert( Ivy_ObjIsAnd(pNode) );
+    Ivy_FraigExtractCone_rec( p, Ivy_ObjFanin0(pNode), vLeaves, vNodes );
+    Ivy_FraigExtractCone_rec( p, Ivy_ObjFanin1(pNode), vLeaves, vNodes );
+    Vec_IntPush( vNodes, pNode->Id );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks equivalence using BDDs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Ivy_FraigExtractCone( Ivy_Man_t * p, Ivy_Obj_t * pObj1, Ivy_Obj_t * pObj2, Vec_Int_t * vLeaves )
+{
+    Aig_Man_t * pMan;
+    Aig_Obj_t * pMiter;
+    Vec_Int_t * vNodes;
+    Ivy_Obj_t * pObjIvy;
+    int i;
+    // collect nodes
+    vNodes  = Vec_IntAlloc( 100 );
+    Ivy_ManConst1(p)->fMarkB = 1;
+    Ivy_FraigExtractCone_rec( p, pObj1, vLeaves, vNodes );
+    Ivy_FraigExtractCone_rec( p, pObj2, vLeaves, vNodes );
+    Ivy_ManConst1(p)->fMarkB = 0;
+    // create new manager
+    pMan = Aig_ManStart( 1000 );
+    Ivy_ManConst1(p)->pEquiv = (Ivy_Obj_t *)Aig_ManConst1(pMan);
+    Ivy_ManForEachNodeVec( p, vLeaves, pObjIvy, i )
+    {
+        pObjIvy->pEquiv = (Ivy_Obj_t *)Aig_ObjCreatePi( pMan );
+        pObjIvy->fMarkB = 0;
+    }
+    // duplicate internal nodes
+    Ivy_ManForEachNodeVec( p, vNodes, pObjIvy, i )
+    {
+
+        pObjIvy->pEquiv = (Ivy_Obj_t *)Aig_And( pMan, (Aig_Obj_t *)Ivy_ObjChild0Equiv(pObjIvy), (Aig_Obj_t *)Ivy_ObjChild1Equiv(pObjIvy) );
+        pObjIvy->fMarkB = 0;
+
+        pMiter = (Aig_Obj_t *)pObjIvy->pEquiv;
+        assert( pMiter->fPhase == pObjIvy->fPhase );
+    }
+    // create the PO
+    pMiter = Aig_Exor( pMan, (Aig_Obj_t *)pObj1->pEquiv, (Aig_Obj_t *)pObj2->pEquiv );
+    pMiter = Aig_NotCond( pMiter, Aig_Regular(pMiter)->fPhase ^ Aig_IsComplement(pMiter) );
+
+/*
+printf( "Polarity = %d\n", pMiter->fPhase );
+    if ( Ivy_ObjIsConst1(pObj1) || Ivy_ObjIsConst1(pObj2) )
+    {
+        pMiter = Aig_NotCond( pMiter, 1 );
+printf( "***************\n" );
+    }
+*/
+    pMiter = Aig_ObjCreatePo( pMan, pMiter );
+//printf( "Polarity = %d\n", pMiter->fPhase );
+    Aig_ManCleanup( pMan );
+    Vec_IntFree( vNodes );
+    return pMan;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks equivalence using BDDs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_FraigCheckCone( Ivy_FraigMan_t * pGlo, Ivy_Man_t * p, Ivy_Obj_t * pObj1, Ivy_Obj_t * pObj2, int nConfLimit )
+{
+    extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fVerbose );
+    Vec_Int_t * vLeaves;
+    Aig_Man_t * pMan;
+    Aig_Obj_t * pObj;
+    int i, RetValue;
+    vLeaves  = Vec_IntAlloc( 100 );
+    pMan     = Ivy_FraigExtractCone( p, pObj1, pObj2, vLeaves );
+    RetValue = Fra_FraigSat( pMan, nConfLimit, 0, 0, 0, 1 ); 
+    if ( RetValue == 0 )
+    {
+        int Counter = 0;
+        memset( pGlo->pPatWords, 0, sizeof(unsigned) * pGlo->nPatWords );
+        Aig_ManForEachPi( pMan, pObj, i )
+            if ( ((int *)pMan->pData)[i] )
+            {
+                int iObjIvy = Vec_IntEntry( vLeaves, i );
+                assert( iObjIvy > 0 && iObjIvy <= Ivy_ManPiNum(p) );
+                Ivy_InfoSetBit( pGlo->pPatWords, iObjIvy-1 );
+//printf( "%d ", iObjIvy );
+Counter++;
+            }
+        assert( Counter > 0 );
+    }
+    Vec_IntFree( vLeaves );
+    if ( RetValue == 1 )
+        printf( "UNSAT\n" );
+    else if ( RetValue == 0 )
+        printf( "SAT\n" );
+    else if ( RetValue == -1 )
+        printf( "UNDEC\n" );
+
+//    p->pModel = (int *)pMan->pData, pMan2->pData = NULL;
+    Aig_ManStop( pMan );
+    return RetValue;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcDprove2.c b/src/base/abci/abcDprove2.c
deleted file mode 100644
index b9b2c10a..00000000
--- a/src/base/abci/abcDprove2.c
+++ /dev/null
@@ -1,405 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [abcDprove2.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Network and node package.]
-
-  Synopsis    [Implementation of "dprove2".]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: abcDprove2.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "abc.h"
-#include "aig.h"
-#include "saig.h"
-#include "fra.h"
-#include "ssw.h"
-#include "gia.h"
-#include "giaAig.h"
-#include "cec.h"
-#include "int.h"
-
-ABC_NAMESPACE_IMPL_START
-
- 
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-extern int Abc_NtkDarBmcInter_int( Aig_Man_t * pMan, Inter_ManParams_t * pPars );
-
-extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
-extern Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan );
-extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
-extern int         Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar );
-
-extern void * Abc_FrameReadSave1();
-extern void * Abc_FrameReadSave2();
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Implements model checking based on abstraction and speculation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_NtkDProve2( Abc_Ntk_t * pNtk, int nConfLast, int fSeparate, int fVeryVerbose, int fVerbose )
-{
-    Abc_Ntk_t * pNtk2;
-    Aig_Man_t * pMan, * pTemp;
-    Aig_Man_t * pSave1 = NULL;
-    Gia_Man_t * pGia, * pSrm;
-    int spectried = 0;
-    int absquit   = 0;
-    int absfail   = 0;
-    int RetValue = -1;
-    int clkTotal = clock();
-    // derive the AIG manager
-    ABC_FREE( pNtk->pModel );
-    ABC_FREE( pNtk->pSeqModel );
-    pMan = Abc_NtkToDar( pNtk, 0, 1 );
-    if ( pMan == NULL )
-    {
-        printf( "Converting miter into AIG has failed.\n" );
-        return RetValue;
-    }
-    assert( pMan->nRegs > 0 );
-
-    if ( fVerbose )
-    {
-        printf( "Starting BMC...\n" );
-        Aig_ManPrintStats( pMan );
-    }
-    // bmc2 -C 10000
-    {
-        int nFrames     = 2000;
-        int nNodeDelta  = 2000;
-        int nBTLimit    = 10000; // different from default
-        int nBTLimitAll = 2000000;
-        Saig_BmcPerform( pMan, 0, nFrames, nNodeDelta, 0, nBTLimit, nBTLimitAll, fVeryVerbose, 0, NULL );
-        pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
-        if ( pNtk->pSeqModel )
-            goto finish;
-    }
-
-    if ( fVerbose )
-    {
-        printf( "Starting \"dprove\"...\n" );
-        Aig_ManPrintStats( pMan );
-    }
-    // dprove -r -F 8
-    {
-        Fra_Sec_t SecPar, * pSecPar = &SecPar;
-        Fra_SecSetDefaultParams( pSecPar );
-        pSecPar->fTryBmc       ^= 1;
-        pSecPar->fRetimeFirst  ^= 1;
-        pSecPar->nFramesMax     = 8;
-        pSecPar->fInterSeparate = 0; //fSeparate;
-        pSecPar->fVerbose       = fVeryVerbose;
-        RetValue = Abc_NtkDarProve( pNtk, pSecPar );
-        // analize the result
-        if ( RetValue != -1 )
-            goto finish;
-    }
-    Aig_ManStop( pMan );
-    pSave1 = (Aig_Man_t *)Abc_FrameReadSave1();
-    pMan = Aig_ManDupSimple( pSave1 );
-
-    // abstraction
-
-    if ( fVerbose )
-    {
-        printf( "Abstraction...\n" );
-        Aig_ManPrintStats( pMan );
-    }
-abstraction:
-    {
-        Gia_ParAbs_t Pars, * pPars = &Pars;
-        Gia_ManAbsSetDefaultParams( pPars );
-        pPars->nConfMaxBmc = 25000;
-        pPars->nRatio      =     2;
-        pPars->fVerbose    = fVeryVerbose;
-/*
-        int nFramesMax  =    10;
-        int nConfMax    = 10000;
-        int fDynamic    =     1;
-        int fExtend     =     0;
-        int fSkipProof  =     0;
-        int nFramesBmc  =  2000;
-        int nConfMaxBmc = 25000;  // default 5000;
-        int nRatio      =     2;  // default 10;
-        int fUseBdds    =     0;
-        int fUseDprove  =     0;
-        int fVerbose    = fVeryVerbose;
-        fExtend    ^= 1;
-        fSkipProof ^= 1;
-*/
-        pMan = Saig_ManCexAbstraction( pTemp = pMan, pPars );
-        // if abstractin has solved the problem
-        if ( pTemp->pSeqModel )
-        {
-            pNtk->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
-            Aig_ManStop( pTemp );
-            goto finish;
-        }
-        Aig_ManStop( pTemp );
-        if ( pMan == NULL ) // abstraction quits
-        {
-            absquit = 1;
-            pMan = Aig_ManDupSimple( pSave1 );
-            goto speculation;
-        }
-    }
-    if ( fVerbose )
-    {
-        printf( "Problem before trimming...\n" );
-        Aig_ManPrintStats( pMan );
-    }
-    // trim off useless primary inputs
-    pMan = Aig_ManDupTrim( pTemp = pMan );
-    Aig_ManStop( pTemp );
-    if ( fVerbose )
-    {
-        printf( "\"dprove\" after abstraction...\n" );
-        Aig_ManPrintStats( pMan );
-    }
-    // dprove -r -F 8
-    {
-        Fra_Sec_t SecPar, * pSecPar = &SecPar;
-        Fra_SecSetDefaultParams( pSecPar );
-        pSecPar->fTryBmc       ^= 1;
-        pSecPar->fRetimeFirst  ^= 1;
-        pSecPar->nFramesMax     = 8;
-        pSecPar->fInterSeparate = 0; //fSeparate;
-        pSecPar->fVerbose       = fVeryVerbose;
-        // convert pMan into pNtk
-        pNtk2 = Abc_NtkFromAigPhase( pMan );
-        RetValue = Abc_NtkDarProve( pNtk2, pSecPar );
-        Abc_NtkDelete( pNtk2 );
-        // analize the result
-        if ( RetValue == 1 )
-            goto finish;
-        if ( RetValue == 0 )
-        {
-            // transfer the counter-example!!!
-            goto finish;
-        }
-        assert( RetValue == -1 );
-        Aig_ManStop( pMan );
-        pMan = (Aig_Man_t *)Abc_FrameReadSave1(); // save2
-    }
-
-speculation:
-    if ( spectried )
-        goto finalbmc;
-    spectried = 1;
-
-    if ( fVerbose )
-    {
-        printf( "Speculation...\n" );
-        Aig_ManPrintStats( pMan );
-    }
-    // convert AIG into GIA
-//    pGia = Gia_ManFromAigSimple( pMan ); // DID NOT WORK!
-    pGia = Gia_ManFromAig( pMan );
-    Aig_ManStop( pMan );
-    // &get, eclass, 
-    {
-        Cec_ParSim_t Pars, * pPars = &Pars;
-        Cec_ManSimSetDefaultParams( pPars );
-        pPars->fSeqSimulate ^= 1;
-        pPars->nWords        = 255;
-        pPars->nFrames       = 1000;
-        Cec_ManSimulation( pGia, pPars );
-    }
-    // (spech)*  where spech = &srm; restore save3; bmc2 -F 100 -C 25000; &resim
-    while ( 1 )
-    {
-        // perform speculative reduction
-        pSrm = Gia_ManSpecReduce( pGia, 0, 0, fVeryVerbose ); // save3
-//        Gia_ManPrintStats( pGia, 0 );
-//        Gia_ManPrintStats( pSrm, 0 );
-        // bmc2 -F 100 -C 25000
-        {
-            Abc_Cex_t * pCex;
-            int nFrames     = 100; // different from default
-            int nNodeDelta  = 2000;
-            int nBTLimit    = 25000; // different from default
-            int nBTLimitAll = 2000000;
-            pTemp = Gia_ManToAig( pSrm, 0 );
-//            Aig_ManPrintStats( pTemp );
-            Gia_ManStop( pSrm );
-            Saig_BmcPerform( pTemp, 0, nFrames, nNodeDelta, 0, nBTLimit, nBTLimitAll, fVeryVerbose, 0, NULL );
-            pCex = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
-            Aig_ManStop( pTemp );
-            if ( pCex == NULL )
-                break;
-            // perform simulation
-            {
-                Cec_ParSim_t Pars, * pPars = &Pars;
-                Cec_ManSimSetDefaultParams( pPars );
-                Cec_ManSeqResimulateCounter( pGia, pPars, pCex );
-                ABC_FREE( pCex );
-            }
-        } 
-    }
-    Gia_ManStop( pGia );
-    // speculatively reduced model is available in pTemp
-    // trim off useless primary inputs
-    if ( fVerbose )
-    {
-        printf( "Problem before trimming...\n" );
-        Aig_ManPrintStats( pTemp );
-    }
-    pMan = Aig_ManDupTrim( pTemp );
-    Aig_ManStop( pTemp );
-    if ( fVerbose )
-    {
-        printf( "After speculation...\n" );
-        Aig_ManPrintStats( pMan );
-    }
-/*
-    // solve the speculatively reduced model
-    // dprove -r -F 8
-    {
-        Fra_Sec_t SecPar, * pSecPar = &SecPar;
-        Fra_SecSetDefaultParams( pSecPar );
-        pSecPar->fTryBmc       ^= 1;
-        pSecPar->fRetimeFirst  ^= 1;
-        pSecPar->nFramesMax     = 8;
-        pSecPar->fVerbose       = fVeryVerbose;
-        pSecPar->fInterSeparate = 0; //fSeparate;
-        // convert pMan into pNtk
-        pNtk2 = Abc_NtkFromAigPhase( pMan );
-        RetValue = Abc_NtkDarProve( pNtk2, pSecPar );
-        Abc_NtkDelete( pNtk2 );
-        // analize the result
-        if ( RetValue == 1 )
-            goto finish;
-        if ( RetValue == 0 )
-            goto finalbmc;
-        // could not solve
-        Aig_ManStop( pMan );
-        pMan = Abc_FrameReadSave1(); // save4
-        if ( absquit || absfail )
-            goto abstraction;
-    }
-*/
-    // scorr; dc2; orpos; int -r -C 25000
-    {
-        Ssw_Pars_t Pars, * pPars = &Pars;
-        Ssw_ManSetDefaultParams( pPars );
-        pMan = Ssw_SignalCorrespondence( pTemp = pMan, pPars );
-        Aig_ManStop( pTemp );
-        if ( fVerbose )
-        {
-            printf( "After \"scorr\"...\n" );
-            Aig_ManPrintStats( pMan );
-        }
-        pMan = Dar_ManCompress2( pTemp = pMan, 1, 0, 1, 0, 0 ); 
-        Aig_ManStop( pTemp );
-        if ( fVerbose )
-        {
-            printf( "After \"dc2\"...\n" );
-            Aig_ManPrintStats( pMan );
-        }
-    }
-    {
-        Inter_ManParams_t Pars, * pPars = &Pars;
-        Inter_ManSetDefaultParams( pPars );
-        pPars->fUseSeparate = fSeparate;
-        pPars->fRewrite     = 1;
-        pPars->nBTLimit     = 25000;
-        if ( Saig_ManPoNum(pMan) > 1 && !fSeparate )
-        {
-            Aig_Man_t * pAux = Aig_ManDupSimple(pMan);
-            pTemp = Aig_ManDupOrpos( pAux, 1 );
-            RetValue = Abc_NtkDarBmcInter_int( pTemp, pPars );
-            Aig_ManStop( pTemp );
-            Aig_ManStop( pAux );
-        }
-        else
-            RetValue = Abc_NtkDarBmcInter_int( pMan, pPars );
-        // analize the result
-        if ( RetValue == 1 )
-            goto finish;
-        if ( RetValue == 0 )
-            goto finalbmc;
-        // could not solve
-//        Aig_ManStop( pMan );
-//        pMan = Abc_FrameReadSave1(); // save4
-        if ( absquit || absfail )
-            goto abstraction;
-    }    
-
-finalbmc:
-    Aig_ManStop( pMan );
-    pMan = pSave1; pSave1 = NULL;
-    if ( fVerbose )
-    {
-        printf( "Final BMC...\n" );
-        Aig_ManPrintStats( pMan );
-    }
-    // bmc2 unlimited
-    {
-        int nFrames     = 2000;
-        int nNodeDelta  = 2000;
-        int nBTLimit    = nConfLast; // different from default
-        int nBTLimitAll = 2000000;
-        Saig_BmcPerform( pMan, 0, nFrames, nNodeDelta, 0, nBTLimit, nBTLimitAll, fVeryVerbose, 0, NULL );
-        ABC_FREE( pNtk->pModel );
-        ABC_FREE( pNtk->pSeqModel );
-        pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
-        if ( pNtk->pSeqModel )
-            goto finish;
-    }
-
-finish:
-    if ( RetValue == 1 )
-        printf( "Networks are equivalent.   " );
-    if ( RetValue == 0 )
-        printf( "Networks are not equivalent.   " );
-    if ( RetValue == -1 )
-        printf( "Networks are UNDECIDED.   " );
-    ABC_PRT( "Time", clock() - clkTotal );
-    if ( pNtk->pSeqModel ) 
-        printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness).\n", pNtk->pSeqModel->iPo, pNtk->pSeqModel->iFrame );
-    // verify counter-example
-    if ( pNtk->pSeqModel ) 
-    {
-        int status = Saig_ManVerifyCex( pMan, pNtk->pSeqModel );
-        if ( status == 0 )
-            printf( "Abc_NtkDarBmc(): Counter-example verification has FAILED.\n" );
-    }
-    if ( pSave1 )  
-        Aig_ManStop( pSave1 );
-    Aig_ManStop( pMan );
-    return RetValue;
-}
-
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-