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

Enabling multi-output solving in 'pdr'.

This commit is contained in:
Alan Mishchenko 2012-12-09 15:12:40 -08:00
parent 58d4012a55
commit 9fc1cd0b3f
2 changed files with 44 additions and 25 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -2145,10 +2145,10 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars, int fOrDecomp )
else
{
int nOutputs = Saig_ManPoNum(pMan) - Saig_ManConstrNum(pMan);
if ( Vec_PtrCountZero(pMan->vSeqModelVec) == 0 )
Abc_Print( 1, "All %d outputs are found to be SAT. ", nOutputs );
else if ( Vec_PtrCountZero(pMan->vSeqModelVec) == nOutputs )
if ( pMan->vSeqModelVec == NULL || Vec_PtrCountZero(pMan->vSeqModelVec) == nOutputs )
Abc_Print( 1, "None of the %d outputs is found to be SAT. ", nOutputs );
else if ( Vec_PtrCountZero(pMan->vSeqModelVec) == 0 )
Abc_Print( 1, "All %d outputs are found to be SAT. ", nOutputs );
else
Abc_Print( 1, "Some outputs (%d out of %d) are proved SAT. ",
nOutputs - Vec_PtrCountZero(pMan->vSeqModelVec), nOutputs );
@ -2719,23 +2719,37 @@ int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars )
RetValue = Pdr_ManSolve( pMan, pPars );
if ( !pPars->fSilent )
{
if ( RetValue == 1 )
Abc_Print( 1, "Property proved. " );
else if ( RetValue == 0 )
if ( pPars->fSolveAll )
{
if ( pMan->pSeqModel == NULL )
Abc_Print( 1, "Abc_NtkDarPdr(): Counter-example is not available.\n" );
int nOutputs = Saig_ManPoNum(pMan) - Saig_ManConstrNum(pMan);
if ( pMan->vSeqModelVec == NULL || Vec_PtrCountZero(pMan->vSeqModelVec) == nOutputs )
Abc_Print( 1, "None of the %d outputs is found to be SAT. ", nOutputs );
else if ( Vec_PtrCountZero(pMan->vSeqModelVec) == 0 )
Abc_Print( 1, "All %d outputs are found to be SAT. ", nOutputs );
else
{
Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pMan->pSeqModel->iPo, pNtk->pName, pMan->pSeqModel->iFrame );
if ( !Saig_ManVerifyCex( pMan, pMan->pSeqModel ) )
Abc_Print( 1, "Abc_NtkDarPdr(): Counter-example verification has FAILED.\n" );
}
Abc_Print( 1, "Some outputs (%d out of %d) are proved SAT. ",
nOutputs - Vec_PtrCountZero(pMan->vSeqModelVec), nOutputs );
}
else if ( RetValue == -1 )
Abc_Print( 1, "Property UNDECIDED. " );
else
assert( 0 );
{
if ( RetValue == 1 )
Abc_Print( 1, "Property proved. " );
else if ( RetValue == 0 )
{
if ( pMan->pSeqModel == NULL )
Abc_Print( 1, "Abc_NtkDarPdr(): Counter-example is not available.\n" );
else
{
Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pMan->pSeqModel->iPo, pNtk->pName, pMan->pSeqModel->iFrame );
if ( !Saig_ManVerifyCex( pMan, pMan->pSeqModel ) )
Abc_Print( 1, "Abc_NtkDarPdr(): Counter-example verification has FAILED.\n" );
}
}
else if ( RetValue == -1 )
Abc_Print( 1, "Property UNDECIDED. " );
else
assert( 0 );
}
ABC_PRT( "Time", clock() - clk );
}
ABC_FREE( pNtk->pSeqModel );

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

@ -606,7 +606,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
else if ( p->pPars->fVerbose )
Abc_Print( 1, "Computation cancelled by the callback.\n" );
p->pPars->iFrame = k;
return -1;
return p->vCexes ? 0 : -1;
}
if ( RetValue == 0 )
{
@ -620,7 +620,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
else if ( p->pPars->fVerbose )
Abc_Print( 1, "Computation cancelled by the callback.\n" );
p->pPars->iFrame = k;
return -1;
return p->vCexes ? 0 : -1;
}
if ( RetValue == 0 )
{
@ -676,9 +676,14 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 1, clock() - clkStart );
if ( !p->pPars->fSilent )
Abc_Print( 1, "Reached conflict limit (%d).\n", p->pPars->nConfLimit );
{
if ( p->timeToStop && clock() > p->timeToStop )
Abc_Print( 1, "Reached timeout (%d seconds).\n", p->pPars->nTimeOut );
else
Abc_Print( 1, "Reached conflict limit (%d).\n", p->pPars->nConfLimit );
}
p->pPars->iFrame = k;
return -1;
return p->vCexes ? 0 : -1;
}
if ( RetValue )
{
@ -689,7 +694,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
if ( !p->pPars->fSilent )
Pdr_ManVerifyInvariant( p );
p->pPars->iFrame = k;
return 1; // UNSAT
return p->vCexes ? 0 : 1; // UNSAT
}
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 0, clock() - clkStart );
@ -698,7 +703,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
if ( p->pPars->pFuncStop && p->pPars->pFuncStop(p->pPars->RunId) )
{
p->pPars->iFrame = k;
return -1;
return p->vCexes ? 0 : -1;
}
if ( p->timeToStop && clock() > p->timeToStop )
{
@ -712,7 +717,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
if ( !p->pPars->fSilent )
Abc_Print( 1, "Reached timeout (%d seconds).\n", p->pPars->nTimeOut );
p->pPars->iFrame = k;
return -1;
return p->vCexes ? 0 : -1;
}
if ( p->pPars->nFrameMax && k >= p->pPars->nFrameMax )
{
@ -721,10 +726,10 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
if ( !p->pPars->fSilent )
Abc_Print( 1, "Reached limit on the number of timeframes (%d).\n", p->pPars->nFrameMax );
p->pPars->iFrame = k;
return -1;
return p->vCexes ? 0 : -1;
}
}
return RetValue;
return p->vCexes ? 0 : RetValue;
}
/**Function*************************************************************