diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-09-05 15:39:18 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-09-05 15:39:18 -0700 |
commit | e9d0466494cbf7a707a450a7e058a0ae4c652f8b (patch) | |
tree | 4433986c02f58247676c0fb032f98c848278eeab /src/sat | |
parent | e651e227886452e088fd8c4b87f8cf48d189f7fb (diff) | |
download | abc-e9d0466494cbf7a707a450a7e058a0ae4c652f8b.tar.gz abc-e9d0466494cbf7a707a450a7e058a0ae4c652f8b.tar.bz2 abc-e9d0466494cbf7a707a450a7e058a0ae4c652f8b.zip |
Updates for the new BMC engine.
Diffstat (limited to 'src/sat')
-rw-r--r-- | src/sat/bmc/bmc.h | 16 | ||||
-rw-r--r-- | src/sat/bmc/bmcBmcAnd.c | 115 | ||||
-rw-r--r-- | src/sat/bmc/bmcLoad.c | 6 | ||||
-rw-r--r-- | src/sat/bmc/bmcUnroll.c | 28 | ||||
-rw-r--r-- | src/sat/bmc/module.make | 1 |
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 \ |