diff options
| author | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-02-18 10:28:16 -0800 |
|---|---|---|
| committer | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-02-18 10:28:16 -0800 |
| commit | 91a0a0fc3b5dfd5aa71122106dbdacf6268e51fb (patch) | |
| tree | 5c8c71f8a15c9727e053e187a11f4428ef309445 /src | |
| parent | 196b3591830e9fbe0877411b8053233c11d0f4ce (diff) | |
| download | abc-91a0a0fc3b5dfd5aa71122106dbdacf6268e51fb.tar.gz abc-91a0a0fc3b5dfd5aa71122106dbdacf6268e51fb.tar.bz2 abc-91a0a0fc3b5dfd5aa71122106dbdacf6268e51fb.zip | |
copied pdr_mansolve
Diffstat (limited to 'src')
| -rw-r--r-- | src/base/abci/abc.c | 3 | ||||
| -rw-r--r-- | src/proof/pdr/pdrIncr.c | 41 |
2 files changed, 41 insertions, 3 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 0e3a1d3a..f12e3727 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -26630,9 +26630,8 @@ int Abc_CommandIPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; } // run the procedure - IPdr_ManSolve( pNtk, pPars ); pPars->fUseBridge = pAbc->fBridgeMode; - pAbc->Status = Abc_NtkDarPdr( pNtk, pPars ); + pAbc->Status = IPdr_ManSolve( pNtk, pPars ); pAbc->nFrames = pNtk->vSeqModelVec ? -1 : pPars->iFrame; Abc_FrameReplacePoStatuses( pAbc, &pPars->vOutMap ); if ( pNtk->vSeqModelVec ) diff --git a/src/proof/pdr/pdrIncr.c b/src/proof/pdr/pdrIncr.c index a2329870..2276384c 100644 --- a/src/proof/pdr/pdrIncr.c +++ b/src/proof/pdr/pdrIncr.c @@ -27,6 +27,7 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -45,7 +46,45 @@ ABC_NAMESPACE_IMPL_START ***********************************************************************/ int IPdr_ManSolve( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars ) { - return 0; + int RetValue = -1; + abctime clk = Abc_Clock(); + Aig_Man_t * pMan; + pMan = Abc_NtkToDar( pNtk, 0, 1 ); + + RetValue = Pdr_ManSolve( pMan, pPars ); + + if ( RetValue == 1 ) + Abc_Print( 1, "Property proved. " ); + else + { + if ( RetValue == 0 ) + { + if ( pMan->pSeqModel == NULL ) + Abc_Print( 1, "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, "Counter-example verification has FAILED.\n" ); + } + } + else if ( RetValue == -1 ) + Abc_Print( 1, "Property UNDECIDED. " ); + else + assert( 0 ); + } + ABC_PRT( "Time", Abc_Clock() - clk ); + + + ABC_FREE( pNtk->pSeqModel ); + pNtk->pSeqModel = pMan->pSeqModel; + pMan->pSeqModel = NULL; + if ( pNtk->vSeqModelVec ) + Vec_PtrFreeFree( pNtk->vSeqModelVec ); + pNtk->vSeqModelVec = pMan->vSeqModelVec; + pMan->vSeqModelVec = NULL; + Aig_ManStop( pMan ); + return RetValue; } //////////////////////////////////////////////////////////////////////// |