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 10:11:52 -08:00
parent 8a08453af2
commit 9f396a0d7e
1 changed files with 9 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -2738,7 +2738,7 @@ int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex )
if ( RetValue == 1 )
Abc_Print( 1, "Property proved. " );
else if ( RetValue == 0 )
Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", (*ppCex)->iPo, pNtk->pName, ppCex? (*ppCex)->iFrame : -1 );
Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pMan->pSeqModel->iPo, pNtk->pName, pMan->pSeqModel->iFrame );
else if ( RetValue == -1 )
Abc_Print( 1, "Property UNDECIDED. " );
else
@ -2746,6 +2746,14 @@ int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex )
ABC_PRT( "Time", clock() - clk );
}
// ABC_FREE( pNtk->pSeqModel );
// pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
if ( ppCex )
*ppCex = pMan->pSeqModel;
else
ABC_FREE( pMan->pSeqModel );
pMan->pSeqModel = NULL;
if ( *ppCex && !Saig_ManVerifyCex( pMan, *ppCex ) )
Abc_Print( 1, "Abc_NtkDarPdr(): Counter-example verification has FAILED.\n" );
Aig_ManStop( pMan );