source: vis_dev/vis-2.3/src/synth/synthUtil.c @ 87

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

vis2.3
File size: 20.4 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [synthUtil.c]
4
5  PackageName [synth]
6
7  Synopsis    [Functions to get or to print some information.]
8
9  Author      [In-Ho Moon, Balakrishna Kumthekar]
10
11  Copyright [This file was created at the University of Colorado at Boulder.
12  The University of Colorado at Boulder makes no warranty about the suitability
13  of this software for any purpose.  It is presented on an AS IS basis.]
14
15******************************************************************************/
16
17#include "synthInt.h"
18
19static char rcsid[] UNUSED = "$Id: synthUtil.c,v 1.13 1998/08/19 22:51:49 mooni Exp $";
20
21/*---------------------------------------------------------------------------*/
22/* Constant declarations                                                     */
23/*---------------------------------------------------------------------------*/
24
25
26/*---------------------------------------------------------------------------*/
27/* Type declarations                                                         */
28/*---------------------------------------------------------------------------*/
29
30
31/*---------------------------------------------------------------------------*/
32/* Structure declarations                                                    */
33/*---------------------------------------------------------------------------*/
34
35
36/*---------------------------------------------------------------------------*/
37/* Variable declarations                                                     */
38/*---------------------------------------------------------------------------*/
39
40/**AutomaticStart*************************************************************/
41
42/*---------------------------------------------------------------------------*/
43/* Static function prototypes                                                */
44/*---------------------------------------------------------------------------*/
45
46static int GetChildTree(bdd_manager *dd, bdd_node *f, char *eq);
47static int GetChildMlTree(bdd_manager *dd, MlTree *tree, char *eq);
48static bdd_node * FindNodeWithIndex(bdd_node *node, int index);
49static void GetZddCoverWithNameRecur(Ntk_Network_t *net, bdd_manager *dd, bdd_node *node, char *cover);
50
51/**AutomaticEnd***************************************************************/
52
53
54/*---------------------------------------------------------------------------*/
55/* Definition of exported functions                                          */
56/*---------------------------------------------------------------------------*/
57
58
59/*---------------------------------------------------------------------------*/
60/* Definition of internal functions                                          */
61/*---------------------------------------------------------------------------*/
62
63/**Function********************************************************************
64
65  Synopsis    [Prints the equation form of a node with internal names.]
66
67  Description [Prints the equation form of a node with internal names.
68  If the string length is bigger than MAX_EQ_LEN, the string is truncated.]
69
70  SideEffects []
71
72  SeeAlso     [SynthPrintZddTreeMessage]
73
74******************************************************************************/
75void
76SynthPrintZddTree(bdd_manager *dd,
77                  bdd_node *f)
78{
79  char  eq[MAX_EQ_LEN];
80
81  GetChildTree(dd, f, eq);
82  fprintf(vis_stdout, "%s\n", eq);
83}
84
85
86/**Function********************************************************************
87
88  Synopsis    [Prints the equation form of a node with internal names,
89  preceded by a message.]
90
91  Description [Prints the equation form of a node with internal names,
92  preceded by a message. If the string length is bigger than MAX_EQ_LEN,
93  the string is truncated.]
94
95  SideEffects []
96
97  SeeAlso     [SynthPrintMlTreeMessage]
98
99******************************************************************************/
100void
101SynthPrintZddTreeMessage(bdd_manager *dd,
102                         bdd_node *f,
103                         char *mess)
104{
105  char  eq[MAX_EQ_LEN];
106
107  GetChildTree(dd, f, eq);
108  fprintf(vis_stdout, "%s%s\n", mess, eq);
109}
110
111
112/**Function********************************************************************
113
114  Synopsis    [Prints the equation form of a tree with internal names,
115  preceded by a message.]
116
117  Description [Prints the equation form of a tree with internal names,
118  preceded by a message. If the string length is bigger than MAX_EQ_LEN,
119  the string is truncated.]
120
121  SideEffects []
122
123  SeeAlso     [SynthPrintZddTreeMessage SynthPrintMlTreeWithName]
124
125******************************************************************************/
126void
127SynthPrintMlTreeMessage(bdd_manager *dd,
128                        MlTree *tree,
129                        char *mess)
130{
131  char  eq[MAX_EQ_LEN];
132
133  if (MlTree_IsComplement(tree)) {
134    tree = MlTree_Regular(tree);
135    GetChildMlTree(dd, tree, eq);
136    (void) fprintf(vis_stdout, "%s%s'\n", mess, eq);
137  } else {
138    GetChildMlTree(dd, tree, eq);
139    (void) fprintf(vis_stdout, "%s%s\n", mess, eq);
140  }
141}
142
143
144/**Function********************************************************************
145
146  Synopsis    [Frees a multi-level tree recursively.]
147
148  Description [Frees a multi-level tree recursively. If the argument flag
149  is set to 0, it does not free recursively.]
150
151  SideEffects []
152
153  SeeAlso     []
154
155******************************************************************************/
156void
157SynthFreeMlTree(MlTree *tree,
158                int flag)
159{
160  if (!tree)
161    return;
162
163  if (tree->ref) {
164    FREE(tree);
165    return;
166  }
167
168  if (tree->support)
169    FREE(tree->support);
170
171  if (flag && tree->leaf == 0) {
172    if (tree->q_ref == 0)
173      SynthFreeMlTree(tree->q, flag);
174    if (tree->d_ref == 0)
175      SynthFreeMlTree(tree->d, flag);
176    if (tree->r_ref == 0)
177      SynthFreeMlTree(tree->r, flag);
178  }
179
180  FREE(tree);
181}
182
183
184/**Function********************************************************************
185
186  Synopsis    [Prints the equation form of a tree with original names
187  and preceded by a message.]
188
189  Description [Prints the equation form of a tree with original names
190  and preceded by a message. If the string length is bigger than
191  MAX_EQ_LEN, the string is truncated.]
192
193  SideEffects []
194
195  SeeAlso     [SynthPrintMlTreeMessage]
196
197******************************************************************************/
198void
199SynthPrintMlTreeWithName(Ntk_Network_t *net,
200                         bdd_manager *dd,
201                         MlTree *tree,
202                         char *mess)
203{
204  char  eq[MAX_EQ_LEN];
205
206  SynthGetChildMlTreeWithName(net, dd, tree, eq);
207  fprintf(vis_stdout, "%s%s\n", mess, eq);
208}
209
210
211/**Function********************************************************************
212
213  Synopsis    [Gets the equation form of a tree with original names.]
214
215  Description [Gets the equation form of a tree with original names.]
216
217  SideEffects []
218
219  SeeAlso     [SynthGetChildMlTree]
220
221******************************************************************************/
222int
223SynthGetChildMlTreeWithName(Ntk_Network_t *net,
224                            bdd_manager *dd,
225                            MlTree *tree,
226                            char *eq)
227{
228  char          q_eq[MAX_EQ_LEN];
229  char          d_eq[MAX_EQ_LEN];
230  char          r_eq[MAX_EQ_LEN];
231  char          qd_eq[MAX_EQ_LEN];
232  bdd_node      *one = bdd_read_one(dd);
233  bdd_node      *zero = bdd_read_zero(dd);
234  bdd_node      *f;
235  int           flag;
236
237  f = tree->node;
238  if (tree->leaf) {
239    flag = SynthGetChildTreeWithName(net, dd, f, eq);
240    return(flag);
241  }
242
243  if (f == one) {
244    sprintf(eq, "one");
245    return(0);
246  } else if (f == zero) {
247    sprintf(eq, "zero");
248    return(0);
249  }
250
251  flag = SynthGetChildMlTreeWithName(net, dd, tree->q, q_eq);
252  if (tree->q_comp)
253    SynthMakeComplementString(q_eq);
254  if (flag)
255    return(1);
256  flag = SynthGetChildMlTreeWithName(net, dd, tree->d, d_eq);
257  if (tree->d_comp)
258    SynthMakeComplementString(d_eq);
259  if (flag)
260    return(1);
261  flag = SynthGetChildMlTreeWithName(net, dd, tree->r, r_eq);
262  if (tree->r_comp)
263    SynthMakeComplementString(r_eq);
264  if (flag)
265    return(1);
266
267  if (strcmp(q_eq, "one") == 0)
268    sprintf(qd_eq, "%s", d_eq);
269  else if (strcmp(q_eq, "zero") == 0)
270    sprintf(qd_eq, "zero");
271  else if (strcmp(d_eq, "one") == 0)
272    sprintf(qd_eq, "%s", q_eq);
273  else if (strcmp(d_eq, "zero") == 0)
274    sprintf(qd_eq, "zero");
275  else {
276    if (strlen(q_eq) + strlen(d_eq) + 1 > MAX_EQ_LEN) {
277      sprintf(eq, "%s", q_eq);
278      if (strlen(eq) == MAX_EQ_LEN - 1) {
279        eq[MAX_EQ_LEN - 2] = '#'; /* truncated */
280        eq[MAX_EQ_LEN - 1] = '\0';
281      } else {
282        eq[strlen(eq)] = '#'; /* truncated */
283        eq[strlen(eq) + 1] = '\0';
284      }
285      return(1);
286    }
287    sprintf(qd_eq, "%s%s", q_eq, d_eq);
288  }
289
290  if (strcmp(r_eq, "zero") == 0)
291    sprintf(eq, "%s", qd_eq);
292  else {
293    if (strlen(qd_eq) + strlen(r_eq) + 1 > MAX_EQ_LEN) {
294      sprintf(eq, "%s", qd_eq);
295      if (strlen(eq) == MAX_EQ_LEN - 1) {
296        eq[MAX_EQ_LEN - 2] = '#'; /* truncated */
297        eq[MAX_EQ_LEN - 1] = '\0';
298      } else {
299        eq[strlen(eq)] = '#'; /* truncated */
300        eq[strlen(eq) + 1] = '\0';
301      }
302      return(1);
303    }
304    sprintf(eq, "(%s + %s)", qd_eq, r_eq);
305  }
306  return(0);
307}
308
309
310/**Function********************************************************************
311
312  Synopsis    [Gets the equation form of a tree which is a leaf node with
313  original names.]
314
315  Description [Gets the equation form of a tree which is a leaf node with
316  original names.]
317
318  SideEffects []
319
320  SeeAlso     [SynthGetChildTree]
321
322******************************************************************************/
323int
324SynthGetChildTreeWithName(Ntk_Network_t *net,
325                          bdd_manager *dd,
326                          bdd_node *f,
327                          char *eq)
328{
329  char          left[MAX_EQ_LEN];
330  char          right[MAX_EQ_LEN];
331  bdd_node      *one = bdd_read_one(dd);
332  bdd_node      *zero = bdd_read_zero(dd);
333  int           id, comp;
334  char          name[MAX_NAME_LEN];
335  int           flag;
336
337  if (f == one) {
338    sprintf(eq, "one");
339    return(0);
340  } else if (f == zero) {
341    sprintf(eq, "zero");
342    return(0);
343  }
344
345  flag = SynthGetChildTreeWithName(net, dd, bdd_bdd_T(f), left);
346  if (flag)
347    return(1);
348  flag = SynthGetChildTreeWithName(net, dd, bdd_bdd_E(f), right);
349  if (flag)
350    return(1);
351
352  id = bdd_node_read_index(f);
353  comp = id & 0x1;
354  id = id >> 1;
355
356  sprintf(name, "%s", Ntk_NodeReadName(Ntk_NetworkFindNodeByMddId(net, id)));
357
358  if (comp)
359    strcat(name, "'");
360
361  if (strcmp(left, "one") == 0) {
362    if (strcmp(right, "zero") == 0)
363      sprintf(eq, "%s", name);
364    else {
365      if (strlen(right) + strlen(name) + 6 > MAX_EQ_LEN) {
366        sprintf(eq, "%s", right);
367        if (strlen(eq) == MAX_EQ_LEN - 1) {
368          eq[MAX_EQ_LEN - 2] = '#'; /* truncated */
369          eq[MAX_EQ_LEN - 1] = '\0';
370        } else {
371          eq[strlen(eq)] = '#'; /* truncated */
372          eq[strlen(eq) + 1] = '\0';
373        }
374        return(1);
375      }
376      sprintf(eq, "(%s + %s)", name, right);
377    }
378  } else {
379    if (strcmp(right, "zero") == 0) {
380      if (strlen(left) + strlen(name) + 1 > MAX_EQ_LEN) {
381        sprintf(eq, "%s", left);
382        if (strlen(eq) == MAX_EQ_LEN - 1) {
383          eq[MAX_EQ_LEN - 2] = '#'; /* truncated */
384          eq[MAX_EQ_LEN - 1] = '\0';
385        } else {
386          eq[strlen(eq)] = '#'; /* truncated */
387          eq[strlen(eq) + 1] = '\0';
388        }
389        return(1);
390      }
391      sprintf(eq, "%s%s", name, left);
392    } else {
393      if (strlen(right) + strlen(left) + strlen(name) + 6 >
394          MAX_EQ_LEN) {
395        sprintf(eq, "%s", right);
396        if (strlen(eq) == MAX_EQ_LEN - 1) {
397          eq[MAX_EQ_LEN - 2] = '#'; /* truncated */
398          eq[MAX_EQ_LEN - 1] = '\0';
399        } else {
400          eq[strlen(eq)] = '#'; /* truncated */
401          eq[strlen(eq) + 1] = '\0';
402        }
403        return(1);
404      }
405      sprintf(eq, "(%s%s + %s)", name, left, right);
406    }
407  }
408  return(0);
409}
410
411
412/**Function********************************************************************
413
414  Synopsis    [Gets the original name of a primary node.]
415
416  Description [Gets the original name of a primary node. Return value
417  shows polarity; 0 means positive variable and 1 means negative.]
418
419  SideEffects []
420
421  SeeAlso     []
422
423******************************************************************************/
424int
425SynthGetPrimaryNodeName(Ntk_Network_t *net,
426                        bdd_node *node,
427                        char *name)
428{
429  int   id;
430  int   comp;
431  char  *ntk_name;
432
433  id = bdd_node_read_index(node);
434  comp = id % 2;
435  id = id >> 1;
436
437  ntk_name = Ntk_NodeReadName(Ntk_NetworkFindNodeByMddId(net, id));
438  sprintf(name, "%s", ntk_name);
439
440  return(comp);
441}
442
443
444/**Function********************************************************************
445
446  Synopsis    [Gets the original name of a primary node with index.]
447
448  Description [Gets the original name of a primary node with index.]
449
450  SideEffects []
451
452  SeeAlso     []
453
454******************************************************************************/
455void
456SynthGetPrimaryIndexName(Ntk_Network_t *net,
457                         int index,
458                         char *name)
459{
460  int   id;
461
462  id = index >> 1;
463  sprintf(name, "%s", Ntk_NodeReadName(Ntk_NetworkFindNodeByMddId(net, id)));
464}
465
466
467/**Function********************************************************************
468
469  Synopsis    [Prints the equation form of a ZDD cover with original names.]
470
471  Description [Prints the equation form of a ZDD cover with original names.
472  If the string length is bigger than MAX_EQ_LEN, the string is truncated.]
473
474  SideEffects []
475
476  SeeAlso     []
477
478******************************************************************************/
479void
480SynthPrintZddCoverWithName(Ntk_Network_t *net,
481                           bdd_manager *dd,
482                           bdd_node *node)
483{
484  char cover[MAX_EQ_LEN];
485
486  fprintf(vis_stdout, "cover =");
487  cover[0] = '\0';
488  GetZddCoverWithNameRecur(net, dd, node, cover);
489  fprintf(vis_stdout, "\n");
490}
491
492
493/**Function********************************************************************
494
495  Synopsis    [Makes the complement name of a node name.]
496
497  Description [Makes the complement name of a node name.]
498
499  SideEffects []
500
501  SeeAlso     []
502
503******************************************************************************/
504void
505SynthMakeComplementString(char *eq)
506{
507  int   len;
508
509  if (strcmp(eq, "zero") == 0) {
510    sprintf(eq, "one");
511    return;
512  } else if (strcmp(eq, "one") == 0) {
513    sprintf(eq, "zero");
514    return;
515  }
516  len = strlen(eq);
517  if (eq[len - 1] == '\'')
518    eq[len - 1] = '\0';
519  else {
520    if (len == MAX_EQ_LEN - 1) {
521      eq[len - 2] = '#'; /* truncated */
522      eq[len - 1] = '\'';
523    } else
524      strcat(eq, "'");
525  }
526}
527
528
529/*---------------------------------------------------------------------------*/
530/* Definition of static functions                                            */
531/*---------------------------------------------------------------------------*/
532
533/**Function********************************************************************
534
535  Synopsis    [Gets an equation form of a ZDD node.]
536
537  Description [Gets an equation form of a ZDD node. Returns 1 if
538  eq string is truncated, otherwise normally returns 0.]
539
540  SideEffects []
541
542  SeeAlso     []
543
544******************************************************************************/
545static int
546GetChildTree(bdd_manager *dd,
547             bdd_node *f,
548             char *eq)
549{
550  char          left[MAX_EQ_LEN];
551  char          right[MAX_EQ_LEN];
552  char          tmp[MAX_NAME_LEN];
553  bdd_node      *one = bdd_read_one(dd);
554  bdd_node      *zero = bdd_read_zero(dd);
555  int           flag; /* truncated */
556
557  if (f == one) {
558    sprintf(eq, "one");
559    return(0);
560  } else if (f == zero) {
561    sprintf(eq, "zero");
562    return(0);
563  }
564
565  flag = GetChildTree(dd, bdd_bdd_T(f), left);
566  if (flag)
567    return(1);
568  flag = GetChildTree(dd, bdd_bdd_E(f), right);
569  if (flag)
570    return(1);
571
572  sprintf(tmp, "v%d", bdd_node_read_index(f));
573  if (strcmp(left, "one") == 0) {
574    if (strcmp(right, "zero") == 0)
575      sprintf(eq, "%s", tmp);
576    else {
577      if (strlen(right) + strlen(tmp) + 6 > MAX_EQ_LEN) {
578        sprintf(eq, "%s", right);
579        if (strlen(eq) == MAX_EQ_LEN - 1) {
580          eq[MAX_EQ_LEN - 2] = '#'; /* truncated */
581          eq[MAX_EQ_LEN - 1] = '\0';
582        } else {
583          eq[strlen(eq)] = '#'; /* truncated */
584          eq[strlen(eq) + 1] = '\0';
585        }
586        return(1);
587      }
588      sprintf(eq, "(%s + %s)", tmp, right);
589    }
590  } else {
591    if (strcmp(right, "zero") == 0) {
592      if (strlen(left) + strlen(tmp) + 1 > MAX_EQ_LEN) {
593        sprintf(eq, "%s", left);
594        if (strlen(eq) == MAX_EQ_LEN - 1) {
595          eq[MAX_EQ_LEN - 2] = '#'; /* truncated */
596          eq[MAX_EQ_LEN - 1] = '\0';
597        } else {
598          eq[strlen(eq)] = '#'; /* truncated */
599          eq[strlen(eq) + 1] = '\0';
600        }
601        return(1);
602      }
603      sprintf(eq, "%s%s", tmp, left);
604    } else {
605      if (strlen(right) + strlen(left) + strlen(tmp) + 6 > MAX_EQ_LEN) {
606        sprintf(eq, "%s", right);
607        if (strlen(eq) == MAX_EQ_LEN - 1) {
608          eq[MAX_EQ_LEN - 2] = '#'; /* truncated */
609          eq[MAX_EQ_LEN - 1] = '\0';
610        } else {
611          eq[strlen(eq)] = '#'; /* truncated */
612          eq[strlen(eq) + 1] = '\0';
613        }
614        return(1);
615      }
616      sprintf(eq, "(%s%s + %s)", tmp, left, right);
617    }
618  }
619  return(0);
620}
621
622
623/**Function********************************************************************
624
625  Synopsis    [Gets the equation form of a tree with internal name.]
626
627  Description [Gets the equation form of a tree with internal name. Returns
628  1 if eq string is truncated, otherwise normally returns 0.]
629
630  SideEffects []
631
632  SeeAlso     []
633
634******************************************************************************/
635static int
636GetChildMlTree(bdd_manager *dd,
637               MlTree *tree,
638               char *eq)
639{
640  char          q_eq[MAX_EQ_LEN];
641  char          d_eq[MAX_EQ_LEN];
642  char          r_eq[MAX_EQ_LEN];
643  char          qd_eq[MAX_EQ_LEN];
644  bdd_node      *one = bdd_read_one(dd);
645  bdd_node      *zero = bdd_read_zero(dd);
646  bdd_node      *f;
647  int           flag;
648
649  f = tree->node;
650  if (tree->leaf) {
651    flag = GetChildTree(dd, f, eq);
652    return(flag);
653  }
654
655  if (f == one) {
656    sprintf(eq, "one");
657    return(0);
658  } else if (f == zero) {
659    sprintf(eq, "zero");
660    return(0);
661  }
662
663  flag = GetChildMlTree(dd, tree->q, q_eq);
664  if (tree->q_comp)
665    SynthMakeComplementString(q_eq);
666  if (flag)
667    return(1);
668  flag = GetChildMlTree(dd, tree->d, d_eq);
669  if (tree->d_comp)
670    SynthMakeComplementString(d_eq);
671  if (flag)
672    return(1);
673  flag = GetChildMlTree(dd, tree->r, r_eq);
674  if (tree->r_comp)
675    SynthMakeComplementString(r_eq);
676  if (flag)
677    return(1);
678
679  if (strcmp(q_eq, "one") == 0)
680    sprintf(qd_eq, "%s", d_eq);
681  else if (strcmp(q_eq, "zero") == 0)
682    sprintf(qd_eq, "zero");
683  else if (strcmp(d_eq, "one") == 0)
684    sprintf(qd_eq, "%s", q_eq);
685  else if (strcmp(d_eq, "zero") == 0)
686    sprintf(qd_eq, "zero");
687  else {
688    if (strlen(q_eq) + strlen(d_eq) + 1 > MAX_EQ_LEN) {
689      sprintf(eq, "%s", q_eq);
690      if (strlen(eq) == MAX_EQ_LEN - 1) {
691        eq[MAX_EQ_LEN - 2] = '#'; /* truncated */
692        eq[MAX_EQ_LEN - 1] = '\0';
693      } else {
694        eq[strlen(eq)] = '#'; /* truncated */
695        eq[strlen(eq) + 1] = '\0';
696      }
697      return(1);
698    }
699    sprintf(qd_eq, "%s%s", q_eq, d_eq);
700  }
701
702  if (strcmp(r_eq, "zero") == 0)
703    sprintf(eq, "%s", qd_eq);
704  else {
705    if (strlen(qd_eq) + strlen(r_eq) + 1 > MAX_EQ_LEN) {
706      sprintf(eq, "%s", qd_eq);
707      if (strlen(eq) == MAX_EQ_LEN - 1) {
708        eq[MAX_EQ_LEN - 2] = '#'; /* truncated */
709        eq[MAX_EQ_LEN - 1] = '\0';
710      } else {
711        eq[strlen(eq)] = '#'; /* truncated */
712        eq[strlen(eq) + 1] = '\0';
713      }
714      return(1);
715    }
716    sprintf(eq, "(%s + %s)", qd_eq, r_eq);
717  }
718  return(0);
719}
720
721
722/**Function********************************************************************
723
724  Synopsis    [Finds a node that has the given index.]
725
726  Description [Finds a node that has the given index among the descendants
727  of the given node (this node included). If there exists a node with
728  the index, the node is returned, otherwise returns NULL.]
729
730  SideEffects []
731
732  SeeAlso     []
733
734******************************************************************************/
735static bdd_node *
736FindNodeWithIndex(bdd_node *node,
737                  int index)
738{
739  bdd_node      *tmp;
740
741  if (bdd_is_constant(node))
742    return(NULL);
743  if (bdd_node_read_index(node) == index)
744    return(node);
745
746  tmp = FindNodeWithIndex(bdd_bdd_T(node), index);
747  if (tmp)
748    return(tmp);
749  return(FindNodeWithIndex(bdd_bdd_E(node), index));
750}
751
752
753/**Function********************************************************************
754
755  Synopsis    [Gets the equation form of a ZDD cover with original names.]
756
757  Description [Gets an equation form of a ZDD cover with original names.]
758
759  SideEffects []
760
761  SeeAlso     []
762
763******************************************************************************/
764static void
765GetZddCoverWithNameRecur(Ntk_Network_t *net,
766                         bdd_manager *dd,
767                         bdd_node *node,
768                         char *cover)
769{
770  bdd_node      *one = bdd_read_one(dd);
771  bdd_node      *zero = bdd_read_zero(dd);
772  int           len, index;
773  char          name[MAX_NAME_LEN], *varName;
774
775  if (node == zero)
776    return;
777
778  if (node == one) {
779    fprintf(vis_stdout, " + %s", cover);
780    return;
781  }
782
783  len = strlen(cover);
784  index = bdd_node_read_index(node);
785  varName = Ntk_NodeReadName(Ntk_NetworkFindNodeByMddId(net, index / 2));
786  if (index % 2 == 0)
787    sprintf(name, "%s", varName);
788  else
789    sprintf(name, "%s'", varName);
790  strcat(cover, name);
791  GetZddCoverWithNameRecur(net, dd, bdd_bdd_T(node), cover);
792  cover[len] = '\0';
793  GetZddCoverWithNameRecur(net, dd, bdd_bdd_E(node), cover);
794  cover[len] = '\0';
795}
796
797
Note: See TracBrowser for help on using the repository browser.