From a0052e22b43ff9d0125ca8e71f96589226e44e42 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 15 Nov 2012 16:00:29 -0800 Subject: Added switch 'cexcut -m' to generate bad states for all frames after G. --- src/aig/gia/gia.h | 3 + src/aig/gia/giaDup.c | 6 +- src/base/abci/abc.c | 26 ++++++--- src/misc/util/utilCex.c | 4 +- src/sat/bmc/bmc.h | 4 +- src/sat/bmc/bmcCexCut.c | 145 +++++++++++++++++++++++++++++++++++++++++++++--- 6 files changed, 164 insertions(+), 24 deletions(-) diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index d261e433..9d361fe8 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -316,6 +316,9 @@ static inline void Gia_ObjSetValue( Gia_Obj_t * pObj, int i ) { static inline int Gia_ObjPhase( Gia_Obj_t * pObj ) { return pObj->fPhase; } static inline int Gia_ObjPhaseReal( Gia_Obj_t * pObj ) { return Gia_Regular(pObj)->fPhase ^ Gia_IsComplement(pObj); } +static inline int Gia_Obj2Lit( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Abc_Var2Lit(Gia_ObjId(p, Gia_Regular(pObj)), Gia_IsComplement(pObj)); } +static inline Gia_Obj_t * Gia_Lit2Obj( Gia_Man_t * p, int iLit ) { return Gia_NotCond(Gia_ManObj(p, Abc_Lit2Var(iLit)), Abc_LitIsCompl(iLit)); } + static inline int Gia_ManIdToCioId( Gia_Man_t * p, int Id ) { return Gia_ObjCioId( Gia_ManObj(p, Id) ); } static inline int Gia_ManCiIdToId( Gia_Man_t * p, int CiId ) { return Gia_ObjId( p, Gia_ManCi(p, CiId) ); } static inline int Gia_ManCoIdToId( Gia_Man_t * p, int CoId ) { return Gia_ObjId( p, Gia_ManCo(p, CoId) ); } diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index eddbd320..3b8980af 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -1233,7 +1233,7 @@ Gia_Man_t * Gia_ManDupWithNewPo( Gia_Man_t * p1, Gia_Man_t * p2 ) // there is no flops in p2 assert( Gia_ManRegNum(p2) == 0 ); // there is only one PO in p2 - assert( Gia_ManPoNum(p2) == 1 ); +// assert( Gia_ManPoNum(p2) == 1 ); // input count of p2 is equal to flop count of p1 assert( Gia_ManPiNum(p2) == Gia_ManRegNum(p1) ); @@ -1255,8 +1255,8 @@ Gia_Man_t * Gia_ManDupWithNewPo( Gia_Man_t * p1, Gia_Man_t * p2 ) Gia_ManForEachAnd( p2, pObj, i ) pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); // add property output - pObj = Gia_ManPo( p2, 0 ); - Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManForEachPo( p2, pObj, i ) + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); // add flop inputs Gia_ManForEachRi( p1, pObj, i ) Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index b490d3e3..89d1c6dd 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -22566,6 +22566,9 @@ int Abc_CommandCexLoad( Abc_Frame_t * pAbc, int argc, char ** argv ) } ABC_FREE( pAbc->pCex ); pAbc->pCex = Abc_CexDup( pAbc->pCex2, -1 ); + // update status + pAbc->nFrames = pAbc->pCex2->iFrame; + pAbc->Status = 0; return 0; usage: @@ -22590,13 +22593,14 @@ usage: int Abc_CommandCexCut( Abc_Frame_t * pAbc, int argc, char ** argv ) { int c; - int iFrStart = 0; - int iFrStop = ABC_INFINITY; - int fCombOnly = 0; - int fUseOne = 0; - int fVerbose = 0; + int iFrStart = 0; + int iFrStop = ABC_INFINITY; + int fCombOnly = 0; + int fUseOne = 0; + int fAllFrames = 0; + int fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "FGcnvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "FGcnmvh" ) ) != EOF ) { switch ( c ) { @@ -22628,6 +22632,9 @@ int Abc_CommandCexCut( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'n': fUseOne ^= 1; break; + case 'm': + fAllFrames ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -22662,7 +22669,7 @@ int Abc_CommandCexCut( Abc_Frame_t * pAbc, int argc, char ** argv ) extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan ); Abc_Ntk_t * pNtkNew; Aig_Man_t * pAig = Abc_NtkToDar( pAbc->pNtkCur, 0, 1 ); - Aig_Man_t * pAigNew = Bmc_AigTargetStates( pAig, pAbc->pCex, iFrStart, iFrStop, fCombOnly, fUseOne, fVerbose ); + Aig_Man_t * pAigNew = Bmc_AigTargetStates( pAig, pAbc->pCex, iFrStart, iFrStop, fCombOnly, fUseOne, fAllFrames, fVerbose ); Aig_ManStop( pAig ); if ( pAigNew == NULL ) { @@ -22687,12 +22694,13 @@ int Abc_CommandCexCut( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: cexcut [-FG num] [-cvh]\n" ); + Abc_Print( -2, "usage: cexcut [-FG num] [-cnmvh]\n" ); Abc_Print( -2, "\t creates logic for bad states using the current CEX\n" ); Abc_Print( -2, "\t-F num : 0-based number of the starting frame [default = %d]\n", iFrStart ); Abc_Print( -2, "\t-G num : 0-based number of the ending frame [default = %d]\n", iFrStop ); Abc_Print( -2, "\t-c : toggle outputting unate combinational circuit [default = %s]\n", fCombOnly? "yes": "no" ); Abc_Print( -2, "\t-n : toggle generating only one bad state [default = %s]\n", fUseOne? "yes": "no" ); + Abc_Print( -2, "\t-m : toggle generating bad states for all frames after G [default = %s]\n", fAllFrames? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; @@ -22764,7 +22772,7 @@ int Abc_CommandCexMerge( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( 1, "There is no saved cex.\n"); return 0; } - if ( iFrStop - iFrStart < pAbc->pCex->iFrame ) + if ( iFrStop - iFrStart + pAbc->pCex->iPo < pAbc->pCex->iFrame ) { Abc_Print( 1, "Current CEX does not allow to shorten the saved CEX.\n"); return 0; diff --git a/src/misc/util/utilCex.c b/src/misc/util/utilCex.c index edb246b9..01afd489 100644 --- a/src/misc/util/utilCex.c +++ b/src/misc/util/utilCex.c @@ -202,9 +202,9 @@ Abc_Cex_t * Abc_CexMerge( Abc_Cex_t * pCex, Abc_Cex_t * pPart, int iFrBeg, int i assert( iFrBeg <= iFrEnd ); assert( pCex->nPis == pPart->nPis ); - assert( iFrEnd - iFrBeg >= pPart->iFrame ); + assert( iFrEnd - iFrBeg + pPart->iPo >= pPart->iFrame ); - nFramesGain = (iFrEnd - iFrBeg) - pPart->iFrame; + nFramesGain = iFrEnd - iFrBeg + pPart->iPo - pPart->iFrame; pNew = Abc_CexAlloc( pCex->nRegs, pCex->nPis, pCex->iFrame + 1 - nFramesGain ); pNew->iPo = pCex->iPo; pNew->iFrame = pCex->iFrame - nFramesGain; diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index 0e37656e..7cc5637b 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -75,8 +75,8 @@ extern int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFra 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 fCombOnly, int fGenAll, int fVerbose ); -extern Aig_Man_t * Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fGenAll, int fVerbose ); +extern Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fGenAll, int fAllFrames, int fVerbose ); +extern Aig_Man_t * Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fGenAll, int fAllFrames, 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 7eafe492..3ce63459 100644 --- a/src/sat/bmc/bmcCexCut.c +++ b/src/sat/bmc/bmcCexCut.c @@ -225,7 +225,135 @@ Gia_Man_t * Bmc_GiaGenerateGiaOne( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Bit_t ** /**Function************************************************************* - Synopsis [] + 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 [] @@ -234,7 +362,7 @@ Gia_Man_t * Bmc_GiaGenerateGiaOne( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Bit_t ** SeeAlso [] ***********************************************************************/ -Gia_Man_t * Bmc_GiaGenerateGiaAll( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Bit_t ** pvInits, int iFrBeg, int iFrEnd ) +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; @@ -319,7 +447,6 @@ Gia_Man_t * Bmc_GiaGenerateGiaAll( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Bit_t ** return pNew; } - /**Function************************************************************* Synopsis [Generate GIA for target bad states.] @@ -331,7 +458,7 @@ Gia_Man_t * Bmc_GiaGenerateGiaAll( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Bit_t ** SeeAlso [] ***********************************************************************/ -Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fUseOne, int fVerbose ) +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; @@ -352,8 +479,10 @@ Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, in if ( fUseOne ) pNew = Bmc_GiaGenerateGiaOne( p, pCex, &vInitNew, iFrBeg, iFrEnd ); - else - pNew = Bmc_GiaGenerateGiaAll( 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 ) { @@ -381,7 +510,7 @@ Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, in SeeAlso [] ***********************************************************************/ -Aig_Man_t * Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fUseOne, int fVerbose ) +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; @@ -392,7 +521,7 @@ Aig_Man_t * Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, in Gia_ManStop( pGia ); return NULL; } - pRes = Bmc_GiaTargetStates( pGia, pCex, iFrBeg, iFrEnd, fCombOnly, fUseOne, fVerbose ); + pRes = Bmc_GiaTargetStates( pGia, pCex, iFrBeg, iFrEnd, fCombOnly, fUseOne, fAllFrames, fVerbose ); Gia_ManStop( pGia ); pAig = Gia_ManToAigSimple( pRes ); Gia_ManStop( pRes ); -- cgit v1.2.3