diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/proof/pdr/pdr.h | 1 | ||||
-rw-r--r-- | src/proof/pdr/pdrCore.c | 18 | ||||
-rw-r--r-- | src/proof/ssw/ssw.h | 2 | ||||
-rw-r--r-- | src/proof/ssw/sswRarity.c | 166 | ||||
-rw-r--r-- | src/sat/bmc/bmc.h | 1 | ||||
-rw-r--r-- | src/sat/bmc/bmcBmc3.c | 21 |
6 files changed, 122 insertions, 87 deletions
diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h index 6e157aad..cfb13356 100644 --- a/src/proof/pdr/pdr.h +++ b/src/proof/pdr/pdr.h @@ -62,6 +62,7 @@ struct Pdr_Par_t_ int iFrame; // explored up to this frame int RunId; // PDR id in this run int(*pFuncStop)(int); // callback to terminate + int(*pFuncOnFail)(int,Abc_Cex_t*); // called for a failed output in MO mode clock_t timeLastSolved; // the time when the last output was solved }; diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index eb21edfc..3df1d7de 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -591,6 +591,15 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) p->vCexes = Vec_PtrStart( Saig_ManPoNum(p->pAig) ); assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL ); Vec_PtrWriteEntry( p->vCexes, p->iOutCur, p->pPars->fStoreCex ? Pdr_ManDeriveCex(p) : (void *)(ABC_PTRINT_T)1 ); + if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(p->iOutCur, p->pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, p->iOutCur) : NULL) ) + { + if ( p->pPars->fVerbose ) + Pdr_ManPrintProgress( p, 1, clock() - clkStart ); + if ( !p->pPars->fSilent ) + Abc_Print( 1, "Quitting due to callback on fail.\n" ); + p->pPars->iFrame = k; + return -1; + } if ( p->pPars->nFailOuts == Saig_ManPoNum(p->pAig) ) return 0; // all SAT p->pPars->timeLastSolved = clock(); @@ -659,6 +668,15 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) p->vCexes = Vec_PtrStart( Saig_ManPoNum(p->pAig) ); assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL ); Vec_PtrWriteEntry( p->vCexes, p->iOutCur, p->pPars->fStoreCex ? Pdr_ManDeriveCex(p) : (void *)(ABC_PTRINT_T)1 ); + if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(p->iOutCur, p->pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, p->iOutCur) : NULL) ) + { + if ( p->pPars->fVerbose ) + Pdr_ManPrintProgress( p, 1, clock() - clkStart ); + if ( !p->pPars->fSilent ) + Abc_Print( 1, "Quitting due to callback on fail.\n" ); + p->pPars->iFrame = k; + return -1; + } if ( !p->pPars->fNotVerbose ) Abc_Print( 1, "Output %*d was asserted in frame %2d (%2d) (solved %*d out of %*d outputs).\n", nOutDigits, p->iOutCur, k, k, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) ); diff --git a/src/proof/ssw/ssw.h b/src/proof/ssw/ssw.h index d81bae20..a05409ee 100644 --- a/src/proof/ssw/ssw.h +++ b/src/proof/ssw/ssw.h @@ -105,7 +105,9 @@ struct Ssw_RarPars_t_ int fMiter; int fUseCex; int fLatchOnly; + int nSolved; Abc_Cex_t * pCex; + int(*pFuncOnFail)(int,Abc_Cex_t*); // called for a failed output in MO mode }; typedef struct Ssw_Sml_t_ Ssw_Sml_t; // sequential simulation manager diff --git a/src/proof/ssw/sswRarity.c b/src/proof/ssw/sswRarity.c index cad7b9ed..013ee130 100644 --- a/src/proof/ssw/sswRarity.c +++ b/src/proof/ssw/sswRarity.c @@ -34,10 +34,7 @@ typedef struct Ssw_RarMan_t_ Ssw_RarMan_t; struct Ssw_RarMan_t_ { // parameters - int nWords; // the number of words to simulate - int nFrames; // the number of frames to simulate - int nBinSize; // the number of flops in one group - int fVerbose; // the verbosiness flag + Ssw_RarPars_t* pPars; int nGroups; // the number of flop groups int nWordsReg; // the number of words in the registers // internal data @@ -64,27 +61,27 @@ struct Ssw_RarMan_t_ static inline int Ssw_RarGetBinPat( Ssw_RarMan_t * p, int iBin, int iPat ) { - assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->nBinSize ); - assert( iPat >= 0 && iPat < (1 << p->nBinSize) ); - return p->pRarity[iBin * (1 << p->nBinSize) + iPat]; + assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->pPars->nBinSize ); + assert( iPat >= 0 && iPat < (1 << p->pPars->nBinSize) ); + return p->pRarity[iBin * (1 << p->pPars->nBinSize) + iPat]; } static inline void Ssw_RarSetBinPat( Ssw_RarMan_t * p, int iBin, int iPat, int Value ) { - assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->nBinSize ); - assert( iPat >= 0 && iPat < (1 << p->nBinSize) ); - p->pRarity[iBin * (1 << p->nBinSize) + iPat] = Value; + assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->pPars->nBinSize ); + assert( iPat >= 0 && iPat < (1 << p->pPars->nBinSize) ); + p->pRarity[iBin * (1 << p->pPars->nBinSize) + iPat] = Value; } static inline void Ssw_RarAddToBinPat( Ssw_RarMan_t * p, int iBin, int iPat ) { - assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->nBinSize ); - assert( iPat >= 0 && iPat < (1 << p->nBinSize) ); - p->pRarity[iBin * (1 << p->nBinSize) + iPat]++; + assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->pPars->nBinSize ); + assert( iPat >= 0 && iPat < (1 << p->pPars->nBinSize) ); + p->pRarity[iBin * (1 << p->pPars->nBinSize) + iPat]++; } static inline int Ssw_RarBitWordNum( int nBits ) { return (nBits>>6) + ((nBits&63) > 0); } -static inline word * Ssw_RarObjSim( Ssw_RarMan_t * p, int Id ) { assert( Id < Aig_ManObjNumMax(p->pAig) ); return p->pObjData + p->nWords * Id; } -static inline word * Ssw_RarPatSim( Ssw_RarMan_t * p, int Id ) { assert( Id < 64 * p->nWords ); return p->pPatData + p->nWordsReg * Id; } +static inline word * Ssw_RarObjSim( Ssw_RarMan_t * p, int Id ) { assert( Id < Aig_ManObjNumMax(p->pAig) ); return p->pObjData + p->pPars->nWords * Id; } +static inline word * Ssw_RarPatSim( Ssw_RarMan_t * p, int Id ) { assert( Id < 64 * p->pPars->nWords ); return p->pPatData + p->nWordsReg * Id; } //////////////////////////////////////////////////////////////////////// @@ -158,7 +155,7 @@ void Ssw_RarManAssingRandomPis( Ssw_RarMan_t * p ) Saig_ManForEachPi( p->pAig, pObj, i ) { pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) ); - for ( w = 0; w < p->nWords; w++ ) + for ( w = 0; w < p->pPars->nWords; w++ ) pSim[w] = Aig_ManRandom64(0); // pSim[0] <<= 1; // pSim[0] = (pSim[0] << 2) | 2; @@ -186,11 +183,11 @@ Abc_Cex_t * Ssw_RarDeriveCex( Ssw_RarMan_t * p, int iFrame, int iPo, int iPatFin int i, r, f, iBit, iPatThis; // compute the pattern sequence iPatThis = iPatFinal; - vTrace = Vec_IntStartFull( iFrame / p->nFrames + 1 ); - Vec_IntWriteEntry( vTrace, iFrame / p->nFrames, iPatThis ); - for ( r = iFrame / p->nFrames - 1; r >= 0; r-- ) + vTrace = Vec_IntStartFull( iFrame / p->pPars->nFrames + 1 ); + Vec_IntWriteEntry( vTrace, iFrame / p->pPars->nFrames, iPatThis ); + for ( r = iFrame / p->pPars->nFrames - 1; r >= 0; r-- ) { - iPatThis = Vec_IntEntry( p->vPatBests, r * p->nWords + iPatThis / 64 ); + iPatThis = Vec_IntEntry( p->vPatBests, r * p->pPars->nWords + iPatThis / 64 ); Vec_IntWriteEntry( vTrace, r, iPatThis ); } // create counter-example @@ -202,7 +199,7 @@ Abc_Cex_t * Ssw_RarDeriveCex( Ssw_RarMan_t * p, int iFrame, int iPo, int iPatFin for ( f = 0; f <= iFrame; f++ ) { Ssw_RarManAssingRandomPis( p ); - iPatThis = Vec_IntEntry( vTrace, f / p->nFrames ); + iPatThis = Vec_IntEntry( vTrace, f / p->pPars->nFrames ); Saig_ManForEachPi( p->pAig, pObj, i ) { pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) ); @@ -365,7 +362,7 @@ void Ssw_RarTranspose( Ssw_RarMan_t * p ) Aig_Obj_t * pObj; word M[64]; int w, r, i; - for ( w = 0; w < p->nWords; w++ ) + for ( w = 0; w < p->pPars->nWords; w++ ) for ( r = 0; r < p->nWordsReg; r++ ) { // save input @@ -389,10 +386,10 @@ void Ssw_RarTranspose( Ssw_RarMan_t * p ) Saig_ManForEachLi( p->pAig, pObj, i ) { word * pBitData = Ssw_RarObjSim( p, Aig_ObjId(pObj) ); - Extra_PrintBinary( stdout, (unsigned *)pBitData, 64*p->nWords ); Abc_Print( 1, "\n" ); + Extra_PrintBinary( stdout, (unsigned *)pBitData, 64*p->pPars->nWords ); Abc_Print( 1, "\n" ); } Abc_Print( 1, "\n" ); - for ( i = 0; i < p->nWords*64; i++ ) + for ( i = 0; i < p->pPars->nWords*64; i++ ) { word * pBitData = Ssw_RarPatSim( p, i ); Extra_PrintBinary( stdout, (unsigned *)pBitData, Aig_ManRegNum(p->pAig) ); Abc_Print( 1, "\n" ); @@ -423,18 +420,18 @@ void Ssw_RarManInitialize( Ssw_RarMan_t * p, Vec_Int_t * vInit ) // constant pObj = Aig_ManConst1( p->pAig ); pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) ); - for ( w = 0; w < p->nWords; w++ ) + for ( w = 0; w < p->pPars->nWords; w++ ) pSim[w] = ~(word)0; // primary inputs Ssw_RarManAssingRandomPis( p ); // flop outputs if ( vInit ) { - assert( Vec_IntSize(vInit) == Saig_ManRegNum(p->pAig) * p->nWords ); + assert( Vec_IntSize(vInit) == Saig_ManRegNum(p->pAig) * p->pPars->nWords ); Saig_ManForEachLo( p->pAig, pObj, i ) { pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) ); - for ( w = 0; w < p->nWords; w++ ) + for ( w = 0; w < p->pPars->nWords; w++ ) pSim[w] = Vec_IntEntry(vInit, w * Saig_ManRegNum(p->pAig) + i) ? ~(word)0 : (word)0; } } @@ -444,7 +441,7 @@ void Ssw_RarManInitialize( Ssw_RarMan_t * p, Vec_Int_t * vInit ) { pSimLi = Ssw_RarObjSim( p, Aig_ObjId(pObjLi) ); pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) ); - for ( w = 0; w < p->nWords; w++ ) + for ( w = 0; w < p->pPars->nWords; w++ ) pSim[w] = pSimLi[w]; } } @@ -466,7 +463,7 @@ int Ssw_RarManPoIsConst0( void * pMan, Aig_Obj_t * pObj ) Ssw_RarMan_t * p = (Ssw_RarMan_t *)pMan; word * pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) ); int w; - for ( w = 0; w < p->nWords; w++ ) + for ( w = 0; w < p->pPars->nWords; w++ ) if ( pSim[w] ) return 0; return 1; @@ -489,7 +486,7 @@ int Ssw_RarManObjIsConst( void * pMan, Aig_Obj_t * pObj ) word * pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) ); word Flip = pObj->fPhase ? ~(word)0 : 0; int w; - for ( w = 0; w < p->nWords; w++ ) + for ( w = 0; w < p->pPars->nWords; w++ ) if ( pSim[w] ^ Flip ) return 0; return 1; @@ -513,7 +510,7 @@ int Ssw_RarManObjsAreEqual( void * pMan, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ) word * pSim1 = Ssw_RarObjSim( p, pObj1->Id ); word Flip = (pObj0->fPhase != pObj1->fPhase) ? ~(word)0 : 0; int w; - for ( w = 0; w < p->nWords; w++ ) + for ( w = 0; w < p->pPars->nWords; w++ ) if ( pSim0[w] ^ pSim1[w] ^ Flip ) return 0; return 1; @@ -553,7 +550,7 @@ unsigned Ssw_RarManObjHashWord( void * pMan, Aig_Obj_t * pObj ) int i; uHash = 0; pSims = (unsigned *)Ssw_RarObjSim( p, pObj->Id ); - for ( i = 0; i < 2 * p->nWords; i++ ) + for ( i = 0; i < 2 * p->pPars->nWords; i++ ) uHash ^= pSims[i] * s_SPrimes[i & 0x7F]; return uHash; } @@ -574,7 +571,7 @@ int Ssw_RarManObjWhichOne( Ssw_RarMan_t * p, Aig_Obj_t * pObj ) word * pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) ); word Flip = pObj->fPhase ? ~(word)0 : 0; int w, i; - for ( w = 0; w < p->nWords; w++ ) + for ( w = 0; w < p->pPars->nWords; w++ ) if ( pSim[w] ^ Flip ) { for ( i = 0; i < 64; i++ ) @@ -597,10 +594,10 @@ int Ssw_RarManObjWhichOne( Ssw_RarMan_t * p, Aig_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -int Ssw_RarManCheckNonConstOutputs( Ssw_RarMan_t * p, int * pnSolvedNow, int iFrame, int fNotVerbose, clock_t Time ) +int Ssw_RarManCheckNonConstOutputs( Ssw_RarMan_t * p, int iFrame, clock_t Time ) { Aig_Obj_t * pObj; - int i, RetValue = 0; + int i; p->iFailPo = -1; p->iFailPat = -1; Saig_ManForEachPo( p->pAig, pObj, i ) @@ -611,29 +608,33 @@ int Ssw_RarManCheckNonConstOutputs( Ssw_RarMan_t * p, int * pnSolvedNow, int iFr continue; if ( Ssw_RarManPoIsConst0(p, pObj) ) continue; - RetValue = 1; p->iFailPo = i; p->iFailPat = Ssw_RarManObjWhichOne( p, pObj ); - if ( pnSolvedNow == NULL ) + if ( !p->pPars->fSolveAll ) break; // remember the one solved - (*pnSolvedNow)++; + p->pPars->nSolved++; if ( p->vCexes == NULL ) p->vCexes = Vec_PtrStart( Saig_ManPoNum(p->pAig) ); assert( Vec_PtrEntry(p->vCexes, i) == NULL ); Vec_PtrWriteEntry( p->vCexes, i, (void *)(ABC_PTRINT_T)1 ); + if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(i, NULL) ) + return 2; // quitting due to callback // print final report - if ( !fNotVerbose ) + if ( !p->pPars->fNotVerbose ) { int nOutDigits = Abc_Base10Log( Saig_ManPoNum(p->pAig) ); Abc_Print( 1, "Output %*d was asserted in frame %4d (solved %*d out of %*d outputs). ", nOutDigits, p->iFailPo, iFrame, - nOutDigits, *pnSolvedNow, + nOutDigits, p->pPars->nSolved, nOutDigits, Saig_ManPoNum(p->pAig) ); Abc_PrintTime( 1, "Time", Time ); } } - return RetValue; + if ( p->iFailPo >= 0 ) // found CEX + return 1; + else + return 0; } /**Function************************************************************* @@ -684,7 +685,7 @@ void Ssw_RarManSimulate( Ssw_RarMan_t * p, Vec_Int_t * vInit, int fUpdate, int f pSim1 = Ssw_RarObjSim( p, Aig_ObjFaninId1(pObj) ); Flip0 = Aig_ObjFaninC0(pObj) ? ~(word)0 : 0; Flip1 = Aig_ObjFaninC1(pObj) ? ~(word)0 : 0; - for ( w = 0; w < p->nWords; w++ ) + for ( w = 0; w < p->pPars->nWords; w++ ) pSim[w] = (Flip0 ^ pSim0[w]) & (Flip1 ^ pSim1[w]); @@ -711,7 +712,7 @@ void Ssw_RarManSimulate( Ssw_RarMan_t * p, Vec_Int_t * vInit, int fUpdate, int f pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) ); pSim0 = Ssw_RarObjSim( p, Aig_ObjFaninId0(pObj) ); Flip = Aig_ObjFaninC0(pObj) ? ~(word)0 : 0; - for ( w = 0; w < p->nWords; w++ ) + for ( w = 0; w < p->pPars->nWords; w++ ) pSim[w] = Flip ^ pSim0[w]; } // refine classes @@ -747,23 +748,20 @@ void Ssw_RarManSimulate( Ssw_RarMan_t * p, Vec_Int_t * vInit, int fUpdate, int f SeeAlso [] ***********************************************************************/ -static Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, int nWords, int nFrames, int nBinSize, int fVerbose ) +static Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, Ssw_RarPars_t * pPars ) { Ssw_RarMan_t * p; // if ( Aig_ManRegNum(pAig) < nBinSize || nBinSize <= 0 ) // return NULL; p = ABC_CALLOC( Ssw_RarMan_t, 1 ); p->pAig = pAig; - p->nWords = nWords; - p->nFrames = nFrames; - p->nBinSize = nBinSize; - p->fVerbose = fVerbose; - p->nGroups = Aig_ManRegNum(pAig) / nBinSize; - p->pRarity = ABC_CALLOC( int, (1 << nBinSize) * p->nGroups ); - p->pPatCosts = ABC_CALLOC( double, p->nWords * 64 ); + p->pPars = pPars; + p->nGroups = Aig_ManRegNum(pAig) / pPars->nBinSize; + p->pRarity = ABC_CALLOC( int, (1 << pPars->nBinSize) * p->nGroups ); + p->pPatCosts = ABC_CALLOC( double, p->pPars->nWords * 64 ); p->nWordsReg = Ssw_RarBitWordNum( Aig_ManRegNum(pAig) ); - p->pObjData = ABC_ALLOC( word, Aig_ManObjNumMax(pAig) * p->nWords ); - p->pPatData = ABC_ALLOC( word, 64 * p->nWords * p->nWordsReg ); + p->pObjData = ABC_ALLOC( word, Aig_ManObjNumMax(pAig) * p->pPars->nWords ); + p->pPatData = ABC_ALLOC( word, 64 * p->pPars->nWords * p->nWordsReg ); p->vUpdConst = Vec_PtrAlloc( 100 ); p->vUpdClass = Vec_PtrAlloc( 100 ); p->vPatBests = Vec_IntAlloc( 100 ); @@ -824,7 +822,7 @@ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits ) Ssw_RarTranspose( p ); // update counters - for ( k = 0; k < p->nWords * 64; k++ ) + for ( k = 0; k < p->pPars->nWords * 64; k++ ) { pData = (unsigned char *)Ssw_RarPatSim( p, k ); for ( i = 0; i < p->nGroups; i++ ) @@ -832,7 +830,7 @@ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits ) } // for each pattern - for ( k = 0; k < p->nWords * 64; k++ ) + for ( k = 0; k < p->pPars->nWords * 64; k++ ) { pData = (unsigned char *)Ssw_RarPatSim( p, k ); // find the cost of its values @@ -849,12 +847,12 @@ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits ) // choose as many as there are words Vec_IntClear( vInits ); - for ( i = 0; i < p->nWords; i++ ) + for ( i = 0; i < p->pPars->nWords; i++ ) { // select the best int iPatBest = -1; double iCostBest = -ABC_INFINITY; - for ( k = 0; k < p->nWords * 64; k++ ) + for ( k = 0; k < p->pPars->nWords * 64; k++ ) if ( iCostBest < p->pPatCosts[k] ) { iCostBest = p->pPatCosts[k]; @@ -870,7 +868,7 @@ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits ) //Abc_Print( 1, "Best pattern %5d\n", iPatBest ); Vec_IntPush( p->vPatBests, iPatBest ); } - assert( Vec_IntSize(vInits) == Aig_ManRegNum(p->pAig) * p->nWords ); + assert( Vec_IntSize(vInits) == Aig_ManRegNum(p->pAig) * p->pPars->nWords ); } @@ -985,7 +983,6 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, Ssw_RarPars_t * pPars ) int nSavedSeed = pPars->nRandSeed; int RetValue = -1; int iFrameFail = -1; - int nSolved = 0; assert( Aig_ManRegNum(pAig) > 0 ); assert( Aig_ManConstrNum(pAig) == 0 ); ABC_FREE( pAig->pSeqModel ); @@ -1002,10 +999,11 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, Ssw_RarPars_t * pPars ) Ssw_RarManPrepareRandom( nSavedSeed ); // create manager - p = Ssw_RarManStart( pAig, pPars->nWords, pPars->nFrames, pPars->nBinSize, pPars->fVerbose ); + p = Ssw_RarManStart( pAig, pPars ); p->vInits = Vec_IntStart( Aig_ManRegNum(pAig) * pPars->nWords ); // perform simulation rounds + pPars->nSolved = 0; timeLastSolved = clock(); for ( r = 0; !pPars->nRounds || (nNumRestart * pPars->nRestart + r < pPars->nRounds); r++ ) { @@ -1022,23 +1020,33 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, Ssw_RarPars_t * pPars ) for ( f = 0; f < pPars->nFrames; f++ ) { Ssw_RarManSimulate( p, f ? NULL : p->vInits, 0, 0 ); - if ( fMiter && Ssw_RarManCheckNonConstOutputs(p, pPars->fSolveAll ? &nSolved : NULL, r * p->nFrames + f, pPars->fNotVerbose, clock() - clkTotal) ) + if ( fMiter ) { - RetValue = 0; - if ( !pPars->fSolveAll ) + int Status = Ssw_RarManCheckNonConstOutputs(p, r * p->pPars->nFrames + f, clock() - clkTotal); + if ( Status == 2 ) { - if ( pPars->fVerbose ) Abc_Print( 1, "\n" ); - // Abc_Print( 1, "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames ); - Ssw_RarManPrepareRandom( nSavedSeed ); - if ( pPars->fVerbose ) - Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts.\n", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart ); - pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->nFrames + f, p->iFailPo, p->iFailPat, pPars->fVerbose ); - // print final report - Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pAig->pSeqModel->iPo, pAig->pName, pAig->pSeqModel->iFrame ); - Abc_PrintTime( 1, "Time", clock() - clkTotal ); + Abc_Print( 1, "Quitting due to callback on fail.\n" ); goto finish; } - timeLastSolved = clock(); + if ( Status == 1 ) // found CEX + { + RetValue = 0; + if ( !pPars->fSolveAll ) + { + if ( pPars->fVerbose ) Abc_Print( 1, "\n" ); + // Abc_Print( 1, "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames ); + Ssw_RarManPrepareRandom( nSavedSeed ); + if ( pPars->fVerbose ) + Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts.\n", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart ); + pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->pPars->nFrames + f, p->iFailPo, p->iFailPat, pPars->fVerbose ); + // print final report + Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pAig->pSeqModel->iPo, pAig->pName, pAig->pSeqModel->iFrame ); + Abc_PrintTime( 1, "Time", clock() - clkTotal ); + goto finish; + } + timeLastSolved = clock(); + } + // else - did not find a counter example } // check timeout if ( pPars->TimeOut && clock() > nTimeToStop ) @@ -1081,7 +1089,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, Ssw_RarPars_t * pPars ) Abc_Print( 1, "Starts =%6d ", nNumRestart ); Abc_Print( 1, "Rounds =%6d ", nNumRestart * pPars->nRestart + ((r==-1)?0:r) ); Abc_Print( 1, "Frames =%6d ", (nNumRestart * pPars->nRestart + r) * pPars->nFrames ); - Abc_Print( 1, "CEX =%6d (%6.2f %%) ", nSolved, 100.0*nSolved/Saig_ManPoNum(p->pAig) ); + Abc_Print( 1, "CEX =%6d (%6.2f %%) ", pPars->nSolved, 100.0*pPars->nSolved/Saig_ManPoNum(p->pAig) ); Abc_PrintTime( 1, "Time", clock() - clkTotal ); } else @@ -1096,10 +1104,10 @@ finish: Vec_IntShrink( p->vInits, Aig_ManRegNum(pAig) ); pAig->pData = p->vInits; p->vInits = NULL; } - if ( nSolved ) + if ( pPars->nSolved ) { if ( pPars->fVerbose && !pPars->fSolveAll ) Abc_Print( 1, "\n" ); - Abc_Print( 1, "Simulation of %d frames for %d rounds with %d restarts asserted %d (out of %d) POs. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart, nSolved, Saig_ManPoNum(p->pAig) ); + Abc_Print( 1, "Simulation of %d frames for %d rounds with %d restarts asserted %d (out of %d) POs. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart, pPars->nSolved, Saig_ManPoNum(p->pAig) ); Abc_PrintTime( 1, "Time", clock() - clkTotal ); } else if ( r == pPars->nRounds && f == pPars->nFrames ) @@ -1175,7 +1183,7 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, Ssw_RarPars_t * pPars ) Ssw_RarManPrepareRandom( nSavedSeed ); // create manager - p = Ssw_RarManStart( pAig, pPars->nWords, pPars->nFrames, pPars->nBinSize, pPars->fVerbose ); + p = Ssw_RarManStart( pAig, pPars ); // compute starting state if needed assert( p->vInits == NULL ); if ( pPars->pCex ) @@ -1216,7 +1224,7 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, Ssw_RarPars_t * pPars ) for ( f = 0; f < pPars->nFrames; f++ ) { Ssw_RarManSimulate( p, f ? NULL : p->vInits, 1, !r && !f ); - if ( pPars->fMiter && Ssw_RarManCheckNonConstOutputs(p, NULL, -1, -1, 0) ) + if ( pPars->fMiter && Ssw_RarManCheckNonConstOutputs(p, -1, 0) ) { if ( !pPars->fVerbose ) Abc_Print( 1, "%s", Abc_FrameIsBatchMode() ? "\n" : "\r" ); @@ -1225,7 +1233,7 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, Ssw_RarPars_t * pPars ) Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts.\n", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart ); Ssw_RarManPrepareRandom( nSavedSeed ); Abc_CexFree( pAig->pSeqModel ); - pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->nFrames + f, p->iFailPo, p->iFailPat, 1 ); + pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->pPars->nFrames + f, p->iFailPo, p->iFailPat, 1 ); // print final report Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pAig->pSeqModel->iPo, pAig->pName, pAig->pSeqModel->iFrame ); Abc_PrintTime( 1, "Time", clock() - clkTotal ); diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index 93bfd78a..19084ada 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -60,6 +60,7 @@ struct Saig_ParBmc_t_ int iFrame; // explored up to this frame int nFailOuts; // the number of failed 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 }; diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c index 0c828dbd..b737749d 100644 --- a/src/sat/bmc/bmcBmc3.c +++ b/src/sat/bmc/bmcBmc3.c @@ -1477,13 +1477,13 @@ clkOther += clock() - clk2; continue; if ( Lit == 1 ) { + RetValue = 0; if ( !pPars->fSolveAll ) { Abc_Cex_t * pCex = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), f*Saig_ManPoNum(pAig)+i ); printf( "Output %d is trivially SAT in frame %d.\n", i, f ); ABC_FREE( pAig->pSeqModel ); pAig->pSeqModel = pCex; - RetValue = 0; goto finish; } pPars->nFailOuts++; @@ -1492,11 +1492,12 @@ clkOther += clock() - clk2; nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) ); if ( p->vCexes == NULL ) p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) ); - if ( pPars->fStoreCex ) - Vec_PtrWriteEntry( p->vCexes, i, Abc_CexMakeTriv( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), f*Saig_ManPoNum(pAig)+i ) ); - else - Vec_PtrWriteEntry( p->vCexes, i, (void *)(ABC_PTRINT_T)1 ); - RetValue = 0; + Vec_PtrWriteEntry( p->vCexes, i, pPars->fStoreCex ? Abc_CexMakeTriv( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), f*Saig_ManPoNum(pAig)+i ) : (void *)(ABC_PTRINT_T)1 ); + if ( pPars->pFuncOnFail && pPars->pFuncOnFail(i, pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, i) : NULL) ) + { + Abc_Print( 1, "Quitting due to callback on fail.\n" ); + goto finish; + } // reset the timeout pPars->timeLastSolved = clock(); nTimeToStop = Saig_ManBmcTimeToStop( pPars, nTimeToStopNG ); @@ -1533,6 +1534,7 @@ nTimeUnsat += clock() - clk2; else if ( status == l_True ) { nTimeSat += clock() - clk2; + RetValue = 0; fFirst = 0; if ( !pPars->fSolveAll ) { @@ -1558,7 +1560,6 @@ nTimeSat += clock() - clk2; } ABC_FREE( pAig->pSeqModel ); pAig->pSeqModel = Saig_ManGenerateCex( p, f, i ); - RetValue = 0; goto finish; } pPars->nFailOuts++; @@ -1568,7 +1569,11 @@ nTimeSat += clock() - clk2; if ( p->vCexes == NULL ) p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) ); Vec_PtrWriteEntry( p->vCexes, i, pPars->fStoreCex? Saig_ManGenerateCex( p, f, i ) : (void *)(ABC_PTRINT_T)1 ); - RetValue = 0; + if ( pPars->pFuncOnFail && pPars->pFuncOnFail(i, pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, i) : NULL) ) + { + Abc_Print( 1, "Quitting due to callback on fail.\n" ); + goto finish; + } // reset the timeout pPars->timeLastSolved = clock(); nTimeToStop = Saig_ManBmcTimeToStop( pPars, nTimeToStopNG ); |