| /**CFile**************************************************************** |
| |
| FileName [bmcChain.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [SAT-based bounded model checking.] |
| |
| Synopsis [Implementation of chain BMC.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - June 20, 2005.] |
| |
| Revision [$Id: bmcChain.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "bmc.h" |
| #include "aig/gia/giaAig.h" |
| #include "sat/cnf/cnf.h" |
| #include "sat/bsat/satSolver.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [Find the first failure.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Abc_Cex_t * Bmc_ChainFailOneOutput( Gia_Man_t * p, int nFrameMax, int nConfMax, int fVerbose, int fVeryVerbose ) |
| { |
| int RetValue; |
| Abc_Cex_t * pCex = NULL; |
| Aig_Man_t * pAig = Gia_ManToAigSimple( p ); |
| Saig_ParBmc_t Pars, * pPars = &Pars; |
| Saig_ParBmcSetDefaultParams( pPars ); |
| pPars->nFramesMax = nFrameMax; |
| pPars->nConfLimit = nConfMax; |
| pPars->fVerbose = fVeryVerbose; |
| RetValue = Saig_ManBmcScalable( pAig, pPars ); |
| if ( RetValue == 0 ) // SAT |
| { |
| pCex = pAig->pSeqModel, pAig->pSeqModel = NULL; |
| if ( fVeryVerbose ) |
| Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d.\n", pCex->iPo, p->pName, pCex->iFrame ); |
| } |
| else if ( fVeryVerbose ) |
| Abc_Print( 1, "No output asserted in %d frames. Resource limit reached.\n", pPars->iFrame+2 ); |
| Aig_ManStop( pAig ); |
| return pCex; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Move GIA into the failing state.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Gia_Man_t * Gia_ManDupWithInit( Gia_Man_t * p ) |
| { |
| Gia_Man_t * pNew; |
| Gia_Obj_t * pObj; |
| int i; |
| pNew = Gia_ManStart( Gia_ManObjNum(p) ); |
| pNew->pName = Abc_UtilStrsav( p->pName ); |
| pNew->pSpec = Abc_UtilStrsav( p->pSpec ); |
| Gia_ManConst0(p)->Value = 0; |
| Gia_ManForEachObj1( p, pObj, i ) |
| { |
| if ( Gia_ObjIsAnd(pObj) ) |
| pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); |
| else if ( Gia_ObjIsCi(pObj) ) |
| { |
| pObj->Value = Gia_ManAppendCi( pNew ); |
| pObj->Value = Abc_LitNotCond( pObj->Value, pObj->fMark0 ); |
| } |
| else if ( Gia_ObjIsCo(pObj) ) |
| { |
| pObj->Value = Gia_ObjFanin0Copy(pObj); |
| pObj->Value = Abc_LitNotCond( pObj->Value, pObj->fMark0 ); |
| pObj->Value = Gia_ManAppendCo( pNew, pObj->Value ); |
| } |
| } |
| Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); |
| return pNew; |
| } |
| Gia_Man_t * Gia_ManVerifyCexAndMove( Gia_Man_t * pGia, Abc_Cex_t * p ) |
| { |
| Gia_Man_t * pNew; |
| Gia_Obj_t * pObj, * pObjRi, * pObjRo; |
| int RetValue, i, k, iBit = 0; |
| Gia_ManCleanMark0(pGia); |
| Gia_ManForEachRo( pGia, pObj, i ) |
| pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++); |
| for ( i = 0; i <= p->iFrame; i++ ) |
| { |
| Gia_ManForEachPi( pGia, pObj, k ) |
| pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++); |
| Gia_ManForEachAnd( pGia, pObj, k ) |
| pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & |
| (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)); |
| Gia_ManForEachCo( pGia, pObj, k ) |
| pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); |
| if ( i == p->iFrame ) |
| break; |
| Gia_ManForEachRiRo( pGia, pObjRi, pObjRo, k ) |
| pObjRo->fMark0 = pObjRi->fMark0; |
| } |
| assert( iBit == p->nBits ); |
| RetValue = Gia_ManPo(pGia, p->iPo)->fMark0; |
| assert( RetValue ); |
| // set PI/PO values to zero and transfer RO values to RI |
| Gia_ManForEachPi( pGia, pObj, k ) |
| pObj->fMark0 = 0; |
| Gia_ManForEachPo( pGia, pObj, k ) |
| pObj->fMark0 = 0; |
| Gia_ManForEachRiRo( pGia, pObjRi, pObjRo, k ) |
| pObjRi->fMark0 = pObjRo->fMark0; |
| // duplicate assuming CI/CO marks are set correctly |
| pNew = Gia_ManDupWithInit( pGia ); |
| Gia_ManCleanMark0(pGia); |
| return pNew; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Find what outputs fail in this state.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Gia_Man_t * Gia_ManDupPosAndPropagateInit( Gia_Man_t * p ) |
| { |
| Gia_Man_t * pNew, * pTemp; |
| Gia_Obj_t * pObj; int i; |
| pNew = Gia_ManStart( Gia_ManObjNum(p) ); |
| pNew->pName = Abc_UtilStrsav( p->pName ); |
| pNew->pSpec = Abc_UtilStrsav( p->pSpec ); |
| Gia_ManConst0(p)->Value = 0; |
| Gia_ManHashAlloc( pNew ); |
| Gia_ManForEachObj1( p, pObj, i ) |
| { |
| if ( Gia_ObjIsAnd(pObj) ) |
| pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); |
| else if ( Gia_ObjIsPi(p, pObj) ) |
| pObj->Value = Gia_ManAppendCi( pNew ); |
| else if ( Gia_ObjIsCi(pObj) ) |
| pObj->Value = 0; |
| else if ( Gia_ObjIsPo(p, pObj) ) |
| Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); |
| } |
| Gia_ManHashStop( pNew ); |
| assert( Gia_ManPiNum(p) == Gia_ManPiNum(pNew) ); |
| assert( Gia_ManPoNum(p) == Gia_ManPoNum(pNew) ); |
| pNew = Gia_ManCleanup( pTemp = pNew ); |
| Gia_ManStop( pTemp ); |
| return pNew; |
| } |
| sat_solver * Gia_ManDeriveSatSolver( Gia_Man_t * p, Vec_Int_t * vSatIds ) |
| { |
| sat_solver * pSat; |
| Aig_Man_t * pAig = Gia_ManToAigSimple( p ); |
| // Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 ); |
| Cnf_Dat_t * pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) ); |
| // save SAT vars for the primary inputs |
| if ( vSatIds ) |
| { |
| Aig_Obj_t * pObj; int i; |
| Vec_IntClear( vSatIds ); |
| Aig_ManForEachCi( pAig, pObj, i ) |
| Vec_IntPush( vSatIds, pCnf->pVarNums[ Aig_ObjId(pObj) ] ); |
| assert( Vec_IntSize(vSatIds) == Gia_ManPiNum(p) ); |
| } |
| Aig_ManStop( pAig ); |
| pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); |
| Cnf_DataFree( pCnf ); |
| assert( p->nRegs == 0 ); |
| return pSat; |
| } |
| Vec_Int_t * Bmc_ChainFindFailedOutputs( Gia_Man_t * p, Vec_Ptr_t * vCexes ) |
| { |
| Vec_Int_t * vOutputs; |
| Vec_Int_t * vSatIds; |
| Gia_Man_t * pInit; |
| Gia_Obj_t * pObj; |
| sat_solver * pSat; |
| int i, j, Lit, status = 0; |
| // derive output logic cones |
| pInit = Gia_ManDupPosAndPropagateInit( p ); |
| // derive SAT solver and test |
| vSatIds = Vec_IntAlloc( Gia_ManPiNum(p) ); |
| pSat = Gia_ManDeriveSatSolver( pInit, vSatIds ); |
| vOutputs = Vec_IntAlloc( 100 ); |
| Gia_ManForEachPo( pInit, pObj, i ) |
| { |
| if ( Gia_ObjFaninLit0p(pInit, pObj) == 0 ) |
| continue; |
| Lit = Abc_Var2Lit( i+1, 0 ); |
| status = sat_solver_solve( pSat, &Lit, &Lit + 1, 0, 0, 0, 0 ); |
| if ( status == l_True ) |
| { |
| // save the index of solved output |
| Vec_IntPush( vOutputs, i ); |
| // create CEX for this output |
| if ( vCexes ) |
| { |
| Abc_Cex_t * pCex = Abc_CexAlloc( Gia_ManRegNum(p), Gia_ManPiNum(p), 1 ); |
| pCex->iFrame = 0; |
| pCex->iPo = i; |
| for ( j = 0; j < Gia_ManPiNum(p); j++ ) |
| if ( sat_solver_var_value( pSat, Vec_IntEntry(vSatIds, j) ) ) |
| Abc_InfoSetBit( pCex->pData, Gia_ManRegNum(p) + j ); |
| Vec_PtrPush( vCexes, pCex ); |
| } |
| } |
| } |
| Gia_ManStop( pInit ); |
| sat_solver_delete( pSat ); |
| Vec_IntFree( vSatIds ); |
| return vOutputs; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Cleanup AIG by removing COs replacing failed out by const0.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline void Gia_ObjMakePoConst0( Gia_Man_t * p, Gia_Obj_t * pObj ) |
| { |
| assert( Gia_ObjIsCo(pObj) ); |
| pObj->iDiff0 = Gia_ObjId( p, pObj ); |
| pObj->fCompl0 = 0; |
| } |
| int Gia_ManCountNonConst0( Gia_Man_t * p ) |
| { |
| Gia_Obj_t * pObj; |
| int i, Count = 0; |
| Gia_ManForEachPo( p, pObj, i ) |
| Count += (Gia_ObjFaninLit0p(p, pObj) != 0); |
| return Count; |
| } |
| Gia_Man_t * Bmc_ChainCleanup( Gia_Man_t * p, Vec_Int_t * vOutputs ) |
| { |
| int i, iOut; |
| Vec_IntForEachEntry( vOutputs, iOut, i ) |
| { |
| Gia_Obj_t * pObj = Gia_ManPo( p, iOut ); |
| assert( Gia_ObjFaninLit0p(p, pObj) != 0 ); |
| Gia_ObjMakePoConst0( p, pObj ); |
| assert( Gia_ObjFaninLit0p(p, pObj) == 0 ); |
| } |
| return Gia_ManCleanup( p ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Bmc_ChainTest( Gia_Man_t * p, int nFrameMax, int nConfMax, int fVerbose, int fVeryVerbose, Vec_Ptr_t ** pvCexes ) |
| { |
| int Iter, IterMax = 10000; |
| Gia_Man_t * pTemp, * pNew = Gia_ManDup(p); |
| Abc_Cex_t * pCex = NULL; |
| Vec_Int_t * vOutputs; |
| abctime clk2, clk = Abc_Clock(); |
| abctime clkBmc = 0; |
| abctime clkMov = 0; |
| abctime clkSat = 0; |
| abctime clkCln = 0; |
| abctime clkSwp = 0; |
| int DepthTotal = 0; |
| if ( pvCexes ) |
| *pvCexes = Vec_PtrAlloc( 1000 ); |
| for ( Iter = 0; Iter < IterMax; Iter++ ) |
| { |
| if ( Gia_ManPoNum(pNew) == 0 ) |
| { |
| if ( fVerbose ) |
| printf( "Finished all POs.\n" ); |
| break; |
| } |
| // run BMC till the first failure |
| clk2 = Abc_Clock(); |
| pCex = Bmc_ChainFailOneOutput( pNew, nFrameMax, nConfMax, fVerbose, fVeryVerbose ); |
| clkBmc += Abc_Clock() - clk2; |
| if ( pCex == NULL ) |
| { |
| if ( fVerbose ) |
| printf( "BMC could not detect a failed output in %d frames with %d conflicts.\n", nFrameMax, nConfMax ); |
| break; |
| } |
| assert( !Iter || pCex->iFrame > 0 ); |
| // move the AIG to the failure state |
| clk2 = Abc_Clock(); |
| pNew = Gia_ManVerifyCexAndMove( pTemp = pNew, pCex ); |
| Gia_ManStop( pTemp ); |
| DepthTotal += pCex->iFrame; |
| clkMov += Abc_Clock() - clk2; |
| // find outputs that fail in this state |
| clk2 = Abc_Clock(); |
| vOutputs = Bmc_ChainFindFailedOutputs( pNew, pvCexes ? *pvCexes : NULL ); |
| assert( Vec_IntFind(vOutputs, pCex->iPo) >= 0 ); |
| // save the counter-example |
| if ( pvCexes ) |
| Vec_PtrPush( *pvCexes, pCex ); |
| else |
| Abc_CexFree( pCex ); |
| clkSat += Abc_Clock() - clk2; |
| // remove them from the AIG |
| clk2 = Abc_Clock(); |
| pNew = Bmc_ChainCleanup( pTemp = pNew, vOutputs ); |
| Gia_ManStop( pTemp ); |
| clkCln += Abc_Clock() - clk2; |
| // perform sequential cleanup |
| clk2 = Abc_Clock(); |
| // pNew = Gia_ManSeqStructSweep( pTemp = pNew, 0, 1, 0 ); |
| // Gia_ManStop( pTemp ); |
| clkSwp += Abc_Clock() - clk2; |
| // printout |
| if ( fVerbose ) |
| { |
| int nNonConst = Gia_ManCountNonConst0(pNew); |
| printf( "Iter %4d : ", Iter+1 ); |
| printf( "Depth =%5d ", DepthTotal ); |
| printf( "FailPo =%5d ", Vec_IntSize(vOutputs) ); |
| printf( "UndecPo =%5d ", nNonConst ); |
| printf( "(%6.2f %%) ", 100.0 * nNonConst / Gia_ManPoNum(pNew) ); |
| printf( "AIG =%8d ", Gia_ManAndNum(pNew) ); |
| Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); |
| } |
| Vec_IntFree( vOutputs ); |
| } |
| printf( "Completed a CEX chain with %d segments, %d frames, and %d failed POs (out of %d). ", |
| Iter, DepthTotal, Gia_ManPoNum(pNew) - Gia_ManCountNonConst0(pNew), Gia_ManPoNum(pNew) ); |
| if ( fVerbose ) |
| { |
| Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); |
| Abc_PrintTimeP( 1, "BMC ", clkBmc, Abc_Clock() - clk ); |
| Abc_PrintTimeP( 1, "Init ", clkMov, Abc_Clock() - clk ); |
| Abc_PrintTimeP( 1, "SAT ", clkSat, Abc_Clock() - clk ); |
| Abc_PrintTimeP( 1, "Clean", clkCln, Abc_Clock() - clk ); |
| // Abc_PrintTimeP( 1, "Sweep", clkSwp, Abc_Clock() - clk ); |
| } |
| Gia_ManStop( pNew ); |
| if ( pvCexes ) |
| printf( "Total number of CEXes collected = %d.\n", Vec_PtrSize(*pvCexes) ); |
| return 0; |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
