diff options
| author | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-02-20 10:13:18 -0800 |
|---|---|---|
| committer | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-02-20 10:13:18 -0800 |
| commit | 222b3741a40af2913132ef385936b955bbc19b4d (patch) | |
| tree | 056ebf100096c226be489b1d51bf238e65a6784d /src/base/wlc | |
| parent | 25ecc3d42973cd832d78b00cbed188171892325d (diff) | |
| download | abc-222b3741a40af2913132ef385936b955bbc19b4d.tar.gz abc-222b3741a40af2913132ef385936b955bbc19b4d.tar.bz2 abc-222b3741a40af2913132ef385936b955bbc19b4d.zip | |
fixed time profiling in pdr
Diffstat (limited to 'src/base/wlc')
| -rw-r--r-- | src/base/wlc/wlcAbs.c | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index 47bd9a3f..902c060d 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -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 ) { abctime clk = Abc_Clock(); + abctime pdrClk; Pdr_Man_t * pPdr; Vec_Vec_t * vClauses = NULL; 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 ); pPdr = Pdr_ManStart( pAig, pPdrPars, NULL ); + pdrClk = Abc_Clock(); if ( vClauses ) { assert( Vec_VecSize( vClauses) >= 2 ); @@ -375,6 +377,7 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) } RetValue = IPdr_ManSolveInt( pPdr ); + pPdr->tTotal += Abc_Clock() - pdrClk; 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 vClauses = IPdr_ManSaveClauses( pPdr, 0 ); + Pdr_ManStop( pPdr ); // update the set of objects to be un-abstracted |