diff options
Diffstat (limited to 'src/sat')
| -rw-r--r-- | src/sat/bmc/bmc.h | 1 | ||||
| -rw-r--r-- | src/sat/bmc/bmcCexCare.c | 54 |
2 files changed, 55 insertions, 0 deletions
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index b0a9210d..19a4679d 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -161,6 +161,7 @@ extern int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * /*=== bmcBmcAnd.c ==========================================================*/ extern int Gia_ManBmcPerform( Gia_Man_t * p, Bmc_AndPar_t * pPars ); /*=== bmcCexCare.c ==========================================================*/ +extern Abc_Cex_t * Bmc_CexCareExtendToObjects( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare ); extern Abc_Cex_t * Bmc_CexCareMinimize( Aig_Man_t * p, Abc_Cex_t * pCex, int fCheck, int fVerbose ); extern void Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose ); /*=== bmcCexCut.c ==========================================================*/ diff --git a/src/sat/bmc/bmcCexCare.c b/src/sat/bmc/bmcCexCare.c index addb89fd..21fea429 100644 --- a/src/sat/bmc/bmcCexCare.c +++ b/src/sat/bmc/bmcCexCare.c @@ -34,6 +34,60 @@ ABC_NAMESPACE_IMPL_START /**Function************************************************************* + Synopsis [Takes CEX and its care-set. Returns care-set of all objects.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Cex_t * Bmc_CexCareExtendToObjects( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare ) +{ + Abc_Cex_t * pNew; + Gia_Obj_t * pObj; + int i, k; + assert( pCex->nPis == pCexCare->nPis ); + assert( pCex->nRegs == pCexCare->nRegs ); + assert( pCex->nBits == pCexCare->nBits ); + // start the counter-example + pNew = Abc_CexAlloc( pCex->nRegs, Gia_ManObjNum(p), pCex->iFrame + 1 ); + pNew->iFrame = pCex->iFrame; + pNew->iPo = pCex->iPo; + // initialize terminary simulation + Gia_ObjTerSimSet0( Gia_ManConst0(p) ); + Gia_ManForEachRi( p, pObj, k ) + Gia_ObjTerSimSet0( pObj ); + for ( i = 0; i <= pCex->iFrame; i++ ) + { + Gia_ManForEachPi( p, pObj, k ) + { + if ( !Abc_InfoHasBit( pCexCare->pData, pCexCare->nRegs + i * pCexCare->nPis + k ) ) + Gia_ObjTerSimSetX( pObj ); + else if ( Abc_InfoHasBit( pCex->pData, pCex->nRegs + i * pCex->nPis + k ) ) + Gia_ObjTerSimSet1( pObj ); + else + Gia_ObjTerSimSet0( pObj ); + } + Gia_ManForEachRo( p, pObj, k ) + Gia_ObjTerSimRo( p, pObj ); + Gia_ManForEachAnd( p, pObj, k ) + Gia_ObjTerSimAnd( pObj ); + Gia_ManForEachCo( p, pObj, k ) + Gia_ObjTerSimCo( pObj ); + // add cares to the exdended counter-example + Gia_ManForEachObj( p, pObj, k ) + if ( !Gia_ObjTerSimGetX(pObj) ) + Abc_InfoSetBit( pNew->pData, pNew->nRegs + pNew->nPis * i + k ); + } + pObj = Gia_ManPo( p, pCex->iPo ); + assert( Gia_ObjTerSimGet1(pObj) ); + return pNew; +} + +/**Function************************************************************* + Synopsis [Backward propagation.] Description [] |