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

copied pdr_mansolve

This commit is contained in:
Yen-Sheng Ho 2017-02-18 10:28:16 -08:00
parent 196b359183
commit 91a0a0fc3b
2 changed files with 41 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
src/base/abci/abc.c
View File

@ -26630,9 +26630,8 @@ int Abc_CommandIPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0; return 0;
} }
// run the procedure // run the procedure
IPdr_ManSolve( pNtk, pPars );
pPars->fUseBridge = pAbc->fBridgeMode; pPars->fUseBridge = pAbc->fBridgeMode;
pAbc->Status = Abc_NtkDarPdr( pNtk, pPars ); pAbc->Status = IPdr_ManSolve( pNtk, pPars );
pAbc->nFrames = pNtk->vSeqModelVec ? -1 : pPars->iFrame; pAbc->nFrames = pNtk->vSeqModelVec ? -1 : pPars->iFrame;
Abc_FrameReplacePoStatuses( pAbc, &pPars->vOutMap ); Abc_FrameReplacePoStatuses( pAbc, &pPars->vOutMap );
if ( pNtk->vSeqModelVec ) if ( pNtk->vSeqModelVec )

41
src/proof/pdr/pdrIncr.c
View File

@ -27,6 +27,7 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS /// /// DECLARATIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS /// /// FUNCTION DEFINITIONS ///
@ -45,7 +46,45 @@ ABC_NAMESPACE_IMPL_START
***********************************************************************/ ***********************************************************************/
int IPdr_ManSolve( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars ) 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;
} }
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////