diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-09-12 16:46:37 -0500 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-09-12 16:46:37 -0500 |
commit | 8248691d8441e22d19d645d738f92b59fb3c95da (patch) | |
tree | d32fe02527426dd661daa4474cac4dce4ada8291 /src/aig/saig/saigAbsStart.c | |
parent | 583bc4d71a403028d60fd676ce72c3c6d1e2e7fe (diff) | |
download | abc-8248691d8441e22d19d645d738f92b59fb3c95da.tar.gz abc-8248691d8441e22d19d645d738f92b59fb3c95da.tar.bz2 abc-8248691d8441e22d19d645d738f92b59fb3c95da.zip |
Added limit on the number of flops to add in one iteration of &abs_refine.
Diffstat (limited to 'src/aig/saig/saigAbsStart.c')
-rw-r--r-- | src/aig/saig/saigAbsStart.c | 22 |
1 files changed, 20 insertions, 2 deletions
diff --git a/src/aig/saig/saigAbsStart.c b/src/aig/saig/saigAbsStart.c index 5f7042c8..71ef98d5 100644 --- a/src/aig/saig/saigAbsStart.c +++ b/src/aig/saig/saigAbsStart.c @@ -168,7 +168,7 @@ Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlo SeeAlso [] ***********************************************************************/ -int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Abc_Cex_t * pCex, int fTryFour, int fSensePath, int fVerbose ) +int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Vec_Int_t * vFlopClasses, Abc_Cex_t * pCex, int nFfToAddMax, int fTryFour, int fSensePath, int fVerbose ) { Aig_Man_t * pAbs; Vec_Int_t * vFlopsNew; @@ -198,7 +198,25 @@ int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Abc_Cex_t * pCex, printf( "Adding %d registers to the abstraction (total = %d). ", Vec_IntSize(vFlopsNew), Aig_ManRegNum(p)+Vec_IntSize(vFlopsNew) ); Abc_PrintTime( 1, "Time", clock() - clk ); } - // vFlopsNew contains PI number that should be kept in pAbs + // vFlopsNew contains PI numbers that should be kept in pAbs + // select the most useful flops among those to be added + if ( nFfToAddMax > 0 && Vec_IntSize(vFlopsNew) > nFfToAddMax ) + { + Vec_Int_t * vFlopsNewBest; + // shift the indices + Vec_IntForEachEntry( vFlopsNew, Entry, i ) + Vec_IntAddToEntry( vFlopsNew, i, -Saig_ManPiNum(p) ); + // create new flops + vFlopsNewBest = Saig_ManCbaFilterFlops( p, pCex, vFlopClasses, vFlopsNew, nFfToAddMax ); + assert( Vec_IntSize(vFlopsNewBest) == nFfToAddMax ); + printf( "Filtering flops based on cost (%d -> %d).\n", Vec_IntSize(vFlopsNew), Vec_IntSize(vFlopsNewBest) ); + // update + Vec_IntFree( vFlopsNew ); + vFlopsNew = vFlopsNewBest; + // shift the indices + Vec_IntForEachEntry( vFlopsNew, Entry, i ) + Vec_IntAddToEntry( vFlopsNew, i, Saig_ManPiNum(p) ); + } // add to the abstraction Vec_IntForEachEntry( vFlopsNew, Entry, i ) { |