From be29f37baaa4eaef52829bc48593d12c8c81e8ba Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 14 Nov 2012 18:20:35 -0800 Subject: Added command 'cexcut' and 'cexmerge'. --- src/sat/bmc/bmc.h | 1 + src/sat/bmc/bmcCexCut.c | 67 +++++++++++++++++++++++++++++++++++++------------ 2 files changed, 52 insertions(+), 16 deletions(-) (limited to 'src/sat/bmc') diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index e1841bbc..5d789dcb 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -76,6 +76,7 @@ extern void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p ); extern int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ); /*=== bmcCexCut.c ==========================================================*/ extern Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fVerbose ); +extern Aig_Man_t * Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fVerbose ); /*=== bmcCexMin.c ==========================================================*/ extern Abc_Cex_t * Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pCex ); diff --git a/src/sat/bmc/bmcCexCut.c b/src/sat/bmc/bmcCexCut.c index 96d46fb3..bbb1bc73 100644 --- a/src/sat/bmc/bmcCexCut.c +++ b/src/sat/bmc/bmcCexCut.c @@ -6,7 +6,7 @@ PackageName [SAT-based bounded model checking.] - Synopsis [] + Synopsis [Derives characterization of bad states.] Author [Alan Mishchenko] @@ -19,6 +19,7 @@ ***********************************************************************/ #include "bmc.h" +#include "aig/gia/giaAig.h" ABC_NAMESPACE_IMPL_START @@ -47,7 +48,7 @@ Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, in Gia_Man_t * pNew, * pTemp; Gia_Obj_t * pObj, * pObjRo, * pObjRi; Vec_Bit_t * vInitNew; - int i, k, iBit = 0; + int i, k, iBit = 0, fCompl0, fCompl1; if ( iFrBeg < 0 ) { printf( "Starting frame is less than 0.\n" ); return NULL; } @@ -57,7 +58,7 @@ Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, in { printf( "Starting frame is more than the last frame of CEX (%d).\n", pCex->iFrame ); return NULL; } if ( iFrEnd > pCex->iFrame ) { printf( "Stopping frame is more than the last frame of CEX (%d).\n", pCex->iFrame ); return NULL; } - if ( iFrBeg >= iFrEnd ) + if ( iFrBeg > iFrEnd ) { printf( "Starting frame (%d) should be less than stopping frame (%d).\n", iFrBeg, iFrEnd ); return NULL; } assert( iFrBeg >= 0 && iFrBeg <= pCex->iFrame ); assert( iFrEnd >= 0 && iFrEnd <= pCex->iFrame ); @@ -65,7 +66,7 @@ Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, in // skip trough the first iFrEnd frames Gia_ManCleanMark0(p); - Gia_ManForEachRo( p, pObj, i ) + Gia_ManForEachRo( p, pObj, k ) pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++); vInitNew = Vec_BitStart( Gia_ManRegNum(p) ); for ( i = 0; i < iFrEnd; i++ ) @@ -90,35 +91,39 @@ Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, in // create new AIG manager pNew = Gia_ManStart( 10000 ); + pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManConst0(p)->Value = 1; Gia_ManForEachPi( p, pObj, k ) pObj->Value = 1; - Gia_ManForEachRo( p, pObjRo, i ) - pObj->Value = Abc_LitNotCond( Gia_ManAppendCi(pNew), !pObjRo->fMark0 ); - Gia_ManHashStart( p ); + Gia_ManForEachRo( p, pObjRo, k ) + pObjRo->Value = Abc_LitNotCond( Gia_ManAppendCi(pNew), !pObjRo->fMark0 ); + Gia_ManHashStart( pNew ); for ( i = iFrEnd; i <= pCex->iFrame; i++ ) { Gia_ManForEachPi( p, pObj, k ) pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++); Gia_ManForEachAnd( p, pObj, k ) { - pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & - (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)); + fCompl0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); + fCompl1 = Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj); + pObj->fMark0 = fCompl0 & fCompl1; if ( pObj->fMark0 ) - pObj->Value = Gia_ManHashAnd( p, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value ); - else if ( !Gia_ObjFanin0(pObj)->fMark0 && !Gia_ObjFanin1(pObj)->fMark0 ) - pObj->Value = Gia_ManHashOr( p, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value ); - else if ( !Gia_ObjFanin0(pObj)->fMark0 ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value ); + else if ( !fCompl0 && !fCompl1 ) + pObj->Value = Gia_ManHashOr( pNew, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value ); + else if ( !fCompl0 ) pObj->Value = Gia_ObjFanin0(pObj)->Value; - else if ( !Gia_ObjFanin1(pObj)->fMark0 ) + else if ( !fCompl1 ) pObj->Value = Gia_ObjFanin1(pObj)->Value; else assert( 0 ); + assert( pObj->Value > 0 ); } Gia_ManForEachCo( p, pObj, k ) { pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); pObj->Value = Gia_ObjFanin0(pObj)->Value; - } + assert( pObj->Value > 0 ); + } if ( i == pCex->iFrame ) break; Gia_ManForEachRiRo( p, pObjRi, pObjRo, k ) @@ -127,7 +132,7 @@ Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, in pObjRo->Value = pObjRi->Value; } } - Gia_ManHashStop( p ); + Gia_ManHashStop( pNew ); assert( iBit == pCex->nBits ); // create PO @@ -143,10 +148,40 @@ Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, in // create new initial state pNew = Gia_ManDupFlip( pTemp = pNew, Vec_BitArray(vInitNew) ); Gia_ManStop( pTemp ); + Vec_BitFree( vInitNew ); return pNew; } +/**Function************************************************************* + + Synopsis [Generate AIG for target bad states.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fVerbose ) +{ + Aig_Man_t * pAig; + Gia_Man_t * pGia, * pRes; + pGia = Gia_ManFromAigSimple( p ); + if ( !Gia_ManVerifyCex( pGia, pCex, 0 ) ) + { + Abc_Print( 1, "Current CEX does not fail AIG \"%s\".\n", p->pName ); + Gia_ManStop( pGia ); + return NULL; + } + pRes = Bmc_GiaTargetStates( pGia, pCex, iFrBeg, iFrEnd, fVerbose ); + pAig = Gia_ManToAigSimple( pRes ); + Gia_ManStop( pGia ); + Gia_ManStop( pRes ); + return pAig; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3