diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-09-21 08:01:00 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-09-21 08:01:00 -0700 |
| commit | 4d71c114a3405f0a2c59a8467c82a8da3f785262 (patch) | |
| tree | 1c4a0fdf938e247b03e832f26c74c8a48af2826b /src/aig/fra/fraSec.c | |
| parent | 3429e6309d0fc9a2d35d81f6483258c6af2fab50 (diff) | |
| download | abc-4d71c114a3405f0a2c59a8467c82a8da3f785262.tar.gz abc-4d71c114a3405f0a2c59a8467c82a8da3f785262.tar.bz2 abc-4d71c114a3405f0a2c59a8467c82a8da3f785262.zip | |
Version abc80921
Diffstat (limited to 'src/aig/fra/fraSec.c')
| -rw-r--r-- | src/aig/fra/fraSec.c | 19 |
1 files changed, 14 insertions, 5 deletions
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index 677123d8..232a789e 100644 --- a/src/aig/fra/fraSec.c +++ b/src/aig/fra/fraSec.c @@ -93,8 +93,6 @@ int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec ) goto finish; // prepare parameters - Ssw_ManSetDefaultParams( pPars2 ); - // prepare parameters memset( pPars, 0, sizeof(Fra_Ssw_t) ); pPars->fLatchCorr = fLatchCorr; pPars->fVerbose = pParSec->fVeryVerbose; @@ -142,7 +140,8 @@ PRT( "Time", clock() - clk ); if ( pParSec->fRetimeFirst && pNew->nRegs ) { clk = clock(); - pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 ); +// pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 ); + pNew = Saig_ManRetimeForward( pTemp = pNew, 100, 0 ); Aig_ManStop( pTemp ); if ( pParSec->fVerbose ) { @@ -172,11 +171,21 @@ clk = clock(); goto finish; } } - pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 1000, 1, pParSec->fVeryVerbose, &nIter, TimeLeft ); + + +// pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 1000, 1, pParSec->fVeryVerbose, &nIter, TimeLeft ); +//Aig_ManDumpBlif( pNew, "ex.blif", NULL, NULL ); + Ssw_ManSetDefaultParamsLcorr( pPars2 ); + pNew = Ssw_LatchCorrespondence( pTemp = pNew, pPars2 ); + nIter = pPars2->nIters; + + // prepare parameters for scorr + Ssw_ManSetDefaultParams( pPars2 ); + if ( pTemp->pSeqModel ) { if ( !Ssw_SmlRunCounterExample( pTemp, pTemp->pSeqModel ) ) - printf( "Fra_FraigLatchCorrespondence(): Counter-example verification has FAILED.\n" ); + printf( "Fra_FraigSec(): Counter-example verification has FAILED.\n" ); if ( Saig_ManPiNum(p) != Saig_ManPiNum(pTemp) ) printf( "The counter-example is invalid because of phase abstraction.\n" ); else |