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

Passing conflict limit to &cec.

This commit is contained in:
Alan Mishchenko 2020-11-22 21:34:33 -10:00
parent 4757c7febc
commit 2e92256fb7
2 changed files with 4 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -37227,8 +37227,8 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( fUseNew ) if ( fUseNew )
{ {
abctime clk = Abc_Clock(); abctime clk = Abc_Clock();
extern Gia_Man_t * Cec4_ManSimulateTest3( Gia_Man_t * p, int fVerbose ); extern Gia_Man_t * Cec4_ManSimulateTest3( Gia_Man_t * p, int nBTLimit, int fVerbose );
Gia_Man_t * pNew = Cec4_ManSimulateTest3( pMiter, pPars->fVerbose ); Gia_Man_t * pNew = Cec4_ManSimulateTest3( pMiter, pPars->nBTLimit, pPars->fVerbose );
if ( Gia_ManAndNum(pNew) == 0 ) if ( Gia_ManAndNum(pNew) == 0 )
Abc_Print( 1, "Networks are equivalent. " ); Abc_Print( 1, "Networks are equivalent. " );
else else

3
src/proof/cec/cecSatG2.c
View File

@ -1802,12 +1802,13 @@ void Cec4_ManSimulateTest2( Gia_Man_t * p, int fVerbose )
if ( fVerbose ) if ( fVerbose )
Abc_PrintTime( 1, "New choice computation time", Abc_Clock() - clk ); Abc_PrintTime( 1, "New choice computation time", Abc_Clock() - clk );
} }
Gia_Man_t * Cec4_ManSimulateTest3( Gia_Man_t * p, int fVerbose ) Gia_Man_t * Cec4_ManSimulateTest3( Gia_Man_t * p, int nBTLimit, int fVerbose )
{ {
Gia_Man_t * pNew = NULL; Gia_Man_t * pNew = NULL;
Cec_ParFra_t ParsFra, * pPars = &ParsFra; Cec_ParFra_t ParsFra, * pPars = &ParsFra;
Cec4_ManSetParams( pPars ); Cec4_ManSetParams( pPars );
pPars->fVerbose = fVerbose; pPars->fVerbose = fVerbose;
pPars->nBTLimit = nBTLimit;
Cec4_ManPerformSweeping( p, pPars, &pNew ); Cec4_ManPerformSweeping( p, pPars, &pNew );
return pNew; return pNew;
} }