ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Functions
absUtil.c File Reference
#include "abs.h"
Include dependency graph for absUtil.c:

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START void Abs_ParSetDefaults (Abs_Par_t *p)
 DECLARATIONS ///.
 
Vec_Int_t * Gia_VtaConvertToGla (Gia_Man_t *p, Vec_Int_t *vVta)
 
Vec_Int_t * Gia_VtaConvertFromGla (Gia_Man_t *p, Vec_Int_t *vGla, int nFrames)
 
void Gia_FlaConvertToGla_rec (Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vGla)
 
Vec_Int_t * Gia_FlaConvertToGla (Gia_Man_t *p, Vec_Int_t *vFla)
 
Vec_Int_t * Gia_GlaConvertToFla (Gia_Man_t *p, Vec_Int_t *vGla)
 
int Gia_GlaCountFlops (Gia_Man_t *p, Vec_Int_t *vGla)
 
int Gia_GlaCountNodes (Gia_Man_t *p, Vec_Int_t *vGla)
 

Function Documentation

◆ Abs_ParSetDefaults()

ABC_NAMESPACE_IMPL_START void Abs_ParSetDefaults ( Abs_Par_t * p)

DECLARATIONS ///.

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

] FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [This procedure sets default parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 44 of file absUtil.c.

45{
46 memset( p, 0, sizeof(Abs_Par_t) );
47 p->nFramesMax = 0; // maximum frames
48 p->nFramesStart = 0; // starting frame
49 p->nFramesPast = 4; // overlap frames
50 p->nConfLimit = 0; // conflict limit
51 p->nLearnedMax = 1000; // max number of learned clauses
52 p->nLearnedStart = 1000; // max number of learned clauses
53 p->nLearnedDelta = 200; // max number of learned clauses
54 p->nLearnedPerce = 70; // max number of learned clauses
55 p->nTimeOut = 0; // timeout in seconds
56 p->nRatioMin = 0; // stop when less than this % of object is abstracted
57 p->nRatioMax = 30; // restart when more than this % of object is abstracted
58 p->fUseTermVars = 0; // use terminal variables
59 p->fUseRollback = 0; // use rollback to the starting number of frames
60 p->fPropFanout = 1; // propagate fanouts during refinement
61 p->fVerbose = 0; // verbose flag
62 p->iFrame = -1; // the number of frames covered
63 p->iFrameProved = -1; // the number of frames proved
64 p->nFramesNoChangeLim = 2; // the number of frames without change to dump abstraction
65}
Abs_Par_t
typedefABC_NAMESPACE_HEADER_START struct Abs_Par_t_ Abs_Par_t
INCLUDES ///.
Definition abs.h:46
p
Cube * p
Definition exorList.c:222
memset
char * memset()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Gia_FlaConvertToGla()

Vec_Int_t * Gia_FlaConvertToGla ( Gia_Man_t * p,
Vec_Int_t * vFla )

Function*************************************************************

Synopsis [Converting FLA vector to GLA vector.]

Description []

SideEffects []

SeeAlso []

Definition at line 173 of file absUtil.c.

174{
175 Vec_Int_t * vGla;
176 Gia_Obj_t * pObj;
177 int i;
178 // mark const0 and relevant CI objects
179 Gia_ManIncrementTravId( p );
180 Gia_ObjSetTravIdCurrent(p, Gia_ManConst0(p));
181 Gia_ManForEachPi( p, pObj, i )
182 Gia_ObjSetTravIdCurrent(p, pObj);
183 Gia_ManForEachRo( p, pObj, i )
184 if ( !Vec_IntEntry(vFla, i) )
185 Gia_ObjSetTravIdCurrent(p, pObj);
186 // label all objects reachable from the PO and selected flops
187 vGla = Vec_IntStart( Gia_ManObjNum(p) );
188 Vec_IntWriteEntry( vGla, 0, 1 );
189 Gia_ManForEachPo( p, pObj, i )
190 Gia_FlaConvertToGla_rec( p, Gia_ObjFanin0(pObj), vGla );
191 Gia_ManForEachRi( p, pObj, i )
192 if ( Vec_IntEntry(vFla, i) )
193 Gia_FlaConvertToGla_rec( p, Gia_ObjFanin0(pObj), vGla );
194 return vGla;
195}
Gia_FlaConvertToGla_rec
void Gia_FlaConvertToGla_rec(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vGla)
Definition absUtil.c:149
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Gia_ManForEachRo
#define Gia_ManForEachRo(p, pObj, i)
Definition gia.h:1252
Gia_ManForEachPo
#define Gia_ManForEachPo(p, pObj, i)
Definition gia.h:1250
Gia_ManForEachPi
#define Gia_ManForEachPi(p, pObj, i)
Definition gia.h:1248
Gia_Obj_t
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
Gia_ManIncrementTravId
void Gia_ManIncrementTravId(Gia_Man_t *p)
Definition giaUtil.c:190
Gia_ManForEachRi
#define Gia_ManForEachRi(p, pObj, i)
Definition gia.h:1254
Here is the call graph for this function:

◆ Gia_FlaConvertToGla_rec()

void Gia_FlaConvertToGla_rec ( Gia_Man_t * p,
Gia_Obj_t * pObj,
Vec_Int_t * vGla )

Function*************************************************************

Synopsis [Converting GLA vector to FLA vector.]

Description []

SideEffects []

SeeAlso []

Definition at line 149 of file absUtil.c.

150{
151 if ( Gia_ObjIsTravIdCurrent(p, pObj) )
152 return;
153 Gia_ObjSetTravIdCurrent(p, pObj);
154 Vec_IntWriteEntry( vGla, Gia_ObjId(p, pObj), 1 );
155 if ( Gia_ObjIsRo(p, pObj) )
156 return;
157 assert( Gia_ObjIsAnd(pObj) );
158 Gia_FlaConvertToGla_rec( p, Gia_ObjFanin0(pObj), vGla );
159 Gia_FlaConvertToGla_rec( p, Gia_ObjFanin1(pObj), vGla );
160}
assert
#define assert(ex)
Definition util_old.h:213
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Gia_GlaConvertToFla()

Vec_Int_t * Gia_GlaConvertToFla ( Gia_Man_t * p,
Vec_Int_t * vGla )

Function*************************************************************

Synopsis [Converting GLA vector to FLA vector.]

Description []

SideEffects []

SeeAlso []

Definition at line 208 of file absUtil.c.

209{
210 Vec_Int_t * vFla;
211 Gia_Obj_t * pObj;
212 int i;
213 vFla = Vec_IntStart( Gia_ManRegNum(p) );
214 Gia_ManForEachRo( p, pObj, i )
215 if ( Vec_IntEntry(vGla, Gia_ObjId(p, pObj)) )
216 Vec_IntWriteEntry( vFla, i, 1 );
217 return vFla;
218}

◆ Gia_GlaCountFlops()

int Gia_GlaCountFlops ( Gia_Man_t * p,
Vec_Int_t * vGla )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 231 of file absUtil.c.

232{
233 Gia_Obj_t * pObj;
234 int i, Count = 0;
235 Gia_ManForEachRo( p, pObj, i )
236 if ( Vec_IntEntry(vGla, Gia_ObjId(p, pObj)) )
237 Count++;
238 return Count;
239}
Here is the caller graph for this function:

◆ Gia_GlaCountNodes()

int Gia_GlaCountNodes ( Gia_Man_t * p,
Vec_Int_t * vGla )

Definition at line 240 of file absUtil.c.

241{
242 Gia_Obj_t * pObj;
243 int i, Count = 0;
244 Gia_ManForEachAnd( p, pObj, i )
245 if ( Vec_IntEntry(vGla, Gia_ObjId(p, pObj)) )
246 Count++;
247 return Count;
248}
Gia_ManForEachAnd
#define Gia_ManForEachAnd(p, pObj, i)
Definition gia.h:1214
Here is the caller graph for this function:

◆ Gia_VtaConvertFromGla()

Vec_Int_t * Gia_VtaConvertFromGla ( Gia_Man_t * p,
Vec_Int_t * vGla,
int nFrames )

Function*************************************************************

Synopsis [Converting GLA vector to VTA vector.]

Description []

SideEffects []

SeeAlso []

Definition at line 111 of file absUtil.c.

112{
113 Vec_Int_t * vVta;
114 int nObjBits, nObjMask, nObjs = Gia_ManObjNum(p);
115 int i, k, j, Entry, Counter, nGlaSize;
116 //. get the GLA size
117 nGlaSize = Vec_IntSum(vGla);
118 // get the bitmask
119 nObjBits = Abc_Base2Log(nObjs);
120 nObjMask = (1 << Abc_Base2Log(nObjs)) - 1;
121 assert( nObjs <= nObjMask );
122 // go through objects
123 vVta = Vec_IntAlloc( 1000 );
124 Vec_IntPush( vVta, nFrames );
125 Counter = nFrames + 2;
126 for ( i = 0; i <= nFrames; i++, Counter += i * nGlaSize )
127 Vec_IntPush( vVta, Counter );
128 for ( i = 0; i < nFrames; i++ )
129 for ( k = 0; k <= i; k++ )
130 Vec_IntForEachEntry( vGla, Entry, j )
131 if ( Entry )
132 Vec_IntPush( vVta, (k << nObjBits) | j );
133 Counter = Vec_IntEntry(vVta, nFrames+1);
134 assert( Vec_IntEntry(vVta, nFrames+1) == Vec_IntSize(vVta) );
135 return vVta;
136}
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54

◆ Gia_VtaConvertToGla()

Vec_Int_t * Gia_VtaConvertToGla ( Gia_Man_t * p,
Vec_Int_t * vVta )

Function*************************************************************

Synopsis [Converting VTA vector to GLA vector.]

Description []

SideEffects []

SeeAlso []

Definition at line 78 of file absUtil.c.

79{
80 Gia_Obj_t * pObj;
81 Vec_Int_t * vGla;
82 int nObjMask, nObjs = Gia_ManObjNum(p);
83 int i, Entry, nFrames = Vec_IntEntry( vVta, 0 );
84 assert( Vec_IntEntry(vVta, nFrames+1) == Vec_IntSize(vVta) );
85 // get the bitmask
86 nObjMask = (1 << Abc_Base2Log(nObjs)) - 1;
87 assert( nObjs <= nObjMask );
88 // go through objects
89 vGla = Vec_IntStart( nObjs );
90 Vec_IntForEachEntryStart( vVta, Entry, i, nFrames+2 )
91 {
92 pObj = Gia_ManObj( p, (Entry & nObjMask) );
93 assert( Gia_ObjIsRo(p, pObj) || Gia_ObjIsAnd(pObj) || Gia_ObjIsConst0(pObj) );
94 Vec_IntAddToEntry( vGla, (Entry & nObjMask), 1 );
95 }
96 Vec_IntWriteEntry( vGla, 0, nFrames );
97 return vGla;
98}
Vec_IntForEachEntryStart
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition vecInt.h:56
Here is the caller graph for this function: