| /**CFile**************************************************************** |
| |
| FileName [bmcCexCut.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [SAT-based bounded model checking.] |
| |
| Synopsis [Derives characterization of bad states.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - June 20, 2005.] |
| |
| Revision [$Id: bmcCexCut.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "bmc.h" |
| #include "aig/gia/giaAig.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [Generate justifying assignments.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Bmc_GiaGenerateJust_rec( Gia_Man_t * p, int iFrame, int iObj, Vec_Bit_t * vValues, Vec_Bit_t * vJustis ) |
| { |
| Gia_Obj_t * pObj; |
| int Shift = Gia_ManObjNum(p) * iFrame; |
| if ( iFrame < 0 ) |
| return 0; |
| assert( iFrame >= 0 ); |
| if ( Vec_BitEntry( vJustis, Shift + iObj ) ) |
| return 0; |
| Vec_BitWriteEntry( vJustis, Shift + iObj, 1 ); |
| pObj = Gia_ManObj( p, iObj ); |
| if ( Gia_ObjIsCo(pObj) ) |
| return Bmc_GiaGenerateJust_rec( p, iFrame, Gia_ObjFaninId0(pObj, iObj), vValues, vJustis ); |
| if ( Gia_ObjIsCi(pObj) ) |
| return Bmc_GiaGenerateJust_rec( p, iFrame-1, Gia_ObjId(p, Gia_ObjRoToRi(p, pObj)), vValues, vJustis ); |
| assert( Gia_ObjIsAnd(pObj) ); |
| if ( Vec_BitEntry( vValues, Shift + iObj ) ) |
| { |
| Bmc_GiaGenerateJust_rec( p, iFrame, Gia_ObjFaninId0(pObj, iObj), vValues, vJustis ); |
| Bmc_GiaGenerateJust_rec( p, iFrame, Gia_ObjFaninId1(pObj, iObj), vValues, vJustis ); |
| } |
| else if ( Vec_BitEntry( vValues, Shift + Gia_ObjFaninId0(pObj, iObj) ) == Gia_ObjFaninC0(pObj) ) |
| Bmc_GiaGenerateJust_rec( p, iFrame, Gia_ObjFaninId0(pObj, iObj), vValues, vJustis ); |
| else if ( Vec_BitEntry( vValues, Shift + Gia_ObjFaninId1(pObj, iObj) ) == Gia_ObjFaninC1(pObj) ) |
| Bmc_GiaGenerateJust_rec( p, iFrame, Gia_ObjFaninId1(pObj, iObj), vValues, vJustis ); |
| else assert( 0 ); |
| return 0; |
| } |
| void Bmc_GiaGenerateJustNonRec( Gia_Man_t * p, int iFrame, Vec_Bit_t * vValues, Vec_Bit_t * vJustis ) |
| { |
| Gia_Obj_t * pObj; |
| int i, k, Shift = Gia_ManObjNum(p) * iFrame; |
| for ( i = iFrame; i >= 0; i--, Shift -= Gia_ManObjNum(p) ) |
| { |
| Gia_ManForEachObjReverse( p, pObj, k ) |
| { |
| if ( k == 0 || Gia_ObjIsPi(p, pObj) ) |
| continue; |
| if ( !Vec_BitEntry( vJustis, Shift + k ) ) |
| continue; |
| if ( Gia_ObjIsAnd(pObj) ) |
| { |
| if ( Vec_BitEntry( vValues, Shift + k ) ) |
| { |
| Vec_BitWriteEntry( vJustis, Shift + Gia_ObjFaninId0(pObj, k), 1 ); |
| Vec_BitWriteEntry( vJustis, Shift + Gia_ObjFaninId1(pObj, k), 1 ); |
| } |
| else if ( Vec_BitEntry( vValues, Shift + Gia_ObjFaninId0(pObj, k) ) == Gia_ObjFaninC0(pObj) ) |
| Vec_BitWriteEntry( vJustis, Shift + Gia_ObjFaninId0(pObj, k), 1 ); |
| else if ( Vec_BitEntry( vValues, Shift + Gia_ObjFaninId1(pObj, k) ) == Gia_ObjFaninC1(pObj) ) |
| Vec_BitWriteEntry( vJustis, Shift + Gia_ObjFaninId1(pObj, k), 1 ); |
| else assert( 0 ); |
| } |
| else if ( Gia_ObjIsCo(pObj) ) |
| Vec_BitWriteEntry( vJustis, Shift + Gia_ObjFaninId0(pObj, k), 1 ); |
| else if ( Gia_ObjIsCi(pObj) && i ) |
| Vec_BitWriteEntry( vJustis, Shift - Gia_ManObjNum(p) + Gia_ObjId(p, Gia_ObjRoToRi(p, pObj)), 1 ); |
| } |
| } |
| } |
| void Bmc_GiaGenerateJust( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Bit_t ** pvValues, Vec_Bit_t ** pvJustis ) |
| { |
| Vec_Bit_t * vValues = Vec_BitStart( Gia_ManObjNum(p) * (pCex->iFrame + 1) ); |
| Vec_Bit_t * vJustis = Vec_BitStart( Gia_ManObjNum(p) * (pCex->iFrame + 1) ); |
| Gia_Obj_t * pObj; |
| int i, k, iBit = 0, fCompl0, fCompl1, fJusti0, fJusti1, Shift; |
| |
| Gia_ManCleanMark0(p); |
| Gia_ManCleanMark1(p); |
| Gia_ManForEachRi( p, pObj, k ) |
| pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++); |
| for ( Shift = i = 0; i <= pCex->iFrame; i++, Shift += Gia_ManObjNum(p) ) |
| { |
| Gia_ManForEachObj( p, pObj, k ) |
| { |
| if ( Gia_ObjIsAnd(pObj) ) |
| { |
| fCompl0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); |
| fCompl1 = Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj); |
| fJusti0 = Gia_ObjFanin0(pObj)->fMark1; |
| fJusti1 = Gia_ObjFanin1(pObj)->fMark1; |
| pObj->fMark0 = fCompl0 & fCompl1; |
| if ( pObj->fMark0 ) |
| pObj->fMark1 = fJusti0 & fJusti1; |
| else if ( !fCompl0 && !fCompl1 ) |
| pObj->fMark1 = fJusti0 | fJusti1; |
| else if ( !fCompl0 ) |
| pObj->fMark1 = fJusti0; |
| else if ( !fCompl1 ) |
| pObj->fMark1 = fJusti1; |
| else assert( 0 ); |
| } |
| else if ( Gia_ObjIsCi(pObj) ) |
| { |
| if ( Gia_ObjIsPi(p, pObj) ) |
| { |
| pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++); |
| pObj->fMark1 = 1; |
| } |
| else |
| { |
| pObj->fMark0 = Gia_ObjRoToRi(p, pObj)->fMark0; |
| pObj->fMark1 = Gia_ObjRoToRi(p, pObj)->fMark1; |
| } |
| } |
| else if ( Gia_ObjIsCo(pObj) ) |
| { |
| pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); |
| pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1; |
| } |
| else if ( Gia_ObjIsConst0(pObj) ) |
| pObj->fMark1 = 1; |
| else assert( 0 ); |
| if ( pObj->fMark0 ) |
| Vec_BitWriteEntry( vValues, Shift + k, 1 ); |
| if ( pObj->fMark1 ) |
| Vec_BitWriteEntry( vJustis, Shift + k, 1 ); |
| } |
| } |
| assert( iBit == pCex->nBits ); |
| Gia_ManCleanMark0(p); |
| Gia_ManCleanMark1(p); |
| // perform backward traversal to mark just nodes |
| pObj = Gia_ManPo( p, pCex->iPo ); |
| assert( Vec_BitEntry(vJustis, Gia_ManObjNum(p) * pCex->iFrame + Gia_ObjId(p, pObj)) == 0 ); |
| // Bmc_GiaGenerateJust_rec( p, pCex->iFrame, Gia_ObjId(p, pObj), vValues, vJustis ); |
| Vec_BitWriteEntry(vJustis, Gia_ManObjNum(p) * pCex->iFrame + Gia_ObjId(p, pObj), 1); |
| Bmc_GiaGenerateJustNonRec( p, pCex->iFrame, vValues, vJustis ); |
| assert( Vec_BitEntry(vJustis, Gia_ManObjNum(p) * pCex->iFrame + Gia_ObjId(p, pObj)) == 1 ); |
| |
| // return the result |
| *pvValues = vValues; |
| *pvJustis = vJustis; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Gia_Man_t * Bmc_GiaGenerateGiaOne( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Bit_t ** pvInits, int iFrBeg, int iFrEnd ) |
| { |
| Vec_Bit_t * vValues; |
| Vec_Bit_t * vJustis; |
| Gia_Man_t * pNew; |
| Gia_Obj_t * pObj; |
| int k, Cube = 1, Counter = 0; |
| Bmc_GiaGenerateJust( p, pCex, &vValues, &vJustis ); |
| // collect flop values in frame iFrBeg |
| *pvInits = Vec_BitStart( Gia_ManRegNum(p) ); |
| Gia_ManForEachRo( p, pObj, k ) |
| if ( Vec_BitEntry(vValues, Gia_ManObjNum(p) * iFrBeg + Gia_ObjId(p, pObj)) ) |
| Vec_BitWriteEntry( *pvInits, k, 1 ); |
| // create GIA with justified values in iFrEnd |
| pNew = Gia_ManStart( 2 * Gia_ManRegNum(p) + 2 ); |
| pNew->pName = Abc_UtilStrsav( p->pName ); |
| Gia_ManForEachRo( p, pObj, k ) |
| { |
| int Literal = Gia_ManAppendCi(pNew); |
| if ( !Vec_BitEntry(vJustis, Gia_ManObjNum(p) * iFrEnd + Gia_ObjId(p, pObj)) ) |
| continue; |
| if ( Vec_BitEntry(vValues, Gia_ManObjNum(p) * iFrEnd + Gia_ObjId(p, pObj)) ) |
| Cube = Gia_ManAppendAnd( pNew, Cube, Literal ); |
| else |
| Cube = Gia_ManAppendAnd( pNew, Cube, Abc_LitNot(Literal) ); |
| Counter++; |
| } |
| // printf( "Only %d flops (out of %d) belong to the care set.\n", Counter, Gia_ManRegNum(p) ); |
| Gia_ManAppendCo( pNew, Cube ); |
| Vec_BitFree( vValues ); |
| Vec_BitFree( vJustis ); |
| return pNew; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Generates all frames from G to the last one.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Gia_Man_t * Bmc_GiaGenerateGiaAllFrames( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Bit_t ** pvInits, int iFrBeg, int iFrEnd ) |
| { |
| Vec_Bit_t * vInitEnd; |
| Gia_Man_t * pNew, * pTemp; |
| Gia_Obj_t * pObj, * pObjRo, * pObjRi; |
| int f, i, k, iBitOld, iBit = 0, fCompl0, fCompl1; |
| |
| // skip trough the first iFrEnd frames |
| Gia_ManCleanMark0(p); |
| Gia_ManForEachRo( p, pObj, k ) |
| pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++); |
| *pvInits = Vec_BitStart( Gia_ManRegNum(p) ); |
| for ( i = 0; i < iFrEnd; i++ ) |
| { |
| // remember values in frame iFrBeg |
| if ( i == iFrBeg ) |
| Gia_ManForEachRo( p, pObjRo, k ) |
| if ( pObjRo->fMark0 ) |
| Vec_BitWriteEntry( *pvInits, k, 1 ); |
| // simulate other values |
| 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)); |
| Gia_ManForEachCo( p, pObj, k ) |
| pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); |
| Gia_ManForEachRiRo( p, pObjRi, pObjRo, k ) |
| pObjRo->fMark0 = pObjRi->fMark0; |
| } |
| assert( i == iFrEnd ); |
| vInitEnd = Vec_BitStart( Gia_ManRegNum(p) ); |
| Gia_ManForEachRo( p, pObjRo, k ) |
| if ( pObjRo->fMark0 ) |
| Vec_BitWriteEntry( vInitEnd, k, 1 ); |
| |
| // create new AIG manager |
| pNew = Gia_ManStart( 10000 ); |
| pNew->pName = Abc_UtilStrsav( p->pName ); |
| Gia_ManForEachRo( p, pObjRo, k ) |
| Gia_ManAppendCi(pNew); |
| Gia_ManHashStart( pNew ); |
| |
| Gia_ManConst0(p)->Value = 1; |
| Gia_ManForEachPi( p, pObj, k ) |
| pObj->Value = 1; |
| |
| iBitOld = iBit; |
| for ( f = iFrEnd; f <= pCex->iFrame; f++ ) |
| { |
| // set up correct init state |
| Gia_ManForEachRo( p, pObjRo, k ) |
| pObjRo->fMark0 = Vec_BitEntry( vInitEnd, k ); |
| // simulate it for a few frames |
| iBit = iBitOld; |
| for ( i = iFrEnd; i < f; 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)); |
| Gia_ManForEachCo( p, pObj, k ) |
| pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); |
| Gia_ManForEachRiRo( p, pObjRi, pObjRo, k ) |
| pObjRo->fMark0 = pObjRi->fMark0; |
| } |
| // start creating values |
| Gia_ManForEachRo( p, pObjRo, k ) |
| pObjRo->Value = Abc_LitNotCond( Gia_Obj2Lit(pNew, Gia_ManPi(pNew, k)), !pObjRo->fMark0 ); |
| for ( i = f; i <= pCex->iFrame; i++ ) |
| { |
| Gia_ManForEachPi( p, pObj, k ) |
| pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++); |
| Gia_ManForEachAnd( p, pObj, k ) |
| { |
| 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( 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 ( !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 ) |
| { |
| pObjRo->fMark0 = pObjRi->fMark0; |
| pObjRo->Value = pObjRi->Value; |
| } |
| } |
| assert( iBit == pCex->nBits ); |
| // create PO |
| Gia_ManAppendCo( pNew, Gia_ManPo(p, pCex->iPo)->Value ); |
| } |
| Gia_ManHashStop( pNew ); |
| Vec_BitFree( vInitEnd ); |
| |
| // cleanup |
| pNew = Gia_ManCleanup( pTemp = pNew ); |
| Gia_ManStop( pTemp ); |
| return pNew; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Generates one frame.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Gia_Man_t * Bmc_GiaGenerateGiaAllOne( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Bit_t ** pvInits, int iFrBeg, int iFrEnd ) |
| { |
| Gia_Man_t * pNew, * pTemp; |
| Gia_Obj_t * pObj, * pObjRo, * pObjRi; |
| int i, k, iBit = 0, fCompl0, fCompl1; |
| |
| // skip trough the first iFrEnd frames |
| Gia_ManCleanMark0(p); |
| Gia_ManForEachRo( p, pObj, k ) |
| pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++); |
| *pvInits = Vec_BitStart( Gia_ManRegNum(p) ); |
| for ( i = 0; i < iFrEnd; i++ ) |
| { |
| // remember values in frame iFrBeg |
| if ( i == iFrBeg ) |
| Gia_ManForEachRo( p, pObjRo, k ) |
| if ( pObjRo->fMark0 ) |
| Vec_BitWriteEntry( *pvInits, k, 1 ); |
| // simulate other values |
| 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)); |
| Gia_ManForEachCo( p, pObj, k ) |
| pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); |
| Gia_ManForEachRiRo( p, pObjRi, pObjRo, k ) |
| pObjRo->fMark0 = pObjRi->fMark0; |
| } |
| assert( i == iFrEnd ); |
| |
| // 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, 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 ) |
| { |
| 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( 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 ( !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 ) |
| { |
| pObjRo->fMark0 = pObjRi->fMark0; |
| pObjRo->Value = pObjRi->Value; |
| } |
| } |
| Gia_ManHashStop( pNew ); |
| assert( iBit == pCex->nBits ); |
| |
| // create PO |
| Gia_ManAppendCo( pNew, Gia_ManPo(p, pCex->iPo)->Value ); |
| // cleanup |
| pNew = Gia_ManCleanup( pTemp = pNew ); |
| Gia_ManStop( pTemp ); |
| return pNew; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Generate GIA for target bad states.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fUseOne, int fAllFrames, int fVerbose ) |
| { |
| Gia_Man_t * pNew, * pTemp; |
| Vec_Bit_t * vInitNew; |
| |
| if ( iFrBeg < 0 ) |
| { printf( "Starting frame is less than 0.\n" ); return NULL; } |
| if ( iFrEnd < 0 ) |
| { printf( "Stopping frame is less than 0.\n" ); return NULL; } |
| if ( iFrBeg > pCex->iFrame ) |
| { 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 ) |
| { 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 ); |
| assert( iFrBeg < iFrEnd ); |
| |
| if ( fUseOne ) |
| pNew = Bmc_GiaGenerateGiaOne( p, pCex, &vInitNew, iFrBeg, iFrEnd ); |
| else if ( fAllFrames ) |
| pNew = Bmc_GiaGenerateGiaAllFrames( p, pCex, &vInitNew, iFrBeg, iFrEnd ); |
| else |
| pNew = Bmc_GiaGenerateGiaAllOne( p, pCex, &vInitNew, iFrBeg, iFrEnd ); |
| |
| if ( !fCombOnly ) |
| { |
| // create new GIA |
| pNew = Gia_ManDupWithNewPo( p, pTemp = pNew ); |
| Gia_ManStop( pTemp ); |
| |
| // 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 fCombOnly, int fUseOne, int fAllFrames, 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, fCombOnly, fUseOne, fAllFrames, fVerbose ); |
| Gia_ManStop( pGia ); |
| pAig = Gia_ManToAigSimple( pRes ); |
| Gia_ManStop( pRes ); |
| return pAig; |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
