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

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START void reoProfileNodesStart (reo_man *p)
 DECLARATIONS ///.
 
void reoProfileAplStart (reo_man *p)
 
void reoProfileWidthStart (reo_man *p)
 
void reoProfileWidthStart2 (reo_man *p)
 
void reoProfileNodesPrint (reo_man *p)
 
void reoProfileAplPrint (reo_man *p)
 
void reoProfileWidthPrint (reo_man *p)
 
void reoProfileWidthVerifyLevel (reo_plane *pPlane, int Level)
 

Function Documentation

◆ reoProfileAplPrint()

void reoProfileAplPrint ( reo_man * p)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 305 of file reoProfile.c.

306{
307 printf( "APL: Total = %8.2f. Average =%6.2f.\n", p->nAplCur, p->nAplCur / (float)p->nSupp );
308}
Cube * p
Definition exorList.c:222
Here is the caller graph for this function:

◆ reoProfileAplStart()

void reoProfileAplStart ( reo_man * p)

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

Synopsis [Start the profile for the APL.]

Description [Computes the total path length. The path length is normalized by dividing it by 2^|supp(f)|. To get the "real" APL, multiply by 2^|supp(f)|. This procedure assumes that Weight field of all nodes has been set to 0.0 before the call, except for the weight of the topmost node, which is set to 1.0 (1.0 is the probability of traversing the topmost node). This procedure assigns the edge weights. Because of the equal probability of selecting 0 and 1 assignment at a node, the edge weights are the same for the node. Instead of storing them, we store the weight of the node, which is the probability of traversing the node (pUnit->Weight) during the top down evalation of the BDD. ]

SideEffects []

SeeAlso []

Definition at line 78 of file reoProfile.c.

79{
80 reo_unit * pER, * pTR;
81 reo_unit * pUnit;
82 double Res, Half;
83 int i;
84
85 // clean the weights of all nodes
86 for ( i = 0; i < p->nSupp; i++ )
87 for ( pUnit = p->pPlanes[i].pHead; pUnit; pUnit = pUnit->Next )
88 pUnit->Weight = 0.0;
89 // to assign the node weights (the probability of visiting each node)
90 // we visit the node after visiting its predecessors
91
92 // set the probability of visits to the top nodes
93 for ( i = 0; i < p->nTops; i++ )
94 Unit_Regular(p->pTops[i])->Weight += 1.0;
95
96 // to compute the path length (the sum of products of edge weight by edge length)
97 // we visit the nodes in any order (the above order will do)
98 Res = 0.0;
99 for ( i = 0; i < p->nSupp; i++ )
100 {
101 p->pPlanes[i].statsCost = 0.0;
102 for ( pUnit = p->pPlanes[i].pHead; pUnit; pUnit = pUnit->Next )
103 {
104 pER = Unit_Regular(pUnit->pE);
105 pTR = Unit_Regular(pUnit->pT);
106 Half = 0.5 * pUnit->Weight;
107 pER->Weight += Half;
108 pTR->Weight += Half;
109 // add to the path length
110 p->pPlanes[i].statsCost += pUnit->Weight;
111 }
112 Res += p->pPlanes[i].statsCost;
113 }
114 p->pPlanes[p->nSupp].statsCost = 0.0;
115 p->nAplBeg = p->nAplCur = Res;
116}
#define Unit_Regular(u)
Definition reo.h:174
struct _reo_unit reo_unit
DATA STRUCTURES ///.
Definition reo.h:60
reo_unit * Next
Definition reo.h:76
double Weight
Definition reo.h:77
reo_unit * pE
Definition reo.h:74
reo_unit * pT
Definition reo.h:75
Here is the caller graph for this function:

◆ reoProfileNodesPrint()

void reoProfileNodesPrint ( reo_man * p)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 289 of file reoProfile.c.

290{
291 printf( "NODES: Total = %6d. Average = %6.2f.\n", p->nNodesCur, p->nNodesCur / (float)p->nSupp );
292}
Here is the caller graph for this function:

◆ reoProfileNodesStart()

ABC_NAMESPACE_IMPL_START void reoProfileNodesStart ( reo_man * p)

DECLARATIONS ///.

CFile****************************************************************

FileName [reoProfile.c]

PackageName [REO: A specialized DD reordering engine.]

Synopsis [Procudures that compute variables profiles (nodes, width, APL).]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - October 15, 2002.]

Revision [

Id
reoProfile.c,v 1.0 2002/15/10 03:00:00 alanmi Exp

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

Synopsis [Start the profile for the BDD nodes.]

Description [TopRef is the first level, on this the given node counts towards the width of the BDDs. (In other words, it is the level of the referencing node plus 1.)]

SideEffects []

SeeAlso []

Definition at line 46 of file reoProfile.c.

47{
48 int Total, i;
49 Total = 0;
50 for ( i = 0; i <= p->nSupp; i++ )
51 {
52 p->pPlanes[i].statsCost = p->pPlanes[i].statsNodes;
53 Total += p->pPlanes[i].statsNodes;
54 }
55 assert( Total == p->nNodesCur );
56 p->nNodesBeg = p->nNodesCur;
57}
#define assert(ex)
Definition util_old.h:213
Here is the caller graph for this function:

◆ reoProfileWidthPrint()

void reoProfileWidthPrint ( reo_man * p)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 321 of file reoProfile.c.

322{
323 int WidthMax;
324 int TotalWidth;
325 int i;
326
327 WidthMax = 0;
328 TotalWidth = 0;
329 for ( i = 0; i <= p->nSupp; i++ )
330 {
331 printf( "Level = %2d. Width = %3d.\n", i, p->pPlanes[i].statsWidth );
332 if ( WidthMax < p->pPlanes[i].statsWidth )
333 WidthMax = p->pPlanes[i].statsWidth;
334 TotalWidth += p->pPlanes[i].statsWidth;
335 }
336 assert( p->nWidthCur == TotalWidth );
337 printf( "WIDTH: " );
338 printf( "Maximum = %5d. ", WidthMax );
339 printf( "Total = %7d. ", p->nWidthCur );
340 printf( "Average = %6.2f.\n", TotalWidth / (float)p->nSupp );
341}
Here is the caller graph for this function:

◆ reoProfileWidthStart()

void reoProfileWidthStart ( reo_man * p)

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

Synopsis [Start the profile for the BDD width. Complexity of the algorithm is O(N + n).]

Description [TopRef is the first level, on which the given node counts towards the width of the BDDs. (In other words, it is the level of the referencing node plus 1.)]

SideEffects []

SeeAlso []

Definition at line 130 of file reoProfile.c.

131{
132 reo_unit * pUnit;
133 int * pWidthStart;
134 int * pWidthStop;
135 int v;
136
137 // allocate and clean the storage for starting and stopping levels
138 pWidthStart = ABC_ALLOC( int, p->nSupp + 1 );
139 pWidthStop = ABC_ALLOC( int, p->nSupp + 1 );
140 memset( pWidthStart, 0, sizeof(int) * (p->nSupp + 1) );
141 memset( pWidthStop, 0, sizeof(int) * (p->nSupp + 1) );
142
143 // go through the non-constant nodes and set the topmost level of their cofactors
144 for ( v = 0; v <= p->nSupp; v++ )
145 for ( pUnit = p->pPlanes[v].pHead; pUnit; pUnit = pUnit->Next )
146 {
147 pUnit->TopRef = REO_TOPREF_UNDEF;
148 pUnit->Sign = 0;
149 }
150
151 // add the topmost level of the width profile
152 for ( v = 0; v < p->nTops; v++ )
153 {
154 pUnit = Unit_Regular(p->pTops[v]);
155 if ( pUnit->TopRef == REO_TOPREF_UNDEF )
156 {
157 // set the starting level
158 pUnit->TopRef = 0;
159 pWidthStart[pUnit->TopRef]++;
160 // set the stopping level
161 if ( pUnit->lev != REO_CONST_LEVEL )
162 pWidthStop[pUnit->lev+1]++;
163 }
164 }
165
166 for ( v = 0; v < p->nSupp; v++ )
167 for ( pUnit = p->pPlanes[v].pHead; pUnit; pUnit = pUnit->Next )
168 {
169 if ( pUnit->pE->TopRef == REO_TOPREF_UNDEF )
170 {
171 // set the starting level
172 pUnit->pE->TopRef = pUnit->lev + 1;
173 pWidthStart[pUnit->pE->TopRef]++;
174 // set the stopping level
175 if ( pUnit->pE->lev != REO_CONST_LEVEL )
176 pWidthStop[pUnit->pE->lev+1]++;
177 }
178 if ( pUnit->pT->TopRef == REO_TOPREF_UNDEF )
179 {
180 // set the starting level
181 pUnit->pT->TopRef = pUnit->lev + 1;
182 pWidthStart[pUnit->pT->TopRef]++;
183 // set the stopping level
184 if ( pUnit->pT->lev != REO_CONST_LEVEL )
185 pWidthStop[pUnit->pT->lev+1]++;
186 }
187 }
188
189 // verify the top reference
190 for ( v = 0; v < p->nSupp; v++ )
191 reoProfileWidthVerifyLevel( p->pPlanes + v, v );
192
193 // derive the profile
194 p->nWidthCur = 0;
195 for ( v = 0; v <= p->nSupp; v++ )
196 {
197 if ( v == 0 )
198 p->pPlanes[v].statsWidth = pWidthStart[v] - pWidthStop[v];
199 else
200 p->pPlanes[v].statsWidth = p->pPlanes[v-1].statsWidth + pWidthStart[v] - pWidthStop[v];
201 p->pPlanes[v].statsCost = p->pPlanes[v].statsWidth;
202 p->nWidthCur += p->pPlanes[v].statsWidth;
203 printf( "Level %2d: Width = %5d.\n", v, p->pPlanes[v].statsWidth );
204 }
205 p->nWidthBeg = p->nWidthCur;
206 ABC_FREE( pWidthStart );
207 ABC_FREE( pWidthStop );
208}
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
#define ABC_FREE(obj)
Definition abc_global.h:267
void reoProfileWidthVerifyLevel(reo_plane *pPlane, int Level)
Definition reoProfile.c:354
#define REO_CONST_LEVEL
Definition reo.h:40
#define REO_TOPREF_UNDEF
Definition reo.h:41
short lev
Definition reo.h:68
int Sign
Definition reo.h:72
short TopRef
Definition reo.h:69
char * memset()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ reoProfileWidthStart2()

void reoProfileWidthStart2 ( reo_man * p)

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

Synopsis [Start the profile for the BDD width. Complexity of the algorithm is O(N * n).]

Description [TopRef is the first level, on which the given node counts towards the width of the BDDs. (In other words, it is the level of the referencing node plus 1.)]

SideEffects []

SeeAlso []

Definition at line 222 of file reoProfile.c.

223{
224 reo_unit * pUnit;
225 int i, v;
226
227 // clean the profile
228 for ( i = 0; i <= p->nSupp; i++ )
229 p->pPlanes[i].statsWidth = 0;
230
231 // clean the node structures
232 for ( v = 0; v <= p->nSupp; v++ )
233 for ( pUnit = p->pPlanes[v].pHead; pUnit; pUnit = pUnit->Next )
234 {
235 pUnit->TopRef = REO_TOPREF_UNDEF;
236 pUnit->Sign = 0;
237 }
238
239 // set the topref to the topmost nodes
240 for ( i = 0; i < p->nTops; i++ )
241 Unit_Regular(p->pTops[i])->TopRef = 0;
242
243 // go through the non-constant nodes and set the topmost level of their cofactors
244 for ( i = 0; i < p->nSupp; i++ )
245 for ( pUnit = p->pPlanes[i].pHead; pUnit; pUnit = pUnit->Next )
246 {
247 if ( pUnit->pE->TopRef > i+1 )
248 pUnit->pE->TopRef = i+1;
249 if ( pUnit->pT->TopRef > i+1 )
250 pUnit->pT->TopRef = i+1;
251 }
252
253 // verify the top reference
254 for ( i = 0; i < p->nSupp; i++ )
255 reoProfileWidthVerifyLevel( p->pPlanes + i, i );
256
257 // compute the profile for the internal nodes
258 for ( i = 0; i < p->nSupp; i++ )
259 for ( pUnit = p->pPlanes[i].pHead; pUnit; pUnit = pUnit->Next )
260 for ( v = pUnit->TopRef; v <= pUnit->lev; v++ )
261 p->pPlanes[v].statsWidth++;
262
263 // compute the profile for the constant nodes
264 for ( pUnit = p->pPlanes[p->nSupp].pHead; pUnit; pUnit = pUnit->Next )
265 for ( v = pUnit->TopRef; v <= p->nSupp; v++ )
266 p->pPlanes[v].statsWidth++;
267
268 // get the width cost
269 p->nWidthCur = 0;
270 for ( i = 0; i <= p->nSupp; i++ )
271 {
272 p->pPlanes[i].statsCost = p->pPlanes[i].statsWidth;
273 p->nWidthCur += p->pPlanes[i].statsWidth;
274 }
275 p->nWidthBeg = p->nWidthCur;
276}
Here is the call graph for this function:

◆ reoProfileWidthVerifyLevel()

void reoProfileWidthVerifyLevel ( reo_plane * pPlane,
int Level )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 354 of file reoProfile.c.

355{
356 reo_unit * pUnit;
357 for ( pUnit = pPlane->pHead; pUnit; pUnit = pUnit->Next )
358 {
359 assert( pUnit->TopRef <= Level );
360 assert( pUnit->pE->TopRef <= Level + 1 );
361 assert( pUnit->pT->TopRef <= Level + 1 );
362 }
363}
reo_unit * pHead
Definition reo.h:90
Here is the caller graph for this function: