diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-09-18 08:01:00 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-09-18 08:01:00 -0700 |
| commit | 655a50101e18176f1163ccfc67cf69d86623d1f2 (patch) | |
| tree | dd31c20fe95145cdc23d30eb0b65ff727881b57b /src/aig/ssw | |
| parent | ce690b29075a23a07673d0a4727f0bf9557ec882 (diff) | |
| download | abc-655a50101e18176f1163ccfc67cf69d86623d1f2.tar.gz abc-655a50101e18176f1163ccfc67cf69d86623d1f2.tar.bz2 abc-655a50101e18176f1163ccfc67cf69d86623d1f2.zip | |
Version abc80918
Diffstat (limited to 'src/aig/ssw')
| -rw-r--r-- | src/aig/ssw/ssw.h | 1 | ||||
| -rw-r--r-- | src/aig/ssw/sswPairs.c | 33 |
2 files changed, 34 insertions, 0 deletions
diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h index 14c10f6a..91c2165a 100644 --- a/src/aig/ssw/ssw.h +++ b/src/aig/ssw/ssw.h @@ -85,6 +85,7 @@ extern Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t /*=== sswPairs.c ===================================================*/ extern int Ssw_SecWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, Vec_Int_t * vIds2, Ssw_Pars_t * pPars ); extern int Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars ); +extern int Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars ); #ifdef __cplusplus } diff --git a/src/aig/ssw/sswPairs.c b/src/aig/ssw/sswPairs.c index 92d3d91d..a11bdf98 100644 --- a/src/aig/ssw/sswPairs.c +++ b/src/aig/ssw/sswPairs.c @@ -430,6 +430,39 @@ int Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars ) return RetValue; } +/**Function************************************************************* + + Synopsis [Runs inductive SEC for the miter of two AIGs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars ) +{ + Aig_Man_t * pAigRes; + int RetValue, clk = clock(); + // try the new AIGs +// printf( "Performing general verification without node pairs.\n" ); + pAigRes = Ssw_SignalCorrespondence( pMiter, pPars ); + // report the results + RetValue = Ssw_MiterStatus( pAigRes, 1 ); + if ( RetValue == 1 ) + printf( "Verification successful. " ); + else if ( RetValue == 0 ) + printf( "Verification failed with a counter-example. " ); + else + printf( "Verification UNDECIDED. The number of remaining regs = %d (total = %d). ", + Aig_ManRegNum(pAigRes), Aig_ManRegNum(pMiter) ); + PRT( "Time", clock() - clk ); + // cleanup + Aig_ManStop( pAigRes ); + return RetValue; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |