source: vis_dev/vis-2.3/src/restr/restrUtil.c @ 53

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

vis2.3

File size: 22.9 KB
Line 
1/**CFile***********************************************************************
2
3 FileName    [restrUtil.c]
4
5 PackageName [restr]
6
7 Synopsis    [Support functions used in the package.]
8
9 Description [Support functions used in the package.]
10
11 SeeAlso     [restrDebug.c]
12
13 Author      [Balakrishna Kumthekar <kumtheka@colorado.edu>]
14
15 Copyright [This file was created at the University of Colorado at
16 Boulder.  The University of Colorado at Boulder makes no warranty
17 about the suitability of this software for any purpose.  It is
18 presented on an AS IS basis.]
19
20******************************************************************************/
21
22#include "restrInt.h"
23
24/*---------------------------------------------------------------------------*/
25/* Constant declarations                                                     */
26/*---------------------------------------------------------------------------*/
27
28
29/*---------------------------------------------------------------------------*/
30/* Type declarations                                                         */
31/*---------------------------------------------------------------------------*/
32
33
34/*---------------------------------------------------------------------------*/
35/* Structure declarations                                                    */
36/*---------------------------------------------------------------------------*/
37
38
39/*---------------------------------------------------------------------------*/
40/* Variable declarations                                                     */
41/*---------------------------------------------------------------------------*/
42
43
44/*---------------------------------------------------------------------------*/
45/* Macro declarations                                                        */
46/*---------------------------------------------------------------------------*/
47
48/**AutomaticStart*************************************************************/
49
50/*---------------------------------------------------------------------------*/
51/* Static function prototypes                                                */
52/*---------------------------------------------------------------------------*/
53
54
55/**AutomaticEnd***************************************************************/
56
57
58/*---------------------------------------------------------------------------*/
59/* Definition of exported functions                                          */
60/*---------------------------------------------------------------------------*/
61
62
63/*---------------------------------------------------------------------------*/
64/* Definition of internal functions                                          */
65/*---------------------------------------------------------------------------*/
66
67/**Function********************************************************************
68
69  Synopsis [Returns the primary output node array for the given network.]
70
71  Description [Returns the primary output node array for the given network.]
72
73  SideEffects [None]
74
75  SeeAlso     [RestrGetNextStateArray]
76
77******************************************************************************/
78array_t *
79RestrGetOutputArray(Ntk_Network_t *network)
80{
81    lsGen                gen;
82    Ntk_Node_t  *node;
83    array_t     *outputArray;
84
85    outputArray = array_alloc(char *, 0);
86    Ntk_NetworkForEachPrimaryOutput(network, gen, node) {
87        array_insert_last(char *, outputArray, Ntk_NodeReadName(node));
88    }
89
90    return outputArray;
91}
92
93/**Function********************************************************************
94
95  Synopsis [Computes the product
96  \prod_{i=0}^{i=n-1} funArray_{i}(x) \equiv funArray_{i}(y)]
97
98  Description [Computes the product
99  \prod_{i=0}^{i=n-1} funArray_{i}(x) \equiv funArray_{i}(y).
100 
101  funArray is an array of BDDs and each has xVars in its
102  support. nVars is the number of xVars and yVars.]
103
104  SideEffects [None]
105
106  SeeAlso     [RestrComputeTRWithIds]
107
108******************************************************************************/
109bdd_node *
110RestrCreateProductOutput(
111  bdd_manager   *ddManager,
112  array_t       *funArray,
113  bdd_node      **xVars,
114  bdd_node      **yVars,
115  int           nVars)
116{
117  bdd_node      *ddtemp, *ddtemp1;
118  bdd_node      *fn, *result;
119  int           i, num = array_n(funArray);
120
121  bdd_ref(result = bdd_read_one(ddManager));
122
123  for(i = 0; i < num; i++) {
124
125    ddtemp = array_fetch(bdd_node *, funArray, i);;
126
127    ddtemp1 = bdd_bdd_swap_variables(ddManager,ddtemp,xVars,yVars,nVars);
128    bdd_ref(ddtemp1);
129    fn = bdd_bdd_xnor(ddManager,ddtemp1,ddtemp);
130    bdd_ref(fn);
131    bdd_recursive_deref(ddManager,ddtemp1);
132    ddtemp1 = bdd_bdd_and(ddManager,result,fn);
133    bdd_ref(ddtemp1);
134    bdd_recursive_deref(ddManager,fn);
135    bdd_recursive_deref(ddManager,result);
136    result = ddtemp1;
137  }
138
139  return result;
140}
141
142/**Function********************************************************************
143
144  Synopsis [The function computes the following relations:
145  \prod_{i=0}^{i=n-1} (y_i \equiv f_i(x)) and
146  \prod_{i=0}^{i=n-1} (y_i \equiv f_i(x)) \wedge (v_i \equiv f_i(u)) and
147  returns them in an array.]
148
149  Description [The function computes the following relations:
150  \prod_{i=0}^{i=n-1} (y_i \equiv f_i(x)) and
151  \prod_{i=0}^{i=n-1} (y_i \equiv f_i(x)) \wedge (v_i \equiv f_i(u)) and
152  returns them in an array.
153 
154  nextBdds is an array of nVar BDDs and has xVars in its
155  support. xVars, yVars, uVars and vVars are arrays of BDD variables.]
156
157  SideEffects [None]
158
159  SeeAlso     [RestrCreateProductOutput]
160
161******************************************************************************/
162array_t *
163RestrComputeTRWithIds(
164  bdd_manager   *ddManager,
165  array_t       *nextBdds,
166  bdd_node      **xVars,
167  bdd_node      **yVars,
168  bdd_node      **uVars,
169  bdd_node      **vVars,
170  int           nVars)
171{
172  bdd_node      *ddtemp1, *ddtemp2;
173  bdd_node      *oldTR, *fn;
174  array_t       *composite;
175  int            i;
176
177
178  /* First compute oldTR(x,y) = \prod_{i=0}^{i=n-1} (y_i \equiv f_i(x)) */
179  bdd_ref(oldTR = bdd_read_one(ddManager));
180
181  for(i = 0; i < nVars; i++) {
182    ddtemp2  = array_fetch(bdd_node *, nextBdds, i);
183
184    fn = bdd_bdd_xnor(ddManager,ddtemp2,yVars[i]);
185    bdd_ref(fn);
186    ddtemp1 = bdd_bdd_and(ddManager,oldTR,fn);
187    bdd_ref(ddtemp1);
188    bdd_recursive_deref(ddManager,fn);
189    bdd_recursive_deref(ddManager,oldTR);
190    oldTR = ddtemp1;
191  }
192 
193  /* fn(u,v) = oldTR(x-->u,y-->v) */
194  ddtemp2 = bdd_bdd_swap_variables(ddManager,oldTR,xVars,uVars,nVars);
195  bdd_ref(ddtemp2);
196  fn = bdd_bdd_swap_variables(ddManager,ddtemp2,yVars,vVars,nVars);
197  bdd_ref(fn);
198  bdd_recursive_deref(ddManager,ddtemp2);
199  ddtemp1 = bdd_bdd_and(ddManager,fn,oldTR);
200  bdd_ref(ddtemp1);
201  bdd_recursive_deref(ddManager,fn);
202
203  /* Return both the relations */
204  composite = array_alloc(bdd_node *,0);
205  array_insert_last(bdd_node *,composite,oldTR);
206  array_insert_last(bdd_node *,composite,ddtemp1);
207
208  return composite;
209}
210
211/**Function********************************************************************
212
213  Synopsis [This function returns the state equivalence relation for an FSM.]
214
215  Description [This function returns the state equivalence relation
216  for an FSM. Lambda is the primary output relation and TR is the
217  state transition relation of the product machine. Lambda has xVars,
218  uVars and piVars in its support. TR has piVars, xVars,yVars,uVars
219  and vVars in its support. nPi is the number of piVars and nVars is
220  the number of xVars. xVars, yVars, uVars and vVars are all of the
221  same size, i.e., nVars. The returned BDD is a function of xVars and
222  uVars.
223
224  For more information on the algorithm, please refer to "Dont care
225  minimization of multi-level sequential logic networks", ICCAD 90.]
226
227  SideEffects [None]
228
229  SeeAlso     [RestrComputeEquivRelationUsingCofactors]
230
231******************************************************************************/
232bdd_node *
233RestrGetEquivRelation(
234  bdd_manager           *mgr,
235  bdd_node        *Lambda,
236  bdd_node        *tranRelation,
237  bdd_node      **xVars,
238  bdd_node      **yVars,
239  bdd_node      **uVars,
240  bdd_node      **vVars,
241  bdd_node      **piVars,
242  int             nVars,
243  int             nPi,
244  boolean restrVerbose)
245
246{
247    bdd_node *initialEsp, *espK;
248    bdd_node *espKPlusOne;
249    bdd_node *inputCube, *nextCube;
250    bdd_node **allPreVars, **allNexVars;
251    bdd_node *temp;
252    int i,depth;
253
254    allPreVars = ALLOC(bdd_node *, 2*nVars);
255    allNexVars = ALLOC(bdd_node *, 2*nVars);
256    for(i = 0; i < nVars;i++) {
257        allPreVars[i] = xVars[i];
258        allNexVars[i] = yVars[i];
259    } 
260    for(i = 0; i < nVars;i++) {
261        allPreVars[i+nVars] = uVars[i];
262        allNexVars[i+nVars] = vVars[i];
263    } 
264
265    nextCube = bdd_bdd_compute_cube(mgr,allNexVars,NIL(int),2*nVars);
266    bdd_ref(nextCube);
267
268    inputCube = bdd_bdd_compute_cube(mgr,piVars,NIL(int),nPi);
269    bdd_ref(inputCube);
270
271    initialEsp = bdd_bdd_univ_abstract(mgr,Lambda,inputCube);
272    bdd_ref(initialEsp);
273
274    espK = bdd_bdd_swap_variables(mgr,initialEsp,allPreVars,
275                                 allNexVars,2*nVars);
276    bdd_ref(espK);
277   
278    depth = 0;
279    do {
280        bdd_node *image, *temp1;
281        image = bdd_bdd_and_abstract(mgr,tranRelation, espK, nextCube);
282        bdd_ref(image);
283
284        temp1 = bdd_bdd_univ_abstract(mgr,image,inputCube);
285        bdd_ref(temp1);
286        bdd_recursive_deref(mgr,image);
287
288        espKPlusOne = bdd_bdd_and(mgr,temp1,initialEsp);
289        bdd_ref(espKPlusOne);
290        bdd_recursive_deref(mgr,temp1);
291        temp1 = bdd_bdd_swap_variables(mgr,espKPlusOne,allPreVars,
292                                     allNexVars,2*nVars);
293        bdd_ref(temp1);
294        bdd_recursive_deref(mgr,espKPlusOne);
295        espKPlusOne = temp1;
296       
297        if (espKPlusOne == espK) {
298          break;
299        }
300        bdd_recursive_deref(mgr,espK);
301        espK = espKPlusOne;
302        depth++;
303    } while (1);
304
305    if (restrVerbose)
306      (void) fprintf(vis_stdout,"** restr info: EQ. relation computation depth = %d\n",
307                     depth);
308
309    bdd_recursive_deref(mgr,espKPlusOne);
310    bdd_recursive_deref(mgr,initialEsp);
311    bdd_recursive_deref(mgr,inputCube);
312    bdd_recursive_deref(mgr,nextCube);
313
314    bdd_ref(temp = bdd_bdd_swap_variables(mgr,espK,allNexVars,
315                                          allPreVars,2*nVars));
316    bdd_recursive_deref(mgr,espK);
317    espK = temp;
318
319    FREE(allPreVars);
320    FREE(allNexVars);
321
322    return espK;
323}
324
325/**Function********************************************************************
326
327  Synopsis [This function returns the state equivalence relation for an FSM.]
328
329  Description [This function returns the state equivalence relation
330  for an FSM. Lambda is the primary output relation and TR is the
331  state transition relation of the product machine. Lambda has xVars,
332  uVars and piVars in its support. TR has piVars, xVars,yVars,uVars
333  and vVars in its support. nPi is the number of piVars and nVars is
334  the number of xVars. xVars, yVars, uVars and vVars are all of the
335  same size, i.e., nVars. The returned BDD is a function of xVars and
336  uVars.
337
338  For more information on the algorithm, please refer to "Extending Equivalence
339  Class Computation to Large FSMs", ICCD 96.]
340
341  SideEffects []
342
343  SeeAlso     [RestrGetEquivRelation]
344
345******************************************************************************/
346bdd_node *
347RestrComputeEquivRelationUsingCofactors(
348  bdd_manager   *mgr,
349  bdd_node      *Lambda,
350  bdd_node      *TR,
351  bdd_node      **xVars,
352  bdd_node      **yVars,
353  bdd_node      **uVars,
354  bdd_node      **vVars,
355  bdd_node      **piVars,
356  int             nVars,
357  int             nPi,
358  boolean         restrVerbose)
359
360{
361  bdd_node *espKxu, *espKyv, *espKPlusOne, *espKMinusOne;
362  bdd_node *espKCofKMinusOne;
363  bdd_node *inputCube, *nextCube;
364  bdd_node *tranRelation;
365  bdd_node *newTran;
366  bdd_node **allPreVars, **allNexVars;
367  int i,depth;
368
369  bdd_ref(tranRelation = TR);
370
371  allPreVars = ALLOC(bdd_node *, 2*nVars);
372  allNexVars = ALLOC(bdd_node *, 2*nVars);
373  for(i = 0; i < nVars;i++) {
374    allPreVars[i] = xVars[i];
375    allNexVars[i] = yVars[i];
376  } 
377  for(i = 0; i < nVars;i++) {
378    allPreVars[i+nVars] = uVars[i];
379    allNexVars[i+nVars] = vVars[i];
380  } 
381
382  /* nextCube is a cube of yVars and vVars */
383  nextCube = bdd_bdd_compute_cube(mgr,allNexVars,NIL(int),2*nVars);
384  bdd_ref(nextCube);
385
386  /* inputCube is a cube of piVars */
387  inputCube = bdd_bdd_compute_cube(mgr,piVars,NIL(int),nPi);
388  bdd_ref(inputCube);
389
390  /* espKxu = \forall_{piVars} Lambda */
391  espKxu = bdd_bdd_univ_abstract(mgr,Lambda,inputCube);
392  bdd_ref(espKxu);
393
394  espKyv = bdd_bdd_swap_variables(mgr,espKxu,allPreVars,
395                                  allNexVars,2*nVars);
396  bdd_ref(espKyv);
397  bdd_ref(espKMinusOne = bdd_read_one(mgr));
398  bdd_ref(espKPlusOne = bdd_read_one(mgr));
399
400  /* The following loop is essentially the following:
401   * E_{k+1} = E_k \wedge (\forall_x(func)) where
402   * func = \exists_{yv} ((TR \downarrow E_k) \wedge (E_k \downarrow E_{k-1}))
403   */
404  depth = 0;
405  while (1) {
406    bdd_node *image, *temp1;
407       
408    bdd_recursive_deref(mgr, espKPlusOne);
409    bdd_ref(espKCofKMinusOne = bdd_bdd_constrain(mgr, espKyv, 
410                                                 espKMinusOne));
411    bdd_recursive_deref(mgr, espKMinusOne);
412    bdd_ref(espKMinusOne = espKyv);
413
414    bdd_ref(newTran = bdd_bdd_constrain(mgr, tranRelation, espKxu));
415
416    image = bdd_bdd_and_abstract(mgr,newTran, espKCofKMinusOne, nextCube);
417    bdd_ref(image);
418    bdd_recursive_deref(mgr, newTran);
419    bdd_recursive_deref(mgr, espKCofKMinusOne);
420
421    temp1 = bdd_bdd_univ_abstract(mgr,image,inputCube);
422    bdd_ref(temp1);
423    bdd_recursive_deref(mgr,image);
424    espKPlusOne = bdd_bdd_and(mgr,temp1,espKxu);
425    bdd_ref(espKPlusOne);
426    bdd_recursive_deref(mgr,temp1);
427
428    if (espKPlusOne == espKxu) {
429      bdd_recursive_deref(mgr,espKMinusOne);
430      bdd_recursive_deref(mgr,espKxu);
431      bdd_recursive_deref(mgr,espKyv);
432      bdd_recursive_deref(mgr,tranRelation);
433      bdd_recursive_deref(mgr,inputCube);
434      bdd_recursive_deref(mgr,nextCube);
435      FREE(allPreVars);
436      FREE(allNexVars);
437      if (restrVerbose) {
438        (void) fprintf(vis_stdout,"** restr info: EQ. relation computation depth = %d\n",
439                       depth);
440      }
441      return espKPlusOne;
442    }
443
444    bdd_recursive_deref(mgr, espKxu);
445    bdd_ref(espKxu = espKPlusOne);
446    bdd_recursive_deref(mgr, espKyv);
447    espKyv = bdd_bdd_swap_variables(mgr,espKxu,allPreVars,
448                                    allNexVars,2*nVars);
449    bdd_ref(espKyv);
450       
451    depth++;
452  }
453
454}
455
456/**Function********************************************************************
457
458  Synopsis [Returns the BDD for the augmented tr.]
459
460  Description [Returns the BDD for the augmented tr. The procedure of
461  augmentation is as follows: If there exists a pair (x,y) in tr and a
462  pair (y,v) in equivRelation, then the augmented tr has an additional
463  pair (x,v) added to it. The newly added edges are called 'ghost
464  edges'. Moreover, tr is a function of xVars and yVars, while
465  equivRelation is a function of yVars and vVars. nVars is the size of
466  yVars and vVars each. The returned BDD has the same support
467  variables as tr.
468
469  The boolean formulation is:
470
471  T^a(x,y) = \exists_z E(y,z) \wedge T(x,z)]
472
473  SideEffects [None]
474
475  SeeAlso     []
476
477******************************************************************************/
478bdd_node *
479RestrComputeTrWithGhostEdges(
480  bdd_manager *mgr,
481  bdd_node **yVars,
482  bdd_node **vVars,
483  bdd_node *tr,
484  bdd_node *equivRelation,
485  int nVars)
486{
487  bdd_node *abstractCube;
488  bdd_node *temp;
489  bdd_node *ghostTR;
490
491  abstractCube = bdd_bdd_compute_cube(mgr,yVars,NIL(int),nVars);
492  bdd_ref(abstractCube);
493
494  temp = bdd_bdd_and_abstract(mgr,tr,equivRelation,abstractCube);
495  bdd_ref(temp);
496  bdd_recursive_deref(mgr,abstractCube);
497
498  ghostTR = bdd_bdd_swap_variables(mgr,temp,vVars,yVars,nVars);
499  bdd_ref(ghostTR);
500  bdd_recursive_deref(mgr,temp);
501
502  return ghostTR;
503}
504
505/**Function********************************************************************
506
507  Synopsis [Returns a 0-1 ADD containing minterms such that the
508  discriminant for those minterms in f is greater than that in g.]
509
510  Description [Returns a 0-1 ADD containing minterms such that the
511  discriminant for those minterms in f is greater than that in g.]
512
513  SideEffects [None]
514
515  SeeAlso     [cuddAddApply.c]
516******************************************************************************/
517bdd_node *
518RestrAddMaximum(
519  bdd_manager *ddManager,
520  bdd_node **f,
521  bdd_node **g)
522{
523  bdd_node *plusInf;
524  bdd_node *zero, *one;
525
526  zero = bdd_read_zero(ddManager);
527  one = bdd_read_one(ddManager);
528  plusInf = bdd_read_plus_infinity(ddManager);
529
530  if(*g == plusInf) {
531    return zero;
532  }
533
534  if(bdd_is_constant(*f) && bdd_is_constant(*g)) {
535    if(bdd_add_value(*f) > bdd_add_value(*g)) {
536      return one;
537    } else {
538      return zero;
539    }
540  }
541  return NULL;
542}
543
544
545/**Function********************************************************************
546
547  Synopsis [Returns a 0-1 ADD containing minterms such that the
548  discriminant for those minterms in f is equal to that in g.]
549
550  Description [Returns a 0-1 ADD containing minterms such that the
551  discriminant for those minterms in f is equal to that in g.]
552
553  SideEffects [None]
554
555  SeeAlso     [cuddAddApply.c]
556
557******************************************************************************/
558bdd_node *
559RestrAddEqual(
560  bdd_manager *ddManager,
561  bdd_node **f,
562  bdd_node **g)
563{
564  bdd_node *zero, *one;
565
566  zero = bdd_read_zero(ddManager);
567  one = bdd_read_one(ddManager);
568
569  if(*f == *g) {
570    return one;
571  }
572
573  if(bdd_is_constant(*f) && bdd_is_constant(*g)) {
574      return zero;
575  }
576  return NULL;
577}
578
579/**Function********************************************************************
580
581  Synopsis [Given an array of BDD ids, return the array of
582  corresponding BDDs.]
583
584  Description [Given an array of BDD ids, return the array of
585  corresponding BDDs.]
586
587  SideEffects [None]
588
589  SeeAlso     []
590
591******************************************************************************/
592bdd_node **
593RestrBddNodeArrayFromIdArray(
594  bdd_manager   *ddManager,
595  array_t       *idArray)
596{
597  bdd_node **xvars;
598  int i,id;
599  int nvars = array_n(idArray);
600
601  xvars = ALLOC(bdd_node *, nvars);
602  if (xvars == NULL)
603    return NULL;
604
605  for(i = 0; i < nvars; i++) {
606    id = array_fetch(int,idArray,i);
607    xvars[i] = bdd_bdd_ith_var(ddManager,id);
608    bdd_ref(xvars[i]);
609  }
610  return xvars;
611}
612
613/**Function********************************************************************
614
615  Synopsis    [Calculate the average bit change in the STG.]
616
617  Description [Calculate the average bit change in the STG. probTR is an ADD
618  representing the absolute transition probability matrix of the STG.
619  xVars and yVars are the present and next state variables respectively. nVars
620  is the number of state variables.
621
622  average bit change = (\exists^+_x(probTr * HD(x,y))). ]
623
624  SideEffects [None]
625
626  SeeAlso []
627******************************************************************************/
628double 
629RestrAverageBitChange(
630  bdd_manager *manager,
631  bdd_node *probTR,
632  bdd_node **xVars,
633  bdd_node **yVars,
634  int nVars)
635{
636  bdd_node *diff, *cube, *PA, *QA;
637  bdd_node **vars;
638  double Mean;
639  int i;
640
641  vars = ALLOC(bdd_node *,2*nVars);
642  for (i = 0; i < nVars; i++) {
643    vars[i] = bdd_add_ith_var(manager,bdd_node_read_index(xVars[i]));
644    bdd_ref(vars[i]);
645  }
646  for (i = nVars; i < 2*nVars; i++) {
647    vars[i] = bdd_add_ith_var(manager,bdd_node_read_index(yVars[i-nVars]));
648    bdd_ref(vars[i]);
649  }
650
651  cube = bdd_add_compute_cube(manager,vars,NIL(int),2*nVars);
652  bdd_ref(cube);
653
654  /* Calculate the Hamming distance ADD. This ADD represents the hamming
655   * distance between two vectors represented by xVars and yVars.
656   */
657  bdd_ref(diff = bdd_add_hamming(manager,xVars,yVars,nVars));
658  bdd_ref(PA = bdd_add_apply(manager,bdd_add_times,probTR,diff));
659  bdd_recursive_deref(manager,diff);
660 
661  /* And now add and abstract all the variables.*/
662  bdd_ref(QA = bdd_add_exist_abstract(manager,PA,cube));
663  bdd_recursive_deref(manager,PA);
664  bdd_recursive_deref(manager,cube);
665  Mean = (double)bdd_add_value(QA);
666  bdd_recursive_deref(manager,QA); 
667
668  for (i = 0; i < 2*nVars; i++) {
669    bdd_recursive_deref(manager,vars[i]);
670  }
671  FREE(vars);
672  return Mean;
673}
674
675/**Function********************************************************************
676
677  Synopsis [Create an extra set of auxillary BDD variables--corresponding to
678  present and next state variables of the network--required during
679  restructuring.]
680
681  SideEffects [None]
682
683  SeeAlso     []
684
685******************************************************************************/
686array_t *
687RestrCreateNewStateVars(
688  Ntk_Network_t *network,
689  bdd_manager *ddManager,
690  bdd_node **xVars,
691  bdd_node **yVars)
692
693{
694  Ntk_Node_t *node1;
695  char *name, *name1;
696  array_t *varValues;
697  array_t *nameArray;
698  int i,id,index;
699  int nVars = Ntk_NetworkReadNumLatches(network);
700
701  array_t *uVarIds, *vVarIds;
702  array_t *result;
703
704  varValues = array_alloc(int, 0);
705  nameArray = array_alloc(char *,0);   
706  uVarIds = array_alloc(int, 0);
707  vVarIds = array_alloc(int, 0);
708  result = array_alloc(array_t *, 0);
709
710  id = bdd_num_vars(ddManager);
711
712  for (i = 0; i < nVars; i++) {
713    index = bdd_node_read_index(yVars[i]);
714    node1 = Ntk_NetworkFindNodeByMddId(network,index);
715    name = Ntk_NodeReadName(node1);
716    name1 = util_strcat3(name,"$NTK2","");
717    array_insert_last(int,varValues,2);
718    array_insert_last(char *,nameArray,name1);
719    array_insert_last(int, vVarIds, id);
720    id++;
721
722    index = bdd_node_read_index(xVars[i]);
723    node1 = Ntk_NetworkFindNodeByMddId(network,index);
724    name = Ntk_NodeReadName(node1);
725    name1 = util_strcat3(name,"$NTK2","");
726    array_insert_last(int,varValues,2);
727    array_insert_last(char *,nameArray,name1);
728    array_insert_last(int, uVarIds, id);
729    id++;
730
731  }
732  mdd_create_variables(ddManager,varValues,nameArray,NIL(array_t));
733
734  arrayForEachItem(char *,nameArray,i,name) {
735    FREE(name);
736  }
737  array_free(nameArray);
738  array_free(varValues);
739
740  array_insert_last(array_t *, result, uVarIds);
741  array_insert_last(array_t *, result, vVarIds);
742
743  return result;
744}
745
746
747/**Function********************************************************************
748
749  Synopsis    [In the absence of initial order of the variables, this
750  function assings MDD Ids to the input, present state and next state
751  variables.]
752
753  Description [In the absence of initial order of the variables, this
754  function assigns MDD Ids to the input, present state and next state
755  variables.
756
757  This procedure is NOT currently used and is here for future purposes.]
758
759  SideEffects [The BDD manager is changed accordingly.]
760
761  SeeAlso []
762******************************************************************************/
763void
764RestrSetInitialOrder(
765  Ntk_Network_t *network,
766  bdd_manager   *ddManager)
767
768{
769  Ntk_Node_t *node, *node1;
770  lsGen gen;
771  char *name;
772  array_t       *varValues;
773  array_t       *nameArray;
774  int           id;
775
776  varValues = array_alloc(int,0);
777  nameArray = array_alloc(char *,0);
778
779  id = 0;
780  Ntk_NetworkForEachLatch(network,gen,node) {
781    node1 = Ntk_NodeReadShadow(node);
782    name = util_strsav(Ntk_NodeReadName(node1));
783    Ntk_NodeSetMddId(node1,id);
784    array_insert_last(int,varValues,2);
785    array_insert_last(char *,nameArray,name);
786    id++;
787
788    name = util_strsav(Ntk_NodeReadName(node));
789    Ntk_NodeSetMddId(node,id);
790    array_insert_last(int,varValues,2);
791    array_insert_last(char *,nameArray,name);
792    id++;
793  }
794
795  Ntk_NetworkForEachPrimaryInput(network,gen,node) {
796    name = util_strsav(Ntk_NodeReadName(node));
797    Ntk_NodeSetMddId(node,id);
798    array_insert_last(int,varValues,2);
799    array_insert_last(char *,nameArray,name);
800    id++;
801  }
802
803  mdd_create_variables(ddManager,varValues,nameArray,NIL(array_t));
804
805  id = 0;
806  arrayForEachItem(char *, nameArray, id, name) {
807    FREE(name);
808  }
809  array_free(nameArray);
810  array_free(varValues);
811
812}
813
Note: See TracBrowser for help on using the repository browser.