From 58d4012a558cbf5f6786dc9fdcadc3f1538bdbe2 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 9 Dec 2012 14:46:16 -0800 Subject: Enabling multi-output solving in 'pdr'. --- src/base/abci/abc.c | 51 ++++++++++++++++++++++++-------------------------- src/base/abci/abcDar.c | 47 ++++++++++++++++++---------------------------- 2 files changed, 42 insertions(+), 56 deletions(-) (limited to 'src/base/abci') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index e7fe63e9..4b7f21bd 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -2292,13 +2292,21 @@ int Abc_CommandPrintStatus( Abc_Frame_t * pAbc, int argc, char ** argv ) } } Abc_Print( 1,"Status = %d Frames = %d ", pAbc->Status, pAbc->nFrames ); - if ( pAbc->pCex == NULL ) + if ( pAbc->pCex == NULL && pAbc->vCexVec == NULL ) Abc_Print( 1,"Cex is not defined.\n" ); else - Abc_Print( 1,"Cex: PIs = %d Regs = %d PO = %d Frame = %d Bits = %d\n", - pAbc->pCex->nPis, pAbc->pCex->nRegs, - pAbc->pCex->iPo, pAbc->pCex->iFrame, - pAbc->pCex->nBits ); + { + if ( pAbc->pCex ) + Abc_CexPrintStats( pAbc->pCex ); + if ( pAbc->vCexVec ) + { + Abc_Cex_t * pTemp; + printf( "\n" ); + Vec_PtrForEachEntry( Abc_Cex_t *, pAbc->vCexVec, pTemp, c ) + if ( pTemp ) + Abc_CexPrintStats( pTemp ); + } + } return 0; usage: @@ -20920,7 +20928,10 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv ) } } if ( pNtk->vSeqModelVec ) + { Abc_FrameReplaceCexVec( pAbc, &pNtk->vSeqModelVec ); + pAbc->nFrames = -1; + } return 0; usage: @@ -22314,10 +22325,9 @@ usage: ***********************************************************************/ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex ); + extern int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars ); Pdr_Par_t Pars, * pPars = &Pars; Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); - Abc_Cex_t * pCex = NULL; int c; Pdr_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); @@ -22437,28 +22447,15 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -2, "The current network is not an AIG (run \"strash\").\n"); return 0; } -/* - if ( pPars->iOutput != -1 && (pPars->iOutput < 0 || pPars->iOutput >= Abc_NtkPoNum(pNtk)) ) - { - Abc_Print( -2, "Output index (%d) is incorrect (can be 0 through %d).\n", - pPars->iOutput, Abc_NtkPoNum(pNtk)-1 ); - return 0; - } -*/ -/* - if ( Abc_NtkPoNum(pNtk) != 1 && pPars->fVerbose ) - { - if ( pPars->iOutput == -1 ) - Abc_Print( -2, "The %d property outputs are ORed together.\n", Abc_NtkPoNum(pNtk) ); - else - Abc_Print( -2, "Working on the primary output with zero-based number %d (out of %d).\n", - pPars->iOutput, Abc_NtkPoNum(pNtk) ); - } -*/ // run the procedure - pAbc->Status = Abc_NtkDarPdr( pNtk, pPars, &pCex ); + pAbc->Status = Abc_NtkDarPdr( pNtk, pPars ); pAbc->nFrames = pPars->iFrame; - Abc_FrameReplaceCex( pAbc, &pCex ); + Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel ); + if ( pNtk->vSeqModelVec ) + { + Abc_FrameReplaceCexVec( pAbc, &pNtk->vSeqModelVec ); + pAbc->nFrames = -1; + } return 0; usage: diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 496855c2..742f90bb 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -2705,57 +2705,46 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Fra_Sec_t * pSecPar ) SeeAlso [] ***********************************************************************/ -int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex ) +int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars ) { int RetValue = -1; clock_t clk = clock(); Aig_Man_t * pMan; - *ppCex = NULL; pMan = Abc_NtkToDar( pNtk, 0, 1 ); if ( pMan == NULL ) { Abc_Print( 1, "Converting network into AIG has failed.\n" ); return -1; } -/* - // perform ORing the primary outputs - if ( pPars->iOutput == -1 ) - { - Aig_Man_t * pTemp = Saig_ManDupOrpos( pMan ); - RetValue = Pdr_ManSolve( pTemp, pPars, ppCex ); - if ( RetValue == 0 ) - (*ppCex)->iPo = Saig_ManFindFailedPoCex( pMan, *ppCex ); - Aig_ManStop( pTemp ); - } - else - RetValue = Pdr_ManSolve( pMan, pPars, ppCex ); -*/ - RetValue = Pdr_ManSolve( pMan, pPars, ppCex ); - - // output the result + RetValue = Pdr_ManSolve( pMan, pPars ); if ( !pPars->fSilent ) { 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. ", pMan->pSeqModel->iPo, pNtk->pName, pMan->pSeqModel->iFrame ); + { + 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 ); -// pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL; - if ( ppCex ) - *ppCex = pMan->pSeqModel; - else - ABC_FREE( pMan->pSeqModel ); + ABC_FREE( pNtk->pSeqModel ); + pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL; - - if ( *ppCex && !Saig_ManVerifyCex( pMan, *ppCex ) ) - Abc_Print( 1, "Abc_NtkDarPdr(): Counter-example verification has FAILED.\n" ); + if ( pNtk->vSeqModelVec ) + Vec_PtrFreeFree( pNtk->vSeqModelVec ); + pNtk->vSeqModelVec = pMan->vSeqModelVec; + pMan->vSeqModelVec = NULL; Aig_ManStop( pMan ); return RetValue; } -- cgit v1.2.3