diff options
| -rw-r--r-- | src/aig/saig/saigBmc3.c | 25 | ||||
| -rw-r--r-- | src/base/abci/abcDar.c | 10 |
2 files changed, 26 insertions, 9 deletions
diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c index 453ea918..508a46c1 100644 --- a/src/aig/saig/saigBmc3.c +++ b/src/aig/saig/saigBmc3.c @@ -1098,6 +1098,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) Gia_ManBmc_t * p; Aig_Obj_t * pObj; int RetValue = -1, fFirst = 1; + int nOutDigits = Aig_Base10Log( Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig) ); int i, f, Lit, status, clk, clk2, clkOther = 0, clkTotal = clock(); if ( pPars->fVerbose && Aig_ManConstrNum(pAig) > 0 ) printf( "Performing BMC with constraints...\n" ); @@ -1119,6 +1120,19 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) Saig_ManBmcMarkPis( pAig, pPars->nPisAbstract ); for ( f = 0; f < pPars->nFramesMax; f++ ) { + // stop BMC after exploring all reachable states + if ( Aig_ManRegNum(pAig) < 30 && f == (1 << Aig_ManRegNum(pAig)) ) + { + Saig_Bmc3ManStop( p ); + return pPars->nFailOuts ? 0 : 1; + } + // stop BMC if all targets are solved + if ( pPars->fSolveAll && pPars->nFailOuts == Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig) ) + { + Saig_Bmc3ManStop( p ); + return 0; + } + // consider the next timeframe pPars->iFrame = f; // resize the array Vec_IntFillExtra( p->vPiVars, (f+1)*Saig_ManPiNum(p->pAig), 0 ); @@ -1158,8 +1172,10 @@ clkOther += clock() - clk2; return 1; } } + if ( pPars->nStart && f < pPars->nStart ) + continue; // solve SAT - clk = clock(); + clk = clock(); Saig_ManForEachPo( pAig, pObj, i ) { if ( i >= Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig) ) @@ -1176,15 +1192,17 @@ clkOther += clock() - clk2; if ( Lit == 1 ) { 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 ); if ( !pPars->fSolveAll ) { + printf( "Output %d is trivially SAT in frame %d.\n", i, f ); ABC_FREE( pAig->pSeqModel ); pAig->pSeqModel = pCex; Saig_Bmc3ManStop( p ); return 0; } pPars->nFailOuts++; + printf( "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n", + nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig) ); if ( p->vCexes == NULL ) p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) ); Vec_PtrWriteEntry( p->vCexes, i, pCex ); @@ -1231,7 +1249,8 @@ clkOther += clock() - clk2; return 0; } pPars->nFailOuts++; - printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness).\n", i, f ); + printf( "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n", + nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig) ); if ( p->vCexes == NULL ) p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) ); Vec_PtrWriteEntry( p->vCexes, i, pCex ); diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index c0822ba9..064529cc 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -1805,8 +1805,7 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars ) pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL; if ( RetValue == 1 ) { -// printf( "No output asserted in %d frames. ", pPars->iFrame ); - printf( "Incorrect return value. " ); + printf( "Explored all reachable states after completing %d frames. ", 1<<Aig_ManRegNum(pMan) ); } else if ( RetValue == -1 ) { @@ -1839,8 +1838,7 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars ) } else { - printf( "Incorrect return value. " ); -// printf( "At least one output asserted (out=%d, frame=%d). ", pCex->iPo, pCex->iFrame ); + printf( "All %d outputs are proved SAT. ", Saig_ManPoNum(pMan) - pMan->nConstrs ); } } ABC_PRT( "Time", clock() - clk ); @@ -3044,8 +3042,8 @@ int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, } else { - printf( "Simulation of %d frames with %d words did not assert the outputs. ", - nFrames, nWords ); +// printf( "Simulation of %d frames with %d words did not assert the outputs. ", +// nFrames, nWords ); } ABC_PRT( "Time", clock() - clk ); Aig_ManStop( pMan ); |