| /**CFile**************************************************************** |
| |
| FileName [bmcBmci.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [SAT-based bounded model checking.] |
| |
| Synopsis [] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - June 20, 2005.] |
| |
| Revision [$Id: bmcBmci.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "bmc.h" |
| #include "sat/cnf/cnf.h" |
| #include "sat/bsat/satStore.h" |
| #include "aig/gia/giaAig.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline Cnf_Dat_t * Cnf_DeriveGiaRemapped( Gia_Man_t * p ) |
| { |
| Cnf_Dat_t * pCnf; |
| Aig_Man_t * pAig = Gia_ManToAigSimple( p ); |
| pAig->nRegs = 0; |
| pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) ); |
| Aig_ManStop( pAig ); |
| return pCnf; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline void Cnf_DataLiftGia( Cnf_Dat_t * p, Gia_Man_t * pGia, int nVarsPlus ) |
| { |
| Gia_Obj_t * pObj; |
| int v; |
| Gia_ManForEachObj( pGia, pObj, v ) |
| if ( p->pVarNums[Gia_ObjId(pGia, pObj)] >= 0 ) |
| p->pVarNums[Gia_ObjId(pGia, pObj)] += nVarsPlus; |
| for ( v = 0; v < p->nLiterals; v++ ) |
| p->pClauses[0][v] += 2*nVarsPlus; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Bmc_BmciUnfold( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Int_t * vFFLits, int fPiReuse ) |
| { |
| Gia_Obj_t * pObj; |
| int i; |
| assert( Gia_ManRegNum(p) == Vec_IntSize(vFFLits) ); |
| Gia_ManConst0(p)->Value = 0; |
| Gia_ManForEachRo( p, pObj, i ) |
| pObj->Value = Vec_IntEntry(vFFLits, i); |
| Gia_ManForEachPi( p, pObj, i ) |
| pObj->Value = fPiReuse ? Gia_ObjToLit(pNew, Gia_ManPi(pNew, Gia_ManPiNum(pNew)-Gia_ManPiNum(p)+i)) : Gia_ManAppendCi(pNew); |
| Gia_ManForEachAnd( p, pObj, i ) |
| pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); |
| Gia_ManForEachRi( p, pObj, i ) |
| Vec_IntWriteEntry( vFFLits, i, Gia_ObjFanin0Copy(pObj) ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Bmc_BmciPart_rec( Gia_Man_t * pNew, Vec_Int_t * vSatMap, int iIdNew, Gia_Man_t * pPart, Vec_Int_t * vPartMap, Vec_Int_t * vCopies ) |
| { |
| Gia_Obj_t * pObj = Gia_ManObj( pNew, iIdNew ); |
| int iLitPart0, iLitPart1, iRes; |
| if ( Vec_IntEntry(vCopies, iIdNew) ) |
| return Vec_IntEntry(vCopies, iIdNew); |
| if ( Vec_IntEntry(vSatMap, iIdNew) >= 0 || Gia_ObjIsCi(pObj) ) |
| { |
| Vec_IntPush( vPartMap, iIdNew ); |
| iRes = Gia_ManAppendCi(pPart); |
| Vec_IntWriteEntry( vCopies, iIdNew, iRes ); |
| return iRes; |
| } |
| assert( Gia_ObjIsAnd(pObj) ); |
| iLitPart0 = Bmc_BmciPart_rec( pNew, vSatMap, Gia_ObjFaninId0(pObj, iIdNew), pPart, vPartMap, vCopies ); |
| iLitPart1 = Bmc_BmciPart_rec( pNew, vSatMap, Gia_ObjFaninId1(pObj, iIdNew), pPart, vPartMap, vCopies ); |
| iLitPart0 = Abc_LitNotCond( iLitPart0, Gia_ObjFaninC0(pObj) ); |
| iLitPart1 = Abc_LitNotCond( iLitPart1, Gia_ObjFaninC1(pObj) ); |
| Vec_IntPush( vPartMap, iIdNew ); |
| iRes = Gia_ManAppendAnd( pPart, iLitPart0, iLitPart1 ); |
| Vec_IntWriteEntry( vCopies, iIdNew, iRes ); |
| return iRes; |
| } |
| Gia_Man_t * Bmc_BmciPart( Gia_Man_t * pNew, Vec_Int_t * vSatMap, Vec_Int_t * vMiters, Vec_Int_t * vPartMap, Vec_Int_t * vCopies ) |
| { |
| Gia_Man_t * pPart; |
| int i, iLit, iLitPart; |
| Vec_IntFill( vCopies, Gia_ManObjNum(pNew), 0 ); |
| Vec_IntFillExtra( vSatMap, Gia_ManObjNum(pNew), -1 ); |
| pPart = Gia_ManStart( 1000 ); |
| pPart->pName = Abc_UtilStrsav( pNew->pName ); |
| Vec_IntClear( vPartMap ); |
| Vec_IntPush( vPartMap, 0 ); |
| Vec_IntForEachEntry( vMiters, iLit, i ) |
| { |
| if ( iLit == -1 ) |
| continue; |
| assert( iLit >= 2 ); |
| iLitPart = Bmc_BmciPart_rec( pNew, vSatMap, Abc_Lit2Var(iLit), pPart, vPartMap, vCopies ); |
| Gia_ManAppendCo( pPart, Abc_LitNotCond(iLitPart, Abc_LitIsCompl(iLit)) ); |
| Vec_IntPush( vPartMap, -1 ); |
| } |
| assert( Gia_ManPoNum(pPart) > 0 ); |
| assert( Vec_IntSize(vPartMap) == Gia_ManObjNum(pPart) ); |
| return pPart; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Bmc_BmciPerform( Gia_Man_t * p, Vec_Int_t * vInit0, Vec_Int_t * vInit1, int nFrames, int nWords, int nTimeOut, int fVerbose ) |
| { |
| int nSatVars = 1; |
| Vec_Int_t * vLits0, * vLits1, * vMiters, * vSatMap, * vPartMap, * vCopies; |
| Gia_Man_t * pNew, * pPart; |
| Gia_Obj_t * pObj; |
| Cnf_Dat_t * pCnf; |
| sat_solver * pSat; |
| int iVar0, iVar1, iLit, iLit0, iLit1; |
| int i, f, status, nChanges, nMiters, RetValue = 1; |
| assert( Vec_IntSize(vInit0) == Gia_ManRegNum(p) ); |
| assert( Vec_IntSize(vInit1) == Gia_ManRegNum(p) ); |
| |
| // start the SAT solver |
| pSat = sat_solver_new(); |
| sat_solver_set_runtime_limit( pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 ); |
| |
| pNew = Gia_ManStart( 10000 ); |
| pNew->pName = Abc_UtilStrsav( p->pName ); |
| Gia_ManHashAlloc( pNew ); |
| Gia_ManConst0(p)->Value = 0; |
| |
| vLits0 = Vec_IntAlloc( Gia_ManRegNum(p) ); |
| Vec_IntForEachEntry( vInit0, iLit, i ) |
| Vec_IntPush( vLits0, iLit < 2 ? iLit : Gia_ManAppendCi(pNew) ); |
| |
| vLits1 = Vec_IntAlloc( Gia_ManRegNum(p) ); |
| Vec_IntForEachEntry( vInit1, iLit, i ) |
| Vec_IntPush( vLits1, iLit < 2 ? iLit : Gia_ManAppendCi(pNew) ); |
| |
| vMiters = Vec_IntAlloc( 1000 ); |
| vSatMap = Vec_IntAlloc( 1000 ); |
| vPartMap = Vec_IntAlloc( 1000 ); |
| vCopies = Vec_IntAlloc( 1000 ); |
| for ( f = 0; f < nFrames; f++ ) |
| { |
| abctime clk = Abc_Clock(); |
| Bmc_BmciUnfold( pNew, p, vLits0, 0 ); |
| Bmc_BmciUnfold( pNew, p, vLits1, 1 ); |
| assert( Vec_IntSize(vLits0) == Vec_IntSize(vLits1) ); |
| nMiters = 0; |
| Vec_IntClear( vMiters ); |
| Vec_IntForEachEntryTwo( vLits0, vLits1, iLit0, iLit1, i ) |
| if ( (iLit0 >= 2 || iLit1 >= 2) && iLit0 != iLit1 ) |
| Vec_IntPush( vMiters, Gia_ManHashXor(pNew, iLit0, iLit1) ), nMiters++; |
| else |
| Vec_IntPush( vMiters, -1 ); |
| assert( Vec_IntSize(vMiters) == Gia_ManRegNum(p) ); |
| if ( Vec_IntSum(vMiters) + Vec_IntSize(vLits1) == 0 ) |
| { |
| if ( fVerbose ) |
| printf( "Reached a fixed point after %d frames. \n", f+1 ); |
| break; |
| } |
| // create new part |
| pPart = Bmc_BmciPart( pNew, vSatMap, vMiters, vPartMap, vCopies ); |
| pCnf = Cnf_DeriveGiaRemapped( pPart ); |
| Cnf_DataLiftGia( pCnf, pPart, nSatVars ); |
| nSatVars += pCnf->nVars; |
| sat_solver_setnvars( pSat, nSatVars ); |
| for ( i = 0; i < pCnf->nClauses; i++ ) |
| if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) ) |
| assert( 0 ); |
| // stitch the clauses |
| Gia_ManForEachPi( pPart, pObj, i ) |
| { |
| iVar0 = pCnf->pVarNums[Gia_ObjId(pPart, pObj)]; |
| iVar1 = Vec_IntEntry( vSatMap, Vec_IntEntry(vPartMap, Gia_ObjId(pPart, pObj)) ); |
| if ( iVar1 == -1 ) |
| continue; |
| sat_solver_add_buffer( pSat, iVar0, iVar1, 0 ); |
| } |
| // transfer variables |
| Gia_ManForEachCand( pPart, pObj, i ) |
| if ( pCnf->pVarNums[i] >= 0 ) |
| { |
| assert( Gia_ObjIsCi(pObj) || Vec_IntEntry( vSatMap, Vec_IntEntry(vPartMap, i) ) == -1 ); |
| Vec_IntWriteEntry( vSatMap, Vec_IntEntry(vPartMap, i), pCnf->pVarNums[i] ); |
| } |
| Cnf_DataFree( pCnf ); |
| Gia_ManStop( pPart ); |
| // perform runs |
| nChanges = 0; |
| Vec_IntForEachEntry( vMiters, iLit, i ) |
| { |
| if ( iLit == -1 ) |
| continue; |
| assert( Vec_IntEntry(vSatMap, Abc_Lit2Var(iLit)) > 0 ); |
| iLit = Abc_Lit2LitV( Vec_IntArray(vSatMap), iLit ); |
| status = sat_solver_solve( pSat, &iLit, &iLit + 1, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); |
| if ( status == l_True ) |
| { |
| nChanges++; |
| continue; |
| } |
| if ( status == l_Undef ) |
| { |
| printf( "Timeout reached after %d seconds. \n", nTimeOut ); |
| RetValue = 0; |
| goto cleanup; |
| } |
| assert( status == l_False ); |
| iLit0 = Vec_IntEntry( vLits0, i ); |
| iLit1 = Vec_IntEntry( vLits1, i ); |
| assert( (iLit0 >= 2 || iLit1 >= 2) && iLit0 != iLit1 ); |
| if ( iLit1 >= 2 ) |
| Vec_IntWriteEntry( vLits1, i, iLit0 ); |
| else |
| Vec_IntWriteEntry( vLits0, i, iLit1 ); |
| iLit0 = Vec_IntEntry( vLits0, i ); |
| iLit1 = Vec_IntEntry( vLits1, i ); |
| assert( iLit0 == iLit1 ); |
| } |
| if ( fVerbose ) |
| { |
| printf( "Frame %4d : ", f+1 ); |
| printf( "Vars =%7d ", nSatVars ); |
| printf( "Clause =%10d ", sat_solver_nclauses(pSat) ); |
| printf( "Conflict =%10d ", sat_solver_nconflicts(pSat) ); |
| printf( "AIG =%7d ", Gia_ManAndNum(pNew) ); |
| printf( "Miters =%5d ", nMiters ); |
| printf( "SAT =%5d ", nChanges ); |
| Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); |
| } |
| if ( nChanges == 0 ) |
| { |
| printf( "Reached a fixed point after %d frames. \n", f+1 ); |
| break; |
| } |
| } |
| cleanup: |
| |
| sat_solver_delete( pSat ); |
| Gia_ManStopP( &pNew ); |
| Vec_IntFree( vLits0 ); |
| Vec_IntFree( vLits1 ); |
| Vec_IntFree( vMiters ); |
| Vec_IntFree( vSatMap ); |
| Vec_IntFree( vPartMap ); |
| Vec_IntFree( vCopies ); |
| return RetValue; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Gia_ManBmciTest( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose ) |
| { |
| Vec_Int_t * vInit0 = Vec_IntStart( Gia_ManRegNum(p) ); |
| Bmc_BmciPerform( p, vInit, vInit0, nFrames, nWords, nTimeOut, fVerbose ); |
| Vec_IntFree( vInit0 ); |
| return 1; |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
