diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-05-06 20:33:06 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-05-06 20:33:06 -0700 |
| commit | e2e3f6a2281b65632a139933cfc5021a84257a3a (patch) | |
| tree | 018a3669e87f318c11b661c9ec9da3e53dc638db /src/aig/saig/saigMiter.c | |
| parent | a0cc621566d5218fde3d82647ff3b32b5f8c09aa (diff) | |
| download | abc-e2e3f6a2281b65632a139933cfc5021a84257a3a.tar.gz abc-e2e3f6a2281b65632a139933cfc5021a84257a3a.tar.bz2 abc-e2e3f6a2281b65632a139933cfc5021a84257a3a.zip | |
Improvements in sequential verification.
Diffstat (limited to 'src/aig/saig/saigMiter.c')
| -rw-r--r-- | src/aig/saig/saigMiter.c | 20 |
1 files changed, 15 insertions, 5 deletions
diff --git a/src/aig/saig/saigMiter.c b/src/aig/saig/saigMiter.c index b470333d..4d775314 100644 --- a/src/aig/saig/saigMiter.c +++ b/src/aig/saig/saigMiter.c @@ -870,8 +870,11 @@ int Ssw_SecSpecial( Aig_Man_t * pPart0, Aig_Man_t * pPart1, int nFrames, int fVe int iOut, nOuts; Aig_Man_t * pMiterCec; int RetValue, clkTotal = clock(); - Aig_ManPrintStats( pPart0 ); - Aig_ManPrintStats( pPart1 ); + if ( fVerbose ) + { + Aig_ManPrintStats( pPart0 ); + Aig_ManPrintStats( pPart1 ); + } // Aig_ManDumpBlif( pPart0, "file0.blif", NULL, NULL ); // Aig_ManDumpBlif( pPart1, "file1.blif", NULL, NULL ); // assert( Aig_ManNodeNum(pPart0) <= Aig_ManNodeNum(pPart1) ); @@ -879,8 +882,8 @@ int Ssw_SecSpecial( Aig_Man_t * pPart0, Aig_Man_t * pPart1, int nFrames, int fVe { printf( "Warning: The design after synthesis is smaller!\n" ); printf( "This warning may indicate that the order of designs is changed.\n" ); - printf( "The solver expects the original disign as first argument and\n" ); - printf( "the modified design as the second argument in Ssw_SecSpecial().\n" ); + printf( "The solver expects the original design as first argument and\n" ); + printf( "the modified design as the second argument in \"absec\".\n" ); } // create two-level miter pMiterCec = Saig_ManCreateMiterTwo( pPart0, pPart1, nFrames ); @@ -950,7 +953,7 @@ int Ssw_SecSpecialMiter( Aig_Man_t * p0, Aig_Man_t * p1, int nFrames, int fVerbo Aig_Man_t * pPart0, * pPart1; int RetValue; if ( fVerbose ) - printf( "Performing sequential verification combinational A/B miter.\n" ); + printf( "Performing sequential verification using combinational A/B miter.\n" ); // consider the case when a miter is given if ( p1 == NULL ) { @@ -964,6 +967,13 @@ int Ssw_SecSpecialMiter( Aig_Man_t * p0, Aig_Man_t * p1, int nFrames, int fVerbo printf( "Demitering has failed.\n" ); return -1; } + if ( Aig_ManRegNum(pPart0) != Aig_ManRegNum(pPart1) ) + { + Aig_ManStop( pPart0 ); + Aig_ManStop( pPart1 ); + printf( "After demitering AIGs have different number of flops. Quitting.\n" ); + return -1; + } } else { |