Updates for the new BMC engine.

5 files changed, 147 insertions, 19 deletions

diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index f1407936..51295a53 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -38,7 +38,10 @@ ABC_NAMESPACE_HEADER_START
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
- 
+
+// unrolling manager 
+typedef struct Unr_Man_t_ Unr_Man_t;
+
 typedef struct Saig_ParBmc_t_ Saig_ParBmc_t;
 struct Saig_ParBmc_t_
 {
@@ -69,14 +72,15 @@ struct Saig_ParBmc_t_
 };
 
  
-typedef struct Bmc_LadPar_t_ Bmc_LadPar_t;
-struct Bmc_LadPar_t_
+typedef struct Bmc_AndPar_t_ Bmc_AndPar_t;
+struct Bmc_AndPar_t_
 {
     int         nStart;         // starting timeframe
     int         nFramesMax;     // maximum number of timeframes 
     int         nConfLimit;     // maximum number of conflicts at a node
     int         fLoadCnf;       // dynamic CNF loading
     int         fVerbose;       // verbose 
+    int         fVeryVerbose;   // very verbose 
     int         fNotVerbose;    // skip line-by-line print-out 
     int         iFrame;         // explored up to this frame
     int         nFailOuts;      // the number of failed outputs
@@ -98,11 +102,17 @@ extern int               Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFra
 /*=== bmcBmc3.c ==========================================================*/
 extern void              Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p );
 extern int               Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars );
+/*=== bmcBmcAnd.c ==========================================================*/
+extern int               Gia_ManBmcPerform( Gia_Man_t * p, Bmc_AndPar_t * pPars );
 /*=== bmcCexCut.c ==========================================================*/
 extern Gia_Man_t *       Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fGenAll, int fAllFrames, int fVerbose );
 extern Aig_Man_t *       Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fGenAll, int fAllFrames, int fVerbose );
 /*=== bmcCexMin.c ==========================================================*/
 extern Abc_Cex_t *       Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pCex );
+/*=== bmcUnroll.c ==========================================================*/
+extern Unr_Man_t *       Unr_ManUnrollStart( Gia_Man_t * pGia, int fVerbose );
+extern Gia_Man_t *       Unr_ManUnrollFrame( Unr_Man_t * p, int f );
+extern void              Unr_ManFree( Unr_Man_t * p );
 
 
 ABC_NAMESPACE_HEADER_END
diff --git a/src/sat/bmc/bmcBmcAnd.c b/src/sat/bmc/bmcBmcAnd.c
new file mode 100644
index 00000000..d3544f6d
--- /dev/null
+++ b/src/sat/bmc/bmcBmcAnd.c
@@ -0,0 +1,115 @@
+/**CFile****************************************************************
+
+  FileName    [bmcBmcAnd.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT-based bounded model checking.]
+
+  Synopsis    [Memory-efficient BMC engine]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: bmcBmcAnd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "bmc.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManCountUnmarked_rec( Gia_Obj_t * pObj )
+{
+    if ( !Gia_ObjIsAnd(pObj) || pObj->fMark0 )
+        return 0;
+    pObj->fMark0 = 1;
+    return 1 + Gia_ManCountUnmarked_rec( Gia_ObjFanin0(pObj) ) + 
+        Gia_ManCountUnmarked_rec( Gia_ObjFanin1(pObj) );
+}
+int Gia_ManCountUnmarked( Gia_Man_t * p, int iStart )
+{
+    int i, Counter = 0;
+    for ( i = iStart; i < Gia_ManPoNum(p); i++ )
+        Counter += Gia_ManCountUnmarked_rec( Gia_ObjFanin0(Gia_ManPo(p, i)) );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
+{
+    Unr_Man_t * p;
+    Gia_Man_t * pFrames;
+    abctime clk = Abc_Clock();
+    int nFramesMax = pPars->nFramesMax ? pPars->nFramesMax : ABC_INFINITY;
+    int i, f, iStart, status = -1, Counter = 0;
+    p = Unr_ManUnrollStart( pGia, pPars->fVeryVerbose );
+    for ( f = 0; f < nFramesMax; f++ )
+    {
+        pFrames = Unr_ManUnrollFrame( p, f );
+        assert( Gia_ManPoNum(pFrames) == (f + 1) * Gia_ManPoNum(pGia) );
+        iStart = f * Gia_ManPoNum(pGia);
+        for ( i = iStart; i < Gia_ManPoNum(pFrames); i++ )
+            if ( Gia_ObjChild0(Gia_ManPo(pFrames, i)) != Gia_ManConst0(pFrames) )
+                break;
+        if ( i == Gia_ManPoNum(pFrames) )
+        {
+            if ( pPars->fVerbose )
+            {
+                printf( "Frame %4d :  Trivally UNSAT.   Memory = %5.1f Mb   ", f, Gia_ManMemory(pFrames) );
+                Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+            }
+            continue;
+        }
+        if ( pPars->fVerbose )
+        {
+            printf( "Frame %4d :  AIG =%9d.   Memory = %5.1f Mb   ", f, Gia_ManCountUnmarked(pFrames, iStart), Gia_ManMemory(pFrames) );
+            Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+        }
+        if ( ++Counter == 10 )
+            break;
+    }
+    Unr_ManFree( p );
+    return status;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/bmc/bmcLoad.c b/src/sat/bmc/bmcLoad.c
index b3d56005..a653861c 100644
--- a/src/sat/bmc/bmcLoad.c
+++ b/src/sat/bmc/bmcLoad.c
@@ -31,7 +31,7 @@ ABC_NAMESPACE_IMPL_START
 typedef struct Bmc_Lad_t_ Bmc_Lad_t;  
 struct Bmc_Lad_t_
 {
-    Bmc_LadPar_t *   pPars;     // parameters
+    Bmc_AndPar_t *   pPars;     // parameters
     Gia_Man_t *      pGia;      // unrolled AIG
     sat_solver *     pSat;      // SAT solvers
     Vec_Int_t *      vSat2Id;   // maps SAT var into its node
@@ -123,7 +123,7 @@ int Bmc_LadAddCnf_rec( Bmc_Lad_t * p, int Id )
   SeeAlso     []
 
 ***********************************************************************/
-Bmc_Lad_t * Bmc_LadStart( Gia_Man_t * pGia, Bmc_LadPar_t * pPars )
+Bmc_Lad_t * Bmc_LadStart( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
 {
     Bmc_Lad_t * p;
     int Lit;
@@ -164,7 +164,7 @@ void Bmc_LadStop( Bmc_Lad_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Bmc_PerformBmc( Gia_Man_t * pGia, Bmc_LadPar_t * pPars )
+void Bmc_PerformBmc( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
 {
     int nConfLimit = 0;
     Bmc_Lad_t * p;
diff --git a/src/sat/bmc/bmcUnroll.c b/src/sat/bmc/bmcUnroll.c
index c05eb66b..9cabcd8b 100644
--- a/src/sat/bmc/bmcUnroll.c
+++ b/src/sat/bmc/bmcUnroll.c
@@ -45,7 +45,6 @@ struct Unr_Obj_t_
     unsigned              Res[1];       // RankMax entries
 };
 
-typedef struct Unr_Man_t_ Unr_Man_t;
 struct Unr_Man_t_
 {
     // input data
@@ -366,14 +365,18 @@ void Unr_ManFree( Unr_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Unr_ManUnrollStart( Unr_Man_t * p )
+Unr_Man_t * Unr_ManUnrollStart( Gia_Man_t * pGia, int fVerbose )
 {
     int i, iHandle;
+    Unr_Man_t * p;
+    p = Unr_ManAlloc( pGia );
+    Unr_ManSetup( p, fVerbose );
     for ( i = 0; i < Gia_ManRegNum(p->pGia); i++ )
         if ( (iHandle = Vec_IntEntry(p->vCoMap, Gia_ManPoNum(p->pGia) + i)) != -1 )
             Unr_ManObjSetValue( Unr_ManObj(p, iHandle), 0 );
+    return p;
 }
-void Unr_ManUnrollFrame( Unr_Man_t * p, int f )
+Gia_Man_t * Unr_ManUnrollFrame( Unr_Man_t * p, int f )
 {
     int i, iLit, iLit0, iLit1, hStart;
     for ( i = 0; i < Gia_ManPiNum(p->pGia); i++ )
@@ -405,14 +408,19 @@ void Unr_ManUnrollFrame( Unr_Man_t * p, int f )
         hStart += Unr_ObjSize( pUnrObj );
     }
     assert( p->pObjs + hStart == p->pEnd );
+    return p->pFrames;
 }
-Gia_Man_t * Unr_ManUnroll( Unr_Man_t * p, int nFrames )
+Gia_Man_t * Unr_ManUnroll( Gia_Man_t * pGia, int nFrames )
 {
+    Unr_Man_t * p;
+    Gia_Man_t * pFrames;
     int f;
-    Unr_ManUnrollStart( p );
+    p = Unr_ManUnrollStart( pGia, 1 );
     for ( f = 0; f < nFrames; f++ )
         Unr_ManUnrollFrame( p, f );
-    return Gia_ManCleanup( p->pFrames );
+    pFrames = Gia_ManCleanup( p->pFrames );
+    Unr_ManFree( p );
+    return pFrames;
 }
 
 /**Function*************************************************************
@@ -472,14 +480,8 @@ void Unr_ManTest( Gia_Man_t * pGia, int nFrames )
 {
     Gia_Man_t * pFrames0, * pFrames1;
     abctime clk = Abc_Clock();
-    Unr_Man_t * p;
-    p = Unr_ManAlloc( pGia );
-    Unr_ManSetup( p, 1 );
-    pFrames0 = Unr_ManUnroll( p, nFrames );
+    pFrames0 = Unr_ManUnroll( pGia, nFrames );
     Abc_PrintTime( 1, "Unroll ", Abc_Clock() - clk );
-
-    Unr_ManFree( p );
-
     clk = Abc_Clock();
     pFrames1 = Unr_ManUnrollSimple( pGia, nFrames );
     Abc_PrintTime( 1, "UnrollS", Abc_Clock() - clk );
diff --git a/src/sat/bmc/module.make b/src/sat/bmc/module.make
index cde439b4..e567e92b 100644
--- a/src/sat/bmc/module.make
+++ b/src/sat/bmc/module.make
@@ -1,6 +1,7 @@
 SRC +=    src/sat/bmc/bmcBmc.c \
     src/sat/bmc/bmcBmc2.c \
     src/sat/bmc/bmcBmc3.c \
+    src/sat/bmc/bmcBmcAnd.c \
     src/sat/bmc/bmcCexCut.c \
     src/sat/bmc/bmcCexDepth.c \
     src/sat/bmc/bmcCexMin1.c \