source: vis_dev/vis-2.3/src/restr/restrFaninout.c @ 80

Last change on this file since 80 was 14, checked in by cecile, 13 years ago

vis2.3
File size: 15.9 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [restrFaninout.c]
4
5  PackageName [restr]
6
7  Synopsis [Routines in this file implement the Fanin and Fanin-Fanout oriented
8  restructuring heuristics.]
9
10  Description [Routines in the file implement the Fanin oriented and
11  Fanin-Fanout oriented restructuring heuristics.
12
13  Please refer to "A symbolic algorithm for low power sequential synthesis,"
14  ISLPED 97, for more details.]
15
16  SeeAlso     [restrHammingD.c restrCProj.c]
17
18  Author      [Balakrishna Kumthekar <kumtheka@colorado.edu>]
19
20  Copyright   [This file was created at the University of Colorado at
21  Boulder.  The University of Colorado at Boulder makes no warranty
22  about the suitability of this software for any purpose.  It is
23  presented on an AS IS basis.]
24
25******************************************************************************/
26
27#include "restrInt.h"
28
29/*---------------------------------------------------------------------------*/
30/* Constant declarations                                                     */
31/*---------------------------------------------------------------------------*/
32
33
34/*---------------------------------------------------------------------------*/
35/* Type declarations                                                         */
36/*---------------------------------------------------------------------------*/
37
38
39/*---------------------------------------------------------------------------*/
40/* Structure declarations                                                    */
41/*---------------------------------------------------------------------------*/
42
43/*---------------------------------------------------------------------------*/
44/* Variable declarations                                                     */
45/*---------------------------------------------------------------------------*/
46
47
48/*---------------------------------------------------------------------------*/
49/* Macro declarations                                                        */
50/*---------------------------------------------------------------------------*/
51
52
53/**AutomaticStart*************************************************************/
54
55/*---------------------------------------------------------------------------*/
56/* Static function prototypes                                                */
57/*---------------------------------------------------------------------------*/
58
59
60/**AutomaticEnd***************************************************************/
61
62
63/*---------------------------------------------------------------------------*/
64/* Definition of exported functions                                          */
65/*---------------------------------------------------------------------------*/
66
67/*---------------------------------------------------------------------------*/
68/* Definition of internal functions                                          */
69/*---------------------------------------------------------------------------*/
70
71/**Function********************************************************************
72
73  Synopsis [This routine implements the Fanin oriented and Fanin-Fanout
74  oriented restructuring heuristics. Returns the BDD of the restructured STG.]
75
76  Description [This routine implements the Fanin oriented and Fanin-Fanout
77  oriented restructuring heuristics. Returns the BDD of the restructured STG.
78
79  <tt>equivRel</tt> is the state equivalence relation of the
80  fsm. <tt>oldTR</tt> if the state transition relation.  <tt>addPTR</tt> is the
81  0-1 ADD of the augmented transition relation. <tt>possessedProbMatrix</tt> is
82  the weighted graph representing the augmented transition relation. The edge
83  weights are the prob. of transition of that edge. <tt>stateProbs</tt> is an
84  ADD representing the steady state probabilities of the fsm. <tt>piVars</tt>
85  are the BDD variables for primary inputs. <tt>heuristic</tt> takes on two
86  values: RestrFanin_c and RestrFaninFanout_c.
87
88  Please refer to "A Symbolic Algorithm for Low-Power Sequential
89  Synthesis", ISLPED 97 for more details.]
90
91  SideEffects [<tt>addPtr</tt> and <tt>possessedProbMatrix</tt> are
92  dereferenced in this routine. <tt>outBdds</tt> and <tt>newInit</tt> are
93  changed to reflect the restructured STG.]
94
95  SeeAlso     [RestrMinimizeFsmByCProj RestrSelectLeastHammingDStates]
96******************************************************************************/
97bdd_node *
98RestrMinimizeFsmByFaninFanout(
99  bdd_manager *ddManager,
100  bdd_node *equivRel,
101  bdd_node *oldTR,
102  bdd_node **addPTR,
103  bdd_node **possessedProbMatrix,
104  bdd_node *initBdd,
105  bdd_node *reachable,
106  bdd_node *stateProbs,
107  bdd_node **piVars,
108  bdd_node **xVars,
109  bdd_node **yVars,
110  bdd_node **uVars,
111  bdd_node **vVars,
112  int nVars,
113  int nPi,
114  RestructureHeuristic heuristic,
115  array_t **outBdds,
116  bdd_node **newInit)
117{
118  bdd_node *temp1, *temp2, *temp3;
119  bdd_node *xCube, *yCube;
120  bdd_node *Rxy,*Rxv;
121  bdd_node *RxvgtRxy, *RxveqRxy; /* These are BDDs */
122  bdd_node **xAddVars,**yAddVars,**vAddVars;
123  bdd_node *priority, *result, *matrix;
124  bdd_node *newEquivRel;
125  bdd_node *oneInitState;
126  bdd_node *hammingWeight;
127  bdd_node *lhs, *rhs;
128  bdd_node *bddCProj;
129  bdd_node *bddCProjvy, *addCProjvy;
130  bdd_node *newCProjvy, *newCProjux;
131  bdd_node *zeroProbs, *zeroProbFactor;
132  bdd_node *weight;
133
134  array_t *newOutBdds;
135  int i, index;
136
137  /* Collect the ADD variables for futre use */
138  xAddVars = ALLOC(bdd_node *,nVars);
139  yAddVars = ALLOC(bdd_node *,nVars);
140  vAddVars = ALLOC(bdd_node *,nVars);
141
142  for(i = 0; i < nVars; i++) {
143    index = bdd_node_read_index(yVars[i]);
144    bdd_ref(yAddVars[i] = bdd_add_ith_var(ddManager,index));
145    index = bdd_node_read_index(vVars[i]);
146    bdd_ref(vAddVars[i] = bdd_add_ith_var(ddManager,index));
147    index = bdd_node_read_index(xVars[i]);
148    bdd_ref(xAddVars[i] = bdd_add_ith_var(ddManager,index));
149  }
150
151  /* Restrict the equivalence relation only to the reachable states */
152  /* temp1 = R(v) */
153  bdd_ref(temp1 = bdd_bdd_swap_variables(ddManager,reachable,xVars,
154                                         vVars,nVars));
155  /* temp2 = R(y) */
156  bdd_ref(temp2 = bdd_bdd_swap_variables(ddManager,reachable,xVars,
157                                         yVars,nVars));
158  /* temp3 = R(v) * R(y) */
159  bdd_ref(temp3 = bdd_bdd_and(ddManager,temp1,temp2));
160  bdd_recursive_deref(ddManager,temp1);
161  bdd_recursive_deref(ddManager,temp2);
162  /* newEquivRel(v,y) = E(v,y) * R(v) * R(y) */
163  bdd_ref(newEquivRel = bdd_bdd_and(ddManager,equivRel,temp3));
164  bdd_recursive_deref(ddManager,temp3);
165
166  /* Select one state from the set of initial states */
167  oneInitState = bdd_bdd_pick_one_minterm(ddManager,initBdd,xVars,nVars);
168  bdd_ref(oneInitState);
169
170  /* Initially an arbitrary choice of a 'nominal representative' for each
171     equivalence class is made--using compatible projection--with the initial
172     state as the reference vertex. bddCProj is as the name indicates, in terms
173     of y and x. bddCProj refers to $\Psi(x,y)$ in the ISLPED 97 reference. */
174
175  bdd_ref(temp1 = bdd_bdd_swap_variables(ddManager,oneInitState,xVars,
176                                         vVars,nVars));
177  bdd_recursive_deref(ddManager,oneInitState);
178  bdd_ref(bddCProjvy = bdd_bdd_cprojection(ddManager, newEquivRel, temp1));
179  bdd_recursive_deref(ddManager,newEquivRel);
180  bdd_recursive_deref(ddManager,temp1);
181  bdd_ref(bddCProj = bdd_bdd_swap_variables(ddManager,bddCProjvy,vVars,
182                                            xVars,nVars));
183  bdd_ref(addCProjvy = bdd_bdd_to_add(ddManager,bddCProjvy));
184  bdd_recursive_deref(ddManager,bddCProjvy);
185
186  /* Let's compute the weight matrix */
187  /* hammingWeight equal (nVars - HD(x,y)) */
188  bdd_ref(temp1 = bdd_add_const(ddManager,(double)nVars));
189  bdd_ref(temp2 = bdd_add_hamming(ddManager,xVars,yVars,nVars));
190  bdd_ref(hammingWeight = bdd_add_apply(ddManager,bdd_add_minus,
191                                        temp1,temp2));
192  bdd_recursive_deref(ddManager,temp1);
193  bdd_recursive_deref(ddManager,temp2);
194
195  /* temp1 = possessedProbMatrix * (nVars - HD(x,y)) */
196  bdd_ref(temp1 = bdd_add_apply(ddManager,bdd_add_times,hammingWeight,
197                                *possessedProbMatrix));
198  bdd_recursive_deref(ddManager,*possessedProbMatrix);
199
200  /* matrix = possessedProbMatrix * (nVars - HD(x,y)) * stateProbs */
201  bdd_ref(matrix = bdd_add_apply(ddManager,bdd_add_times,temp1,
202                                 stateProbs));
203  bdd_recursive_deref(ddManager,temp1);
204
205  /* Compute the contribution of the edges that have a state with zero
206   * probability as its source node. The contribution is measured in terms
207   * of the hamming distance between the end points of the edge.
208   * The total weight on any edge is the sum of "matrix" as computed
209   * above and "zeroProbFactor" as computed below.
210   */
211  bdd_ref(temp1 = bdd_add_bdd_strict_threshold(ddManager,stateProbs,0.0));
212  bdd_ref(temp2 = bdd_not_bdd_node(temp1));
213  bdd_recursive_deref(ddManager,temp1);
214  /* zeroProbs evaluates to 1 for those states which have zero steady state
215   * probability. zeroProbs is a 0-1 ADD.
216   */
217  bdd_ref(zeroProbs = bdd_bdd_to_add(ddManager,temp2));
218  bdd_recursive_deref(ddManager,temp2);
219
220  /* temp1 = (1 - HD(x,y)/nVars) */
221  bdd_ref(temp2 = bdd_add_const(ddManager,(double)nVars));
222  bdd_ref(temp1 = bdd_add_apply(ddManager,bdd_add_divide,hammingWeight,
223                                temp2));
224  bdd_recursive_deref(ddManager,temp2);
225  bdd_recursive_deref(ddManager,hammingWeight);
226
227  /* temp2 = (1 - HD(x,y)/nVars) * zeroProbs(x) */
228  bdd_ref(temp2 = bdd_add_apply(ddManager,bdd_add_times,temp1,zeroProbs));
229  bdd_recursive_deref(ddManager,temp1);
230  bdd_recursive_deref(ddManager,zeroProbs);
231
232  /* zeroProbFactor = (1 - HD(x,y)/nVars) * zeroProbs(x) * addPTR */
233  bdd_ref(zeroProbFactor = bdd_add_apply(ddManager,bdd_add_times,
234                                         *addPTR,temp2));
235  bdd_recursive_deref(ddManager,*addPTR);
236  bdd_recursive_deref(ddManager,temp2);
237
238  /* Total edge weight = matrix + zeroProbFactor */
239  bdd_ref(weight = bdd_add_apply(ddManager,bdd_add_plus,matrix,
240                                 zeroProbFactor));
241  bdd_recursive_deref(ddManager,matrix);
242  bdd_recursive_deref(ddManager,zeroProbFactor);
243   
244  /* lhs = Abs(x) (weight(x,y)*CProj(v,y)) */
245  bdd_ref(temp1 = bdd_add_apply(ddManager,bdd_add_times,weight,
246                                addCProjvy));
247  bdd_ref(temp3 = bdd_add_compute_cube(ddManager,xAddVars,NIL(int),nVars));
248  bdd_ref(lhs = bdd_add_exist_abstract(ddManager,temp1,temp3));
249  bdd_recursive_deref(ddManager,temp1);
250  bdd_recursive_deref(ddManager,temp3);
251
252  /* Now lhs is a function of x and y */
253  bdd_ref(temp1 = bdd_add_swap_variables(ddManager,lhs,vAddVars,xAddVars,
254                                         nVars));
255  bdd_recursive_deref(ddManager,lhs);
256  lhs = temp1;
257
258  if (heuristic == RestrFaninFanout_c) {
259    /* let's compute the rhs */
260    bdd_ref(temp1 = bdd_add_swap_variables(ddManager,addCProjvy,yAddVars,
261                                           xAddVars, nVars));
262    bdd_recursive_deref(ddManager,addCProjvy);
263    bdd_ref(rhs = bdd_add_apply(ddManager,bdd_add_times,weight,temp1));
264    bdd_recursive_deref(ddManager,temp1);
265    bdd_recursive_deref(ddManager,weight);
266    temp1 = rhs;
267    bdd_ref(temp3 = bdd_add_compute_cube(ddManager,yAddVars,NIL(int),nVars));
268    bdd_ref(rhs = bdd_add_exist_abstract(ddManager,temp1,temp3));
269    bdd_recursive_deref(ddManager,temp1);
270    bdd_recursive_deref(ddManager,temp3);
271
272    /* rhs is now a function of x and y */
273    bdd_ref(temp1 = bdd_add_swap_variables(ddManager,rhs,xAddVars,
274                                           yAddVars,nVars));
275    bdd_recursive_deref(ddManager,rhs);
276    bdd_ref(rhs = bdd_add_swap_variables(ddManager,temp1,vAddVars,
277                                         xAddVars,nVars));
278    bdd_recursive_deref(ddManager,temp1);
279
280    /* take the average of lhs and rhs */
281    bdd_ref(temp1 = bdd_add_apply(ddManager,bdd_add_plus,lhs,rhs));
282    bdd_recursive_deref(ddManager,lhs);
283    bdd_recursive_deref(ddManager,rhs);
284    bdd_ref(temp2 = bdd_add_const(ddManager,(double)2.0));
285    bdd_ref(Rxy = bdd_add_apply(ddManager,bdd_add_divide,temp1,temp2));
286    bdd_recursive_deref(ddManager,temp1);
287    bdd_recursive_deref(ddManager,temp2); 
288  }
289  else {
290    bdd_recursive_deref(ddManager,weight);
291    bdd_recursive_deref(ddManager,addCProjvy);
292    Rxy = lhs;
293  }
294
295  /* Rxv = Rxy(x,v) */
296  bdd_ref(Rxv = bdd_add_swap_variables(ddManager,Rxy,yAddVars,vAddVars,
297                                       nVars));
298  /* RxvgtRxy(x,v,y) = Rxv(x,v) > Rxy(x,y) */
299  bdd_ref(temp1 = bdd_add_apply(ddManager,RestrAddMaximum,Rxv,Rxy));
300  bdd_ref(RxvgtRxy = bdd_add_bdd_threshold(ddManager,temp1,(double) 1.0));
301  bdd_recursive_deref(ddManager,temp1);
302
303  /* RxveqRxy(x,v,y) = Rxz(x,v) == Rxy(x,y) */
304  bdd_ref(temp1 = bdd_add_apply(ddManager,RestrAddEqual,Rxv,Rxy));
305  bdd_ref(RxveqRxy = bdd_add_bdd_threshold(ddManager,temp1,(double) 1.0));
306  bdd_recursive_deref(ddManager,temp1);
307  bdd_recursive_deref(ddManager,Rxv);
308  bdd_recursive_deref(ddManager,Rxy);
309
310  /* temp1 is the tie-break function. (RxveqRxy . temp1 = temp2)*/
311  bdd_ref(temp1 = bdd_dxygtdxz(ddManager,nVars,xVars,yVars,vVars));
312  bdd_ref(temp2 = bdd_bdd_and(ddManager,RxveqRxy,temp1));
313  bdd_recursive_deref(ddManager,temp1);
314  bdd_recursive_deref(ddManager,RxveqRxy);
315
316  bdd_ref(priority = bdd_bdd_or(ddManager,temp2,RxvgtRxy));
317  bdd_recursive_deref(ddManager,RxvgtRxy);
318  bdd_recursive_deref(ddManager,temp2);
319
320  /* temp1 represents the pair (oldrepresentative,newprepresentative) in terms
321   of x and y respectively */
322  bdd_ref(temp1 = bdd_priority_select(ddManager,bddCProj,xVars,
323                                      yVars,vVars,priority,nVars,NULL));
324  bdd_recursive_deref(ddManager,priority);
325
326  bdd_ref(xCube = bdd_bdd_compute_cube(ddManager,xVars,NIL(int),nVars));
327  bdd_ref(yCube = bdd_bdd_compute_cube(ddManager,yVars,NIL(int),nVars));
328
329  /* newCProjvy is in terms of v,y */
330  /* v represents the new representative of equivalent states */
331
332  bdd_ref(temp2 = bdd_bdd_swap_variables(ddManager,temp1,yVars,vVars,
333                                         nVars));
334  bdd_recursive_deref(ddManager,temp1);
335  bdd_ref(newCProjvy = bdd_bdd_and_abstract(ddManager,bddCProj,temp2,
336                                            xCube));
337  bdd_recursive_deref(ddManager,bddCProj);
338  bdd_recursive_deref(ddManager,temp2);
339
340  bdd_ref(temp1 = bdd_bdd_swap_variables(ddManager,newCProjvy,yVars,
341                                         xVars,nVars));
342  bdd_ref(newCProjux = bdd_bdd_swap_variables(ddManager,temp1,vVars,
343                                              uVars,nVars));
344  bdd_recursive_deref(ddManager,temp1);
345
346  /* Change the output functions accordingly */
347  newOutBdds = array_alloc(bdd_node *,0);
348  arrayForEachItem(bdd_node *,*outBdds,i,temp3) {
349    bdd_ref(temp1 = bdd_bdd_and_abstract(ddManager,temp3,newCProjux,
350                                         xCube));
351    bdd_ref(temp2 = bdd_bdd_swap_variables(ddManager,temp1,uVars,xVars,
352                                           nVars));
353    bdd_recursive_deref(ddManager,temp1);
354    bdd_recursive_deref(ddManager,temp3);
355    array_insert_last(bdd_node *,newOutBdds,temp2);
356  }
357  array_free(*outBdds);
358  *outBdds = newOutBdds;
359
360  /* Change the initBdd accordingly */
361  bdd_ref(temp1 = bdd_bdd_and_abstract(ddManager,initBdd,newCProjux,xCube));
362  bdd_ref(*newInit = bdd_bdd_swap_variables(ddManager,temp1,uVars,xVars,
363                                            nVars));
364  bdd_recursive_deref(ddManager,temp1);
365
366  /* Compute the new transition relation w.r.t the new CProjection function.
367   * result = newCProjux * oldTR(x,y) * newCProjvy
368   */
369  bdd_ref(temp1 = bdd_bdd_and(ddManager,xCube,yCube));
370  bdd_recursive_deref(ddManager,xCube);
371  bdd_recursive_deref(ddManager,yCube);
372  bdd_ref(temp2 = bdd_bdd_and(ddManager,newCProjux,oldTR));
373  bdd_recursive_deref(ddManager,newCProjux);
374  bdd_ref(temp3 = bdd_bdd_and(ddManager,temp2,newCProjvy));
375  bdd_recursive_deref(ddManager,newCProjvy);
376  bdd_recursive_deref(ddManager,temp2);
377  bdd_ref(result = bdd_bdd_exist_abstract(ddManager,temp3,temp1));
378  bdd_recursive_deref(ddManager,temp1);
379  bdd_recursive_deref(ddManager,temp3);
380
381  bdd_ref(temp1 = bdd_bdd_swap_variables(ddManager,result,uVars,xVars,
382                                         nVars));
383  bdd_ref(temp2 = bdd_bdd_swap_variables(ddManager,temp1,vVars,yVars,
384                                         nVars));
385  bdd_recursive_deref(ddManager,temp1);
386  bdd_recursive_deref(ddManager,result);
387  result = temp2;
388
389  /* Clean up */
390  for(i = 0; i < nVars; i++) {
391    bdd_recursive_deref(ddManager,yAddVars[i]);
392    bdd_recursive_deref(ddManager,vAddVars[i]);
393    bdd_recursive_deref(ddManager,xAddVars[i]);
394  }
395  FREE(yAddVars);
396  FREE(vAddVars);
397  FREE(xAddVars);
398 
399  /* Return the restructred STG */
400  return result;
401}
402
403
404/*---------------------------------------------------------------------------*/
405/* Definition of static functions                                            */
406/*---------------------------------------------------------------------------*/
Note: See TracBrowser for help on using the repository browser.