Skip to content

A
abc
Commit e9d04664 by Alan Mishchenko
Options

Updates for the new BMC engine.

parent e651e227
Showing with 186 additions and 25 deletions
abclib.dsp
......@@ -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
......
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 );
......
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 )
......
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 []
......
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;
}
src/sat/bmc/bmc.h
......@@ -39,6 +39,9 @@ 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
......
src/sat/bmc/bmcBmcAnd.c 0 → 100644
/**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
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;
......
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 );
......
src/sat/bmc/module.make
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 \
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment