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

Fixed the overflow timeout problem in bmc/bmc2/bmc3/int/pdr/sim, etc.

This commit is contained in:
Alan Mishchenko 2011-10-31 15:04:47 -05:00
parent 868a1b9aeb
commit 5b75410a5e
3 changed files with 12 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
src/base/abci/abcDar.c
View File

@ -1694,7 +1694,7 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int
{
Aig_Man_t * pMan;
int status, RetValue = -1, clk = clock();
int nTimeLimit = nTimeOut ? clock() + nTimeOut * CLOCKS_PER_SEC : 0;
int nTimeLimit = nTimeOut ? time(NULL) + nTimeOut : 0;
// derive the AIG manager
pMan = Abc_NtkToDar( pNtk, 0, 1 );
@ -1722,7 +1722,7 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int
else if ( RetValue == -1 )
{
printf( "No output asserted in %d frames. Resource limit reached ", iFrame );
if ( nTimeLimit < clock() )
if ( time(NULL) > nTimeLimit )
printf( "(timeout %d sec). ", nTimeLimit );
else
printf( "(conf limit %d). ", nBTLimit );
@ -1804,7 +1804,7 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars )
{
Aig_Man_t * pMan;
int status, RetValue = -1, clk = clock();
int nTimeOut = pPars->nTimeOut ? clock() + pPars->nTimeOut * CLOCKS_PER_SEC : 0;
int nTimeOut = pPars->nTimeOut ? time(NULL) + pPars->nTimeOut : 0;
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
{
@ -1825,7 +1825,7 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars )
if ( pPars->nFailOuts == 0 )
{
printf( "No output asserted in %d frames. Resource limit reached ", pPars->iFrame );
if ( nTimeOut < clock() )
if ( time(NULL) > nTimeOut )
printf( "(timeout %d sec). ", pPars->nTimeOut );
else
printf( "(conf limit %d). ", pPars->nConfLimit );
@ -1833,7 +1833,7 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars )
else
{
printf( "The total of %d outputs asserted in %d frames. Resource limit reached ", pPars->nFailOuts, pPars->iFrame );
if ( nTimeOut < clock() )
if ( time(NULL) > nTimeOut )
printf( "(timeout %d sec). ", pPars->nTimeOut );
else
printf( "(conf limit %d). ", pPars->nConfLimit );

8
src/misc/extra/extraBddMisc.c
View File

@ -1348,9 +1348,9 @@ extraTransferPermuteRecur(
if ( st_lookup( table, ( char * ) f, ( char ** ) &res ) )
return ( Cudd_NotCond( res, comple ) );
if ( ddS->TimeStop && ddS->TimeStop < clock() )
if ( ddS->TimeStop && time(NULL) > ddS->TimeStop )
return NULL;
if ( ddD->TimeStop && ddD->TimeStop < clock() )
if ( ddD->TimeStop && time(NULL) > ddD->TimeStop )
return NULL;
/* Recursive step. */
@ -1909,9 +1909,9 @@ DdNode * extraBddAndPermute( DdHashTable * table, DdManager * ddF, DdNode * bF,
return bRes;
Counter++;
if ( ddF->TimeStop && ddF->TimeStop < clock() )
if ( ddF->TimeStop && time(NULL) > ddF->TimeStop )
return NULL;
if ( ddG->TimeStop && ddG->TimeStop < clock() )
if ( ddG->TimeStop && time(NULL) > ddG->TimeStop )
return NULL;
// find the topmost variable in F and G using var order of F

6
src/misc/extra/extraBddTime.c
View File

@ -225,7 +225,7 @@ cuddBddAndRecurTime(
}
// if ( TimeOut && ((*pRecCalls)++ % CHECK_FACTOR) == 0 && TimeOut < clock() )
if ( TimeOut && TimeOut < clock() )
if ( TimeOut && time(NULL) > TimeOut )
return NULL;
/* Here we can skip the use of cuddI, because the operands are known
@ -379,7 +379,7 @@ cuddBddAndAbstractRecurTime(
}
// if ( TimeOut && ((*pRecCalls)++ % CHECK_FACTOR) == 0 && TimeOut < clock() )
if ( TimeOut && TimeOut < clock() )
if ( TimeOut && time(NULL) > TimeOut )
return NULL;
if (topf == top) {
@ -596,7 +596,7 @@ extraTransferPermuteRecurTime(
if ( st_lookup( table, ( char * ) f, ( char ** ) &res ) )
return ( Cudd_NotCond( res, comple ) );
if ( TimeOut && TimeOut < clock() )
if ( TimeOut && time(NULL) > TimeOut )
return NULL;
/* Recursive step. */