diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2014-02-11 11:58:25 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2014-02-11 11:58:25 -0800 |
| commit | 0ff592524818c895517db80a0795b5faea6cf8b5 (patch) | |
| tree | d399d23387ee38e0940128b9ee67da0d07598e68 /src/sat | |
| parent | 367b02aecd32fe66729e3b8b75bba669ed828900 (diff) | |
| download | abc-0ff592524818c895517db80a0795b5faea6cf8b5.tar.gz abc-0ff592524818c895517db80a0795b5faea6cf8b5.tar.bz2 abc-0ff592524818c895517db80a0795b5faea6cf8b5.zip | |
Experiments with inductive don't-cares.
Diffstat (limited to 'src/sat')
| -rw-r--r-- | src/sat/bmc/bmc.h | 2 | ||||
| -rw-r--r-- | src/sat/bmc/bmcICheck.c | 12 |
2 files changed, 11 insertions, 3 deletions
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index 2f7af2ba..b3e2d8e8 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -132,7 +132,7 @@ extern Aig_Man_t * Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, i extern Abc_Cex_t * Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pCex ); /*=== bmcICheck.c ==========================================================*/ extern void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fEmpty, int fVerbose ); -extern void Bmc_PerformISearch( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fReverse, int fDump, int fVerbose ); +extern Vec_Int_t * Bmc_PerformISearch( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fReverse, int fDump, int fVerbose ); /*=== bmcUnroll.c ==========================================================*/ extern Unr_Man_t * Unr_ManUnrollStart( Gia_Man_t * pGia, int fVerbose ); extern Gia_Man_t * Unr_ManUnrollFrame( Unr_Man_t * p, int f ); diff --git a/src/sat/bmc/bmcICheck.c b/src/sat/bmc/bmcICheck.c index c70ed9b3..f404def5 100644 --- a/src/sat/bmc/bmcICheck.c +++ b/src/sat/bmc/bmcICheck.c @@ -397,9 +397,9 @@ void Bmc_PerformISearchOne( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fRe Gia_ManStop( pMiter ); // Vec_IntFree( vLits ); } -void Bmc_PerformISearch( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fReverse, int fDump, int fVerbose ) +Vec_Int_t * Bmc_PerformISearch( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fReverse, int fDump, int fVerbose ) { - Vec_Int_t * vLits; + Vec_Int_t * vLits, * vFlops; int i, f; printf( "Solving M-inductiveness for design %s with %d AND nodes and %d flip-flops:\n", Gia_ManName(p), Gia_ManAndNum(p), Gia_ManRegNum(p) ); @@ -426,7 +426,15 @@ void Bmc_PerformISearch( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fRever printf( "%d ", i ); printf( "\n" ); } + // save flop indexes + vFlops = Vec_IntAlloc( Gia_ManRegNum(p) ); + for ( i = 0; i < Gia_ManRegNum(p); i++ ) + if ( !Abc_LitIsCompl(Vec_IntEntry(vLits, i)) ) + Vec_IntPush( vFlops, 1 ); + else + Vec_IntPush( vFlops, 0 ); Vec_IntFree( vLits ); + return vFlops; } //////////////////////////////////////////////////////////////////////// |