luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Adding runtime limit per output to multi-output BMC (bmc3 -H <num_sec>).

This commit is contained in:
Alan Mishchenko 2013-05-03 18:26:18 -07:00
parent 0ca8a245da
commit a59968ce8c
3 changed files with 59 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
src/base/abci/abc.c
View File

@ -21041,7 +21041,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
Saig_ParBmcSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "SFTGCDJILaxdruvzh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "SFTGHCDJILaxdruvzh" ) ) != EOF )
{
switch ( c )
{
@ -21089,6 +21089,17 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nTimeOutGap < 0 )
goto usage;
break;
case 'H':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-H\" should be followed by an integer.\n" );
goto usage;
}
pPars->nTimeOutOne = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nTimeOutOne < 0 )
goto usage;
break;
case 'C':
if ( globalUtilOptind >= argc )
{
@ -21219,12 +21230,13 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: bmc3 [-SFTGCDJI num] [-L file] [-axduvzh]\n" );
Abc_Print( -2, "usage: bmc3 [-SFTGHCDJI num] [-L file] [-axduvzh]\n" );
Abc_Print( -2, "\t performs bounded model checking with dynamic unrolling\n" );
Abc_Print( -2, "\t-S num : the starting time frame [default = %d]\n", pPars->nStart );
Abc_Print( -2, "\t-F num : the max number of time frames (0 = unused) [default = %d]\n", pPars->nFramesMax );
Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->nTimeOut );
Abc_Print( -2, "\t-G num : approximate runtime gap since the last CEX [default = %d]\n", pPars->nTimeOutGap );
Abc_Print( -2, "\t-H num : approximate runtime per output (with \"-a\") [default = %d]\n", pPars->nTimeOutOne );
Abc_Print( -2, "\t-C num : max conflicts at an output [default = %d]\n", pPars->nConfLimit );
Abc_Print( -2, "\t-D num : max conflicts after jumping (0 = infinity) [default = %d]\n", pPars->nConfLimitJump );
Abc_Print( -2, "\t-J num : the number of timeframes to jump (0 = not used) [default = %d]\n", pPars->nFramesJump );

2
src/sat/bmc/bmc.h
View File

@ -49,6 +49,7 @@ struct Saig_ParBmc_t_
int nFramesJump; // the number of tiemframes to jump
int nTimeOut; // approximate timeout in seconds
int nTimeOutGap; // approximate timeout in seconds since the last change
int nTimeOutOne; // timeout per output in multi-output solving
int nPisAbstract; // the number of PIs to abstract
int fSolveAll; // does not stop at the first SAT output
int fStoreCex; // enable storing CEXes in the MO mode
@ -59,6 +60,7 @@ struct Saig_ParBmc_t_
int fNotVerbose; // skip line-by-line print-out
int iFrame; // explored up to this frame
int nFailOuts; // the number of failed outputs
int nDropOuts; // the number of dropped outputs
clock_t timeLastSolved; // the time when the last output was solved
int(*pFuncOnFail)(int,Abc_Cex_t*); // called for a failed output in MO mode
};

53
src/sat/bmc/bmcBmc3.c
View File

@ -43,6 +43,7 @@ struct Gia_ManBmc_t_
Vec_Int_t * vId2Num; // number of each node
Vec_Ptr_t * vTerInfo; // ternary information
Vec_Ptr_t * vId2Var; // SAT vars for each object
clock_t * pTime4Outs; // timeout per output
// hash table
int * pTable;
int nTable;
@ -700,7 +701,7 @@ Vec_Int_t * Saig_ManBmcComputeMappingRefs( Aig_Man_t * p, Vec_Int_t * vMap )
SeeAlso []
***********************************************************************/
Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig )
Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig, int nTimeOutOne )
{
Gia_ManBmc_t * p;
Aig_Obj_t * pObj;
@ -736,6 +737,13 @@ Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig )
// hash table
p->nTable = 1000003;
p->pTable = ABC_CALLOC( int, 6 * p->nTable ); // 2.4 MB
// time spent on each outputs
if ( nTimeOutOne )
{
p->pTime4Outs = ABC_ALLOC( clock_t, Saig_ManPoNum(pAig) );
for ( i = 0; i < Saig_ManPoNum(pAig); i++ )
p->pTime4Outs[i] = nTimeOutOne * CLOCKS_PER_SEC;
}
return p;
}
@ -770,6 +778,7 @@ void Saig_Bmc3ManStop( Gia_ManBmc_t * p )
Vec_VecFree( (Vec_Vec_t *)p->vId2Var );
Vec_PtrFreeFree( p->vTerInfo );
sat_solver_delete( p->pSat );
ABC_FREE( p->pTime4Outs );
ABC_FREE( p->pTable );
ABC_FREE( p->pSopSizes );
ABC_FREE( p->pSops[1] );
@ -1309,6 +1318,7 @@ void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p )
p->fNotVerbose = 0; // skip line-by-line print-out
p->iFrame = -1; // explored up to this frame
p->nFailOuts = 0; // the number of failed outputs
p->nDropOuts = 0; // the number of timed out outputs
p->timeLastSolved = 0; // time when the last one was solved
}
@ -1383,11 +1393,14 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
int nOutDigits = Abc_Base10Log( Saig_ManPoNum(pAig) );
int i, f, k, Lit, status;
clock_t clk, clk2, clkOther = 0, clkTotal = clock();
clock_t nTimeToStopNG = pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + clock(): 0;
clock_t nTimeToStop = Saig_ManBmcTimeToStop( pPars, nTimeToStopNG );
clock_t nTimeUnsat = 0, nTimeSat = 0, nTimeUndec = 0;
clock_t nTimeUnsat = 0, nTimeSat = 0, nTimeUndec = 0, clkOne;
clock_t nTimeToStopNG, nTimeToStop;
if ( pPars->nTimeOutOne )
pPars->nTimeOut = pPars->nTimeOutOne * Saig_ManPoNum(pAig);
nTimeToStopNG = pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + clock(): 0;
nTimeToStop = Saig_ManBmcTimeToStop( pPars, nTimeToStopNG );
// create BMC manager
p = Saig_Bmc3ManStart( pAig );
p = Saig_Bmc3ManStart( pAig, pPars->nTimeOutOne );
p->pPars = pPars;
if ( pPars->fVerbose )
{
@ -1413,9 +1426,9 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
goto finish;
}
// stop BMC if all targets are solved
if ( pPars->fSolveAll && pPars->nFailOuts == Saig_ManPoNum(pAig) )
if ( pPars->fSolveAll && pPars->nFailOuts + pPars->nDropOuts >= Saig_ManPoNum(pAig) )
{
RetValue = 0;
RetValue = pPars->nFailOuts ? 0 : 1;
goto finish;
}
// consider the next timeframe
@ -1469,6 +1482,9 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
// skip solved outputs
if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) )
continue;
// skip output whose time has run out
if ( p->pTime4Outs && p->pTime4Outs[i] == 0 )
continue;
// add constraints for this output
clk2 = clock();
Lit = Saig_ManBmcCreateCnf( p, pObj, f );
@ -1505,11 +1521,25 @@ clkOther += clock() - clk2;
sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
continue;
}
// solve th is output
// solve this output
fUnfinished = 0;
sat_solver_compress( p->pSat );
clk2 = clock();
if ( p->pTime4Outs )
{
assert( p->pTime4Outs[i] > 0 );
clkOne = clock();
sat_solver_set_runtime_limit( p->pSat, p->pTime4Outs[i] + clock() );
}
status = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( p->pTime4Outs )
{
clock_t timeSince = clock() - clkOne;
assert( p->pTime4Outs[i] > 0 );
p->pTime4Outs[i] = (p->pTime4Outs[i] > timeSince) ? p->pTime4Outs[i] - timeSince : 0;
if ( p->pTime4Outs[i] == 0 && status != l_True )
pPars->nDropOuts++;
}
if ( status == l_False )
{
nTimeUnsat += clock() - clk2;
@ -1591,7 +1621,8 @@ nTimeUndec += clock() - clk2;
fUnfinished = 1;
break;
}
goto finish;
if ( p->pTime4Outs == NULL )
goto finish;
}
}
if ( pPars->fVerbose )
@ -1608,7 +1639,9 @@ nTimeUndec += clock() - clk2;
// printf( "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
printf( "Uni =%7.0f. ",(double)sat_solver_count_assigned(p->pSat) );
if ( pPars->fSolveAll )
printf( "CEX =%7d. ", pPars->nFailOuts );
printf( "CEX =%5d. ", pPars->nFailOuts );
if ( pPars->nTimeOutOne )
printf( "T/O =%4d. ", pPars->nDropOuts );
// ABC_PRT( "Time", clock() - clk );
// printf( "%4.0f MB", 4.0*Vec_IntSize(p->vVisited) /(1<<20) );
printf( "%4.0f MB", 4.0*(f+1)*p->nObjNums /(1<<20) );