From fcdd9148b456e7efec1db8b4cf81adbb305401d7 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 12 Jun 2014 21:27:14 -0700 Subject: Various modifications. --- src/proof/cec/cecCec.c | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) (limited to 'src/proof/cec/cecCec.c') diff --git a/src/proof/cec/cecCec.c b/src/proof/cec/cecCec.c index f3b1a3b0..b43700ae 100644 --- a/src/proof/cec/cecCec.c +++ b/src/proof/cec/cecCec.c @@ -66,14 +66,13 @@ void Cec_ManTransformPattern( Gia_Man_t * p, int iOut, int * pValues ) SeeAlso [] ***********************************************************************/ -int Cec_ManVerifyOld( Gia_Man_t * pMiter, int fVerbose, int * piOutFail ) +int Cec_ManVerifyOld( Gia_Man_t * pMiter, int fVerbose, int * piOutFail, abctime clkTotal ) { // extern int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose ); extern int Ssw_SecCexResimulate( Aig_Man_t * p, int * pModel, int * pnOutputs ); Gia_Man_t * pTemp = Gia_ManTransformMiter( pMiter ); Aig_Man_t * pMiterCec = Gia_ManToAig( pTemp, 0 ); int RetValue, iOut, nOuts; - abctime clkTotal = Abc_Clock(); if ( piOutFail ) *piOutFail = -1; Gia_ManStop( pTemp ); @@ -83,12 +82,12 @@ int Cec_ManVerifyOld( Gia_Man_t * pMiter, int fVerbose, int * piOutFail ) if ( RetValue == 1 ) { Abc_Print( 1, "Networks are equivalent. " ); -Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal ); } else if ( RetValue == 0 ) { Abc_Print( 1, "Networks are NOT EQUIVALENT. " ); -Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal ); if ( pMiterCec->pData == NULL ) Abc_Print( 1, "Counter-example is not available.\n" ); else @@ -113,7 +112,7 @@ Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal ); else { Abc_Print( 1, "Networks are UNDECIDED. " ); -Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal ); } fflush( stdout ); Aig_ManStop( pMiterCec ); @@ -275,7 +274,7 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars ) if ( pPars->fVerbose ) Abc_Print( 1, "Calling the old CEC engine.\n" ); fflush( stdout ); - RetValue = Cec_ManVerifyOld( pNew, pPars->fVerbose, &pPars->iOutFail ); + RetValue = Cec_ManVerifyOld( pNew, pPars->fVerbose, &pPars->iOutFail, clkTotal ); p->pCexComb = pNew->pCexComb; pNew->pCexComb = NULL; if ( p->pCexComb && !Gia_ManVerifyCex( p, p->pCexComb, 1 ) ) Abc_Print( 1, "Counter-example simulation has failed.\n" ); -- cgit v1.2.3