| /**CFile**************************************************************** |
| |
| FileName [absUtil.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [Abstraction package.] |
| |
| Synopsis [Interface to pthreads.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - June 20, 2005.] |
| |
| Revision [$Id: absUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "abs.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [This procedure sets default parameters.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Abs_ParSetDefaults( Abs_Par_t * p ) |
| { |
| memset( p, 0, sizeof(Abs_Par_t) ); |
| p->nFramesMax = 0; // maximum frames |
| p->nFramesStart = 0; // starting frame |
| p->nFramesPast = 4; // overlap frames |
| p->nConfLimit = 0; // conflict limit |
| p->nLearnedMax = 1000; // max number of learned clauses |
| p->nLearnedStart = 1000; // max number of learned clauses |
| p->nLearnedDelta = 200; // max number of learned clauses |
| p->nLearnedPerce = 70; // max number of learned clauses |
| p->nTimeOut = 0; // timeout in seconds |
| p->nRatioMin = 0; // stop when less than this % of object is abstracted |
| p->nRatioMax = 30; // restart when more than this % of object is abstracted |
| p->fUseTermVars = 0; // use terminal variables |
| p->fUseRollback = 0; // use rollback to the starting number of frames |
| p->fPropFanout = 1; // propagate fanouts during refinement |
| p->fVerbose = 0; // verbose flag |
| p->iFrame = -1; // the number of frames covered |
| p->iFrameProved = -1; // the number of frames proved |
| p->nFramesNoChangeLim = 2; // the number of frames without change to dump abstraction |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Converting VTA vector to GLA vector.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vVta ) |
| { |
| Gia_Obj_t * pObj; |
| Vec_Int_t * vGla; |
| int nObjMask, nObjs = Gia_ManObjNum(p); |
| int i, Entry, nFrames = Vec_IntEntry( vVta, 0 ); |
| assert( Vec_IntEntry(vVta, nFrames+1) == Vec_IntSize(vVta) ); |
| // get the bitmask |
| nObjMask = (1 << Abc_Base2Log(nObjs)) - 1; |
| assert( nObjs <= nObjMask ); |
| // go through objects |
| vGla = Vec_IntStart( nObjs ); |
| Vec_IntForEachEntryStart( vVta, Entry, i, nFrames+2 ) |
| { |
| pObj = Gia_ManObj( p, (Entry & nObjMask) ); |
| assert( Gia_ObjIsRo(p, pObj) || Gia_ObjIsAnd(pObj) || Gia_ObjIsConst0(pObj) ); |
| Vec_IntAddToEntry( vGla, (Entry & nObjMask), 1 ); |
| } |
| Vec_IntWriteEntry( vGla, 0, nFrames ); |
| return vGla; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Converting GLA vector to VTA vector.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Int_t * Gia_VtaConvertFromGla( Gia_Man_t * p, Vec_Int_t * vGla, int nFrames ) |
| { |
| Vec_Int_t * vVta; |
| int nObjBits, nObjMask, nObjs = Gia_ManObjNum(p); |
| int i, k, j, Entry, Counter, nGlaSize; |
| //. get the GLA size |
| nGlaSize = Vec_IntSum(vGla); |
| // get the bitmask |
| nObjBits = Abc_Base2Log(nObjs); |
| nObjMask = (1 << Abc_Base2Log(nObjs)) - 1; |
| assert( nObjs <= nObjMask ); |
| // go through objects |
| vVta = Vec_IntAlloc( 1000 ); |
| Vec_IntPush( vVta, nFrames ); |
| Counter = nFrames + 2; |
| for ( i = 0; i <= nFrames; i++, Counter += i * nGlaSize ) |
| Vec_IntPush( vVta, Counter ); |
| for ( i = 0; i < nFrames; i++ ) |
| for ( k = 0; k <= i; k++ ) |
| Vec_IntForEachEntry( vGla, Entry, j ) |
| if ( Entry ) |
| Vec_IntPush( vVta, (k << nObjBits) | j ); |
| Counter = Vec_IntEntry(vVta, nFrames+1); |
| assert( Vec_IntEntry(vVta, nFrames+1) == Vec_IntSize(vVta) ); |
| return vVta; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Converting GLA vector to FLA vector.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Gia_FlaConvertToGla_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vGla ) |
| { |
| if ( Gia_ObjIsTravIdCurrent(p, pObj) ) |
| return; |
| Gia_ObjSetTravIdCurrent(p, pObj); |
| Vec_IntWriteEntry( vGla, Gia_ObjId(p, pObj), 1 ); |
| if ( Gia_ObjIsRo(p, pObj) ) |
| return; |
| assert( Gia_ObjIsAnd(pObj) ); |
| Gia_FlaConvertToGla_rec( p, Gia_ObjFanin0(pObj), vGla ); |
| Gia_FlaConvertToGla_rec( p, Gia_ObjFanin1(pObj), vGla ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Converting FLA vector to GLA vector.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Int_t * Gia_FlaConvertToGla( Gia_Man_t * p, Vec_Int_t * vFla ) |
| { |
| Vec_Int_t * vGla; |
| Gia_Obj_t * pObj; |
| int i; |
| // mark const0 and relevant CI objects |
| Gia_ManIncrementTravId( p ); |
| Gia_ObjSetTravIdCurrent(p, Gia_ManConst0(p)); |
| Gia_ManForEachPi( p, pObj, i ) |
| Gia_ObjSetTravIdCurrent(p, pObj); |
| Gia_ManForEachRo( p, pObj, i ) |
| if ( !Vec_IntEntry(vFla, i) ) |
| Gia_ObjSetTravIdCurrent(p, pObj); |
| // label all objects reachable from the PO and selected flops |
| vGla = Vec_IntStart( Gia_ManObjNum(p) ); |
| Vec_IntWriteEntry( vGla, 0, 1 ); |
| Gia_ManForEachPo( p, pObj, i ) |
| Gia_FlaConvertToGla_rec( p, Gia_ObjFanin0(pObj), vGla ); |
| Gia_ManForEachRi( p, pObj, i ) |
| if ( Vec_IntEntry(vFla, i) ) |
| Gia_FlaConvertToGla_rec( p, Gia_ObjFanin0(pObj), vGla ); |
| return vGla; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Converting GLA vector to FLA vector.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Int_t * Gia_GlaConvertToFla( Gia_Man_t * p, Vec_Int_t * vGla ) |
| { |
| Vec_Int_t * vFla; |
| Gia_Obj_t * pObj; |
| int i; |
| vFla = Vec_IntStart( Gia_ManRegNum(p) ); |
| Gia_ManForEachRo( p, pObj, i ) |
| if ( Vec_IntEntry(vGla, Gia_ObjId(p, pObj)) ) |
| Vec_IntWriteEntry( vFla, i, 1 ); |
| return vFla; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Gia_GlaCountFlops( Gia_Man_t * p, Vec_Int_t * vGla ) |
| { |
| Gia_Obj_t * pObj; |
| int i, Count = 0; |
| Gia_ManForEachRo( p, pObj, i ) |
| if ( Vec_IntEntry(vGla, Gia_ObjId(p, pObj)) ) |
| Count++; |
| return Count; |
| } |
| int Gia_GlaCountNodes( Gia_Man_t * p, Vec_Int_t * vGla ) |
| { |
| Gia_Obj_t * pObj; |
| int i, Count = 0; |
| Gia_ManForEachAnd( p, pObj, i ) |
| if ( Vec_IntEntry(vGla, Gia_ObjId(p, pObj)) ) |
| Count++; |
| return Count; |
| } |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
