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

Promising alternative of CEX minimization in 'pdr'.

This commit is contained in:
Alan Mishchenko 2017-02-16 13:37:46 -08:00
parent 61b665ac8d
commit 632ca7ed11
4 changed files with 61 additions and 41 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -26171,7 +26171,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, "MFCDQTHGSaxrmuyfsipdegjonctvwzh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDQTHGSaxrmuyfsipdegjonctkvwzh" ) ) != EOF )
{
switch ( c )
{
@ -26328,6 +26328,9 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
case 't':
pPars->fUseAbs ^= 1;
break;
case 'k':
pPars->fUseSimpleRef ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
@ -26369,7 +26372,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: pdr [-MFCDQTHGS <num>] [-axrmuyfsipdegjonctvwzh]\n" );
Abc_Print( -2, "usage: pdr [-MFCDQTHGS <num>] [-axrmuyfsipdegjonctkvwzh]\n" );
Abc_Print( -2, "\t model checking using property directed reachability (aka IC3)\n" );
Abc_Print( -2, "\t pioneered by Aaron R. Bradley (http://theory.stanford.edu/~arbrad/)\n" );
Abc_Print( -2, "\t with improvements by Niklas Een (http://een.se/niklas/)\n" );
@ -26400,6 +26403,7 @@ usage:
Abc_Print( -2, "\t-n : * toggle skipping \'down\' in generalization [default = %s]\n", pPars->fSkipDown? "yes": "no" );
Abc_Print( -2, "\t-c : * toggle handling CTGs in \'down\' [default = %s]\n", pPars->fCtgs? "yes": "no" );
Abc_Print( -2, "\t-t : toggle using abstraction [default = %s]\n", pPars->fUseAbs? "yes": "no" );
Abc_Print( -2, "\t-k : toggle using simplified refinement [default = %s]\n", pPars->fUseSimpleRef? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-w : toggle printing detailed stats default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
Abc_Print( -2, "\t-z : toggle suppressing report about solved outputs [default = %s]\n", pPars->fNotVerbose? "yes": "no" );

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

@ -65,6 +65,7 @@ struct Pdr_Par_t_
int fSkipDown; // skips the application of down
int fCtgs; // handle CTGs in down
int fUseAbs; // use abstraction
int fUseSimpleRef; // simplified CEX refinement
int fVerbose; // verbose output`
int fVeryVerbose; // very verbose output
int fNotVerbose; // not printing line by line progress

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

@ -60,8 +60,6 @@ void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars )
pPars->nRestLimit = 0; // limit on the number of proof-obligations
pPars->nRandomSeed = 91648253; // value to seed the SAT solver with
pPars->fTwoRounds = 0; // use two rounds for generalization
pPars->fSkipDown = 1; // apply down in generalization
pPars->fCtgs = 0; // handle CTGs in down
pPars->fMonoCnf = 0; // monolythic CNF
pPars->fNewXSim = 0; // updated X-valued simulation
pPars->fFlopPrio = 0; // use structural flop priorities
@ -70,6 +68,10 @@ void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars )
pPars->fUseSupp = 1; // using support variables in the invariant
pPars->fShortest = 0; // forces bug traces to be shortest
pPars->fUsePropOut = 1; // use property output
pPars->fSkipDown = 1; // apply down in generalization
pPars->fCtgs = 0; // handle CTGs in down
pPars->fUseAbs = 0; // use abstraction
pPars->fUseSimpleRef = 0; // simplified CEX refinement
pPars->fVerbose = 0; // verbose output
pPars->fVeryVerbose = 0; // very verbose output
pPars->fNotVerbose = 0; // not printing line-by-line progress

87
src/proof/pdr/pdrMan.c
View File

@ -482,45 +482,58 @@ Abc_Cex_t * Pdr_ManDeriveCexAbs( Pdr_Man_t * p )
}
if ( Vec_IntSize(p->vMapPpi2Ff) == 0 ) // no PPIs -- this is a real CEX
return Pdr_ManDeriveCex(p);
// create the counter-example
pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig) - Vec_IntSize(p->vMapPpi2Ff), Saig_ManPiNum(p->pAig) + Vec_IntSize(p->vMapPpi2Ff), nFrames );
pCex->iPo = p->iOutCur;
pCex->iFrame = nFrames-1;
for ( pObl = p->pQueue, f = 0; pObl; pObl = pObl->pNext, f++ )
for ( i = pObl->pState->nLits; i < pObl->pState->nTotal; i++ )
{
Lit = pObl->pState->Lits[i];
if ( lit_sign(Lit) )
continue;
if ( lit_var(Lit) < nPis ) // PI literal
Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + lit_var(Lit) );
else
{
int iPPI = nPis + Vec_IntEntry(p->vMapFf2Ppi, lit_var(Lit) - nPis);
assert( iPPI < pCex->nPis );
Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + iPPI );
}
}
assert( f == nFrames );
// perform CEX minimization
pAbs = Gia_ManDupAbs( p->pGia, p->vMapPpi2Ff, p->vMapFf2Ppi );
pCexCare = Bmc_CexCareMinimizeAig( pAbs, nPis, pCex, 1, 0, 0 );
Gia_ManStop( pAbs );
assert( pCexCare->nPis == pCex->nPis );
Abc_CexFree( pCex );
// detect care PPIs
for ( f = 0; f < nFrames; f++ )
if ( p->pPars->fUseSimpleRef )
{
for ( i = nPis; i < pCexCare->nPis; i++ )
if ( Abc_InfoHasBit(pCexCare->pData, pCexCare->nRegs + pCexCare->nPis * f + i) )
{
if ( Vec_IntEntry(p->vAbsFlops, Vec_IntEntry(p->vMapPpi2Ff, i-nPis)) == 0 ) // currently abstracted
Vec_IntWriteEntry( p->vAbsFlops, Vec_IntEntry(p->vMapPpi2Ff, i-nPis), 1 ), nFfRefined++;
}
// rely on ternary simulation to perform refinement
Vec_IntForEachEntry( p->vMapPpi2Ff, Flop, i )
{
assert( Vec_IntEntry(p->vAbsFlops, Flop) == 0 );
Vec_IntWriteEntry( p->vAbsFlops, Flop, 1 );
nFfRefined++;
}
}
else
{
// create the counter-example
pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig) - Vec_IntSize(p->vMapPpi2Ff), Saig_ManPiNum(p->pAig) + Vec_IntSize(p->vMapPpi2Ff), nFrames );
pCex->iPo = p->iOutCur;
pCex->iFrame = nFrames-1;
for ( pObl = p->pQueue, f = 0; pObl; pObl = pObl->pNext, f++ )
for ( i = pObl->pState->nLits; i < pObl->pState->nTotal; i++ )
{
Lit = pObl->pState->Lits[i];
if ( lit_sign(Lit) )
continue;
if ( lit_var(Lit) < nPis ) // PI literal
Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + lit_var(Lit) );
else
{
int iPPI = nPis + Vec_IntEntry(p->vMapFf2Ppi, lit_var(Lit) - nPis);
assert( iPPI < pCex->nPis );
Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + iPPI );
}
}
assert( f == nFrames );
// perform CEX minimization
pAbs = Gia_ManDupAbs( p->pGia, p->vMapPpi2Ff, p->vMapFf2Ppi );
pCexCare = Bmc_CexCareMinimizeAig( pAbs, nPis, pCex, 1, 0, 0 );
Gia_ManStop( pAbs );
assert( pCexCare->nPis == pCex->nPis );
Abc_CexFree( pCex );
// detect care PPIs
for ( f = 0; f < nFrames; f++ )
{
for ( i = nPis; i < pCexCare->nPis; i++ )
if ( Abc_InfoHasBit(pCexCare->pData, pCexCare->nRegs + pCexCare->nPis * f + i) )
{
if ( Vec_IntEntry(p->vAbsFlops, Vec_IntEntry(p->vMapPpi2Ff, i-nPis)) == 0 ) // currently abstracted
Vec_IntWriteEntry( p->vAbsFlops, Vec_IntEntry(p->vMapPpi2Ff, i-nPis), 1 ), nFfRefined++;
}
}
Abc_CexFree( pCexCare );
if ( nFfRefined == 0 ) // no refinement -- this is a real CEX
return Pdr_ManDeriveCex(p);
}
Abc_CexFree( pCexCare );
if ( nFfRefined == 0 ) // no refinement -- this is a real CEX
return Pdr_ManDeriveCex(p);
//printf( "CEX-based refinement refined %d flops.\n", nFfRefined );
p->nCexesTotal++;
p->nCexes++;