source: vis_dev/vis-2.3/src/synth/synthWrite.c

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

vis2.3
File size: 50.6 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [synthWrite.c]
4
5  PackageName [synth]
6
7  Synopsis    [Functions to write blif file and equation file.]
8
9  Description []
10
11  Author      [In-Ho Moon, Balakrishna Kumthekar]
12
13  Copyright [This file was created at the University of Colorado at Boulder.
14  The University of Colorado at Boulder makes no warranty about the suitability
15  of this software for any purpose.  It is presented on an AS IS basis.]
16
17******************************************************************************/
18
19#include "synthInt.h"
20
21static char rcsid[] UNUSED = "$Id: synthWrite.c,v 1.43 2005/05/11 20:18:39 hhhan Exp $";
22
23/*---------------------------------------------------------------------------*/
24/* Constant declarations                                                     */
25/*---------------------------------------------------------------------------*/
26
27
28/*---------------------------------------------------------------------------*/
29/* Type declarations                                                         */
30/*---------------------------------------------------------------------------*/
31
32
33/*---------------------------------------------------------------------------*/
34/* Structure declarations                                                    */
35/*---------------------------------------------------------------------------*/
36
37/**Struct**********************************************************************
38
39  Synopsis    [Type to store a line of the truth table of a node.
40  The entire truth table is implemented as a linked list of
41  objects of this type.]
42
43  Description []
44
45  SeeAlso     []
46
47******************************************************************************/
48typedef struct TruthTableLine {
49  char *values;    /* string of 1, 0, and - */
50  struct TruthTableLine *next; /* pointer to next table line */
51} TruthTableLine;
52
53
54/*---------------------------------------------------------------------------*/
55/* Variable declarations                                                     */
56/*---------------------------------------------------------------------------*/
57
58static  char            *DefaultPrefix = "_n";
59static  char            *InternalNodePrefix;
60static  st_table        *NodeNameTable; /* to keep all node names for
61                                         * primary input, primary output
62                                         * latch input and output
63                                         */
64
65/**AutomaticStart*************************************************************/
66
67/*---------------------------------------------------------------------------*/
68/* Static function prototypes                                                */
69/*---------------------------------------------------------------------------*/
70
71static void WriteMlBlif(Ntk_Network_t *net, bdd_manager *dd, MlTree *tree, FILE *fout, int no, bdd_node **ofuncs, int *oflags, int top_flag, int verbosity);
72static void WriteLeafMlBlif(Ntk_Network_t *net, bdd_manager *dd, MlTree *tree, FILE *fout, int no, bdd_node **ofuncs, int *oflags, int top_flag, int verbosity);
73static void WriteBlifBinary(bdd_manager *dd, bdd_node *node, char *name, FILE *fout, int *support);
74static void WriteEqnOfTree(FILE *fout, Ntk_Network_t *net, bdd_manager *dd, MlTree *tree, bdd_node **ofuncs);
75static int GetEqnOfTree(Ntk_Network_t *net, bdd_manager *dd, MlTree *top, MlTree *tree, char *eq, bdd_node **ofuncs);
76static void WriteMlTreeBlif(FILE *fout, Ntk_Network_t *net, bdd_manager *dd, MlTree *tree, bdd_node **ofuncs, int no, char *func_name, int ref);
77static void WriteMultiLevelBlif(FILE *fout, Ntk_Network_t *net, bdd_manager *dd, MlTree *tree, bdd_node **ofuncs, int no);
78static TruthTableLine * GetMultiLevelBlifRecur(Ntk_Network_t *net, bdd_manager *dd, MlTree *top, MlTree *tree, bdd_node **ofuncs, int no, st_table *table, int ni);
79static int GetMultiLevelNodes(Ntk_Network_t *net, bdd_manager *dd, MlTree *top, MlTree *tree, bdd_node **ofuncs, int no, st_table *table, int ni);
80static int GetLeafNodes(Ntk_Network_t *net, bdd_manager *dd, MlTree *tree, bdd_node **ofuncs, int no, st_table *table, int ni);
81static TruthTableLine * GetTautologyLine(int ni);
82static TruthTableLine * GetLeafLines(Ntk_Network_t *net, bdd_manager *dd, MlTree *tree, bdd_node **ofuncs, int no, st_table *table, int ni);
83static TruthTableLine * GetBlifBinary(TruthTableLine *line, bdd_manager *dd, bdd_node *node, char *values, int *support, int ni);
84static TruthTableLine * GetComplementOneLine(TruthTableLine *line, int ni, int flag);
85static TruthTableLine * GetComplementLines(TruthTableLine *lines, int ni, int flag);
86static TruthTableLine * GetAndLines(TruthTableLine *line1, TruthTableLine *line2, int ni, int flag);
87static bdd_node * GetDdNodeOfMlTree(MlTree *tree, int comp);
88static int GetMlTreeName(Ntk_Network_t *net, bdd_node **ofuncs, MlTree *tree, char *name);
89static char ** GetAllVarNameArray(bdd_manager *dd);
90
91/**AutomaticEnd***************************************************************/
92
93
94/*---------------------------------------------------------------------------*/
95/* Definition of exported functions                                          */
96/*---------------------------------------------------------------------------*/
97
98
99/*---------------------------------------------------------------------------*/
100/* Definition of internal functions                                          */
101/*---------------------------------------------------------------------------*/
102
103
104/**Function********************************************************************
105
106  Synopsis    [Compares two strings to see which one is first in
107  alphabetic order.]
108
109  Description [Compares two strings to see which one is first in
110  alphabetic order.]
111
112  SideEffects []
113
114  SeeAlso     [qsort]
115
116******************************************************************************/
117int
118SynthStringCompare(char **a,
119                   char **b)
120{
121  char  *pa, *pb;
122
123  pa = *a;
124  pb = *b;
125
126  if (*pa == '\0') {
127    if (*pb == '\0')
128      return(0);
129    else
130      return(-1);
131  } else if (*pb == '\0')
132    return(1);
133  while (*pa != '\0' && *pb != '\0') {
134    if (*pa > *pb)
135      return(1);
136    if (*pa < *pb)
137      return(-1);
138    pa++;
139    pb++;
140    if (*pa == '\0') {
141      if (*pb == '\0')
142        return(0);
143      else
144        return(-1);
145    } else if (*pb == '\0')
146      return(1);
147  }
148  return(0);
149}
150
151
152/**Function********************************************************************
153
154  Synopsis    [Write a blif file of the factorized network.]
155
156  Description [Write a blif file of the factorized network. There are 2
157  ways of writing a blif file depending on argument ml_mode. If
158  ml_mode is 0, then the resulting blif file will be based on the
159  factorized multi level tree that has 3 children; quotient, divisor,
160  and remainder. If ml_mode is 1, then the resulting blif file will be
161  generated as follows. All top nodes and all nodes that are shared will
162  be output nodes of .names in blif file. By default, ml_mode is 0.]
163
164  SideEffects []
165
166  SeeAlso     []
167
168******************************************************************************/
169void
170SynthWriteBlifFile(Ntk_Network_t *net,
171                   bdd_manager *dd,
172                   MlTree **tree,
173                   char *filename,
174                   int no,
175                   bdd_node **ofuncs,
176                   int *initStates,
177                   int ml_mode,
178                   int verbosity)
179{
180  FILE          *fout;
181  int           i, j;
182  int           *oflags;
183  char          out_name[MAX_NAME_LEN], name[MAX_NAME_LEN];
184  lsGen         gen;
185  Ntk_Node_t    *node;
186  char          **sorted_name;
187  int           ni, po;
188  int           polarity;
189
190  fout = Cmd_FileOpen(filename, "w", NIL(char *), 0);
191  if (!fout) {
192    (void)fprintf(vis_stdout,
193                  "** synth error: Error in opening file [%s]\n", filename);
194    return;
195  }
196
197  fprintf(fout, ".model %s\n", Ntk_NetworkReadName(net));
198  fprintf(fout, ".inputs");
199
200  /* Write list of primary inputs sorted lexicographically. */
201  ni = Ntk_NetworkReadNumPrimaryInputs(net);
202  sorted_name = ALLOC(char *, ni * sizeof(char *));
203  i = 0;
204  Ntk_NetworkForEachPrimaryInput(net, gen, node) {
205    sorted_name[i++] = Ntk_NodeReadName(node);
206  }
207  qsort(sorted_name, ni, sizeof(char *),
208        (int (*)(const void *, const void *)) SynthStringCompare);
209  for (i = 0; i < ni; i++)
210    fprintf(fout," %s", sorted_name[i]);
211  FREE(sorted_name);
212
213  fprintf(fout, "\n");
214  fprintf(fout, ".outputs");
215
216  /* Write list of primary outputs sorted lexicographically. */
217  po = Ntk_NetworkReadNumPrimaryOutputs(net);
218  sorted_name = ALLOC(char *, po * sizeof(char *));
219  i = 0;
220  Ntk_NetworkForEachPrimaryOutput(net, gen, node) {
221    sorted_name[i++] = Ntk_NodeReadName(node);
222  }
223  qsort(sorted_name, po, sizeof(char *),
224        (int (*)(const void *, const void *))SynthStringCompare);
225  for (i = 0; i < po; i++)
226    fprintf(fout," %s", sorted_name[i]);
227  FREE(sorted_name);
228  fprintf(fout, "\n");
229
230  /* Print list of latches. */
231  i = 0;
232  Ntk_NetworkForEachLatch(net, gen, node) {
233    fprintf(fout,".latch %s", Ntk_NodeReadName(Ntk_LatchReadDataInput(node)));
234    fprintf(fout, " %s", Ntk_NodeReadName(node));
235    fprintf(fout, " %d\n", initStates[i]);
236    i++;
237  }
238
239  oflags = ALLOC(int, no);
240  (void)memset((void *)oflags, 0, no * sizeof(int));
241  for (i = 0; i < no; i++) {
242    if (!tree[i])
243      continue;
244    if (bdd_is_constant(tree[i]->node)) {
245      if (tree[i]->comp) {
246        for (j = 0; j < no; j++) {
247          if (tree[i]->complement == ofuncs[j] && oflags[j] == 0) {
248            sprintf(out_name, "%s", SynthGetIthOutputName(j));
249            break;
250          }
251        }
252      } else {
253        for (j = 0; j < no; j++) {
254          if (tree[i]->node == ofuncs[j] && oflags[j] == 0) {
255            sprintf(out_name, "%s", SynthGetIthOutputName(j));
256            break;
257          }
258        }
259      }
260      if (j == no)
261        SynthGetInternalNodeName(out_name, tree[i]->id);
262      else {
263        if (oflags[j])
264          continue;
265        else
266          oflags[j] = 1;
267      }
268      fprintf(fout, "\n.names %s\n", out_name);
269      if (tree[i]->node == bdd_read_one(dd)) {
270        if (tree[i]->comp)
271          fprintf(fout, "0\n");
272        else
273          fprintf(fout, "1\n");
274      } else {
275        if (tree[i]->comp)
276          fprintf(fout, "1\n");
277        else
278          fprintf(fout, "0\n");
279      }
280      continue;
281    } else if (tree[i]->ref) {
282      for (j = 0; j < no; j++) {
283        if ((((tree[i]->comp == 0 && tree[i]->node == ofuncs[j]) ||
284              (tree[i]->comp && tree[i]->complement == ofuncs[j]))) &&
285            oflags[j] == 0) {
286          sprintf(out_name, "%s", SynthGetIthOutputName(j));
287          break;
288        }
289      }
290      if (j == no)
291        SynthGetInternalNodeName(out_name, tree[i]->id);
292      else {
293        if (oflags[j])
294          continue;
295        else
296          oflags[j] = 1;
297      }
298      polarity = GetMlTreeName(net, ofuncs, tree[i], name);
299      if (strcmp(out_name, name) == 0)
300        SynthGetPrimaryNodeName(net, tree[i]->node, name);
301      fprintf(fout, "\n.names %s %s\n", name, out_name);
302      if (polarity == 0) {
303        if (tree[i]->comp)
304          fprintf(fout, "0 1\n");
305        else
306          fprintf(fout, "1 1\n");
307      } else {
308        if (tree[i]->comp)
309          fprintf(fout, "1 1\n");
310        else
311          fprintf(fout, "0 1\n");
312      }
313      continue;
314    }
315    if (ml_mode == 0) {
316      if (tree[i]->pi) {
317        tree[i]->pi = 0;
318        WriteMlBlif(net, dd, tree[i], fout, no, ofuncs, oflags, 1, verbosity);
319        tree[i]->pi = 1;
320      } else {
321        WriteMlBlif(net, dd, tree[i], fout, no, ofuncs, oflags, 1, verbosity);
322      }
323    } else {
324      for (j = 0; j < no; j++) {
325        if (tree[i]->node == ofuncs[j]) {
326          if (oflags[j])
327            continue;
328          else
329            oflags[j] = 1;
330          sprintf(out_name, "%s", SynthGetIthOutputName(j));
331          break;
332        }
333      }
334      if (j == no)
335        SynthGetInternalNodeName(out_name, tree[i]->id);
336      if (tree[i]->pi) {
337        tree[i]->pi = 0;
338        WriteMlTreeBlif(fout, net, dd, tree[i], ofuncs, no, out_name, 1);
339        tree[i]->pi = 1;
340      } else {
341        WriteMlTreeBlif(fout, net, dd, tree[i], ofuncs, no, out_name, 1);
342      }
343    }
344  }
345  FREE(oflags);
346
347  fprintf(fout, "\n.end\n");
348  fclose(fout);
349}
350
351
352/**Function********************************************************************
353
354  Synopsis    [Writes header of equation format for a network.]
355
356  Description [Writes header of equation format for a network.]
357
358  SideEffects []
359
360  SeeAlso     []
361
362******************************************************************************/
363void
364SynthWriteEqnHeader(FILE *fout,
365                  Ntk_Network_t *net,
366                  bdd_manager *dd)
367{
368  int           i;
369  lsGen         gen;
370  Ntk_Node_t    *node;
371  char          **sorted_name;
372  int           ni, po;
373
374  /* Write list of primary inputs sorted lexicographically. */
375  ni = Ntk_NetworkReadNumPrimaryInputs(net);
376  sorted_name = ALLOC(char *, ni * sizeof(char *));
377  i = 0;
378  Ntk_NetworkForEachPrimaryInput(net, gen, node) {
379    sorted_name[i++] = Ntk_NodeReadName(node);
380  }
381  qsort(sorted_name, ni, sizeof(char *),
382        (int (*)(const void *, const void *))SynthStringCompare);
383  fprintf(fout, "INORDER");
384  for (i = 0; i < ni; i++)
385    fprintf(fout," %s", sorted_name[i]);
386  fprintf(fout, "\n");
387  FREE(sorted_name);
388
389  /* Write list of primary outputs sorted lexicographically. */
390  po = Ntk_NetworkReadNumPrimaryOutputs(net);
391  sorted_name = ALLOC(char *, po * sizeof(char *));
392  i = 0;
393  Ntk_NetworkForEachPrimaryOutput(net, gen, node) {
394    sorted_name[i++] = Ntk_NodeReadName(node);
395  }
396  qsort(sorted_name, po, sizeof(char *),
397        (int (*)(const void *, const void *))SynthStringCompare);
398  fprintf(fout, "OUTORDER");
399  for (i = 0; i < po; i++)
400    fprintf(fout," %s", sorted_name[i]);
401  fprintf(fout, "\n");
402  FREE(sorted_name);
403}
404
405
406/**Function********************************************************************
407
408  Synopsis    [Writes an equation of a factorized tree.]
409
410  Description [Writes an equation of a factorized tree.]
411
412  SideEffects []
413
414  SeeAlso     []
415
416******************************************************************************/
417void
418SynthWriteEqn(FILE *fout,
419              Ntk_Network_t *net,
420              bdd_manager *dd,
421              MlTree *tree,
422              bdd_node **ofuncs,
423              char *func_name,
424              int ref)
425{
426  char  name[MAX_NAME_LEN];
427  int   polarity = 0;
428
429  if (tree->top || tree->shared) {
430    if (ref) {
431      /* If tree is shared we print the name of the original function
432       * unless it is a constant.
433       */
434      if (tree->ref) {
435        if (tree->node == bdd_read_zero(dd))
436          sprintf(name, "zero");
437        else if (tree->node == bdd_read_one(dd))
438          sprintf(name, "one");
439        else
440          polarity = GetMlTreeName(net, ofuncs, tree, name);
441        if (polarity == 0) {
442          if (tree->comp)
443            SynthMakeComplementString(name);
444        } else {
445          if (!tree->comp)
446            SynthMakeComplementString(name);
447        }
448        fprintf(fout, "%s = %s\n", func_name, name);
449        return;
450      }
451    }
452    WriteEqnOfTree(fout, net, dd, tree, ofuncs);
453  }
454
455  if (tree->leaf) {
456    return;
457  }
458
459  if (tree->q_ref == 0)
460    SynthWriteEqn(fout, net, dd, tree->q, ofuncs, NULL, ref);
461  if (tree->d_ref == 0)
462    SynthWriteEqn(fout, net, dd, tree->d, ofuncs, NULL, ref);
463  if (tree->r_ref == 0)
464    SynthWriteEqn(fout, net, dd, tree->r, ofuncs, NULL, ref);
465}
466
467
468/**Function********************************************************************
469
470  Synopsis    [Set the prefix of internal node name.]
471
472  Description [Set the prefix of internal node name.]
473
474  SideEffects []
475
476  SeeAlso     []
477
478******************************************************************************/
479void
480SynthSetInternalNodePrefix(char *prefix)
481{
482  if (prefix)
483    InternalNodePrefix = prefix;
484  else
485    InternalNodePrefix = DefaultPrefix;
486}
487
488
489/**Function********************************************************************
490
491  Synopsis    [Creates a st_table to keep all node names for primary
492  input, primary output, latch input and output nodes.]
493
494  Description [Creates a st_table to keep all node names for primary
495  input, primary output, latch input and output nodes. This table is used
496  when we make internal node names, to see if there is a same name.]
497
498  SideEffects []
499
500  SeeAlso     [SynthFreeNodeNameTable SynthGetInternalNodeName]
501
502******************************************************************************/
503void
504SynthSetupNodeNameTable(Ntk_Network_t *net)
505{
506  lsGen         gen;
507  Ntk_Node_t    *node;
508
509  if (NodeNameTable) {
510    (void)fprintf(vis_stdout,
511        "** synth warning: table already exists in SynthSetupNodeNameTable.\n");
512    st_free_table(NodeNameTable);
513  }
514
515  NodeNameTable = st_init_table(strcmp, st_strhash);
516
517  /* Register all primary input node names. */
518  Ntk_NetworkForEachPrimaryInput(net, gen, node) {
519    st_insert(NodeNameTable, Ntk_NodeReadName(node), (char *)NULL);
520  }
521
522  /* Register all primary output node names. */
523  Ntk_NetworkForEachPrimaryOutput(net, gen, node) {
524    st_insert(NodeNameTable, Ntk_NodeReadName(node), (char *)NULL);
525  }
526
527  /* Register all latch input and output node names. */
528  Ntk_NetworkForEachLatch(net, gen, node) {
529    st_insert(NodeNameTable, Ntk_NodeReadName(Ntk_LatchReadDataInput(node)),
530              (char *)NULL);
531    st_insert(NodeNameTable, Ntk_NodeReadName(node), (char *)NULL);
532  }
533}
534
535
536/**Function********************************************************************
537
538  Synopsis    [Frees the st_table named NodeNameTable.]
539
540  Description [Frees the st_table named NodeNameTable.]
541
542  SideEffects []
543
544  SeeAlso     [SynthSetupNodeNameTable SynthGetInternalNodeName]
545
546******************************************************************************/
547void
548SynthFreeNodeNameTable(void)
549{
550  st_free_table(NodeNameTable);
551  NodeNameTable = NIL(st_table);
552}
553
554
555/**Function********************************************************************
556
557  Synopsis    [Returns a proper internal node name.]
558
559  Description [Returns a proper internal node name. Internal node name
560  is made by "prefix+id". If NodeNameTable exists, fist lookup the table
561  to see if the name already exists. If it exists, another prefix
562  "_synth_" is used. Then, whenever a same name exists, extra prefix "_"
563  is used.]
564
565  SideEffects []
566
567  SeeAlso     [SynthSetupNodeNameTable SynthFreeNodeNameTable]
568
569******************************************************************************/
570void
571SynthGetInternalNodeName(char *name, int id)
572{
573  sprintf(name, "%s%d", InternalNodePrefix, id);
574  if (NodeNameTable) {
575    if (st_lookup(NodeNameTable, name, NIL(char *))) {
576      int       pos;
577
578      sprintf(name, "_synth_%s%d", InternalNodePrefix, id);
579      pos = 7; /* _synth_ */
580      while (st_lookup(NodeNameTable, name, NIL(char *))) {
581        sprintf(&name[pos], "_%s%d", InternalNodePrefix, id);
582        pos++;
583      }
584    }
585  } else {
586    (void)fprintf(vis_stdout,
587                  "** synth warning: skipping internal node name checking.\n");
588  }
589}
590
591
592/**Function********************************************************************
593
594  Synopsis    [Dumps Bdds of all output nodes.]
595
596  Description [Dumps Bdds of all output nodes. just for debug]
597
598  SideEffects []
599
600  SeeAlso     []
601
602******************************************************************************/
603void
604SynthDumpBlif(Ntk_Network_t *net,
605              bdd_manager *dd,
606              int no,
607              bdd_node **ofuncs,
608              char **onames,
609              int *initStates,
610              char *model)
611{
612  int           size;
613  bdd_node      **bdds;
614  FILE          *fout;
615  char          **inames;
616  char          filename[MAX_NAME_LEN];
617  int           i;
618  lsGen         gen;
619  Ntk_Node_t    *node;
620  char          **sorted_name;
621  int           ni, po;
622
623  sprintf(filename, "%s.debug.blif", model);
624  fout = fopen(filename, "w");
625  if (!fout) {
626    (void)fprintf(vis_stderr,
627                  "** synth error: Can't open the file %s.\n", filename);
628    return;
629  }
630
631  fprintf(fout, ".model %s\n", model);
632  fprintf(fout, ".inputs");
633
634  /* Write list of primary inputs sorted lexicographically. */
635  ni = Ntk_NetworkReadNumPrimaryInputs(net);
636  sorted_name = ALLOC(char *, ni * sizeof(char *));
637  i = 0;
638  Ntk_NetworkForEachPrimaryInput(net, gen, node) {
639    sorted_name[i++] = Ntk_NodeReadName(node);
640  }
641  qsort(sorted_name, ni, sizeof(char *),
642        (int (*)(const void *, const void *))SynthStringCompare);
643  for (i = 0; i < ni; i++)
644    fprintf(fout," %s", sorted_name[i]);
645  FREE(sorted_name);
646
647  fprintf(fout, "\n");
648  fprintf(fout, ".outputs");
649
650  /* Write list of primary outputs sorted lexicographically. */
651  po = Ntk_NetworkReadNumPrimaryOutputs(net);
652  sorted_name = ALLOC(char *, po * sizeof(char *));
653  i = 0;
654  Ntk_NetworkForEachPrimaryOutput(net, gen, node) {
655    sorted_name[i++] = Ntk_NodeReadName(node);
656  }
657  qsort(sorted_name, po, sizeof(char *),
658        (int (*)(const void *, const void *))SynthStringCompare);
659  for (i = 0; i < po; i++)
660    fprintf(fout," %s", sorted_name[i]);
661  FREE(sorted_name);
662  fprintf(fout, "\n");
663
664  /* Print list of latches. */
665  i = 0;
666  Ntk_NetworkForEachLatch(net, gen, node) {
667    fprintf(fout,".latch %s", Ntk_NodeReadName(Ntk_LatchReadDataInput(node)));
668    fprintf(fout, " %s", Ntk_NodeReadName(node));
669    fprintf(fout, " %d\n", initStates[i]);
670    i++;
671  }
672
673  bdds = ALLOC(bdd_node *, no);
674
675  for (i = 0; i < no; i++) {
676    bdds[i] = bdd_make_bdd_from_zdd_cover(dd, ofuncs[i]);
677    bdd_ref(bdds[i]);
678  }
679
680  inames = GetAllVarNameArray(dd);
681  if (!inames) {
682    for (i = 0; i < no; i++)
683      bdd_recursive_deref(dd, bdds[i]);
684    FREE(bdds);
685    fclose(fout);
686    (void)fprintf(vis_stderr, "** synth error: Out of memory.\n");
687    return;
688  }
689
690  bdd_dump_blif_body(dd, no, bdds, inames, onames, fout);
691  fprintf(fout, ".end\n");
692
693  size = bdd_num_vars(dd);
694  for (i = 0; i < size; i++)
695    FREE(inames[i]);
696  FREE(inames);
697
698  for (i = 0; i < no; i++)
699    bdd_recursive_deref(dd, bdds[i]);
700
701  FREE(bdds);
702  fclose(fout);
703}
704
705
706/*---------------------------------------------------------------------------*/
707/* Definition of static functions                                            */
708/*---------------------------------------------------------------------------*/
709
710/**Function********************************************************************
711
712  Synopsis    [Writes a part of a blif file for each output function.]
713
714  Description [Writes a part of a blif file for each output function.
715  The resulting blif file will be based on the factorized multi level tree
716  that has 3 children: quotient, divisor, and remainder.]
717
718  SideEffects []
719
720  SeeAlso     [WriteMlTreeBlif]
721
722******************************************************************************/
723static void
724WriteMlBlif(Ntk_Network_t *net,
725            bdd_manager *dd,
726            MlTree *tree,
727            FILE *fout,
728            int no,
729            bdd_node **ofuncs,
730            int *oflags,
731            int top_flag,
732            int verbosity)
733{
734  int           i;
735  char          name[MAX_NAME_LEN], q_name[MAX_NAME_LEN];
736  char          d_name[MAX_NAME_LEN], r_name[MAX_NAME_LEN];
737  char          eq[MAX_EQ_LEN];
738  bdd_node      *one = bdd_read_one(dd);
739  bdd_node      *zero = bdd_read_zero(dd);
740  char          q, d, r;
741  int           comp;
742
743  if (tree->leaf) {
744    WriteLeafMlBlif(net, dd, tree, fout, no, ofuncs, oflags, top_flag,
745                    verbosity);
746    return;
747  }
748
749  if (!tree->ref) {
750    if (!tree->q_ref)
751      WriteMlBlif(net, dd, tree->q, fout, no, ofuncs, oflags, 0, verbosity);
752    if (!tree->d_ref)
753      WriteMlBlif(net, dd, tree->d, fout, no, ofuncs, oflags, 0, verbosity);
754    if (!tree->r_ref)
755      WriteMlBlif(net, dd, tree->r, fout, no, ofuncs, oflags, 0, verbosity);
756  }
757
758  for (i = 0; i < no; i++) {
759    if (tree->node == ofuncs[i]) {
760      if (top_flag == 0)
761        return;
762
763      if (oflags[i])
764        continue;
765      else
766        oflags[i] = 1;
767      sprintf(name, "%s",  SynthGetIthOutputName(i));
768      break;
769    }
770  }
771  if (i == no)
772    SynthGetInternalNodeName(name, tree->id);
773
774  fprintf(fout, "\n");
775  if (verbosity > 2) {
776    SynthGetChildMlTreeWithName(net, dd, tree, eq);
777    (void)fprintf(fout, "# %s\n", eq);
778  }
779
780  if (tree->q->pi) {
781    comp = SynthGetPrimaryNodeName(net, tree->q->node, q_name);
782
783    if (comp)
784      q = '0';
785    else
786      q = '1';
787    if (tree->q_comp) {
788      if (q == '0')
789        q = '1';
790      else
791        q = '0';
792    }
793  } else {
794    for (i = 0; i < no; i++) {
795      if (tree->q->node == ofuncs[i]) {
796        sprintf(q_name, "%s",  SynthGetIthOutputName(i));
797        break;
798      }
799    }
800    if (i == no)
801      SynthGetInternalNodeName(q_name, tree->q->id);
802    if (tree->q_comp)
803      q = '0';
804    else
805      q = '1';
806  }
807  if (tree->d->pi) {
808    comp = SynthGetPrimaryNodeName(net, tree->d->node, d_name);
809
810    if (comp)
811      d = '0';
812    else
813      d = '1';
814    if (tree->d_comp) {
815      if (d == '0')
816        d = '1';
817      else
818        d = '0';
819    }
820  } else {
821    for (i = 0; i < no; i++) {
822      if (tree->d->node == ofuncs[i]) {
823        sprintf(d_name, "%s", SynthGetIthOutputName(i));
824        break;
825      }
826    }
827    if (i == no)
828      SynthGetInternalNodeName(d_name, tree->d->id);
829    if (tree->d_comp)
830      d = '0';
831    else
832      d = '1';
833  }
834  if (tree->r->pi) {
835    comp = SynthGetPrimaryNodeName(net, tree->r->node, r_name);
836
837    if (comp)
838      r = '0';
839    else
840      r = '1';
841    if (tree->r_comp) {
842      if (r == '0')
843        r = '1';
844      else
845        r = '0';
846    }
847  } else {
848    for (i = 0; i < no; i++) {
849      if (tree->r->node == ofuncs[i]) {
850        sprintf(r_name, "%s", SynthGetIthOutputName(i));
851        break;
852      }
853    }
854    if (i == no)
855      SynthGetInternalNodeName(r_name, tree->r->id);
856    if (tree->r_comp)
857      r = '0';
858    else
859      r = '1';
860  }
861
862  if (GetDdNodeOfMlTree(tree->q, tree->q_comp) == zero ||
863      GetDdNodeOfMlTree(tree->d, tree->d_comp) == zero) {
864    if (GetDdNodeOfMlTree(tree->r, tree->r_comp) == one) {
865      fprintf(fout, ".names %s\n", name);
866      fprintf(fout, "1\n");
867    } else if (GetDdNodeOfMlTree(tree->r, tree->r_comp) == zero) {
868      fprintf(fout, ".names %s\n", name);
869      fprintf(fout, "0\n");
870    } else {
871      fprintf(fout, ".names %s %s\n", r_name, name);
872      fprintf(fout, "%c 1\n", r);
873    }
874  } else if (GetDdNodeOfMlTree(tree->q, tree->q_comp) == one) {
875    if (GetDdNodeOfMlTree(tree->d, tree->d_comp) == one) {
876      fprintf(fout, ".names %s\n", name);
877      fprintf(fout, "1\n");
878    } else if (GetDdNodeOfMlTree(tree->d, tree->d_comp) == zero) {
879      if (GetDdNodeOfMlTree(tree->r, tree->r_comp) == one) {
880        fprintf(fout, ".names %s\n", name);
881        fprintf(fout, "1\n");
882      } else if (GetDdNodeOfMlTree(tree->r, tree->r_comp) == zero) {
883        fprintf(fout, ".names %s\n", name);
884        fprintf(fout, "0\n");
885      } else {
886        fprintf(fout, ".names %s %s\n", r_name, name);
887        fprintf(fout, "%c 1\n", r);
888      }
889    } else {
890      if (GetDdNodeOfMlTree(tree->r, tree->r_comp) == one) {
891        fprintf(fout, ".names %s\n", name);
892        fprintf(fout, "1\n");
893      } else if (GetDdNodeOfMlTree(tree->r, tree->r_comp) == zero) {
894        fprintf(fout, ".names %s %s\n", d_name, name);
895        fprintf(fout, "%c 1\n", d);
896      } else {
897        fprintf(fout, ".names %s %s %s\n", d_name, r_name,
898                name);
899        fprintf(fout, "%c- 1\n", d);
900        fprintf(fout, "-%c 1\n", r);
901      }
902    }
903  } else if (GetDdNodeOfMlTree(tree->d, tree->d_comp) == one) {
904    if (GetDdNodeOfMlTree(tree->q, tree->q_comp) == one) {
905      fprintf(fout, ".names %s\n", name);
906      fprintf(fout, "1\n");
907    } else if (GetDdNodeOfMlTree(tree->q, tree->q_comp) == zero) {
908      if (GetDdNodeOfMlTree(tree->r, tree->r_comp) == one) {
909        fprintf(fout, ".names %s\n", name);
910        fprintf(fout, "1\n");
911      } else if (GetDdNodeOfMlTree(tree->r, tree->r_comp) == zero) {
912        fprintf(fout, ".names %s\n", name);
913        fprintf(fout, "0\n");
914      } else {
915        fprintf(fout, ".names %s %s\n", r_name, name);
916        fprintf(fout, "%c 1\n", r);
917      }
918    } else {
919      if (GetDdNodeOfMlTree(tree->r, tree->r_comp) == one) {
920        fprintf(fout, ".names %s\n", name);
921        fprintf(fout, "1\n");
922      } else if (GetDdNodeOfMlTree(tree->r, tree->r_comp) == zero) {
923        fprintf(fout, ".names %s %s\n", q_name, name);
924        fprintf(fout, "%c 1\n", q);
925      } else {
926        fprintf(fout, ".names %s %s %s\n", q_name, r_name, name);
927        fprintf(fout, "%c- 1\n", q);
928        fprintf(fout, "-%c 1\n", r);
929      }
930    }
931  } else {
932    if (GetDdNodeOfMlTree(tree->r, tree->r_comp) == one) {
933      fprintf(fout, ".names %s\n", name);
934      fprintf(fout, "1\n");
935    } else if (GetDdNodeOfMlTree(tree->r, tree->r_comp) == zero) {
936      fprintf(fout, ".names %s %s %s\n", q_name, d_name, name);
937      fprintf(fout, "%c%c 1\n", q, d);
938    } else {
939      fprintf(fout, ".names %s %s %s %s\n", q_name, d_name, r_name, name);
940      fprintf(fout, "%c%c- 1\n", q, d);
941      fprintf(fout, "--%c 1\n", r);
942    }
943  }
944}
945
946/**Function********************************************************************
947
948  Synopsis    [Writes a .names block in blif file for each tree that is a leaf
949  node.]
950
951  Description [Writes a .names block in blif file for each tree that is a leaf
952  node.]
953
954  SideEffects []
955
956  SeeAlso     []
957
958******************************************************************************/
959static void
960WriteLeafMlBlif(Ntk_Network_t *net,
961                bdd_manager *dd,
962                MlTree *tree,
963                FILE *fout,
964                int no,
965                bdd_node **ofuncs,
966                int *oflags,
967                int top_flag,
968                int verbosity)
969{
970  int           i, count, *support;
971  char          name[MAX_EQ_LEN];
972  bdd_node      *one = bdd_read_one(dd);
973  bdd_node      *zero = bdd_read_zero(dd);
974  char          out_name[MAX_NAME_LEN];
975  bdd_node      *node;
976  Ntk_Node_t    *ntk_node;
977  int           sizeZ;
978
979  sizeZ = bdd_num_zdd_vars(dd);
980
981  if (tree->node == one || tree->node == zero || tree->pi)
982    return;
983
984  if (tree->comp)
985    node = tree->complement;
986  else
987    node = tree->node;
988  for (i = 0; i < no; i++) {
989    if (node == ofuncs[i]) {
990      if (top_flag == 0)
991        return;
992
993      if (oflags[i])
994        continue;
995      else
996        oflags[i] = 1;
997      sprintf(out_name, "%s", SynthGetIthOutputName(i));
998      break;
999    }
1000  }
1001  if (i == no)
1002    SynthGetInternalNodeName(out_name, tree->id);
1003  else {
1004    ntk_node = Ntk_NetworkFindNodeByName(net, out_name);
1005    if (Ntk_NodeTestIsLatch(ntk_node))
1006      return;
1007  }
1008
1009  fprintf(fout, "\n");
1010  if (verbosity > 2) {
1011    SynthGetChildMlTreeWithName(net, dd, tree, name);
1012    fprintf(fout, "# %s\n", name);
1013  }
1014  fprintf(fout, ".names ");
1015
1016  support = ALLOC(int, sizeZ);
1017  if (!support)
1018    return;
1019  (void)memset((void *)support, 0, sizeof(int) * sizeZ);
1020  SynthZddSupportStep(bdd_regular(node), support);
1021  SynthZddClearFlag(bdd_regular(node));
1022  count = 0;
1023  for (i = 0; i < sizeZ; i++) {
1024    if (support[i]) {
1025      SynthGetPrimaryIndexName(net, i, name);
1026      fprintf(fout, "%s ", name);
1027      if (i % 2 == 0) {
1028        support[i] = count;
1029        i++;
1030        if (support[i])
1031          support[i] = count;
1032      } else {
1033        support[i] = count;
1034      }
1035      count++;
1036    }
1037  }
1038  fprintf(fout, "%s\n", out_name);
1039
1040  for (i = 0; i < count; i++)
1041    name[i] = '-';
1042  name[count] = '\0';
1043  WriteBlifBinary(dd, node, name, fout, support);
1044  FREE(support);
1045}
1046
1047
1048/**Function********************************************************************
1049
1050  Synopsis    [Writes all cubes of the node in .name block.]
1051
1052  Description [Writes all cubes of the node in .name block. This can be done
1053  by finding all paths to the constant 1 node from the node.]
1054
1055  SideEffects []
1056
1057  SeeAlso     []
1058
1059******************************************************************************/
1060static void
1061WriteBlifBinary(bdd_manager *dd,
1062                bdd_node *node,
1063                char *name,
1064                FILE *fout,
1065                int *support)
1066{
1067  bdd_node      *one = bdd_read_one(dd);
1068  bdd_node      *zero = bdd_read_zero(dd);
1069  int           id = bdd_node_read_index(node);
1070
1071  if (node == zero)
1072    return;
1073
1074  if (node == one) {
1075    fprintf(fout, "%s 1\n", name);
1076    return;
1077  }
1078
1079  if (id % 2 == 0)
1080    name[support[id]] = '1';
1081  else
1082    name[support[id]] = '0';
1083  WriteBlifBinary(dd, bdd_bdd_T(node), name, fout, support);
1084  name[support[id]] = '-';
1085  WriteBlifBinary(dd, bdd_bdd_E(node), name, fout, support);
1086  name[support[id]] = '-';
1087}
1088
1089
1090/**Function********************************************************************
1091
1092  Synopsis    [Writes multi level equations of a tree.]
1093
1094  Description [Writes multi level equations of a tree.]
1095
1096  SideEffects []
1097
1098  SeeAlso     []
1099
1100******************************************************************************/
1101static void
1102WriteEqnOfTree(FILE *fout,
1103               Ntk_Network_t *net,
1104               bdd_manager *dd,
1105               MlTree *tree,
1106               bdd_node **ofuncs)
1107{
1108  char  eq[MAX_EQ_LEN];
1109  char  name[MAX_NAME_LEN];
1110  int   polarity = 0;
1111
1112  polarity = GetMlTreeName(net, ofuncs, tree, name);
1113  eq[0] = '\0';
1114  GetEqnOfTree(net, dd, tree, tree, eq, ofuncs);
1115  if (polarity)
1116    SynthMakeComplementString(eq);
1117  fprintf(fout, "%s = %s\n", name, eq);
1118}
1119
1120
1121/**Function********************************************************************
1122
1123  Synopsis    [Gets multi level equations of a tree.]
1124
1125  Description [Gets multi level equations of a tree.]
1126
1127  SideEffects []
1128
1129  SeeAlso     []
1130
1131******************************************************************************/
1132static int
1133GetEqnOfTree(Ntk_Network_t *net,
1134             bdd_manager *dd,
1135             MlTree *top,
1136             MlTree *tree,
1137             char *eq,
1138             bdd_node **ofuncs)
1139{
1140  char          q_eq[MAX_EQ_LEN];
1141  char          d_eq[MAX_EQ_LEN];
1142  char          r_eq[MAX_EQ_LEN];
1143  char          qd_eq[MAX_EQ_LEN];
1144  bdd_node      *one = bdd_read_one(dd);
1145  bdd_node      *zero = bdd_read_zero(dd);
1146  bdd_node      *f;
1147  int           flag;
1148  int           polarity = 0;
1149
1150  if (tree != top && tree->shared) {
1151    polarity = GetMlTreeName(net, ofuncs, tree, eq);
1152    if (polarity)
1153      SynthMakeComplementString(eq);
1154    return(0);
1155  }
1156
1157  f = tree->node;
1158  if (tree->leaf) {
1159    flag = SynthGetChildTreeWithName(net, dd, f, eq);
1160    return(flag);
1161  }
1162
1163  if (f == one) {
1164    sprintf(eq, "one");
1165    return(0);
1166  } else if (f == zero) {
1167    sprintf(eq, "zero");
1168    return(0);
1169  }
1170
1171  q_eq[0] = d_eq[0] = r_eq[0] = '\0';
1172  flag = GetEqnOfTree(net, dd, top, tree->q, q_eq, ofuncs);
1173  if (tree->q_comp)
1174    SynthMakeComplementString(q_eq);
1175  if (flag)
1176    return(1);
1177  if (GetDdNodeOfMlTree(tree->d, tree->d_comp) == one)
1178    d_eq[0] = '\0';
1179  else {
1180    flag = GetEqnOfTree(net, dd, top, tree->d, d_eq, ofuncs);
1181    if (tree->d_comp)
1182      SynthMakeComplementString(d_eq);
1183    if (flag)
1184      return(1);
1185  }
1186  flag = GetEqnOfTree(net, dd, top, tree->r, r_eq, ofuncs);
1187  if (tree->r_comp)
1188    SynthMakeComplementString(r_eq);
1189  if (flag)
1190    return(1);
1191
1192  if (strcmp(q_eq, "one") == 0)
1193    sprintf(qd_eq, "%s", d_eq);
1194  else if (strcmp(q_eq, "zero") == 0)
1195    sprintf(qd_eq, "zero");
1196  else if (strcmp(d_eq, "one") == 0)
1197    sprintf(qd_eq, "%s", q_eq);
1198  else if (strcmp(d_eq, "zero") == 0)
1199    sprintf(qd_eq, "zero");
1200  else {
1201    if (strlen(q_eq) + strlen(d_eq) + 1 > MAX_EQ_LEN) {
1202      sprintf(eq, "%s", q_eq);
1203      if (strlen(eq) == MAX_EQ_LEN - 1) {
1204        eq[MAX_EQ_LEN - 2] = '#'; /* truncated */
1205        eq[MAX_EQ_LEN - 1] = '\0';
1206      } else {
1207        eq[strlen(eq)] = '#'; /* truncated */
1208        eq[strlen(eq) + 1] = '\0';
1209      }
1210      return(1);
1211    }
1212    sprintf(qd_eq, "%s %s", q_eq, d_eq);
1213  }
1214
1215  if (strcmp(r_eq, "zero") == 0)
1216    sprintf(eq, "%s", qd_eq);
1217  else {
1218    if (strlen(qd_eq) + strlen(r_eq) + 1 > MAX_EQ_LEN) {
1219      sprintf(eq, "%s", qd_eq);
1220      if (strlen(eq) == MAX_EQ_LEN - 1) {
1221        eq[MAX_EQ_LEN - 2] = '#'; /* truncated */
1222        eq[MAX_EQ_LEN - 1] = '\0';
1223      } else {
1224        eq[strlen(eq)] = '#'; /* truncated */
1225        eq[strlen(eq) + 1] = '\0';
1226      }
1227      return(1);
1228    }
1229    sprintf(eq, "(%s + %s)", qd_eq, r_eq);
1230  }
1231  return(0);
1232}
1233
1234
1235/**Function********************************************************************
1236
1237  Synopsis    [Writes a part of a blif file for each output function.]
1238
1239  Description [Writes a part of a blif file for each output function.
1240  All top nodes and all nodes that are shared will be output nodes of
1241  .names in blif file.]
1242
1243  SideEffects []
1244
1245  SeeAlso     []
1246
1247******************************************************************************/
1248static void
1249WriteMlTreeBlif(FILE *fout,
1250                Ntk_Network_t *net,
1251                bdd_manager *dd,
1252                MlTree *tree,
1253                bdd_node **ofuncs,
1254                int no,
1255                char *func_name,
1256                int ref)
1257{
1258  char  name[MAX_NAME_LEN];
1259  int   polarity = 0;
1260
1261  if (tree->top || tree->shared) {
1262    if (ref) {
1263      if (tree->ref) {
1264        polarity = GetMlTreeName(net, ofuncs, tree, name);
1265        fprintf(fout, "\n.names %s %s\n", name, func_name);
1266        if (polarity == 0) {
1267          if (tree->comp)
1268            fprintf(fout, "0 1\n");
1269          else
1270            fprintf(fout, "1 1\n");
1271        } else {
1272          if (tree->comp)
1273            fprintf(fout, "1 1\n");
1274          else
1275            fprintf(fout, "0 1\n");
1276        }
1277        return;
1278      }
1279    }
1280    WriteMultiLevelBlif(fout, net, dd, tree, ofuncs, no);
1281  }
1282
1283  if (tree->leaf)
1284    return;
1285
1286  if (tree->q_ref == 0)
1287    WriteMlTreeBlif(fout, net, dd, tree->q, ofuncs, no, NULL, ref);
1288  if (tree->d_ref == 0)
1289    WriteMlTreeBlif(fout, net, dd, tree->d, ofuncs, no, NULL, ref);
1290  if (tree->r_ref == 0)
1291    WriteMlTreeBlif(fout, net, dd, tree->r, ofuncs, no, NULL, ref);
1292}
1293
1294
1295/**Function********************************************************************
1296
1297  Synopsis    [Writes a .names block in blif file for each tree that is a
1298  top node or a shared node.]
1299
1300  Description [Writes a .names block in blif file for each tree that is a
1301  top node or a shared node.]
1302
1303  SideEffects []
1304
1305  SeeAlso     []
1306
1307******************************************************************************/
1308static void
1309WriteMultiLevelBlif(FILE *fout,
1310                    Ntk_Network_t *net,
1311                    bdd_manager *dd,
1312                    MlTree *tree,
1313                    bdd_node **ofuncs,
1314                    int no)
1315{
1316  int                   i, ni;
1317  char                  name[MAX_NAME_LEN];
1318  TruthTableLine        *lines, *cur, *next;
1319  st_table              *table;
1320  char                  **sorted_name, *key;
1321  st_generator          *gen;
1322  int                   pos;
1323  Ntk_Node_t            *ntk_node;
1324  int                   polarity = 0;
1325
1326  polarity = GetMlTreeName(net, ofuncs, tree, name);
1327  for (i = 0; i < no; i++) {
1328    if (tree->node == ofuncs[i]) {
1329      ntk_node = Ntk_NetworkFindNodeByName(net, name);
1330      if (Ntk_NodeTestIsLatch(ntk_node))
1331        return;
1332    }
1333  }
1334
1335  table = st_init_table(strcmp, st_strhash);
1336  ni = 0;
1337  ni = GetMultiLevelNodes(net, dd, tree, tree, ofuncs, no, table, ni);
1338  sorted_name = ALLOC(char *, ni * sizeof(char *));
1339  i = 0;
1340  st_foreach_item_int(table, gen, (char **)&key, &pos) {
1341    sorted_name[i] = key;
1342    i++;
1343  }
1344  qsort(sorted_name, ni, sizeof(char *),
1345        (int (*)(const void *, const void *))SynthStringCompare);
1346  for (i = 0; i < ni; i++) {
1347    st_insert(table, (char *)sorted_name[i], (char *)(long)i);
1348  }
1349  lines = GetMultiLevelBlifRecur(net, dd, tree, tree, ofuncs, no, table, ni);
1350  fprintf(fout, "\n.names");
1351  for (i = 0; i < ni; i++)
1352    fprintf(fout, " %s", sorted_name[i]);
1353  fprintf(fout, " %s\n", name);
1354  cur = lines;
1355  while (cur) {
1356    next = cur->next;
1357    if (polarity == 0)
1358      fprintf(fout, "%s 1\n", cur->values);
1359    else
1360      fprintf(fout, "%s 0\n", cur->values);
1361    FREE(cur->values);
1362    FREE(cur);
1363    cur = next;
1364  }
1365  st_free_table(table);
1366  for (i = 0; i < ni; i++)
1367    FREE(sorted_name[i]);
1368  FREE(sorted_name);
1369}
1370
1371
1372/**Function********************************************************************
1373
1374  Synopsis    [Gets all cube list of a .name block.]
1375
1376  Description [Gets all cube list of a .name block.]
1377
1378  SideEffects []
1379
1380  SeeAlso     []
1381
1382******************************************************************************/
1383static TruthTableLine *
1384GetMultiLevelBlifRecur(Ntk_Network_t *net,
1385                       bdd_manager *dd,
1386                       MlTree *top,
1387                       MlTree *tree,
1388                       bdd_node **ofuncs,
1389                       int no,
1390                       st_table *table,
1391                       int ni)
1392{
1393  bdd_node              *one = bdd_read_one(dd);
1394  bdd_node              *zero = bdd_read_zero(dd);
1395  bdd_node              *f;
1396  TruthTableLine        *line;
1397  TruthTableLine        *cur, *q_line, *d_line, *r_line;
1398  int                   pos;
1399  char                  name[MAX_NAME_LEN];
1400  int                   polarity = 0;
1401
1402  line = (TruthTableLine *)NULL;
1403
1404  if (tree != top && tree->shared) {
1405    polarity = GetMlTreeName(net, ofuncs, tree, name);
1406    line = GetTautologyLine(ni);
1407    if (st_lookup_int(table, (char *)name, (int *)(&pos))) {
1408      if (polarity == 0)
1409        line->values[pos] = '1';
1410      else
1411        line->values[pos] = '0';
1412    }
1413    return(line);
1414  }
1415
1416  f = tree->node;
1417  if (tree->leaf) {
1418    line = GetLeafLines(net, dd, tree, ofuncs, no, table, ni);
1419    return(line);
1420  }
1421
1422  if (f == one || f == zero)
1423    return(line);
1424
1425  q_line = GetMultiLevelBlifRecur(net, dd, top, tree->q, ofuncs,
1426                                  no, table, ni);
1427  if (q_line && tree->q_comp)
1428    q_line = GetComplementLines(q_line, ni, 1);
1429  if (GetDdNodeOfMlTree(tree->d, tree->d_comp) == one)
1430    d_line = (TruthTableLine *)NULL;
1431  else {
1432    d_line = GetMultiLevelBlifRecur(net, dd, top, tree->d, ofuncs, no,
1433                                    table, ni);
1434    if (d_line && tree->d_comp)
1435      d_line = GetComplementLines(d_line, ni, 1);
1436  }
1437  if (q_line && d_line)
1438    line = GetAndLines(q_line, d_line, ni, 1);
1439  else if (q_line)
1440    line = q_line;
1441  else if (d_line)
1442    line = d_line;
1443  r_line = GetMultiLevelBlifRecur(net, dd, top, tree->r, ofuncs, no, table, ni);
1444  if (r_line && tree->r_comp)
1445    r_line = GetComplementLines(r_line, ni, 1);
1446  if (r_line) {
1447    cur = line;
1448    while (cur) {
1449      if (!cur->next) {
1450        cur->next = r_line;
1451        break;
1452      }
1453      cur = cur->next;
1454    }
1455  }
1456
1457  return(line);
1458}
1459
1460
1461/**Function********************************************************************
1462
1463  Synopsis    [Get the names of all input nodes of .name block for an output
1464  tree.]
1465
1466  Description [Get the names of all input nodes of .name block for an output
1467  tree.]
1468
1469  SideEffects []
1470
1471  SeeAlso     []
1472
1473******************************************************************************/
1474static int
1475GetMultiLevelNodes(Ntk_Network_t *net,
1476                   bdd_manager *dd,
1477                   MlTree *top,
1478                   MlTree *tree,
1479                   bdd_node **ofuncs,
1480                   int no,
1481                   st_table *table,
1482                   int ni)
1483{
1484  bdd_node      *one = bdd_read_one(dd);
1485  bdd_node      *zero = bdd_read_zero(dd);
1486  bdd_node      *f;
1487  char          name[MAX_NAME_LEN], *st_name;
1488  int           pos;
1489
1490  if (tree != top && tree->shared) {
1491    (void) GetMlTreeName(net, ofuncs, tree, name);
1492    if (!st_lookup_int(table, (char *)name, (int *)(&pos))) {
1493      st_name = ALLOC(char, strlen(name) + 1);
1494      strcpy(st_name, name);
1495      st_insert(table, (char *)st_name, (char *)(long)ni);
1496      ni++;
1497    }
1498    return(ni);
1499  }
1500
1501  f = tree->node;
1502  if (tree->leaf) {
1503    ni = GetLeafNodes(net, dd, tree, ofuncs, no, table, ni);
1504    return(ni);
1505  }
1506
1507  if (f == one || f == zero)
1508    return(ni);
1509
1510  ni = GetMultiLevelNodes(net, dd, top, tree->q, ofuncs, no, table, ni);
1511  if (GetDdNodeOfMlTree(tree->d, tree->d_comp) != one)
1512    ni = GetMultiLevelNodes(net, dd, top, tree->d, ofuncs, no, table, ni);
1513  ni = GetMultiLevelNodes(net, dd, top, tree->r, ofuncs, no, table, ni);
1514
1515  return(ni);
1516}
1517
1518
1519/**Function********************************************************************
1520
1521  Synopsis    [Get the names of all input nodes of a tree which is a leaf
1522  node.]
1523
1524  Description [Get the names of all input nodes of a tree which is a leaf
1525  node.]
1526
1527  SideEffects []
1528
1529  SeeAlso     []
1530
1531******************************************************************************/
1532static int
1533GetLeafNodes(Ntk_Network_t *net,
1534             bdd_manager *dd,
1535             MlTree *tree,
1536             bdd_node **ofuncs,
1537             int no,
1538             st_table *table,
1539             int ni)
1540{
1541  int           i, *support;
1542  char          name[MAX_NAME_LEN], *st_name;
1543  bdd_node      *one = bdd_read_one(dd);
1544  bdd_node      *zero = bdd_read_zero(dd);
1545  bdd_node      *node;
1546  int           pos, sizeZ = bdd_num_zdd_vars(dd);
1547
1548  if (tree->node == one || tree->node == zero)
1549    return(ni);
1550
1551  if (tree->comp)
1552    node = tree->complement;
1553  else
1554    node = tree->node;
1555
1556  support = ALLOC(int, sizeZ);
1557  if (!support)
1558    return(ni);
1559  (void)memset((void *)support, 0, sizeof(int) * sizeZ);
1560  SynthZddSupportStep(bdd_regular(node), support);
1561  SynthZddClearFlag(bdd_regular(node));
1562  for (i = 0; i < sizeZ; i++) {
1563    if (support[i]) {
1564      SynthGetPrimaryIndexName(net, i, name);
1565      if (!st_lookup_int(table, (char *)name, (int *)(&pos))) {
1566        st_name = ALLOC(char, strlen(name) + 1);
1567        strcpy(st_name, name);
1568        st_insert(table, (char *)st_name, (char *)(long)ni);
1569        ni++;
1570      }
1571    }
1572  }
1573  FREE(support);
1574  return(ni);
1575}
1576
1577
1578/**Function********************************************************************
1579
1580  Synopsis    [Gets a tautologous TruthTableLine.]
1581
1582  Description [Gets a tautologous TruthTableLine.]
1583
1584  SideEffects []
1585
1586  SeeAlso     []
1587
1588******************************************************************************/
1589static TruthTableLine *
1590GetTautologyLine(int ni)
1591{
1592  int                   i;
1593  TruthTableLine        *line;
1594
1595  line = ALLOC(TruthTableLine, 1);
1596  (void)memset((void *)line, 0, sizeof(TruthTableLine));
1597  line->values = (char *)malloc(ni + 1);
1598  for (i = 0; i < ni; i++)
1599    line->values[i] = '-';
1600  line->values[ni] = '\0';
1601  return(line);
1602}
1603
1604
1605/**Function********************************************************************
1606
1607  Synopsis    [Gets a list of TruthTableLine for a tree which is a leaf node.]
1608
1609  Description [Gets a list of TruthTableLine for a tree which is a leaf node.]
1610
1611  SideEffects []
1612
1613  SeeAlso     []
1614
1615******************************************************************************/
1616static TruthTableLine *
1617GetLeafLines(Ntk_Network_t *net,
1618             bdd_manager *dd,
1619             MlTree *tree,
1620             bdd_node **ofuncs,
1621             int no,
1622             st_table *table,
1623             int ni)
1624{
1625  int                   i, *support;
1626  char                  values[MAX_EQ_LEN];
1627  bdd_node              *one = bdd_read_one(dd);
1628  bdd_node              *zero = bdd_read_zero(dd);
1629  bdd_node              *node;
1630  TruthTableLine        *line;
1631  int                   pos, sizeZ = bdd_num_zdd_vars(dd);
1632  char                  name[MAX_NAME_LEN];
1633
1634  line = (TruthTableLine *)NULL;
1635
1636  if (tree->node == one || tree->node == zero)
1637    return(line);
1638
1639  if (tree->comp)
1640    node = tree->complement;
1641  else
1642    node = tree->node;
1643
1644  support = ALLOC(int, sizeZ);
1645  if (!support)
1646    return(line);
1647  (void)memset((void *)support, 0, sizeof(int) * sizeZ);
1648  SynthZddSupportStep(bdd_regular(node), support);
1649  SynthZddClearFlag(bdd_regular(node));
1650  for (i = 0; i < sizeZ; i++) {
1651    if (support[i]) {
1652      SynthGetPrimaryIndexName(net, i, name);
1653      if (!st_lookup_int(table, (char *)name, (int *)(&pos))) {
1654        fprintf(vis_stdout,
1655                "** synth error: Failed to find %s in hash.\n", name);
1656      }
1657      support[i] = pos;
1658    }
1659  }
1660
1661  for (i = 0; i < ni; i++)
1662    values[i] = '-';
1663  values[ni] = '\0';
1664  line = GetBlifBinary(line, dd, node, values, support, ni);
1665  FREE(support);
1666  return(line);
1667}
1668
1669
1670/**Function********************************************************************
1671
1672  Synopsis    [Gets a list of TruthTableLine for a tree which is a leaf node.]
1673
1674  Description [Gets a list of TruthTableLine for a tree which is a leaf node.]
1675
1676  SideEffects []
1677
1678  SeeAlso     [GetLeafLines]
1679
1680******************************************************************************/
1681static TruthTableLine *
1682GetBlifBinary(TruthTableLine *line,
1683              bdd_manager *dd,
1684              bdd_node *node,
1685              char *values,
1686              int *support,
1687              int ni)
1688{
1689  bdd_node              *one = bdd_read_one(dd);
1690  bdd_node              *zero = bdd_read_zero(dd);
1691  TruthTableLine        *new_, *cur;
1692  int                   id = bdd_node_read_index(node);
1693
1694  if (node == zero)
1695    return(line);
1696
1697  if (node == one) {
1698    new_ = ALLOC(TruthTableLine, 1);
1699    (void)memset((void *)new_, 0, sizeof(TruthTableLine));
1700    new_->values = ALLOC(char,ni+1);
1701    strcpy(new_->values, values);
1702    if (line) {
1703      cur = line;
1704      while (cur->next)
1705        cur = cur->next;
1706      cur->next = new_;
1707    } else
1708      line = new_;
1709    return(line);
1710  }
1711
1712  if (id % 2 == 0)
1713    values[support[id]] = '1';
1714  else
1715    values[support[id]] = '0';
1716  line = GetBlifBinary(line, dd, bdd_bdd_T(node), values, support, ni);
1717  values[support[id]] = '-';
1718  line = GetBlifBinary(line, dd, bdd_bdd_E(node), values, support, ni);
1719  values[support[id]] = '-';
1720  return(line);
1721}
1722
1723
1724/**Function********************************************************************
1725
1726  Synopsis    [Returns the complemented TruthTableLine only for the first one.]
1727
1728  Description [Returns the complemented TruthTableLine only for the first one.]
1729
1730  SideEffects []
1731
1732  SeeAlso     []
1733
1734******************************************************************************/
1735static TruthTableLine *
1736GetComplementOneLine(TruthTableLine *line,
1737                     int ni,
1738                     int flag)
1739{
1740  int                   i;
1741  TruthTableLine        *new_line, *start, *last;
1742
1743  start = last = (TruthTableLine *)NULL;
1744
1745  for (i = 0; i < ni; i++) {
1746    if (line->values[i] != '-') {
1747      new_line = GetTautologyLine(ni);
1748      if (line->values[i] == '1')
1749        new_line->values[i] = '0';
1750      else
1751        new_line->values[i] = '1';
1752      if (last) {
1753        last->next = new_line;
1754        last = new_line;
1755      } else
1756        start = last = new_line;
1757    }
1758  }
1759
1760  if (flag) {
1761    FREE(line->values);
1762    FREE(line);
1763  }
1764
1765  return(start);
1766}
1767
1768
1769/**Function********************************************************************
1770
1771  Synopsis    [Returns the complemented TruthTableLine.]
1772
1773  Description [Returns the complemented TruthTableLine.]
1774
1775  SideEffects []
1776
1777  SeeAlso     []
1778
1779******************************************************************************/
1780static TruthTableLine *
1781GetComplementLines(TruthTableLine *lines,
1782                   int ni,
1783                   int flag)
1784{
1785  TruthTableLine        *first, *cur, *next;
1786
1787  if (!lines)
1788    return(lines);
1789
1790  first = lines;
1791  cur = first->next;
1792  first = GetComplementOneLine(first, ni, flag);
1793  while (cur) {
1794    next = cur->next;
1795    cur = GetComplementOneLine(cur, ni, flag);
1796    first = GetAndLines(first, cur, ni, flag);
1797    cur = next;
1798  }
1799  return(first);
1800}
1801
1802
1803/**Function********************************************************************
1804
1805  Synopsis    [Returns the result of Boolean AND for two TruthTableLine.]
1806
1807  Description [Returns the result of Boolean AND for two TruthTableLine.]
1808
1809  SideEffects []
1810
1811  SeeAlso     []
1812
1813******************************************************************************/
1814static TruthTableLine *
1815GetAndLines(TruthTableLine *line1,
1816            TruthTableLine *line2,
1817            int ni,
1818            int flag)
1819{
1820  int                   i;
1821  TruthTableLine        *cur1, *cur2, *next1, *next2;
1822  TruthTableLine        *start, *last;
1823  TruthTableLine        *new_line;
1824
1825  start = last = (TruthTableLine *)NULL;
1826
1827  cur1 = line1;
1828  while (cur1) {
1829    next1 = cur1->next;
1830    cur2 = line2;
1831    while (cur2) {
1832      new_line = GetTautologyLine(ni);
1833      strcpy(new_line->values, cur1->values);
1834      for (i = 0; i < ni; i++) {
1835        if (cur2->values[i] != '-')
1836          new_line->values[i] = cur2->values[i];
1837      }
1838      if (last) {
1839        last->next = new_line;
1840        last = new_line;
1841      } else {
1842        start = last = new_line;
1843      }
1844      cur2 = cur2->next;
1845    }
1846    if (flag) {
1847      FREE(cur1->values);
1848      FREE(cur1);
1849    }
1850    cur1 = next1;
1851  }
1852
1853  if (flag) {
1854    cur2 = line2;
1855    while (cur2) {
1856      next2 = cur2->next;
1857      FREE(cur2->values);
1858      FREE(cur2);
1859      cur2 = next2;
1860    }
1861  }
1862
1863  return(start);
1864}
1865
1866
1867/**Function********************************************************************
1868
1869  Synopsis    [Returns the node or the complement node of a tree.]
1870
1871  Description [Returns the node or the complement node of a tree.]
1872
1873  SideEffects []
1874
1875  SeeAlso     []
1876
1877******************************************************************************/
1878static bdd_node *
1879GetDdNodeOfMlTree(MlTree *tree,
1880                  int comp)
1881{
1882  if (comp)
1883    return(tree->complement);
1884  return(tree->node);
1885}
1886
1887/**Function********************************************************************
1888
1889  Synopsis    [Gets the node name of a tree.]
1890
1891  Description [Gets the node name of a tree. Return value shows polarity;
1892  0 means positive node and 1 means negative.]
1893
1894  SideEffects []
1895
1896  SeeAlso     []
1897
1898******************************************************************************/
1899static int
1900GetMlTreeName(Ntk_Network_t *net,
1901              bdd_node **ofuncs,
1902              MlTree *tree,
1903              char *name)
1904{
1905  int   i, no;
1906  int   polarity = 0; /* positive */
1907
1908  no = Ntk_NetworkReadNumCombOutputs(net) - Ntk_NetworkReadNumLatches(net);
1909  for (i = 0; i < no; i++) {
1910    if (tree->node == ofuncs[i]) {
1911      sprintf(name, "%s", SynthGetIthOutputName(i));
1912      break;
1913    }
1914  }
1915  if (i == no) {
1916    if (tree->pi)
1917      polarity = SynthGetPrimaryNodeName(net, tree->node, name);
1918    else
1919      SynthGetInternalNodeName(name, tree->id);
1920  }
1921
1922  return(polarity);
1923}
1924
1925/**Function********************************************************************
1926
1927  Synopsis    [Gets the original name of a tree.]
1928
1929  Description [Gets the original name of a tree.]
1930
1931  SideEffects []
1932
1933  SeeAlso     []
1934
1935******************************************************************************/
1936static char **
1937GetAllVarNameArray(bdd_manager *dd)
1938{
1939  int           size, i, j;
1940  mvar_type     var;
1941  char          **nameArray, *name;
1942
1943  size = bdd_num_vars(dd);
1944  nameArray = ALLOC(char *, size);
1945  if (!nameArray)
1946    return(NIL(char *));
1947
1948  for (i = 0; i < size; i++) {
1949    var = mdd_get_var_by_id(dd, i);
1950    name = ALLOC(char, strlen(var.name) + 1);
1951    if (!name) {
1952      for (j = 0; j < i; j++)
1953        FREE(nameArray[j]);
1954      FREE(nameArray);
1955      return(NIL(char *));
1956    }
1957    strcpy(name, var.name);
1958    nameArray[i] = name;
1959  }
1960 
1961  return(nameArray);
1962}
Note: See TracBrowser for help on using the repository browser.