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

Improvements to 'bmc3' (start frame; stop when all POs are SAT; stop when 2^nRegs frames are completed).

This commit is contained in:
Alan Mishchenko 2011-07-31 20:22:57 +07:00
parent d5955db960
commit 0d65c49048
2 changed files with 26 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

25
src/aig/saig/saigBmc3.c
View File

@ -1098,6 +1098,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
Gia_ManBmc_t * p; Gia_ManBmc_t * p;
Aig_Obj_t * pObj; Aig_Obj_t * pObj;
int RetValue = -1, fFirst = 1; 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(); int i, f, Lit, status, clk, clk2, clkOther = 0, clkTotal = clock();
if ( pPars->fVerbose && Aig_ManConstrNum(pAig) > 0 ) if ( pPars->fVerbose && Aig_ManConstrNum(pAig) > 0 )
printf( "Performing BMC with constraints...\n" ); 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 ); Saig_ManBmcMarkPis( pAig, pPars->nPisAbstract );
for ( f = 0; f < pPars->nFramesMax; f++ ) 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; pPars->iFrame = f;
// resize the array // resize the array
Vec_IntFillExtra( p->vPiVars, (f+1)*Saig_ManPiNum(p->pAig), 0 ); Vec_IntFillExtra( p->vPiVars, (f+1)*Saig_ManPiNum(p->pAig), 0 );
@ -1158,8 +1172,10 @@ clkOther += clock() - clk2;
return 1; return 1;
} }
} }
if ( pPars->nStart && f < pPars->nStart )
continue;
// solve SAT // solve SAT
clk = clock(); clk = clock();
Saig_ManForEachPo( pAig, pObj, i ) Saig_ManForEachPo( pAig, pObj, i )
{ {
if ( i >= Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig) ) if ( i >= Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig) )
@ -1176,15 +1192,17 @@ clkOther += clock() - clk2;
if ( Lit == 1 ) if ( Lit == 1 )
{ {
Abc_Cex_t * pCex = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), f*Saig_ManPoNum(pAig)+i ); 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 ) if ( !pPars->fSolveAll )
{ {
printf( "Output %d is trivially SAT in frame %d.\n", i, f );
ABC_FREE( pAig->pSeqModel ); ABC_FREE( pAig->pSeqModel );
pAig->pSeqModel = pCex; pAig->pSeqModel = pCex;
Saig_Bmc3ManStop( p ); Saig_Bmc3ManStop( p );
return 0; return 0;
} }
pPars->nFailOuts++; 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 ) if ( p->vCexes == NULL )
p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) ); p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
Vec_PtrWriteEntry( p->vCexes, i, pCex ); Vec_PtrWriteEntry( p->vCexes, i, pCex );
@ -1231,7 +1249,8 @@ clkOther += clock() - clk2;
return 0; return 0;
} }
pPars->nFailOuts++; 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 ) if ( p->vCexes == NULL )
p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) ); p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
Vec_PtrWriteEntry( p->vCexes, i, pCex ); Vec_PtrWriteEntry( p->vCexes, i, pCex );

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

@ -1805,8 +1805,7 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars )
pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL; pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
if ( RetValue == 1 ) if ( RetValue == 1 )
{ {
// printf( "No output asserted in %d frames. ", pPars->iFrame ); printf( "Explored all reachable states after completing %d frames. ", 1<<Aig_ManRegNum(pMan) );
printf( "Incorrect return value. " );
} }
else if ( RetValue == -1 ) else if ( RetValue == -1 )
{ {
@ -1839,8 +1838,7 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars )
} }
else else
{ {
printf( "Incorrect return value. " ); printf( "All %d outputs are proved SAT. ", Saig_ManPoNum(pMan) - pMan->nConstrs );
// printf( "At least one output asserted (out=%d, frame=%d). ", pCex->iPo, pCex->iFrame );
} }
} }
ABC_PRT( "Time", clock() - clk ); ABC_PRT( "Time", clock() - clk );
@ -3044,8 +3042,8 @@ int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize,
} }
else else
{ {
printf( "Simulation of %d frames with %d words did not assert the outputs. ", // printf( "Simulation of %d frames with %d words did not assert the outputs. ",
nFrames, nWords ); // nFrames, nWords );
} }
ABC_PRT( "Time", clock() - clk ); ABC_PRT( "Time", clock() - clk );
Aig_ManStop( pMan ); Aig_ManStop( pMan );