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

Adding switch 'pdr -i' to start push_clauses from an intermediate timeframe.

This commit is contained in:
Alan Mishchenko 2013-10-15 09:04:27 -07:00
parent 1692c1a57a
commit f9900a4c3b
3 changed files with 11 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -23650,7 +23650,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
Pdr_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "MFCRTHGaxrmspdgvwzh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "MFCRTHGaxrmsipdgvwzh" ) ) != EOF )
{
switch ( c )
{
@ -23746,6 +23746,9 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
case 's':
pPars->fShortest ^= 1;
break;
case 'i':
pPars->fShiftStart ^= 1;
break;
case 'p':
pPars->fReuseProofOblig ^= 1;
break;
@ -23796,7 +23799,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: pdr [-MFCRTHG <num>] [-axrmsdgvwzh]\n" );
Abc_Print( -2, "usage: pdr [-MFCRTHG <num>] [-axrmsipdgvwzh]\n" );
Abc_Print( -2, "\t model checking using property directed reachability (aka IC3)\n" );
Abc_Print( -2, "\t pioneered by Aaron Bradley (http://ecee.colorado.edu/~bradleya/ic3/)\n" );
Abc_Print( -2, "\t with improvements by Niklas Een (http://een.se/niklas/)\n" );
@ -23812,7 +23815,8 @@ usage:
Abc_Print( -2, "\t-r : toggle using more effort in generalization [default = %s]\n", pPars->fTwoRounds? "yes": "no" );
Abc_Print( -2, "\t-m : toggle using monolythic CNF computation [default = %s]\n", pPars->fMonoCnf? "yes": "no" );
Abc_Print( -2, "\t-s : toggle creating only shortest counter-examples [default = %s]\n", pPars->fShortest? "yes": "no" );
Abc_Print( -2, "\t-p : toggle using proof-obligations from the last timeframe [default = %s]\n", pPars->fReuseProofOblig? "yes": "no" );
Abc_Print( -2, "\t-i : toggle clause pushing from an intermediate timeframe [default = %s]\n", pPars->fShiftStart? "yes": "no" );
Abc_Print( -2, "\t-p : toggle reusing proof-obligations in the last timeframe [default = %s]\n", pPars->fReuseProofOblig? "yes": "no" );
Abc_Print( -2, "\t-d : toggle dumping inductive invariant [default = %s]\n", pPars->fDumpInv? "yes": "no" );
Abc_Print( -2, "\t-g : toggle skipping expensive generalization step [default = %s]\n", pPars->fSkipGeneral? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" );

1
src/proof/pdr/pdr.h
View File

@ -52,6 +52,7 @@ struct Pdr_Par_t_
int fMonoCnf; // monolythic CNF
int fDumpInv; // dump inductive invariant
int fShortest; // forces bug traces to be shortest
int fShiftStart; // allows clause pushing to start from an intermediate frame
int fReuseProofOblig; // reuses proof-obligationgs in the last timeframe
int fSkipGeneral; // skips expensive generalization step
int fVerbose; // verbose output`

7
src/proof/pdr/pdrCore.c
View File

@ -137,10 +137,11 @@ int Pdr_ManPushClauses( Pdr_Man_t * p )
Pdr_Set_t * pTemp, * pCubeK, * pCubeK1;
Vec_Ptr_t * vArrayK, * vArrayK1;
int i, j, k, m, RetValue = 0, RetValue2, kMax = Vec_PtrSize(p->vSolvers)-1;
int iStartFrame = p->pPars->fShiftStart ? p->iUseFrame : 1;
int Counter = 0;
abctime clk = Abc_Clock();
assert( p->iUseFrame > 0 );
Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, 1, kMax )
Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, iStartFrame, kMax )
{
Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare );
vArrayK1 = Vec_VecEntry( p->vClauses, k+1 );
@ -441,9 +442,7 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
pThis = Pdr_QueueHead( p );
if ( pThis->iFrame == 0 )
return 0; // SAT
if ( pThis->iFrame > kMax ) // finished this level
return 1;
if ( p->nQueLim && p->nQueCur >= p->nQueLim )
{
@ -586,7 +585,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
{
p->nFrames = k;
assert( k == Vec_PtrSize(p->vSolvers)-1 );
p->iUseFrame = ABC_INFINITY;
p->iUseFrame = Abc_MaxInt(k, 1);
Saig_ManForEachPo( p->pAig, pObj, p->iOutCur )
{
// skip disproved outputs