source: vis_dev/vis-2.3/src/restr/restrRestructure.c @ 97

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

vis2.3

File size: 42.5 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [restrRestructure.c]
4
5  PackageName [restr]
6
7  Synopsis [This file contains a main procedure that restructures an STG and
8  transforms it into a new multilevel circuit.]
9
10  Description [This file contains a main procedure that restructures an STG and
11  transforms it into a new multilevel circuit.
12
13  Please refer to "A symbolic algorithm for low power sequential synthesis,"
14  ISLPED 97, for more details.]
15
16  SeeAlso     [restrHammingD.c restrFaninout.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/*---------------------------------------------------------------------------*/
46extern int restrCreatedPart;
47extern int restrCreatedFsm;
48extern boolean restrVerbose;
49
50/*---------------------------------------------------------------------------*/
51/* Macro declarations                                                        */
52/*---------------------------------------------------------------------------*/
53
54
55/**AutomaticStart*************************************************************/
56
57/*---------------------------------------------------------------------------*/
58/* Static function prototypes                                                */
59/*---------------------------------------------------------------------------*/
60
61static array_t * BuildFunctions(graph_t *partition, array_t *rootNames);
62static bdd_node ** AddPowerSolve(bdd_manager *mgr, bdd_node *bddTr, bdd_node *init, bdd_node **x, bdd_node **y, bdd_node **pi, st_table *inputProb, int nVars, int nPi);
63static bdd_node * PerformRestructure(bdd_manager *ddManager, bdd_node *prunedTR, bdd_node *equivRel, bdd_node *reachable, bdd_node *initBdd, bdd_node **piVars, bdd_node **xVars, bdd_node **yVars, bdd_node **uVars, bdd_node **vVars, st_table *inputProb, int nVars, int nPi, RestructureHeuristic heuristic, boolean equivClasses, array_t **outBdds, bdd_node **newInit, bdd_node **stateProbs);
64static st_table * CreateNameToMvfTable(bdd_manager *ddManager, array_t *outBdds, array_t *nextBdds, array_t *outputArray, array_t *tranFunArray);
65static st_table * CreateCareTable(Ntk_Network_t *network, mdd_t *reachMdd);
66static enum st_retval StMvfFree(char *key, char *value, char *arg);
67static void CountEquivalentClasses(bdd_manager *ddManager, bdd_node *equivRel, bdd_node *initBdd, bdd_node **xVars, bdd_node **uVars, int nVars);
68static array_t * GetBddArrayFromMvfArray(array_t *mvfArray);
69static bdd_node * DoMarkovPowerAnalysis(bdd_manager *ddManager, bdd_node *prunedTR, bdd_node *initBdd, bdd_node **piVars, bdd_node **xVars, bdd_node **yVars, st_table *inputProb, int nVars, int nPi);
70static array_t * ExtractTransitionFuns(bdd_manager *ddManager, bdd_node *finalTR, bdd_node **yVars, int nVars);
71static array_t * GetBddArrayFromNameArray(Fsm_Fsm_t *fsm, array_t *nameArray);
72static void ExpandReachableSet(bdd_manager *ddManager, bdd_node **reachable, bdd_node *equivRel, bdd_node **xVars, bdd_node **uVars, int nVars);
73static graph_t * CreateNewPartition(Ntk_Network_t *network, bdd_manager *ddManager, array_t *outBdds, array_t *nextBdds, array_t *outputArray, array_t *tranFunArray);
74static Fsm_Fsm_t * CreateNewFsm(Ntk_Network_t *network, graph_t *partition, bdd_manager *ddManager, bdd_node *finalTR, bdd_node *initBdd, bdd_node *reachable, bdd_node *stateProbs, bdd_node **xVars, bdd_node **yVars, bdd_node **piVars, st_table *inputProb, int nVars, int nPi);
75
76/**AutomaticEnd***************************************************************/
77
78
79/*---------------------------------------------------------------------------*/
80/* Definition of exported functions                                          */
81/*---------------------------------------------------------------------------*/
82
83/*---------------------------------------------------------------------------*/
84/* Definition of internal functions                                          */
85/*---------------------------------------------------------------------------*/
86
87/**Function********************************************************************
88
89  Synopsis [This function performs the complete task of STG restructuring and
90  logic implementation.]
91
92  Description [The STG restructuring process proceeds as follows: First a state
93  equivalence relation E(x,y) is derived from the current STG of the finite
94  state machine. If the parameter <tt>nonReachEquiv</tt> is set E(x,y) is used
95  to extend the set of reachable states R(x) to include those states equivalent
96  to R(x) but unreachable. This sometimes provides extra flexibility when
97  choosing an edge. To perform the restructuring transformation, edges are
98  first added (clearly driven by E(x,y)) to the original STG and then
99  undesirable edges are removed, in such a way that the functional behavior of
100  the machine is not affected. We say that the original STG is transformed into
101  an <tt>augmented</tt> STG.
102
103  The steady state probabilities of the STG are computed using Markovian
104  analysis. The edges of the augmented STG are then labeled by a cost function
105  which depends on the absolute transition probability and hamming distance
106  between the ends of the edge. After the appropriate <tt>heuristic</tt> is
107  applied, the new (restructured) STG is then translated in to a multi-level
108  boolean network.
109
110  <tt>heuristic</tt> takes on four options: ham: Hamming distance based
111  heuristic is used, fanin: Fanin oriented heuristic, faninout: Fanin-Fanout
112  oriented heuristic, cproj: C-Projection. For more information please refer to
113  "A symbolic algorithm for low power sequential synthesis," ISLPED 97.
114
115  <tt>equivClasses</tt> prints the number of equivalent classes in the STG.
116
117  <tt>inputProb</tt> is optional. If not specified, equiprobabale primary
118  inputs are assumed. Else, the table contains the pair, (PI_name,prob), where
119  <tt>prob</tt> is the probability of the PI signal being 1.
120
121  <tt>synthInfo</tt> specifies synthesis specific options. For more information
122  look at synth.h]
123
124  The BDD variable order at the end of the algorithm is dumped into
125  <tt>orderFileName</tt>.
126
127  SideEffects [Network partition and FSM data structure are hooked to the
128  network if necessary. They are however, cleared at the end of this
129  procedure.]
130
131  SeeAlso     [Synth_InitializeInfo]
132
133******************************************************************************/
134int
135RestrCommandRestructureFsm(
136  Fsm_Fsm_t *fsm,                         
137  RestructureHeuristic heuristic,
138  char *orderFileName,
139  boolean equivClasses,
140  boolean nonReachEquiv,
141  boolean eqvMethod,
142  st_table *inputProb,
143  Synth_InfoData_t *synthInfo)
144{
145
146  graph_t *partition;
147  Ntk_Network_t *network1;
148  bdd_manager *ddManager;
149
150  array_t *outputArray, *tranFunArray;
151  array_t *outBdds, *nextBdds;
152  array_t *tranRelationPair;
153  array_t *newStateVars;
154
155  st_table *careTable;
156
157  int i;
158  int nVars, nPi;
159  int noRestruct = 0;
160  boolean status;
161
162  bdd_node *Lambda, *productTranRel, *prunedTR, *initialTR;
163  bdd_node *equivRel;
164  bdd_node *stateProbs;
165  bdd_node *finalTR = NIL(bdd_node);
166  bdd_node **xVars,**yVars,**uVars,**vVars;
167  bdd_node **piVars;
168  bdd_node *ddTemp, *reachable, *initBdd;
169  bdd_node *newInit;
170
171  mdd_t *reachStates, *mddTemp;
172  mdd_t *careMdd;
173
174  FILE *outFile;
175
176  network1 = Fsm_FsmReadNetwork(fsm);
177  ddManager = (bdd_manager *)Ntk_NetworkReadMddManager(network1);
178
179  /* Get the bdd_node for primary, present and next state variables.*/
180  piVars = RestrBddNodeArrayFromIdArray(ddManager, 
181                                        Fsm_FsmReadInputVars(fsm));
182  xVars = RestrBddNodeArrayFromIdArray(ddManager, 
183                                       Fsm_FsmReadPresentStateVars(fsm));
184  yVars = RestrBddNodeArrayFromIdArray(ddManager,
185                                       Fsm_FsmReadNextStateVars(fsm));
186  /* Create new state variables for duplicate machine. */
187  newStateVars = RestrCreateNewStateVars(network1, ddManager,xVars,yVars);
188  uVars = RestrBddNodeArrayFromIdArray(ddManager,
189                                       array_fetch(array_t *, 
190                                                   newStateVars, 0));
191  vVars = RestrBddNodeArrayFromIdArray(ddManager,
192                                       array_fetch(array_t *, 
193                                                   newStateVars, 1));
194
195  /* Free memory: Delete the id array for new state variables.*/
196  array_free(array_fetch(array_t *,newStateVars,0));
197  array_free(array_fetch(array_t *,newStateVars,1));
198  array_free(newStateVars);
199
200  /* outputArray is the list of primary outputs. It is my responsibility to
201  free it later. Both outputArray and tranFunArray are char * arrays.  Get the
202  BDDs for output functions and transition functions.  Duplicate functions are
203  returned.*/
204
205  /* tranFunArray should not be freed */
206  outputArray = RestrGetOutputArray(network1);
207  tranFunArray = Fsm_FsmReadNextStateFunctionNames(fsm);
208  outBdds = GetBddArrayFromNameArray(fsm,outputArray);
209  nextBdds = GetBddArrayFromNameArray(fsm,tranFunArray);
210
211  nVars = array_n(Fsm_FsmReadNextStateVars(fsm));
212  nPi = array_n(Fsm_FsmReadInputVars(fsm));
213
214  /* Compute Lambda = AND (out1 xnor out1$NTK2) and Transition relation.
215   out1$NTK2 is the corresponding primary output (of output1) in the duplicate
216   machine.*/
217  if (restrVerbose) {
218    fprintf(vis_stdout,"** restr info: Computing product output ... ");
219  }
220  Lambda = RestrCreateProductOutput(ddManager,outBdds,xVars, uVars, nVars);
221  if (restrVerbose) {
222    fprintf(vis_stdout,"Done.\n");
223  }
224
225  if (restrVerbose) {
226    fprintf(vis_stdout,"** restr info: Computing TR of product machine ... ");
227  }
228  /* Compute the transition relation for both the single FSM and the product
229     machine.  tranRelationPair[0] is the TR of single FSM and
230     tranRelationPair[1] is the TR of product machine. 
231     TR(x,w,y) = \prod_{i=0}^{i=n-1} (y_i \equiv f_i(w,x))
232     productTR(x,u,w,y,v) = TR(x,w,y) * TR(u,w,v) */
233  tranRelationPair = RestrComputeTRWithIds(ddManager,nextBdds,xVars, yVars,
234                                           uVars,vVars,nVars);
235  if (restrVerbose) {
236    fprintf(vis_stdout,"Done.\n");
237  }
238
239  productTranRel = array_fetch(bdd_node *,tranRelationPair,1);
240
241  /* Compute the state equivalence relation for the FSM */
242  /* The support of equivRel is xVars and uVars. */
243  if (restrVerbose) {
244    fprintf(vis_stdout,"** restr info: Computing the equivalence relation ... ");
245  }
246
247  if (eqvMethod) {
248    equivRel = RestrComputeEquivRelationUsingCofactors(ddManager,Lambda,
249                                                       productTranRel,
250                                                       xVars, yVars, uVars,
251                                                       vVars, piVars,
252                                                       nVars, nPi,
253                                                       restrVerbose);
254    bdd_recursive_deref(ddManager,Lambda);
255  } else {
256    equivRel = RestrGetEquivRelation(ddManager,Lambda,productTranRel,
257                                     xVars,yVars,uVars,vVars,
258                                     piVars,nVars,nPi,restrVerbose);
259    bdd_recursive_deref(ddManager,Lambda);
260  }
261  if (restrVerbose) {
262    fprintf(vis_stdout,"Done.\n");
263  }
264  /* Delete the product transition relation, as we no longer need it. */
265  bdd_recursive_deref(ddManager,productTranRel);
266
267  /* Compute the initial states */
268  mddTemp = Fsm_FsmComputeInitialStates(fsm);
269  initBdd = bdd_extract_node_as_is(mddTemp);
270  bdd_ref(initBdd);
271  mdd_free(mddTemp);
272
273  /* Compute the reachable states. */
274  reachStates = Fsm_FsmComputeReachableStates(fsm,0,0,0,0,0,0,1000,
275                                              Fsm_Rch_Default_c,0,0,
276                                              NIL(array_t),FALSE, NIL(array_t));
277
278  reachable = bdd_extract_node_as_is(reachStates);
279  bdd_ref(reachable);
280  mdd_free(reachStates);
281
282  /* Check to see if there are any usable equivalence classes */
283  if (bdd_count_minterm(ddManager,equivRel,2*nVars) == pow(2.0,nVars)) {
284    fprintf(vis_stdout,"** restr info: Number of equivalence classes equals ");
285    fprintf(vis_stdout,"number of possible states. \n");
286    fprintf(vis_stdout,"** restr info: Restructuring will not help.\n");
287    fprintf(vis_stdout,"** restr info: Proceeding with synthesis.\n");
288    bdd_recursive_deref(ddManager,equivRel);
289    /* Do not perform restructuring */
290    noRestruct = 1;
291  }
292
293  /* Expand the reachable set R(x) to include those states which are equivalent
294   to R(x) but unreachable. */
295  if(nonReachEquiv && !noRestruct) {
296    ExpandReachableSet(ddManager,&reachable,equivRel,xVars,uVars,nVars);
297  }
298
299  if (noRestruct) {
300    /* Only synthesize the network */
301    bdd_recursive_deref(ddManager,equivRel);
302    bdd_recursive_deref(ddManager,
303                        array_fetch(bdd_node *,tranRelationPair,0));
304    array_free(tranRelationPair);
305  } else {
306    /* Constrain the original TR */
307    initialTR = array_fetch(bdd_node *, tranRelationPair, 0);
308    /* bdd_ref(prunedTR = bdd_bdd_and(ddManager,initialTR,reachable)); */
309    bdd_ref(prunedTR = initialTR);
310    bdd_recursive_deref(ddManager,initialTR);
311    array_free(tranRelationPair);
312
313    finalTR = PerformRestructure(ddManager,prunedTR,equivRel,reachable,
314                                   initBdd,piVars,xVars,yVars,uVars,
315                                   vVars,inputProb,nVars,nPi,heuristic,
316                                   equivClasses,&outBdds,&newInit,
317                                   &stateProbs);
318    /* equivRel is dereferenced in the above procedure */
319    if (prunedTR == finalTR) {
320      fprintf(vis_stdout,"** restr info: Restructuring produces no changes. \n");
321      fprintf(vis_stdout,"** restr info: Proceeding with synthesis. \n");
322      bdd_recursive_deref(ddManager,stateProbs);
323      noRestruct = 1;
324    }
325
326    bdd_recursive_deref(ddManager,prunedTR);
327    bdd_recursive_deref(ddManager,initBdd);
328
329    /* reachable can be deleted after computing the new reachable states.  Also
330     need to perform markov analysis to find final bit change. */
331    initBdd = newInit;
332    if (!noRestruct) {
333      arrayForEachItem(bdd_node *, nextBdds, i, ddTemp) {
334        bdd_recursive_deref(ddManager,ddTemp);
335      }
336      array_free(nextBdds);
337      nextBdds = ExtractTransitionFuns(ddManager,finalTR,yVars,nVars);
338    }
339  }
340
341  /* Create a partition for the new view of the fsm/network */
342  if (!noRestruct) {
343    partition = CreateNewPartition(network1,ddManager,outBdds,nextBdds,
344                                   outputArray,tranFunArray);
345    array_free(outBdds);
346    array_free(nextBdds);
347    /* Create the FSM and perform markov ananlysis */
348    /* finalTR, stateProbs and reachabale are deleted in CreateNewFsm */
349    fsm = CreateNewFsm(network1,partition,ddManager,finalTR,initBdd,
350                       reachable,stateProbs,xVars,yVars,piVars,
351                       inputProb,nVars,nPi);
352  } else {
353    /* Remove the outBdds, nextBdds */
354    arrayForEachItem(bdd_node *, outBdds, i, ddTemp) {
355      bdd_recursive_deref(ddManager,ddTemp);
356    }
357    arrayForEachItem(bdd_node *, nextBdds, i, ddTemp) {
358      bdd_recursive_deref(ddManager,ddTemp);
359    }
360    array_free(outBdds);
361    array_free(nextBdds);
362  }
363
364  /* First create the care table for next state and primary output
365   functions. */
366  careMdd = Fsm_FsmComputeReachableStates(fsm,0,0,0,0,0,0,1000,
367                                          Fsm_Rch_Default_c,0,0,
368                                          NIL(array_t),FALSE, NIL(array_t));
369
370  careTable = CreateCareTable(network1,careMdd);
371
372  /* Synthesize the restructured FSM */
373  status = Synth_SynthesizeFsm(fsm,careTable,synthInfo,0);
374
375  /* Clean up */
376  if (!noRestruct) {
377    Ntk_NetworkFreeApplInfo(network1,RESTR_PART_NETWORK_APPL_KEY);
378    Ntk_NetworkFreeApplInfo(network1,RESTR_FSM_NETWORK_APPL_KEY);
379  }
380  mdd_free(careMdd);
381  st_free_table(careTable);
382
383  /* Dump the current BDD variable order, for future use. */
384  if(orderFileName) {
385    outFile = fopen(orderFileName,"w");
386    if(outFile) {
387      int size = array_n(mdd_ret_mvar_list(ddManager));
388      int index;
389      mvar_type var;
390      for(i = 0; i < size;i++) {
391        index = bdd_get_id_from_level(ddManager,i);
392        var = mdd_get_var_by_id(ddManager,index);
393        fprintf(outFile,"%s\n",var.name);
394      }
395      fclose(outFile);
396    } else {
397      fprintf(vis_stderr,"** restr error: Cannot open %s .\n",orderFileName);
398    }
399  }
400
401  /* Clean up */
402  for(i = 0; i < nVars; i++) {
403    bdd_recursive_deref(ddManager,xVars[i]);
404    bdd_recursive_deref(ddManager,yVars[i]);
405    bdd_recursive_deref(ddManager,uVars[i]);
406    bdd_recursive_deref(ddManager,vVars[i]);
407  }
408  for(i = 0 ; i < nPi; i++) {
409    bdd_recursive_deref(ddManager,piVars[i]);
410  }
411  FREE(xVars);
412  FREE(yVars);
413  FREE(uVars);
414  FREE(vVars);
415  FREE(piVars);
416
417  array_free(outputArray);
418
419  return (status);
420}
421
422
423/*---------------------------------------------------------------------------*/
424/* Definition of static functions                                            */
425/*---------------------------------------------------------------------------*/
426
427/**Function********************************************************************
428
429  Synopsis [Returns an array of Mvfs given node names.]
430
431  SideEffects [None]
432
433  SeeAlso     []
434
435******************************************************************************/
436static array_t *
437BuildFunctions(
438  graph_t *partition,
439  array_t *rootNames)
440{
441  char *name;
442  vertex_t *vertexPtr;
443  Mvf_Function_t *mvf1;
444  int i;
445  array_t *result;
446
447  result = array_alloc(Mvf_Function_t *,0);
448  arrayForEachItem(char *,rootNames,i,name) {
449    vertexPtr = Part_PartitionFindVertexByName(partition,name);
450    mvf1 = Mvf_FunctionDuplicate(Part_VertexReadFunction(vertexPtr));
451    array_insert(Mvf_Function_t *,result,i,mvf1);
452  }
453
454  return result;
455}
456
457/**Function********************************************************************
458
459  Synopsis [Performs markovian analysis.]
460
461  Description [Returns a pair of ADDs. The ADD for steady state
462  probabilities is at index 0 and the one-step transition probability
463  is returned in index 1. bddTr is the BDD of the transition relation
464  representing the STG. init is an ADD of initial probability vector.]
465
466  SideEffects [None]
467
468  SeeAlso     []
469
470******************************************************************************/
471static bdd_node **
472AddPowerSolve(
473  bdd_manager   *mgr,
474  bdd_node      *bddTr,         
475  bdd_node      *init,   
476  bdd_node      **x,
477  bdd_node      **y,
478  bdd_node      **pi,
479  st_table      *inputProb,
480  int            nVars,
481  int            nPi)
482{
483  bdd_node      *temp1, *temp, *q, *Correction;
484  bdd_node        **result, *tr;
485  bdd_node        **xAddVars, **yAddVars;
486  bdd_node      *initG, *NewG;
487  bdd_node      *inputCube,*xCube; 
488  bdd_node      *newTr, *probMatrix;
489  int           iter = 0;
490  int           i;
491  double        max,relTol = 0.0001;
492 
493  /* Initialize variables */
494  result = ALLOC(bdd_node *, 2);
495  xAddVars = ALLOC(bdd_node *, nVars);
496  yAddVars = ALLOC(bdd_node *, nVars);
497  for (i = 0; i < nVars; i++) {
498    bdd_ref(xAddVars[i] = bdd_add_ith_var(mgr, bdd_node_read_index(x[i])));
499    bdd_ref(yAddVars[i] = bdd_add_ith_var(mgr, bdd_node_read_index(y[i])));
500  }
501  bdd_ref(tr = bdd_bdd_to_add(mgr, bddTr));
502 
503  /* Create the input cube for abstraction */
504  bdd_ref(temp1 = bdd_bdd_compute_cube(mgr, pi, NIL(int), nPi));
505  bdd_ref(inputCube = bdd_bdd_to_add(mgr, temp1));
506  bdd_recursive_deref(mgr, temp1);
507
508  /* Compute the one-step transition probability matrix. */
509  if (inputProb) {
510    bdd_ref(probMatrix = Mark_addInProb(mgr,tr,inputCube,inputProb));
511    bdd_recursive_deref(mgr,inputCube);
512    bdd_recursive_deref(mgr,tr);
513  }
514  else {
515    bdd_ref(Correction = bdd_add_const(mgr,(1.0/(double)(1 << nPi))));
516    bdd_ref(q = bdd_add_exist_abstract(mgr,tr,inputCube));
517    bdd_recursive_deref(mgr,inputCube);
518    bdd_recursive_deref(mgr,tr);
519    /* apply correction to the transition relation matrix and print it */
520    bdd_ref(probMatrix = bdd_add_apply(mgr, bdd_add_times, q, Correction));
521    bdd_recursive_deref(mgr,Correction);
522    bdd_recursive_deref(mgr,q);
523  }
524  result[1] = probMatrix;
525
526  /* Prepare the initial prob. vector. and the transition prob. matrix. */
527  initG = bdd_add_swap_variables(mgr,init,xAddVars,yAddVars,nVars);
528  bdd_ref(initG);
529  /* Put transition prob. matrix in appropriate form (transpose). */
530  newTr = bdd_add_swap_variables(mgr,probMatrix,xAddVars,yAddVars,nVars);
531  bdd_ref(newTr);
532
533  /* Calculate the x-cube for abstraction */
534  bdd_ref(xCube = bdd_add_compute_cube(mgr,xAddVars,NIL(int),nVars));
535
536  /* Loop until convergence */
537  do {
538    iter++;
539    bdd_ref(temp = bdd_add_matrix_multiply(mgr,newTr,initG,yAddVars,nVars));
540    bdd_ref(temp1 = bdd_add_exist_abstract(mgr,temp,xCube));
541    bdd_ref(NewG = bdd_add_apply(mgr,bdd_add_divide,temp,temp1));
542    bdd_recursive_deref(mgr,temp);
543    bdd_recursive_deref(mgr,temp1);
544    temp = NewG; 
545    bdd_ref(q = bdd_add_swap_variables(mgr,temp,xAddVars,yAddVars,nVars));
546    max = bdd_add_value(bdd_add_find_max(mgr,initG));
547
548    if(bdd_equal_sup_norm(mgr,q,initG,relTol*max,0)) {
549      bdd_recursive_deref(mgr,initG);
550      bdd_recursive_deref(mgr,q);
551      bdd_recursive_deref(mgr,xCube);
552      bdd_recursive_deref(mgr,newTr);
553
554      bdd_ref(temp1 = bdd_add_apply(mgr,bdd_add_times,probMatrix,temp));
555      if (restrVerbose) {
556        fprintf(vis_stdout,"** restr info: Average state bit change = %f\n",
557                RestrAverageBitChange(mgr,temp1,x,y,nVars));
558      }
559     
560      bdd_recursive_deref(mgr,temp1);
561      for(i = 0;i < nVars; i++) {
562        bdd_recursive_deref(mgr,xAddVars[i]);
563        bdd_recursive_deref(mgr,yAddVars[i]);
564      }
565      FREE(xAddVars);
566      FREE(yAddVars);
567      result[0] = temp;
568      return result;
569    }
570    bdd_recursive_deref(mgr,initG);
571    bdd_recursive_deref(mgr,temp);
572    initG = q;
573
574  } while (1);
575
576} /* end of AddPowerSolve */
577
578/**Function********************************************************************
579
580  Synopsis [This routine performs the preprocessing steps of markovian analysis
581  and the augmented STG computation. After the preprocessing steps the core
582  restructuring steps are performed. Returns the BDD of the restructured STG.]
583
584  SideEffects [<tt>outBdds</tt>, <tt>newInit</tt> are changed to
585  reflect the restructured finite state machine. Steady state
586  probabilities are returned in <tt>stateProbs</tt>]
587
588  SeeAlso     []
589
590******************************************************************************/
591static bdd_node *
592PerformRestructure(
593  bdd_manager *ddManager,
594  bdd_node *prunedTR,
595  bdd_node *equivRel,
596  bdd_node *reachable,
597  bdd_node *initBdd,
598  bdd_node **piVars,
599  bdd_node **xVars,
600  bdd_node **yVars,
601  bdd_node **uVars,
602  bdd_node **vVars,
603  st_table *inputProb,
604  int nVars,
605  int nPi,
606  RestructureHeuristic heuristic,
607  boolean equivClasses,
608  array_t **outBdds,
609  bdd_node **newInit,
610  bdd_node **stateProbs)
611{
612  /* equivRel is a function of uVars and xVars */
613  /* prunedTR is a funciton of xVars, piVars and yVars */
614
615  bdd_node *possessedProbMatrix;
616  bdd_node *possessedTR = NIL(bdd_node);
617  bdd_node *addPTR;
618  bdd_node *finalTR;
619  bdd_node *ddTemp;
620  bdd_node *localStateProbs = NIL(bdd_node);
621
622  if(equivClasses) {
623    CountEquivalentClasses(ddManager,equivRel,initBdd,xVars,uVars,nVars);
624  }
625
626  /* Change the support of equivRel */
627  bdd_ref(ddTemp = bdd_bdd_swap_variables(ddManager,equivRel,xVars,yVars,
628                                          nVars));
629  bdd_recursive_deref(ddManager,equivRel);
630  bdd_ref(equivRel = bdd_bdd_swap_variables(ddManager,ddTemp,uVars,vVars,
631                                            nVars));
632  bdd_recursive_deref(ddManager, ddTemp);
633
634  /* The support of possessedTR is xVars and yVars and inputs.
635   * If there exists an edge between x and y, and y == v, then
636   * the following function adds an edge between x and v. These new
637   * edges are referred to as ghost edges.
638   */
639 
640  if (heuristic != RestrCProjection_c) {
641    possessedTR = RestrComputeTrWithGhostEdges(ddManager, yVars, vVars, 
642                                               prunedTR, equivRel, nVars);
643  }
644
645  /* stateProbs will not be used in the case of CProj and hammingD methods.  We
646   can still compute the stateProbs to find the initial average bit change on
647   the state lines. */
648  *stateProbs = DoMarkovPowerAnalysis(ddManager,prunedTR,
649                                      initBdd,piVars,xVars, 
650                                      yVars,inputProb,nVars,nPi);
651   
652  if (!(heuristic == RestrCProjection_c || heuristic == RestrHammingD_c)) {
653    bdd_node *temp, *cube;
654
655    bdd_ref(cube = bdd_bdd_compute_cube(ddManager,piVars,NIL(int),nPi));
656    bdd_ref(temp = bdd_bdd_exist_abstract(ddManager,possessedTR,cube));
657    bdd_ref(addPTR = bdd_bdd_to_add(ddManager,temp));
658    bdd_recursive_deref(ddManager,temp);
659
660    bdd_ref(temp = bdd_bdd_to_add(ddManager, possessedTR));
661    bdd_recursive_deref(ddManager, possessedTR);
662
663    /* possessedProbMatrix is a weighted augmented STG where the weights are
664       the transition probabilities */
665    if (inputProb) {
666      bdd_ref(possessedProbMatrix = Mark_addInProb(ddManager,temp,cube,
667                                                   inputProb));
668    } else {
669      /* Assume equi probable primary inputs */
670      bdd_node *q, *Correction;
671      bdd_node *inputCube;
672
673      bdd_ref(inputCube = bdd_bdd_to_add(ddManager,cube));
674      bdd_ref(Correction = bdd_add_const(ddManager,
675                                         (1.0/(double)(1 << nPi))));
676      bdd_ref(q = bdd_add_exist_abstract(ddManager,temp,inputCube));
677      bdd_ref(possessedProbMatrix = bdd_add_apply(ddManager,
678                                                  bdd_add_times,
679                                                  q, Correction));
680      bdd_recursive_deref(ddManager,Correction);
681      bdd_recursive_deref(ddManager,q);
682      bdd_recursive_deref(ddManager,inputCube);
683    }
684    bdd_recursive_deref(ddManager,cube);
685    bdd_recursive_deref(ddManager,temp);
686    localStateProbs = *stateProbs;
687  }
688
689  switch(heuristic) {
690  case RestrCProjection_c:
691    finalTR = RestrMinimizeFsmByCProj(ddManager,equivRel,
692                                      prunedTR,initBdd,
693                                      xVars,yVars,uVars,vVars,piVars,
694                                      nVars,nPi,outBdds,newInit);
695    break;
696  case RestrFanin_c:
697  case RestrFaninFanout_c:
698    ddTemp = bdd_read_background(ddManager);
699    bdd_set_background(ddManager, 
700                       bdd_read_plus_infinity(ddManager));
701
702    /* addPTR and possessedProbMatrix are deleted in the following
703     * procedure. */
704    finalTR = RestrMinimizeFsmByFaninFanout(ddManager,equivRel, prunedTR, 
705                                            &addPTR,&possessedProbMatrix,initBdd,
706                                            reachable,localStateProbs,piVars,xVars,
707                                            yVars, uVars,vVars,
708                                            nVars, nPi,heuristic,outBdds,newInit);
709
710    /* Replace the original background value */
711    bdd_set_background(ddManager,ddTemp);
712    break; 
713  case RestrHammingD_c: 
714  default : 
715   
716    /* BALA, testing ... */
717    /* Remove the edges out of the initial state. */
718    {
719/*       bdd_node *outEdges; */
720
721/*       bdd_ref(outEdges = bdd_bdd_and(ddManager,prunedTR,initBdd)); */
722/*       bdd_ref(adjustedTR = bdd_bdd_and(ddManager,prunedTR, */
723/*                                     bdd_not_bdd_node(outEdges))); */
724/*       finalTR = RestrSelectLeastHammingDStates(ddManager,adjustedTR, */
725/*                                             possessedTR,xVars, */
726/*                                             yVars,vVars,nVars,nPi); */
727     
728      finalTR = RestrSelectLeastHammingDStates(ddManager,prunedTR,
729                                               possessedTR,xVars,
730                                               yVars,vVars,nVars,nPi);
731      bdd_recursive_deref(ddManager,possessedTR);
732      bdd_ref(*newInit = initBdd);
733      break;
734    }
735  }
736
737  bdd_recursive_deref(ddManager,equivRel);
738  return finalTR;
739}
740
741/**Function********************************************************************
742
743  Synopsis [Returns a table of (rootNames,rootMvfs). The parameters
744  <tt>outBdds</tt> and <tt>nextBdds</tt> aare arrays of bdd_node *.
745  <tt>outputArray</tt> and <tt>tranFunArray</tt> are arrays of strings and are
746  in one-to-one correspondence with <tt>outBdds</tt> and <tt>nextBdds</tt>.]
747
748  SideEffects [None]
749
750  SeeAlso     []
751
752******************************************************************************/
753static st_table *
754CreateNameToMvfTable(
755  bdd_manager *ddManager,                 
756  array_t *outBdds,
757  array_t *nextBdds,
758  array_t *outputArray,
759  array_t *tranFunArray)
760{
761  st_table *nameToMvf;
762  bdd_node *ddTemp;
763  int i;
764
765  /* Initialize variables */
766  nameToMvf = st_init_table(strcmp, st_strhash);
767
768  arrayForEachItem(bdd_node *, outBdds, i, ddTemp) {
769    bdd_node *temp;
770    mdd_t *regular, *complement;
771    Mvf_Function_t *mvf;
772    char *name;
773
774    bdd_ref(temp = bdd_not_bdd_node(ddTemp));
775
776    regular = bdd_construct_bdd_t(ddManager,ddTemp);
777    complement = bdd_construct_bdd_t(ddManager,temp);
778
779    mvf = (Mvf_Function_t *)array_alloc(mdd_t *, 0);
780    array_insert(mdd_t *, mvf, 0, complement);
781    array_insert(mdd_t *, mvf, 1, regular);
782
783    name = array_fetch(char *, outputArray, i);
784    st_insert(nameToMvf,name,(char *)mvf);
785  }
786
787  arrayForEachItem(bdd_node *, nextBdds, i, ddTemp) {
788    bdd_node *temp;
789    mdd_t *regular, *complement;
790    Mvf_Function_t *mvf;
791    char *name;
792
793    bdd_ref(temp = bdd_not_bdd_node(ddTemp));
794
795    regular = bdd_construct_bdd_t(ddManager,ddTemp);
796    complement = bdd_construct_bdd_t(ddManager,temp);
797
798    mvf = (Mvf_Function_t *)array_alloc(mdd_t *, 0);
799    array_insert(mdd_t *, mvf, 0, complement);
800    array_insert(mdd_t *, mvf, 1, regular);
801
802    name = array_fetch(char *, tranFunArray, i);
803    st_insert(nameToMvf,name,(char *)mvf);
804  }
805
806  return nameToMvf;
807}
808
809
810/**Function********************************************************************
811
812  Synopsis [Create a (name,mdd_t*) table.]
813
814  SideEffects [None]
815
816  SeeAlso     []
817
818******************************************************************************/
819static st_table *
820CreateCareTable(
821  Ntk_Network_t *network,
822  mdd_t *reachMdd)
823{
824  lsGen gen;
825  Ntk_Node_t *node;
826  st_table *careTable;
827
828  careTable = st_init_table(strcmp, st_strhash);
829  Ntk_NetworkForEachPrimaryOutput(network, gen, node) {
830    char *name;
831    name = Ntk_NodeReadName(node);
832    st_insert(careTable,name,(char *)reachMdd);
833  }
834  Ntk_NetworkForEachLatch(network,gen,node){
835    char *name;
836    name = Ntk_NodeReadName(Ntk_LatchReadDataInput(node));
837    st_insert(careTable,name,(char *)reachMdd);
838  }
839
840  return careTable;
841}
842
843/**Function********************************************************************
844
845  Synopsis    [Routine to free members of an st_table.]
846
847  SideEffects [None]
848
849  SeeAlso []
850******************************************************************************/
851static enum st_retval
852StMvfFree(
853  char *key,
854  char *value,
855  char *arg)
856{
857  /* This will free the memory associated with the array also */
858  Mvf_FunctionFree((Mvf_Function_t *)value);
859 
860  return(ST_CONTINUE);
861 
862} /* end of StMvfFree */
863
864
865/**Function********************************************************************
866
867  Synopsis [Routine to count number of equivalence classes in a relation.]
868
869  SideEffects [None]
870
871  SeeAlso     []
872
873******************************************************************************/
874static void
875CountEquivalentClasses(
876  bdd_manager *ddManager,
877  bdd_node *equivRel,
878  bdd_node *initBdd,
879  bdd_node **xVars,
880  bdd_node **uVars,
881  int nVars)
882{
883  bdd_node *resultXU,*uCube;
884  bdd_node *oneInitState,*classes;
885
886  oneInitState = bdd_bdd_pick_one_minterm(ddManager,initBdd,xVars,nVars);
887  bdd_ref(oneInitState);
888
889  bdd_ref(resultXU = bdd_bdd_cprojection(ddManager,equivRel,oneInitState));
890  bdd_recursive_deref(ddManager,oneInitState);
891
892#ifdef RESTR_DIAG
893  {
894    /* The following is valid only when equivRel is the equivalence relation on
895       the complete set of states.*/
896    bdd_node *xCube,*tautology;
897    bdd_node *one;
898    one = bdd_read_one(ddManager);
899    bdd_ref(xCube = bdd_bdd_compute_cube(ddManager,xVars,NIL(int),nVars));
900    bdd_ref(tautology = bdd_bdd_exist_abstract(ddManager,resultXU,xCube));
901    assert(tautology == one);
902    bdd_recursive_deref(ddManager,tautology);
903    bdd_recursive_deref(ddManager,xCube);
904  }
905#endif
906
907#ifdef RESTR_DIAG
908  {
909    bdd_node *uCube,*zero,*classes;
910    bdd_node *oneClass,*temp,*rep;
911    int i;
912
913    zero = bdd_not_bdd_node(bdd_read_one(ddManager));
914    /* Extract the classes */
915    bdd_ref(uCube = bdd_bdd_compute_cube(ddManager,uVars,NIL(int),nVars));
916    bdd_ref(classes = bdd_bdd_exist_abstract(ddManager,resultXU,uCube));
917    bdd_recursive_deref(ddManager,uCube);
918   
919    i = 0;
920    (void) fprintf(vis_stdout,"\n** restr diag: EQUIVALENT CLASSES:\n");
921    while (classes != zero) {
922      i++;
923      bdd_ref(rep = bdd_bdd_pick_one_minterm(ddManager,classes,
924                                             xVars,nVars));
925      (void) fprintf(vis_stdout,"** restr diag: Class %d\n",i);
926      (void) fprintf(vis_stdout,"** restr diag: Class representative:\n");
927      RestrPrintBddNode(ddManager,rep);
928
929      /* Extract the complete class now */
930      bdd_ref(temp = bdd_bdd_cofactor(ddManager,resultXU,rep));
931      bdd_ref(oneClass = bdd_bdd_swap_variables(ddManager,temp,uVars,
932                                                xVars,nVars));
933      bdd_recursive_deref(ddManager,temp);
934      (void) fprintf(vis_stdout,"** restr diag: Class members:\n");
935      RestrPrintBddNode(ddManager,oneClass);
936      bdd_recursive_deref(ddManager,oneClass);
937
938      /* Remove rep from classes */
939      bdd_ref(temp = bdd_bdd_and(ddManager,classes,bdd_not_bdd_node(rep)));
940      bdd_recursive_deref(ddManager,rep);
941      bdd_recursive_deref(ddManager,classes);
942      classes = temp;
943    }
944    (void) fprintf(vis_stdout,"** restr diag: Number of classes = %d\n",i);
945  }
946#endif
947
948  /* Compute uCube and extract the u variables from resultXU */
949  bdd_ref(uCube = bdd_bdd_compute_cube(ddManager,uVars,NIL(int),nVars));
950  bdd_ref(classes = bdd_bdd_exist_abstract(ddManager,resultXU,uCube));
951  bdd_recursive_deref(ddManager,uCube);
952  bdd_recursive_deref(ddManager,resultXU);
953
954  fprintf(vis_stdout, "** restr info: Number of Equivalence Classes = %g\n",
955          bdd_count_minterm(ddManager,classes,nVars));
956 
957  bdd_recursive_deref(ddManager,classes);
958}
959
960
961/**Function********************************************************************
962
963  Synopsis [Convert an array of Mvf_Function_t * to an array of bdd_node *]
964
965  SideEffects [None]
966
967  SeeAlso     []
968
969******************************************************************************/
970static array_t *
971GetBddArrayFromMvfArray(array_t *mvfArray)
972{
973  int     i;
974  array_t *bddArray;
975  Mvf_Function_t *mvf;
976
977  bddArray = array_alloc(bdd_node *,0);
978
979  arrayForEachItem(Mvf_Function_t *, mvfArray,i,mvf) {
980    mdd_t     *mddTemp;
981    bdd_node    *ddNode;
982
983    mddTemp = array_fetch(mdd_t *, mvf, 1);
984    ddNode = bdd_extract_node_as_is(mddTemp);
985    bdd_ref(ddNode);
986
987    array_insert_last(bdd_node *, bddArray, ddNode);
988  }
989  return bddArray;
990}
991
992/**Function********************************************************************
993
994  Synopsis [Perform markovian analysis. The ADD for steady state probabilities
995  of the STG is returned.]
996
997  SideEffects [None]
998
999  SeeAlso     []
1000
1001******************************************************************************/
1002static bdd_node *
1003DoMarkovPowerAnalysis(
1004  bdd_manager *ddManager,
1005  bdd_node *prunedTR,
1006  bdd_node *initBdd,
1007  bdd_node **piVars,
1008  bdd_node **xVars,
1009  bdd_node **yVars,
1010  st_table *inputProb,
1011  int nVars,
1012  int nPi)
1013{
1014  bdd_node **result, *stateProbs;
1015  bdd_node *init;
1016 
1017  bdd_ref(init = bdd_bdd_to_add(ddManager,initBdd));
1018  if (restrVerbose) 
1019    (void) fprintf(vis_stdout,"** restr info: Initial average state bit change:\n");
1020
1021  result = AddPowerSolve(ddManager,prunedTR,init,xVars,yVars,
1022                              piVars,inputProb,nVars,nPi);
1023 
1024  bdd_recursive_deref(ddManager,result[1]);
1025  stateProbs = result[0];
1026  bdd_recursive_deref(ddManager,init);
1027  FREE(result);
1028 
1029  return stateProbs;
1030}
1031
1032/**Function********************************************************************
1033
1034  Synopsis [Given a relation R(X,Y) returns the array of functions y_i=f(X).]
1035
1036  SideEffects [None]
1037
1038  SeeAlso     []
1039
1040******************************************************************************/
1041static array_t *
1042ExtractTransitionFuns(
1043  bdd_manager   *ddManager,
1044  bdd_node      *finalTR,
1045  bdd_node      **yVars,
1046  int           nVars)
1047{
1048  bdd_node      *completeCube, *extractCube;
1049  bdd_node      *fun, *tranFun;
1050  array_t       *allTranFuns;
1051  int           i;
1052
1053  allTranFuns = array_alloc(bdd_node *,0);
1054
1055  completeCube = bdd_bdd_compute_cube(ddManager,yVars,NIL(int),nVars);
1056  bdd_ref(completeCube);
1057
1058  for(i = 0;i < nVars; i++) {
1059    extractCube = bdd_bdd_cofactor(ddManager,completeCube,yVars[i]);
1060    bdd_ref(extractCube);
1061    fun = bdd_bdd_exist_abstract(ddManager,finalTR,extractCube);
1062    bdd_ref(fun);
1063    bdd_recursive_deref(ddManager,extractCube);
1064    tranFun = bdd_bdd_cofactor(ddManager,fun,yVars[i]);
1065    bdd_ref(tranFun);
1066
1067#ifdef RESTR_DIAG
1068    {
1069      /* The following is to test if there are multiple edges out of a state
1070         with the same input label: in short to check if the relation is
1071         deterministic or not. */
1072
1073      bdd_node *yBar,*yNot,*inter;
1074      bdd_ref(yNot = bdd_not_bdd_node(yVars[i]));
1075      bdd_ref(yBar = bdd_bdd_cofactor(ddManager,fun,yNot));
1076      bdd_recursive_deref(ddManager,yNot);
1077      bdd_ref(inter = bdd_bdd_and(ddManager,yBar,tranFun));
1078      yNot = bdd_not_bdd_node(bdd_read_one(ddManager));
1079      assert(inter == yNot);
1080      bdd_recursive_deref(ddManager,inter);
1081      bdd_recursive_deref(ddManager,yBar);
1082    }
1083#endif
1084
1085    bdd_recursive_deref(ddManager,fun);
1086    array_insert_last(bdd_node *,allTranFuns,tranFun);
1087  }
1088
1089  bdd_recursive_deref(ddManager,completeCube);
1090  return allTranFuns;
1091}
1092
1093/**Function********************************************************************
1094
1095  Synopsis [Returns an array of BDDs given the node names of a network.]
1096
1097  SideEffects [None]
1098
1099  SeeAlso     []
1100
1101******************************************************************************/
1102static array_t *
1103GetBddArrayFromNameArray(
1104  Fsm_Fsm_t *fsm,
1105  array_t *nameArray)
1106{
1107  graph_t *partition;
1108  array_t *bdds,*mvfs;
1109 
1110  partition = Fsm_FsmReadPartition(fsm);
1111  mvfs = BuildFunctions(partition,nameArray);
1112  bdds = GetBddArrayFromMvfArray(mvfs);
1113  Mvf_FunctionArrayFree(mvfs);
1114
1115  return bdds;
1116}
1117
1118/**Function********************************************************************
1119
1120  Synopsis [Expand the reachable set R(x) to include those states which are
1121  equivalent to R(x) but potentially not reachable.]
1122
1123  SideEffects [<tt>reachable</tt> is updated.]
1124
1125  SeeAlso     []
1126
1127******************************************************************************/
1128static void
1129ExpandReachableSet(
1130  bdd_manager *ddManager,
1131  bdd_node **reachable,
1132  bdd_node *equivRel,
1133  bdd_node **xVars,
1134  bdd_node **uVars,
1135  int nVars)
1136{
1137  bdd_node *xcube,*potUnReach,*extReach;
1138  bdd_node *temp1;
1139
1140  bdd_ref(xcube = bdd_bdd_compute_cube(ddManager,xVars,NIL(int),nVars));
1141  /* potUnReach = \exists_x (E(x,u) * R(x)) */
1142  bdd_ref(potUnReach = bdd_bdd_and_abstract(ddManager,*reachable,
1143                                            equivRel,xcube));
1144  bdd_recursive_deref(ddManager,xcube);
1145  /* temp1(x) = potUnReach(u) */
1146  bdd_ref(temp1 = bdd_bdd_swap_variables(ddManager,potUnReach,uVars,
1147                                         xVars,nVars));
1148  bdd_recursive_deref(ddManager,potUnReach);
1149  /* extReach(x) = R(x) + potUnReach(x) */
1150  bdd_ref(extReach = bdd_bdd_or(ddManager,*reachable,temp1));
1151  bdd_recursive_deref(ddManager,temp1);
1152  bdd_recursive_deref(ddManager,*reachable);
1153  *reachable = extReach;
1154}
1155
1156/**Function********************************************************************
1157
1158  Synopsis [Create a partition for the new view of the fsm/network]
1159
1160  SideEffects [The new view is attached to the network.]
1161
1162  SeeAlso     [CreateNewFsm]
1163
1164******************************************************************************/
1165static graph_t *
1166CreateNewPartition(
1167  Ntk_Network_t *network,                 
1168  bdd_manager *ddManager,
1169  array_t *outBdds,
1170  array_t *nextBdds,
1171  array_t *outputArray,
1172  array_t *tranFunArray)
1173{
1174  st_table *nameToMvf;
1175  graph_t *partition;
1176
1177  /* Create a table of next state and output Mvfs with their names as key to
1178     the table. This table is used to create a partition for the network. */
1179  nameToMvf = CreateNameToMvfTable(ddManager,outBdds,nextBdds,
1180                                   outputArray,tranFunArray);
1181  /* Delete the old partition and old fsm as we dont need it any more */
1182  if (restrCreatedPart) {
1183    Ntk_NetworkFreeApplInfo(network,RESTR_PART_NETWORK_APPL_KEY);
1184    restrCreatedPart = 0;
1185  }
1186  if (restrCreatedFsm) {
1187    Ntk_NetworkFreeApplInfo(network,RESTR_FSM_NETWORK_APPL_KEY);
1188    restrCreatedFsm = 0;
1189  }
1190
1191  /* Create a new partition from the new root functions */
1192  partition = Part_NetworkCreatePartitionFromMvfs(network,nameToMvf);
1193  Ntk_NetworkAddApplInfo(network, RESTR_PART_NETWORK_APPL_KEY,
1194                         (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
1195                         (void *) partition);
1196  st_foreach(nameToMvf,StMvfFree,NIL(char));
1197  st_free_table(nameToMvf);
1198
1199  return partition;
1200}
1201
1202/**Function********************************************************************
1203
1204  Synopsis [Create the FSM data structure for the restructured STG and perform
1205  markov analysis to estimate the final state average bit change.]
1206
1207  SideEffects [<tt>reachable,initBdd,stateProbs,finalTR</tt> are dereferenced in this
1208  function.]
1209
1210  SeeAlso     [CreateNewPatition]
1211
1212******************************************************************************/
1213static Fsm_Fsm_t *
1214CreateNewFsm(
1215  Ntk_Network_t *network,
1216  graph_t *partition,
1217  bdd_manager *ddManager,
1218  bdd_node *finalTR,
1219  bdd_node *initBdd,
1220  bdd_node *reachable,
1221  bdd_node *stateProbs,
1222  bdd_node **xVars,
1223  bdd_node **yVars,
1224  bdd_node **piVars,
1225  st_table *inputProb,
1226  int nVars,
1227  int nPi)
1228{
1229  Fsm_Fsm_t *fsm;
1230  mdd_t *reachStates;
1231  mdd_t *mddTemp;
1232  bdd_node *ddTemp;
1233  bdd_node **markovResult;
1234
1235  /* Create a new Fsm for the restructured network. */
1236  fsm = Fsm_FsmCreateFromNetworkWithPartition(network,
1237                                              Part_PartitionDuplicate(partition));
1238  assert(fsm != NIL(Fsm_Fsm_t));
1239  Ntk_NetworkAddApplInfo(network, RESTR_FSM_NETWORK_APPL_KEY,
1240                         (Ntk_ApplInfoFreeFn) Fsm_FsmFreeCallback,
1241                         (void *) fsm); 
1242  /* We need to update the initial states as the
1243     Fsm_FsmCreateFromNetworkWithPartition will pick up old initial state from
1244     the network. Fsm_FsmSetInitialStates deletes old inital states. */
1245  mddTemp = bdd_construct_bdd_t(ddManager,initBdd);
1246  Fsm_FsmSetInitialStates(fsm,mddTemp);
1247
1248  /* Compute the new reachable states */
1249  reachStates = Fsm_FsmComputeReachableStates(fsm,0,0,0,0,0,0,1000,
1250                                              Fsm_Rch_Default_c,0,0,
1251                                              NIL(array_t),FALSE, NIL(array_t));
1252
1253  bdd_recursive_deref(ddManager,reachable);
1254  reachable = bdd_extract_node_as_is(reachStates);
1255  bdd_ref(reachable);
1256  mdd_free(reachStates);
1257       
1258  /* Constrain the transition relation */
1259  bdd_ref(ddTemp = bdd_bdd_constrain(ddManager,finalTR,reachable));
1260  bdd_recursive_deref(ddManager,finalTR);
1261  finalTR = ddTemp;
1262
1263  /* Use the state probs. of the original STG as the initial guess to compute
1264     the state probs. of the restructured STG. */
1265  if (restrVerbose)
1266    (void) fprintf(vis_stdout,"** restr info: Final average state bit change:\n");
1267
1268  markovResult = AddPowerSolve(ddManager, finalTR, stateProbs, xVars,
1269                                    yVars,piVars,inputProb,nVars,nPi);
1270  bdd_recursive_deref(ddManager, markovResult[0]);
1271  bdd_recursive_deref(ddManager, markovResult[1]);
1272  FREE(markovResult);
1273       
1274  bdd_recursive_deref(ddManager,stateProbs);
1275  bdd_recursive_deref(ddManager,finalTR);
1276  bdd_recursive_deref(ddManager,reachable);
1277
1278  return fsm;
1279}
Note: See TracBrowser for help on using the repository browser.