luke/abc
1
0
Fork 0
mirror of https://github.com/YosysHQ/abc.git synced 2026-09-07 11:11:19 +02:00
Code Issues Packages Projects Releases Wiki Activity

Various modifications.

Browse Source
This commit is contained in:
Alan Mishchenko
2014-06-12 21:27:14 -07:00
parent 865f6fd43f
commit fcdd9148b4
13 changed files with 141 additions and 104 deletions
Download Patch File Download Diff File Expand all files Collapse all files
src/proof/cec/cecCec.c
+5 -6
View File
@@ -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" );