| /**CFile**************************************************************** |
| |
| FileName [int2Bmc.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [Interpolation engine.] |
| |
| Synopsis [BMC used inside IMC.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - Dec 1, 2013.] |
| |
| Revision [$Id: int2Bmc.c,v 1.00 2013/12/01 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "int2Int.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Trasnforms AIG to transition into the init state.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Gia_Man_t * Int2_ManDupInit( Gia_Man_t * p, int fVerbose ) |
| { |
| Gia_Man_t * pNew, * pTemp; |
| Gia_Obj_t * pObj, * pObjRi, * pObjRo; |
| int i, iCtrl; |
| assert( Gia_ManRegNum(p) > 0 ); |
| pNew = Gia_ManStart( 10000 ); |
| pNew->pName = Abc_UtilStrsav( p->pName ); |
| pNew->pSpec = Abc_UtilStrsav( p->pSpec ); |
| Gia_ManConst0(p)->Value = 0; |
| Gia_ManForEachCi( p, pObj, i ) |
| { |
| if ( i == Gia_ManPiNum(p) ) |
| iCtrl = Gia_ManAppendCi( pNew ); |
| pObj->Value = Gia_ManAppendCi( pNew ); |
| } |
| Gia_ManHashAlloc( pNew ); |
| Gia_ManForEachAnd( p, pObj, i ) |
| pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); |
| Gia_ManForEachPo( p, pObj, i ) |
| pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); |
| Gia_ManForEachRiRo( p, pObjRi, pObjRo, i ) |
| Gia_ManAppendCo( pNew, Gia_ManHashMux( pNew, iCtrl, pObjRo->Value, Gia_ObjFanin0Copy(pObjRi) ) ); |
| Gia_ManHashStop( pNew ); |
| Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); |
| // remove dangling |
| pNew = Gia_ManCleanup( pTemp = pNew ); |
| if ( fVerbose ) |
| printf( "Before cleanup = %d nodes. After cleanup = %d nodes.\n", |
| Gia_ManAndNum(pTemp), Gia_ManAndNum(pNew) ); |
| Gia_ManStop( pTemp ); |
| return pNew; |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns 1 if AIG has transition into init state.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Int2_ManCheckInit( Gia_Man_t * p ) |
| { |
| sat_solver * pSat; |
| Cnf_Dat_t * pCnf; |
| Gia_Man_t * pNew; |
| Gia_Obj_t * pObj; |
| Vec_Int_t * vLits; |
| int i, Lit, RetValue = 0; |
| assert( Gia_ManRegNum(p) > 0 ); |
| pNew = Jf_ManDeriveCnf( p, 0 ); |
| pCnf = (Cnf_Dat_t *)pNew->pData; pNew->pData = NULL; |
| pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); |
| if ( pSat != NULL ) |
| { |
| vLits = Vec_IntAlloc( Gia_ManRegNum(p) ); |
| Gia_ManForEachRi( pNew, pObj, i ) |
| { |
| Lit = pCnf->pVarNums[ Gia_ObjId(pNew, Gia_ObjFanin0(pObj)) ]; |
| Lit = Abc_Var2Lit( Lit, Gia_ObjFaninC0(pObj) ); |
| Vec_IntPush( vLits, Abc_LitNot(Lit) ); |
| } |
| if ( sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 ) == l_True ) |
| RetValue = 1; |
| Vec_IntFree( vLits ); |
| sat_solver_delete( pSat ); |
| } |
| Cnf_DataFree( pCnf ); |
| Gia_ManStop( pNew ); |
| return RetValue; |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Creates the BMC instance in the SAT solver.] |
| |
| Description [The PIs are mapped in the natural order. The flop inputs |
| are the last Gia_ManRegNum(p) variables of resulting SAT solver.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Gia_Man_t * Int2_ManFrameInit( Gia_Man_t * p, int nFrames, int fVerbose ) |
| { |
| Gia_Man_t * pFrames, * pTemp; |
| Gia_Obj_t * pObj; |
| int i, f; |
| pFrames = Gia_ManStart( 10000 ); |
| pFrames->pName = Abc_UtilStrsav( p->pName ); |
| pFrames->pSpec = Abc_UtilStrsav( p->pSpec ); |
| Gia_ManConst0(p)->Value = 0; |
| // perform structural hashing |
| Gia_ManHashAlloc( pFrames ); |
| for ( f = 0; f < nFrames; f++ ) |
| { |
| Gia_ManForEachPi( p, pObj, i ) |
| pObj->Value = Gia_ManAppendCi( pFrames ); |
| Gia_ManForEachRo( p, pObj, i ) |
| pObj->Value = f ? Gia_ObjRoToRi(p, pObj)->Value : 0; |
| Gia_ManForEachAnd( p, pObj, i ) |
| pObj->Value = Gia_ManHashAnd( pFrames, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); |
| Gia_ManForEachRi( p, pObj, i ) |
| pObj->Value = Gia_ObjFanin0Copy(pObj); |
| } |
| Gia_ManHashStop( pFrames ); |
| // create flop inputs |
| Gia_ManForEachRi( p, pObj, i ) |
| pObj->Value = Gia_ManAppendCo( pFrames, Gia_ObjFanin0Copy(pObj) ); |
| // remove dangling |
| pFrames = Gia_ManCleanup( pTemp = pFrames ); |
| if ( fVerbose ) |
| printf( "Before cleanup = %d nodes. After cleanup = %d nodes.\n", |
| Gia_ManAndNum(pTemp), Gia_ManAndNum(pFrames) ); |
| Gia_ManStop( pTemp ); |
| return pFrames; |
| } |
| sat_solver * Int2_ManSetupBmcSolver( Gia_Man_t * p, int nFrames ) |
| { |
| Gia_Man_t * pFrames, * pTemp; |
| Cnf_Dat_t * pCnf; |
| sat_solver * pSat; |
| // unfold for the given number of timeframes |
| pFrames = Int2_ManFrameInit( p, nFrames, 1 ); |
| assert( Gia_ManRegNum(pFrames) == 0 ); |
| // derive CNF for the timeframes |
| pFrames = Jf_ManDeriveCnf( pTemp = pFrames, 0 ); Gia_ManStop( pTemp ); |
| pCnf = (Cnf_Dat_t *)pFrames->pData; pFrames->pData = NULL; |
| // create SAT solver |
| pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); |
| if ( pSat != NULL ) |
| { |
| Gia_Obj_t * pObj; |
| int i, nVars = sat_solver_nvars( pSat ); |
| sat_solver_setnvars( pSat, nVars + Gia_ManPoNum(pFrames) ); |
| // add clauses for the POs |
| Gia_ManForEachCo( pFrames, pObj, i ) |
| sat_solver_add_buffer( pSat, nVars + i, pCnf->pVarNums[Gia_ObjId(pFrames, Gia_ObjFanin0(pObj))], Gia_ObjFaninC0(pObj) ); |
| } |
| Cnf_DataFree( pCnf ); |
| Gia_ManStop( pFrames ); |
| return pSat; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline int Int2_ManCheckFrames( Int2_Man_t * p, int iFrame, int iObj ) |
| { |
| Vec_Int_t * vMapFrame = (Vec_Int_t *)Vec_PtrEntry(p->vMapFrames, iFrame); |
| return Vec_IntEntry(vMapFrame, iObj); |
| } |
| static inline void Int2_ManWriteFrames( Int2_Man_t * p, int iFrame, int iObj, int iRes ) |
| { |
| Vec_Int_t * vMapFrame = (Vec_Int_t *)Vec_PtrEntry(p->vMapFrames, iFrame); |
| assert( Vec_IntEntry(vMapFrame, iObj) == -1 ); |
| Vec_IntWriteEntry( vMapFrame, iObj, iRes ); |
| } |
| void Int2_ManCreateFrames( Int2_Man_t * p, int iFrame, Vec_Int_t * vPrefCos ) |
| { |
| Gia_Obj_t * pObj; |
| int i, Entry, iLit; |
| // create storage room for unfolded IDs |
| for ( i = Vec_PtrSize(p->vMapFrames); i <= iFrame; i++ ) |
| Vec_PtrPush( p->vMapFrames, Vec_IntStartFull( Gia_ManObjNum(p->pGia) ) ); |
| assert( Vec_PtrSize(p->vMapFrames) == iFrame + 1 ); |
| // create constant 0 node |
| if ( f == 0 ) |
| { |
| iLit = 1; |
| Int2_ManWriteFrames( p, iFrame, iObj, 0 ); |
| sat_solver_addclause( p->pGiaPref, &iLit, &iLit + 1 ); |
| } |
| // start the stack |
| Vec_IntClear( p->vStack ); |
| Vec_IntForEachEntry( vPrefCos, Entry, i ) |
| { |
| pObj = Gia_ManCo( p->pGia, Entry ); |
| Vec_IntPush( p->vStack, iFrame ); |
| Vec_IntPush( p->vStack, Gia_ObjId(p->pGia, pObj) ); |
| } |
| // construct unfolded AIG |
| while ( Vec_IntSize(p->vStack) > 0 ) |
| { |
| int iObj = Vec_IntPop(p->vStack); |
| int iFrame = Vec_IntPop(p->vStack); |
| if ( Int2_ManCheckFrames(p, iFrame, iObj) >= 0 ) |
| continue; |
| pObj = Gia_ManObj( p->pGia, iObj ); |
| if ( Gia_ObjIsPi(p->pGia, pObj) ) |
| Int2_ManWriteFrames( p, iFrame, iObj, Gia_ManAppendCi(p->pFrames) ); |
| else if ( iFrame == 0 && Gia_ObjIsRo(p->pGia, iObj) ) |
| Int2_ManWriteFrames( p, iFrame, iObj, 0 ); |
| else if ( Gia_ObjIsRo(p->pGia, iObj) ) |
| { |
| int iObjF = Gia_ObjId( p->pGia, Gia_ObjRoToRi(p->pGia, pObj) ); |
| int iLit = Int2_ManCheckFrames( p, iFrame-1, iObjF ); |
| if ( iLit >= 0 ) |
| Int2_ManWriteFrames( p, iFrame, iObj, iLit ); |
| else |
| { |
| Vec_IntPush( p->vStack, iFrame ); |
| Vec_IntPush( p->vStack, iObj ); |
| Vec_IntPush( p->vStack, iFrame-1 ); |
| Vec_IntPush( p->vStack, iObjF ); |
| } |
| } |
| else if ( Gia_ObjIsCo(pObj) ) |
| { |
| int iObjF = Gia_ObjFaninId0(p->pGia, iObj) ); |
| int iLit = Int2_ManCheckFrames( p, iFrame, iObjF ); |
| if ( iLit >= 0 ) |
| Int2_ManWriteFrames( p, iFrame, iObj, Abc_LitNotCond(iLit, Gia_ObjFaninC0(pObj)) ); |
| else |
| { |
| Vec_IntPush( p->vStack, iFrame ); |
| Vec_IntPush( p->vStack, iObj ); |
| Vec_IntPush( p->vStack, iFrame ); |
| Vec_IntPush( p->vStack, iObjF ); |
| } |
| } |
| else if ( Gia_ObjIsAnd(pObj) ) |
| { |
| int iObjF0 = Gia_ObjFaninId0(p->pGia, iObj) ); |
| int iLit0 = Int2_ManCheckFrames( p, iFrame, iObjF0 ); |
| int iObjF1 = Gia_ObjFaninId1(p->pGia, iObj) ); |
| int iLit1 = Int2_ManCheckFrames( p, iFrame, iObjF1 ); |
| if ( iLit0 >= 0 && iLit1 >= 0 ) |
| { |
| Entry = Gia_ManObjNum(pFrames); |
| iLit = Gia_ManHashAnd(pFrames, iLit0, iLit1); |
| Int2_ManWriteFrames( p, iFrame, iObj, iLit ); |
| if ( Entry < Gia_ManObjNum(pFrames) ) |
| { |
| assert( !Abc_LitIsCompl(iLit) ); |
| sat_solver_add_and( p->pGiaPref, Abc_Lit2Var(iLit), Abc_Lit2Var(iLit0), Abc_Lit2Var(iLit1), Abc_LitIsCompl(iLit0), Abc_LitIsCompl(iLit1), 0 ); |
| } |
| } |
| else |
| { |
| Vec_IntPush( p->vStack, iFrame ); |
| Vec_IntPush( p->vStack, iObj ); |
| if ( iLit0 < 0 ) |
| { |
| Vec_IntPush( p->vStack, iFrame ); |
| Vec_IntPush( p->vStack, iObjF0 ); |
| } |
| if ( iLit1 < 0 ) |
| { |
| Vec_IntPush( p->vStack, iFrame ); |
| Vec_IntPush( p->vStack, iObjF1 ); |
| } |
| } |
| } |
| else assert( 0 ); |
| } |
| } |
| int Int2_ManCheckBmc( Int2_Man_t * p, Vec_Int_t * vCube ) |
| { |
| int status; |
| if ( vCube == NULL ) |
| { |
| Gia_Obj_t * pObj; |
| int i, iLit; |
| Gia_ManForEachPo( p->pGia, pObj, i ) |
| { |
| iLit = Int2_ManCheckFrames( p, 0, Gia_ObjId(p->pGia, pObj) ); |
| if ( iLit == 0 ) |
| continue; |
| if ( iLit == 1 ) |
| return 0; |
| status = sat_solver_solve( p->pSatPref, &iLit, &iLit + 1, 0, 0, 0, 0 ); |
| if ( status == l_False ) |
| continue; |
| if ( status == l_True ) |
| return 0; |
| return -1; |
| } |
| return 1; |
| } |
| status = sat_solver_solve( p->pSatPref, Vec_IntArray(vCube), Vec_IntArray(vCube) + Vec_IntSize(vCube), 0, 0, 0, 0 ); |
| if ( status == l_False ) |
| return 1; |
| if ( status == l_True ) |
| return 0; |
| return -1; |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
