diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-02-28 08:01:00 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-02-28 08:01:00 -0800 |
commit | f65983c2c0810cfb933f696952325a81d2378987 (patch) | |
tree | 4e4ea6ec9da3b6906edd476a85d1d301352e1a02 /src/aig/fra/fraSec.c | |
parent | 7d23cc522e416ae1f3d2d53292ef438d1a08b0d7 (diff) | |
download | abc-f65983c2c0810cfb933f696952325a81d2378987.tar.gz abc-f65983c2c0810cfb933f696952325a81d2378987.tar.bz2 abc-f65983c2c0810cfb933f696952325a81d2378987.zip |
Version abc80228
Diffstat (limited to 'src/aig/fra/fraSec.c')
-rw-r--r-- | src/aig/fra/fraSec.c | 71 |
1 files changed, 8 insertions, 63 deletions
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index a43d83b1..75d297cf 100644 --- a/src/aig/fra/fraSec.c +++ b/src/aig/fra/fraSec.c @@ -40,73 +40,17 @@ SeeAlso [] ***********************************************************************/ -int Fra_FraigSec2( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose ) -{ - Aig_Man_t * pNew; - int nFrames, RetValue, nIter, clk, clkTotal = clock(); - int fLatchCorr = 0; - if ( nFramesFix ) - { - nFrames = nFramesFix; - // perform seq sweeping for one frame number - pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, 0, fVeryVerbose, &nIter ); - } - else - { - // perform seq sweeping while increasing the number of frames - for ( nFrames = 1; ; nFrames++ ) - { -clk = clock(); - pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, 0, fVeryVerbose, &nIter ); - RetValue = Fra_FraigMiterStatus( pNew ); - if ( fVerbose ) - { - printf( "FRAMES %3d : Iters = %3d. ", nFrames, nIter ); - if ( RetValue == 1 ) - printf( "UNSAT " ); - else - printf( "UNDECIDED " ); -PRT( "Time", clock() - clk ); - } - if ( RetValue != -1 ) - break; - Aig_ManStop( pNew ); - } - } - - // get the miter status - RetValue = Fra_FraigMiterStatus( pNew ); - Aig_ManStop( pNew ); - - // report the miter - if ( RetValue == 1 ) - printf( "Networks are equivalent after seq sweeping with K=%d frames (%d iters). ", nFrames, nIter ); - else if ( RetValue == 0 ) - printf( "Networks are NOT EQUIVALENT. " ); - else - printf( "Networks are UNDECIDED after seq sweeping with K=%d frames (%d iters). ", nFrames, nIter ); -PRT( "Time", clock() - clkTotal ); - return RetValue; -} - - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fRetimeFirst, int fVerbose, int fVeryVerbose ) { + Fra_Ssw_t Pars, * pPars = &Pars; Fra_Sml_t * pSml; Aig_Man_t * pNew, * pTemp; int nFrames, RetValue, nIter, clk, clkTotal = clock(); int fLatchCorr = 0; + // prepare parameters + memset( pPars, 0, sizeof(Fra_Ssw_t) ); + pPars->fLatchCorr = fLatchCorr; + pPars->fVerbose = fVeryVerbose; pNew = Aig_ManDup( p, 1 ); if ( fVerbose ) @@ -185,13 +129,14 @@ PRT( "Time", clock() - clk ); for ( nFrames = 1; nFrames <= nFramesMax; nFrames *= 2 ) { clk = clock(); - pNew = Fra_FraigInduction( pTemp = pNew, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, 0, fVeryVerbose, &nIter ); + pPars->nFramesK = nFrames; + pNew = Fra_FraigInduction( pTemp = pNew, pPars ); Aig_ManStop( pTemp ); RetValue = Fra_FraigMiterStatus( pNew ); if ( fVerbose ) { printf( "K-step (K=%2d,I=%3d): Latches = %5d. Nodes = %6d. ", - nFrames, nIter, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); + nFrames, pPars->nIters, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); PRT( "Time", clock() - clk ); } if ( RetValue != -1 ) |