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

fixed time profiling in pdr

This commit is contained in:
Yen-Sheng Ho 2017-02-20 10:13:18 -08:00
parent 25ecc3d429
commit 222b3741a4
1 changed files with 4 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/base/wlc/wlcAbs.c
View File

@ -313,6 +313,7 @@ static int Wlc_NtkRemoveFromAbstraction( Wlc_Ntk_t * p, Vec_Int_t * vRefine, Vec
int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
{ {
abctime clk = Abc_Clock(); abctime clk = Abc_Clock();
abctime pdrClk;
Pdr_Man_t * pPdr; Pdr_Man_t * pPdr;
Vec_Vec_t * vClauses = NULL; Vec_Vec_t * vClauses = NULL;
int nIters, nNodes, nDcFlops, RetValue = -1; int nIters, nNodes, nDcFlops, RetValue = -1;
@ -368,6 +369,7 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
pAig = Gia_ManToAigSimple( pGia ); pAig = Gia_ManToAigSimple( pGia );
pPdr = Pdr_ManStart( pAig, pPdrPars, NULL ); pPdr = Pdr_ManStart( pAig, pPdrPars, NULL );
pdrClk = Abc_Clock();
if ( vClauses ) { if ( vClauses ) {
assert( Vec_VecSize( vClauses) >= 2 ); assert( Vec_VecSize( vClauses) >= 2 );
@ -375,6 +377,7 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
} }
RetValue = IPdr_ManSolveInt( pPdr ); RetValue = IPdr_ManSolveInt( pPdr );
pPdr->tTotal += Abc_Clock() - pdrClk;
pCex = pAig->pSeqModel; pAig->pSeqModel = NULL; pCex = pAig->pSeqModel; pAig->pSeqModel = NULL;
@ -403,6 +406,7 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
// spurious CEX, continue solving // spurious CEX, continue solving
vClauses = IPdr_ManSaveClauses( pPdr, 0 ); vClauses = IPdr_ManSaveClauses( pPdr, 0 );
Pdr_ManStop( pPdr ); Pdr_ManStop( pPdr );
// update the set of objects to be un-abstracted // update the set of objects to be un-abstracted