From 632ca7ed11be3bd57ac1a730a9775658c17d9b53 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 16 Feb 2017 13:37:46 -0800 Subject: Promising alternative of CEX minimization in 'pdr'. --- src/base/abci/abc.c | 8 +++-- src/proof/pdr/pdr.h | 1 + src/proof/pdr/pdrCore.c | 6 ++-- src/proof/pdr/pdrMan.c | 79 ++++++++++++++++++++++++++++--------------------- 4 files changed, 57 insertions(+), 37 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 44e4bc16..52684f8c 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -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 ] [-axrmuyfsipdegjonctvwzh]\n" ); + Abc_Print( -2, "usage: pdr [-MFCDQTHGS ] [-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" ); diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h index 534e8e4b..51b04606 100644 --- a/src/proof/pdr/pdr.h +++ b/src/proof/pdr/pdr.h @@ -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 diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index 40e86727..efb4154f 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -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 diff --git a/src/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c index abe8c0a8..a076223b 100644 --- a/src/proof/pdr/pdrMan.c +++ b/src/proof/pdr/pdrMan.c @@ -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++ ) + if ( p->pPars->fUseSimpleRef ) + { + // rely on ternary simulation to perform refinement + Vec_IntForEachEntry( p->vMapPpi2Ff, Flop, 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( Vec_IntEntry(p->vAbsFlops, Flop) == 0 ); + Vec_IntWriteEntry( p->vAbsFlops, Flop, 1 ); + nFfRefined++; } - 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++ ) + } + else { - for ( i = nPis; i < pCexCare->nPis; i++ ) - if ( Abc_InfoHasBit(pCexCare->pData, pCexCare->nRegs + pCexCare->nPis * f + i) ) + // 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++ ) { - 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++; + 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++; -- cgit v1.2.3