diff options
| -rw-r--r-- | abclib.dsp | 4 | ||||
| -rw-r--r-- | src/aig/gia/gia.h | 1 | ||||
| -rw-r--r-- | src/aig/gia/giaDup.c | 3 | ||||
| -rw-r--r-- | src/aig/gia/giaMan.c | 21 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 18 | ||||
| -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 |
10 files changed, 187 insertions, 26 deletions
@@ -1419,6 +1419,10 @@ SOURCE=.\src\sat\bmc\bmcBmc3.c # End Source File # Begin Source File +SOURCE=.\src\sat\bmc\bmcBmcAnd.c +# End Source File +# Begin Source File + SOURCE=.\src\sat\bmc\bmcCexCut.c # End Source File # Begin Source File diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 7653dc62..2d3cf518 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -1018,6 +1018,7 @@ extern void Gia_ManSolveProblem( Gia_Man_t * pGia, Emb_Par_t * pP extern Gia_Man_t * Gia_ManStart( int nObjsMax ); extern void Gia_ManStop( Gia_Man_t * p ); extern void Gia_ManStopP( Gia_Man_t ** p ); +extern float Gia_ManMemory( Gia_Man_t * p ); extern void Gia_ManPrintStats( Gia_Man_t * p, int fTents, int fSwitch, int fCut ); extern void Gia_ManPrintStatsShort( Gia_Man_t * p ); extern void Gia_ManPrintMiterStatus( Gia_Man_t * p ); diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 2e911ba8..e8e186cf 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -907,7 +907,7 @@ Gia_Man_t * Gia_ManDupMarked( Gia_Man_t * p ) Gia_Obj_t * pObj; int i, nRos = 0, nRis = 0; int CountMarked = 0; - Gia_ManForEachObj1( p, pObj, i ) + Gia_ManForEachObj( p, pObj, i ) CountMarked += pObj->fMark0; Gia_ManFillValue( p ); pNew = Gia_ManStart( Gia_ManObjNum(p) - CountMarked ); @@ -945,6 +945,7 @@ Gia_Man_t * Gia_ManDupMarked( Gia_Man_t * p ) nRis += Gia_ObjIsRi(p, pObj); } } + assert( pNew->nObjsAlloc == pNew->nObjs ); assert( nRos == nRis ); Gia_ManSetRegNum( pNew, nRos ); if ( p->pReprs && p->pNexts ) diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index a573e9e7..58057136 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -129,6 +129,27 @@ void Gia_ManStop( Gia_Man_t * p ) /**Function************************************************************* + Synopsis [Returns memory used in megabytes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +float Gia_ManMemory( Gia_Man_t * p ) +{ + word Memory = sizeof(Gia_Man_t); + Memory += sizeof(Gia_Obj_t) * Gia_ManObjNum(p); + Memory += sizeof(int) * Gia_ManCiNum(p); + Memory += sizeof(int) * Gia_ManCoNum(p); + Memory += sizeof(int) * p->nHTable * (p->pHTable != NULL); + return (float)(int)(Memory / (1 << 20)) + (float)(1e-6 * (int)(Memory % (1 << 20))); +} + +/**Function************************************************************* + Synopsis [Stops the AIG manager.] Description [] diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 4c986d9c..da3726f3 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -31611,21 +31611,22 @@ usage: ***********************************************************************/ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern void Bmc_PerformBmc( Gia_Man_t * pGia, Bmc_LadPar_t * pPars ); +// extern void Bmc_PerformBmc( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ); int c; - Bmc_LadPar_t Pars, * pPars = &Pars; - memset( pPars, 0, sizeof(Bmc_LadPar_t) ); + Bmc_AndPar_t Pars, * pPars = &Pars; + memset( pPars, 0, sizeof(Bmc_AndPar_t) ); pPars->nStart = 0; // starting timeframe pPars->nFramesMax = 0; // maximum number of timeframes pPars->nConfLimit = 0; // maximum number of conflicts at a node pPars->fLoadCnf = 0; // dynamic CNF loading pPars->fVerbose = 0; // verbose + pPars->fVeryVerbose = 0; // very verbose pPars->fNotVerbose = 0; // skip line-by-line print-out pPars->iFrame = 0; // explored up to this frame pPars->nFailOuts = 0; // the number of failed outputs pPars->nDropOuts = 0; // the number of dropped outputs Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "SFcvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "SFcvwh" ) ) != EOF ) { switch ( c ) { @@ -31657,6 +31658,9 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'v': pPars->fVerbose ^= 1; break; + case 'w': + pPars->fVeryVerbose ^= 1; + break; case 'h': goto usage; default: @@ -31668,16 +31672,18 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9Rpm(): There is no AIG.\n" ); return 0; } - Bmc_PerformBmc( pAbc->pGia, pPars ); +// Bmc_PerformBmc( pAbc->pGia, pPars ); + Gia_ManBmcPerform( pAbc->pGia, pPars ); return 0; usage: - Abc_Print( -2, "usage: &bmc [-SF num] [-cvh]\n" ); + Abc_Print( -2, "usage: &bmc [-SF num] [-cvwh]\n" ); Abc_Print( -2, "\t performs bounded model checking\n" ); Abc_Print( -2, "\t-S num : the starting timeframe [default = %d]\n", pPars->nStart ); Abc_Print( -2, "\t-F num : the maximum number of timeframes [default = %d]\n", pPars->nFramesMax ); Abc_Print( -2, "\t-c : toggle dynamic CNF loading [default = %s]\n", pPars->fLoadCnf? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-w : toggle printing information about unfolding [default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } 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 \ |