From 05b61206e4689a5d4bfb4370e8a8217736f4231c Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 18 Apr 2011 23:27:51 -0700 Subject: Adding constant correspondence. --- src/aig/cec/cec.h | 2 ++ src/aig/cec/cecClass.c | 11 +++++++++++ src/aig/cec/cecCore.c | 4 +++- src/aig/cec/cecCorr.c | 1 + 4 files changed, 17 insertions(+), 1 deletion(-) (limited to 'src/aig/cec') diff --git a/src/aig/cec/cec.h b/src/aig/cec/cec.h index e4547f5e..9e2237d7 100644 --- a/src/aig/cec/cec.h +++ b/src/aig/cec/cec.h @@ -68,6 +68,7 @@ struct Cec_ParSim_t_ // int fFirstStop; // stop on the first sat output int fSeqSimulate; // performs sequential simulation int fLatchCorr; // consider only latch outputs + int fConstCorr; // consider only constants int fVeryVerbose; // verbose stats int fVerbose; // verbose stats }; @@ -137,6 +138,7 @@ struct Cec_ParCor_t_ int nLevelMax; // (scorr only) the max number of levels int nStepsMax; // (scorr only) the max number of induction steps int fLatchCorr; // consider only latch outputs + int fConstCorr; // consider only constants int fUseRings; // use rings int fMakeChoices; // use equilvaences as choices int fUseCSat; // use circuit-based solver diff --git a/src/aig/cec/cecClass.c b/src/aig/cec/cecClass.c index 95414851..b6118038 100644 --- a/src/aig/cec/cecClass.c +++ b/src/aig/cec/cecClass.c @@ -759,6 +759,17 @@ references: Cec_ManSimSimDeref( p, Ent ); } } + + if ( p->pPars->fConstCorr ) + { + Vec_IntForEachEntry( p->vRefinedC, i, k ) + { + Gia_ObjSetRepr( p->pAig, i, GIA_VOID ); + Cec_ManSimSimDeref( p, i ); + } + Vec_IntClear( p->vRefinedC ); + } + if ( Vec_IntSize(p->vRefinedC) > 0 ) Cec_ManSimProcessRefined( p, p->vRefinedC ); assert( vInfoCis == NULL || iCiId == Gia_ManCiNum(p->pAig) ); diff --git a/src/aig/cec/cecCore.c b/src/aig/cec/cecCore.c index 369c4a40..bf41304b 100644 --- a/src/aig/cec/cecCore.c +++ b/src/aig/cec/cecCore.c @@ -78,6 +78,7 @@ void Cec_ManSimSetDefaultParams( Cec_ParSim_t * p ) p->fCheckMiter = 0; // the circuit is the miter // p->fFirstStop = 0; // stop on the first sat output p->fDualOut = 0; // miter with separate outputs + p->fConstCorr = 0; // consider only constants p->fSeqSimulate = 0; // performs sequential simulation p->fVeryVerbose = 0; // verbose stats p->fVerbose = 0; // verbose stats @@ -187,6 +188,7 @@ void Cec_ManCorSetDefaultParams( Cec_ParCor_t * p ) p->nLevelMax = -1; // (scorr only) the max number of levels p->nStepsMax = -1; // (scorr only) the max number of induction steps p->fLatchCorr = 0; // consider only latch outputs + p->fConstCorr = 0; // consider only constants p->fUseRings = 1; // combine classes into rings p->fUseCSat = 1; // use circuit-based solver // p->fFirstStop = 0; // stop on the first sat output @@ -359,7 +361,7 @@ Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars ) pParsSim->nWords = pPars->nWords; pParsSim->nFrames = pPars->nRounds; pParsSim->fCheckMiter = pPars->fCheckMiter; - pParsSim->fDualOut = pPars->fDualOut; + pParsSim->fDualOut = pPars->fDualOut; pParsSim->fVerbose = pPars->fVerbose; pSim = Cec_ManSimStart( p->pAig, pParsSim ); // SAT solving diff --git a/src/aig/cec/cecCorr.c b/src/aig/cec/cecCorr.c index 565ca47e..59d091d8 100644 --- a/src/aig/cec/cecCorr.c +++ b/src/aig/cec/cecCorr.c @@ -859,6 +859,7 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) pParsSim->nFrames = pPars->nFrames; pParsSim->fVerbose = pPars->fVerbose; pParsSim->fLatchCorr = pPars->fLatchCorr; + pParsSim->fConstCorr = pPars->fConstCorr; pParsSim->fSeqSimulate = 1; // create equivalence classes of registers pSim = Cec_ManSimStart( pAig, pParsSim ); -- cgit v1.2.3