diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-02-01 15:47:55 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-02-01 15:47:55 -0800 |
commit | d4291dab37a647ac3d8d0f4e91e571bbb4e3553b (patch) | |
tree | 84c00511c7c6b3d21a8521cee25c8034fd5be464 /src/aig/saig/saigTempor.c | |
parent | 624af674a0e7f1a675917afaaf371db6a5588821 (diff) | |
download | abc-d4291dab37a647ac3d8d0f4e91e571bbb4e3553b.tar.gz abc-d4291dab37a647ac3d8d0f4e91e571bbb4e3553b.tar.bz2 abc-d4291dab37a647ac3d8d0f4e91e571bbb4e3553b.zip |
Cumulative changes of the last two weeks.
Diffstat (limited to 'src/aig/saig/saigTempor.c')
-rw-r--r-- | src/aig/saig/saigTempor.c | 61 |
1 files changed, 55 insertions, 6 deletions
diff --git a/src/aig/saig/saigTempor.c b/src/aig/saig/saigTempor.c index 80bde75c..74f4a9d3 100644 --- a/src/aig/saig/saigTempor.c +++ b/src/aig/saig/saigTempor.c @@ -147,6 +147,32 @@ Aig_Man_t * Saig_ManTemporDecompose( Aig_Man_t * pAig, int nFrames ) /**Function************************************************************* + Synopsis [Find index of first non-zero entry.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Vec_IntLastNonZeroBeforeLimit( Vec_Int_t * vTemp, int Limit ) +{ + int Entry, i; + if ( vTemp == NULL ) + return -1; + Vec_IntForEachEntryReverse( vTemp, Entry, i ) + { + if ( i >= Limit ) + continue; + if ( Entry ) + return i; + } + return -1; +} + +/**Function************************************************************* + Synopsis [] Description [] @@ -156,19 +182,33 @@ Aig_Man_t * Saig_ManTemporDecompose( Aig_Man_t * pAig, int nFrames ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Saig_ManTempor( Aig_Man_t * pAig, int nFrames, int TimeOut, int nConfLimit, int fUseBmc, int fVerbose, int fVeryVerbose ) +Aig_Man_t * Saig_ManTempor( Aig_Man_t * pAig, int nFrames, int TimeOut, int nConfLimit, int fUseBmc, int fUseTransSigs, int fVerbose, int fVeryVerbose ) { - extern int Saig_ManPhasePrefixLength( Aig_Man_t * p, int fVerbose, int fVeryVerbose ); + extern int Saig_ManPhasePrefixLength( Aig_Man_t * p, int fVerbose, int fVeryVerbose, Vec_Int_t ** pvTrans ); + + Vec_Int_t * vTransSigs = NULL; int RetValue, nFramesFinished = -1; assert( nFrames >= 0 ); if ( nFrames == 0 ) { - nFrames = Saig_ManPhasePrefixLength( pAig, fVerbose, fVeryVerbose ); + nFrames = Saig_ManPhasePrefixLength( pAig, fVerbose, fVeryVerbose, &vTransSigs ); if ( nFrames == 1 ) { + Vec_IntFreeP( &vTransSigs ); printf( "The leading sequence has length 1. Temporal decomposition is not performed.\n" ); return NULL; } + if ( fUseTransSigs ) + { + int Entry, i, iLast = -1; + Vec_IntForEachEntry( vTransSigs, Entry, i ) + iLast = Entry ? i :iLast; + if ( iLast > 0 && iLast < nFrames ) + { + Abc_Print( 1, "Reducing frame count from %d to %d to fit the last transient.\n", nFrames, iLast ); + nFrames = iLast; + } + } Abc_Print( 1, "Using computed frame number (%d).\n", nFrames ); } else @@ -176,18 +216,27 @@ Aig_Man_t * Saig_ManTempor( Aig_Man_t * pAig, int nFrames, int TimeOut, int nCon // run BMC2 if ( fUseBmc ) { - RetValue = Saig_BmcPerform( pAig, 0, nFrames, 5000, TimeOut, nConfLimit, 0, fVerbose, 0, &nFramesFinished ); + RetValue = Saig_BmcPerform( pAig, 0, nFrames, 2000, TimeOut, nConfLimit, 0, fVerbose, 0, &nFramesFinished ); if ( RetValue == 0 ) { + Vec_IntFreeP( &vTransSigs ); printf( "A cex found in the first %d frames.\n", nFrames ); return NULL; } if ( nFramesFinished < nFrames ) { - printf( "BMC for %d frames could not be completed. A cex may exist!\n", nFrames ); - return NULL; + int iLastBefore = Vec_IntLastNonZeroBeforeLimit( vTransSigs, nFramesFinished ); + if ( iLastBefore < 1 || !fUseTransSigs ) + { + Vec_IntFreeP( &vTransSigs ); + printf( "BMC for %d frames could not be completed. A cex may exist!\n", nFrames ); + return NULL; + } + assert( iLastBefore < nFramesFinished ); + printf( "BMC succeeded to frame %d. Adjusting frame count to be (%d) based on the last transient signal.\n", nFramesFinished, iLastBefore ); } } + Vec_IntFreeP( &vTransSigs ); return Saig_ManTemporDecompose( pAig, nFrames ); } |