source: vis_dev/vis-2.3/src/synth/synthOpt.c @ 83

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

vis2.3
File size: 25.7 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [synthOpt.c]
4
5  PackageName [synth]
6
7  Synopsis    [Multilevel optimization functions.]
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: synthOpt.c,v 1.53 2005/05/11 20:18:25 hhhan 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
40int     OutputOrdering = 1; /*
41                            ** 0 : just use VIS's order
42                            ** 1 : smaller first in terms of support
43                            ** 2 : smaller first in terms of bdd size
44                            */
45
46static  int     UseFuncDivisor = 1;
47static  float   SuppFactor = 10.0;
48static  float   ProbFactor = 10.0;
49static  int     *SupportCount;
50static  float   *Probability;
51static  char    **outputNames;
52
53extern  int     TryNodeSharing;
54extern  int     noMemoryFlag;
55extern  int     VerifyTreeMode;
56
57/**AutomaticStart*************************************************************/
58
59/*---------------------------------------------------------------------------*/
60/* Static function prototypes                                                */
61/*---------------------------------------------------------------------------*/
62
63static void GetOutputOrder(bdd_manager *dd, bdd_node **ofuncs, int no, int *order, int verbosity);
64static int IsSubsetOfSupportForOneWord(unsigned int mask1, unsigned int mask2);
65static int IsNullSupport(int size, unsigned int *mask);
66static void PrintSupportMask(int n, int size, unsigned int *mask);
67static int GetNumberOfSupport(int n, int size, unsigned int *mask);
68static int factorizeNetwork(Ntk_Network_t *net, bdd_manager *dd, bdd_node **ofuncs, MlTree **tree, int no, int *out_order, st_table *table, char **combOutNames, int divisor, MlTree *(* factoring_func)(bdd_manager *, st_table *, bdd_node *, int, int *, MlTree *, int, MlTree *, int), int verbosity);
69
70/**AutomaticEnd***************************************************************/
71
72
73/*---------------------------------------------------------------------------*/
74/* Definition of exported functions                                          */
75/*---------------------------------------------------------------------------*/
76
77
78/*---------------------------------------------------------------------------*/
79/* Definition of internal functions                                          */
80/*---------------------------------------------------------------------------*/
81
82/**Function********************************************************************
83
84  Synopsis [Optimizes a network by factorizing.]
85
86  Description [Optimizes a network by factorizing.]
87
88  SideEffects []
89
90  SeeAlso     []
91
92******************************************************************************/
93void
94SynthMultiLevelOptimize(Ntk_Network_t *network,
95                        bdd_node **combOutBdds,
96                        bdd_node **combUpperBdds,
97                        char **combOutNames,
98                        int *initStates,
99                        Synth_InfoData_t *synthInfo,
100                        int verbosity)
101{
102  bdd_manager           *dd = (bdd_manager *)Ntk_NetworkReadMddManager(network);
103  bdd_node              *top;
104  bdd_node              **ofuncs;
105  int                   i, no;
106  int                   factoring, divisor;
107  char                  *filename;
108  char                  *filehead;
109  MlTree                **tree;
110  bdd_node              *zdd_I;
111  st_table              *table;
112  int                   nml, tml;
113  int                   *out_order;
114  FILE                  *feqn;
115  MlTree                *(* factoring_func)(bdd_manager *, st_table *,
116                                            bdd_node *, int, int *, MlTree *,
117                                            int, MlTree *, int);
118  int                   autoDyn, autoDynZ;
119  bdd_reorder_type_t    method, methodZ;
120  int                   error;
121
122  factoring = synthInfo->factoring;
123  divisor = synthInfo->divisor;
124  filehead = synthInfo->filehead;
125  TryNodeSharing = synthInfo->trySharing;
126  SynthSetInternalNodePrefix(synthInfo->prefix);
127
128  /* Save reordering status and set reordering mode specific to
129   * synthesis.
130   */
131  autoDyn = bdd_reordering_status(dd, &method);
132  autoDynZ = bdd_reordering_zdd_status(dd, &methodZ);
133
134  switch (synthInfo->reordering) {
135  case 0 :
136    bdd_dynamic_reordering_disable(dd);
137    bdd_dynamic_reordering_zdd_disable(dd);
138    break;
139  case 1 :
140    bdd_dynamic_reordering(dd, method, BDD_REORDER_VERBOSITY_DEFAULT);
141    bdd_dynamic_reordering_zdd_disable(dd);
142    break;
143  case 2 :
144    bdd_dynamic_reordering_disable(dd);
145    bdd_dynamic_reordering_zdd(dd, methodZ, BDD_REORDER_VERBOSITY_DEFAULT);
146    break;
147  case 3 :
148    bdd_dynamic_reordering(dd, method, BDD_REORDER_VERBOSITY_DEFAULT);
149    bdd_dynamic_reordering_zdd(dd, methodZ, BDD_REORDER_VERBOSITY_DEFAULT);
150    break;
151  default :
152    bdd_dynamic_reordering_disable(dd);
153    bdd_dynamic_reordering_zdd_disable(dd);
154    break;
155  }
156
157  if (factoring == 0)
158    factoring_func = SynthSimpleFactorTree;
159  else
160    factoring_func = SynthGenericFactorTree;
161
162  /* outputNames is a static global variable for this file. */
163  outputNames = combOutNames;
164
165  /* Initialize the node-tree table and other factoring-related variables.
166   * The table contains pairs of a ZDD node and the corresponding multi-level
167   * tree.
168   */
169  table = st_init_table(st_ptrcmp, st_ptrhash);
170  SynthInitMlTable();
171
172  /* Create ZDD variables for the positive and negative literals. */
173  bdd_zdd_vars_from_bdd_vars(dd, 2);
174
175  /* Since we currently support only blif files, the number of
176   * functions to synthesize should not include the initial
177   * inputs of latches in case of sequential ckts.
178   */
179  no = Ntk_NetworkReadNumCombOutputs(network) -
180    Ntk_NetworkReadNumLatches(network);
181
182  /* Compute two-level covers for all the functions to be synthesized. */
183  ofuncs = ALLOC(bdd_node *, no);
184  for (i = 0; i < no; i++) {
185    if (verbosity) {
186      (void)fprintf(vis_stdout, "** synth info: Synthesizing output [%d(%s)]\n",
187                    i, combOutNames[i]);
188    }
189    bdd_ref(top = bdd_zdd_isop(dd, combOutBdds[i], combUpperBdds[i],
190                               &zdd_I));
191    bdd_ref(zdd_I);
192    bdd_recursive_deref(dd, top);
193    ofuncs[i] = zdd_I;
194  }
195
196  if (VerifyTreeMode == 2)
197    SynthDumpBlif(network, dd, no, ofuncs, combOutNames, initStates, filehead);
198
199  /* Initialize array of factoring trees and determine the order in
200   * which the functions will be processed. Then proceed to factor.
201   */
202  tree = ALLOC(MlTree *, no);
203  (void)memset((void *)tree, 0, no * sizeof(MlTree *));
204  out_order = ALLOC(int, no);
205  GetOutputOrder(dd, ofuncs, no, out_order, verbosity);
206  error = factorizeNetwork(network, dd, ofuncs, tree, no, out_order,
207                   table, combOutNames, divisor, factoring_func, verbosity);
208  FREE(out_order);
209
210  if (error) {
211    (void)fprintf(vis_stderr,
212                  "** synth error: synthesize_network has finished abnormally");
213    if (noMemoryFlag)
214      (void)fprintf(vis_stderr, " due to lack of memory\n");
215    else
216      (void)fprintf(vis_stderr, " for some reason\n");
217    goto cleanup;
218  }
219
220  /* Count total number of literals in multi-level network. */
221  tml = 0;
222  for (i = 0; i < no; i++) {
223    if (tree[i]) {
224      nml = SynthCountMlLiteral(dd, tree[i], 1);
225      tml += nml;
226    }
227  }
228  (void)fprintf(vis_stdout,
229                "** synth info: Total number of literals = %d\n", tml);
230
231  /* Write network in eqn and blif formats. */
232  SynthSetupNodeNameTable(network);
233  filename = ALLOC(char, strlen(filehead) + 9);
234  if (synthInfo->eqn) {
235    sprintf(filename, "%s.eqn", filehead);
236    feqn = Cmd_FileOpen(filename, "w", NIL(char *), 0);
237    if (feqn) {
238      fprintf(feqn, "** synth info: Total number of literals = %d\n", tml);
239      SynthWriteEqnHeader(feqn, network, dd);
240      for (i = 0; i < no; i++) {
241        if (tree[i])
242          SynthWriteEqn(feqn, network, dd, tree[i], ofuncs, combOutNames[i], 1);
243      }
244      fclose(feqn);
245    } else {
246      (void)fprintf(vis_stdout,
247                    "** synth error: Error in opening file [%s]\n", filename);
248    }
249  }
250  sprintf(filename, "%s.ml.blif", filehead);
251  SynthWriteBlifFile(network, dd, tree, filename, no, ofuncs, initStates,
252                     0, verbosity);
253  FREE(filename);
254  SynthFreeNodeNameTable();
255
256 cleanup:
257  /* Clean up. */
258  for (i = 0; i < no; i++) {
259    if (!tree[i])
260      continue;
261    bdd_recursive_deref_zdd(dd, tree[i]->node);
262    /* frees some trees not in node-tree table */
263    if (tree[i]->ref)
264      SynthFreeMlTree(tree[i], 0);
265  }
266
267  SynthClearMlTable(dd, table);
268  st_free_table(table);
269  FREE(tree);
270
271  for (i = 0; i < no; i++) {
272    if (!ofuncs[i])
273      continue;
274    bdd_recursive_deref_zdd(dd, ofuncs[i]);
275  }
276
277  FREE(ofuncs);
278
279  /* Restore reordering status. */
280  if (autoDyn)
281    bdd_dynamic_reordering(dd, method, BDD_REORDER_VERBOSITY_DEFAULT);
282  else
283    bdd_dynamic_reordering_disable(dd);
284  if (autoDynZ)
285    bdd_dynamic_reordering_zdd(dd, methodZ, BDD_REORDER_VERBOSITY_DEFAULT);
286  else
287    bdd_dynamic_reordering_zdd_disable(dd);
288}
289
290
291/**Function********************************************************************
292
293  Synopsis [Sets the optional variable UseFuncDivisor.]
294
295  Description [Sets the optional variable UseFuncDivisor. Currently
296  UseFuncDivisor has always the initial value of 1, this is because it
297  seems does better almost always than 0.]
298
299  SideEffects []
300
301  SeeAlso     []
302
303******************************************************************************/
304void
305SynthSetUseFuncDivisor(int mode)
306{
307  UseFuncDivisor = mode;
308}
309
310
311/**Function********************************************************************
312
313  Synopsis [Sets the optional variable OutputOrdering.]
314
315  Description [Sets the optional variable OutputOrdering.]
316
317  SideEffects []
318
319  SeeAlso     []
320
321******************************************************************************/
322void
323SynthSetOutputOrdering(int mode)
324{
325  OutputOrdering = mode;
326}
327
328
329/**Function********************************************************************
330
331  Synopsis [Sets the cost factors to get a divisor for low power.]
332
333  Description [Sets the cost factors to get a divisor for low power.]
334
335  SideEffects []
336
337  SeeAlso     []
338
339******************************************************************************/
340void
341SynthSetCostFactors(float supp,
342                    float prob)
343{
344  SuppFactor = supp;
345  ProbFactor = prob;
346}
347
348
349/**Function********************************************************************
350
351  Synopsis [Sets the variable SupportCount.]
352
353  Description [Sets the variable SupportCount.]
354
355  SideEffects []
356
357  SeeAlso     []
358
359******************************************************************************/
360void
361SynthSetSupportCount(int *count)
362{
363  SupportCount = count;
364}
365
366
367/**Function********************************************************************
368
369  Synopsis [Sets the variable Probability.]
370
371  Description [Sets the variable Probability.]
372
373  SideEffects []
374
375  SeeAlso     []
376
377******************************************************************************/
378void
379SynthSetProbability(float *prob)
380{
381  Probability = prob;
382}
383
384
385/**Function********************************************************************
386
387  Synopsis [Finds a good divisor for low power.]
388
389  Description [Finds a good divisor for low power.]
390
391  SideEffects []
392
393  SeeAlso     []
394
395******************************************************************************/
396int
397SynthFindDivisorForLowPower(int *count,
398                            int nvars,
399                            int min_count,
400                            int min_pos)
401{
402  int   i, v;
403  float cost, best;
404
405  if ((!SupportCount) || (!Probability))
406    return(-1);
407
408  v = min_pos;
409  if (SuppFactor == 0.0 && ProbFactor == 0.0)
410    best = (float)SupportCount[min_pos] * Probability[min_pos];
411  else {
412    best = (float)SupportCount[min_pos] * SuppFactor +
413      Probability[min_pos] * ProbFactor;
414  }
415
416  for (i = min_pos + 1; i < nvars; i++) {
417    if (count[i] == min_count) {
418      if (SuppFactor == 0.0 && ProbFactor == 0.0)
419        cost = (float)SupportCount[i] * Probability[i];
420      else {
421        cost = (float)SupportCount[i] * SuppFactor +
422          Probability[i] * ProbFactor;
423      }
424      if (cost > best) {
425        best = cost;
426        v = i;
427      }
428    }
429  }
430
431  return(v);
432}
433
434
435/**Function********************************************************************
436
437  Synopsis [Returns the i-th output name.]
438
439  Description [Returns the i-th output name.]
440
441  SideEffects []
442
443  SeeAlso     []
444
445******************************************************************************/
446char *
447SynthGetIthOutputName(int i)
448{
449  return outputNames[i];
450}
451
452
453/**Function********************************************************************
454
455  Synopsis    [Checks whether one support set is a subset of the other
456  support set.]
457
458  Description [Checks whether one support set is a subset of the other
459  support set. A support set is represented by a bit-vector. If the
460  index 0 variable of a unique table is in the support of a function,
461  then the MSB bit is set to 1. In general, for the variable of index
462  i, the i-th bit from the MSB is set to 1. The argument size means
463  the number of words (word = sizeof(int)). If the sets are the same,
464  SynthIsSubsetOfSupport returns 2. If the first set is a subset of
465  the second, it returns 1, otherwise it returns 0.]
466
467  SideEffects []
468
469  SeeAlso     [IsSubsetOfSupportForOneWord IsNullSupport]
470
471******************************************************************************/
472int
473SynthIsSubsetOfSupport(int size,
474                       unsigned int *mask1,
475                       unsigned int *mask2)
476{
477  int   i, tmp, flag = 0;
478
479  if (!mask2)
480    return(1);
481
482  if (IsNullSupport(size, mask1) && IsNullSupport(size, mask2))
483    return(0);
484  else if (IsNullSupport(size, mask1))
485    return(0);
486  else if (IsNullSupport(size, mask2))
487    return(1);
488
489  for (i = 0; i < size; i++) {
490    tmp = IsSubsetOfSupportForOneWord(mask1[i], mask2[i]);
491    if (tmp == 0)
492      return(0);
493    flag |= tmp;
494  }
495
496  return(flag);
497}
498
499
500/*---------------------------------------------------------------------------*/
501/* Definition of static functions                                            */
502/*---------------------------------------------------------------------------*/
503
504/**Function********************************************************************
505
506  Synopsis [This function orders the output functions. With this
507  output ordering, the lowest indexed output function is factorized
508  first.]
509
510  Description [This function orders the output functions. With this
511  output ordering, the lowest indexed output function is factorized
512  first. If OutputOrder is 0, the output order is just the same as the
513  order VIS has. If OutputOrder is 1, the smallest function (in terms
514  of the number of support variables) will be placed first in the
515  order. In case of tie, the function with the smaller BDD is placed
516  before the other in the order. If OutputOrder is 2, the smallest
517  function in terms of BDD size is first.]
518
519  SideEffects []
520
521  SeeAlso     [SynthMultiLevelOptimize]
522
523******************************************************************************/
524static void
525GetOutputOrder(bdd_manager *dd,
526               bdd_node **ofuncs,
527               int no,
528               int *order,
529               int verbosity)
530{
531  int           i, j, k, flag;
532  int           *support, *bddsize;
533  int           size;
534  unsigned int  **mask;
535  int           word, sizeZ;
536  int           pos, bit, bit_mask;
537  int           insert_flag, s1, s2;
538
539  if (no == 1) {
540    order[0] = 0;
541    return;
542  }
543
544  if (OutputOrdering == 0) {
545    for (i = 0; i < no; i++)
546      order[i] = i;
547    return;
548  }
549
550  bddsize = ALLOC(int, no);
551  if (OutputOrdering == 2) {
552    for (i = 0; i < no; i++) {
553      if (!ofuncs[i]) {
554        order[i] = i;
555        bddsize[i] = 0;
556        continue;
557      }
558
559      bddsize[i] = bdd_node_size(ofuncs[i]);
560
561      /* Insert i-th output at the right place in the order. */
562      for (j = 0; j < i; j++) {
563        if (bddsize[i] < bddsize[order[j]]) {
564          for (k = i; k > j; k--)
565            order[k] = order[k - 1];
566          order[j] = i;
567          break;
568        }
569      }
570
571      if (j == i)
572        order[i] = i;
573    }
574
575    if (verbosity) {
576      fprintf(vis_stdout, "output order :");
577      for (i = 0; i < no; i++)
578        fprintf(vis_stdout, " %d", order[i]);
579      fprintf(vis_stdout, "\n");
580      if (verbosity > 1) {
581        for (i = 0; i < no; i++)
582          fprintf(vis_stdout, "%d - %d", i, bddsize[i]);
583      }
584    }
585
586    FREE(bddsize);
587    return;
588  }
589
590  /* Here OutputOrdering should be 1. */
591  mask = ALLOC(unsigned int *, no);
592  sizeZ = bdd_num_zdd_vars(dd);
593  support = ALLOC(int, sizeZ);
594  word = sizeof(int) * 8;
595  size = sizeZ / word + 1;
596
597  for (i = 0; i < no; i++) {
598    if (!ofuncs[i]) {
599      mask[i] = (unsigned int *)NULL;
600      order[i] = i;
601      bddsize[i] = 0;
602      continue;
603    }
604
605    mask[i] = ALLOC(unsigned int, size);
606    (void)memset((void *)mask[i], 0, size * sizeof(int));
607    (void)memset((void *)support, 0, sizeof(int) * sizeZ);
608    SynthZddSupportStep(bdd_regular(ofuncs[i]), support);
609    SynthZddClearFlag(bdd_regular(ofuncs[i]));
610    /* Pack the support array into a bit vector. */
611    for (j = 0; j < sizeZ; j++) {
612      if (support[j]) {
613        pos = j / word;
614        bit = j % word;
615        bit_mask = 01 << bit;
616        mask[i][pos] |= bit_mask;
617      }
618    }
619    bddsize[i] = bdd_node_size(ofuncs[i]);
620
621    for (j = 0; j < i; j++) {
622      insert_flag = 0;
623      flag = SynthIsSubsetOfSupport(size, mask[i], mask[order[j]]);
624      if (flag == 1)
625        insert_flag = 1;
626      else if (flag == 2) {
627        s1 = GetNumberOfSupport(sizeZ, size, mask[i]);
628        s2 = GetNumberOfSupport(sizeZ, size, mask[order[j]]);
629        if (s1 < s2 || (s1 == s2 && bddsize[i] < bddsize[order[j]]))
630          insert_flag = 1;
631      }
632      if (insert_flag) {
633        for (k = i; k > j; k--)
634          order[k] = order[k - 1];
635        order[j] = i;
636        break;
637      }
638    }
639
640    if (j == i)
641      order[i] = i;
642  }
643  FREE(support);
644  FREE(bddsize);
645
646  if (verbosity) {
647    fprintf(vis_stdout, "output order :");
648    for (i = 0; i < no; i++)
649      fprintf(vis_stdout, " %d", order[i]);
650    fprintf(vis_stdout, "\n");
651    if (verbosity > 1) {
652      for (i = 0; i < no; i++) {
653        if (mask[i])
654          PrintSupportMask(sizeZ, size, mask[i]);
655      }
656    }
657  }
658
659  for (i = 0; i < no; i++) {
660    if (mask[i])
661      FREE(mask[i]);
662  }
663  FREE(mask);
664}
665
666
667/**Function********************************************************************
668
669  Synopsis [Checks whether a set of support for one word is subset of the
670  other set of support for one word.]
671
672  Description [Checks whether a set of support for one word is subset of
673  the other set of support for one word. SynthIsSubsetOfSupport() calls
674  this function for each word.]
675
676  SideEffects []
677
678  SeeAlso     [SynthIsSubsetOfSupport]
679
680******************************************************************************/
681static int
682IsSubsetOfSupportForOneWord(unsigned int mask1,
683                            unsigned int mask2)
684{
685  unsigned int  tmp;
686
687  if (mask1 == mask2)
688    return(2);
689
690  tmp = mask1 | mask2;
691  if (tmp != mask2)
692    return(0);
693  return(1);
694}
695
696
697/**Function********************************************************************
698
699  Synopsis [Checks if a support set is empty.]
700
701  Description [Checks if a support set is empty.]
702
703  SideEffects []
704
705  SeeAlso     []
706
707******************************************************************************/
708static int
709IsNullSupport(int size,
710              unsigned int *mask)
711{
712  int   i;
713
714  for (i = 0; i < size; i++) {
715    if (mask[i] != 0)
716      return(0);
717  }
718  return(1);
719}
720
721
722/**Function********************************************************************
723
724  Synopsis [Prints the support of a function.]
725
726  Description [Prints the support of a function. The argument n is the
727  number of variables and size is the number of word and mask is the
728  array of support mask. The first line shows column index by modulo 10
729  and the next line shows which variables are support by printing 1.]
730
731  SideEffects []
732
733  SeeAlso     []
734
735******************************************************************************/
736static void
737PrintSupportMask(int n,
738                 int size,
739                 unsigned int *mask)
740{
741  int   i, j, pos, last;
742  char  *support;
743  char  *mark;
744  int   bit;
745
746  support = ALLOC(char,n);
747  mark = ALLOC(char,n);
748
749  pos = 0;
750  for (i = 0; i < size; i++) {
751    if (i == (size - 1))
752      last = n % 32;
753    else
754      last = 32;
755    bit = 01;
756    for (j = 0; j < last; j++) {
757      sprintf(&mark[pos], "%d", pos % 10);
758      if (mask[i] & bit)
759        support[pos] = '1';
760      else
761        support[pos] = '0';
762      pos++;
763      bit = bit << 1;
764    }
765  }
766  mark[pos] = support[pos] = '\0';
767
768  fprintf(vis_stdout, "%s\n", mark);
769  fprintf(vis_stdout, "%s\n", support);
770
771  FREE(support);
772  FREE(mark);
773}
774
775
776/**Function********************************************************************
777
778  Synopsis [Returns the number of support variables of a function.]
779
780  Description [Returns the number of support variables of a function.]
781
782  SideEffects [none]
783
784  SeeAlso     []
785
786******************************************************************************/
787static int
788GetNumberOfSupport(int n,
789                   int size,
790                   unsigned int *mask)
791{
792  int   i, j, last;
793  int   bit;
794  int   count;
795
796  count = 0;
797  for (i = 0; i < size; i++) {
798    if (i == (size - 1))
799      last = n % 32;
800    else
801      last = 32;
802    bit = 01;
803    for (j = 0; j < last; j++) {
804      if (mask[i] & bit)
805        count++;
806      bit = bit << 1;
807    }
808  }
809  return(count);
810}
811
812
813/**Function********************************************************************
814
815  Synopsis [Factorizes a network.]
816
817  Description [Factorizes a network. If successful, it returns 0,
818  otherwise it returns 1 due to lack of memory.]
819
820  SideEffects []
821
822  SeeAlso     [SynthMultiLevelOptimize]
823
824******************************************************************************/
825static int
826factorizeNetwork(Ntk_Network_t *net,
827                 bdd_manager *dd,
828                 bdd_node **ofuncs,
829                 MlTree **tree,
830                 int no,
831                 int *out_order,
832                 st_table *table,
833                 char **combOutNames,
834                 int divisor,
835                 MlTree *(* factoring_func)(bdd_manager *, st_table *,
836                                            bdd_node *, int, int *, MlTree *,
837                                            int, MlTree *, int),
838                 int verbosity)
839{
840  int           i, j, k;
841  int           ref;
842  int           nml;
843  MlTree        *tmp_tree;
844  int           flag;
845  int           comp_flag;
846
847  SynthSetZddDivisorFunc(divisor); /* set static variable in synthFactor.c */
848
849  for (k = 0; k < no; k++) {
850    i = out_order[k];
851    if (!ofuncs[i]) {
852      tree[i] = NULL;
853      continue;
854    }
855    if (verbosity)
856      SynthPrintZddCoverWithName(net, dd, ofuncs[i]);
857
858    tree[i] = (MlTree *)NULL;
859    ref = 0;
860    if (ofuncs[i] == bdd_read_one(dd) || ofuncs[i] == bdd_read_zero(dd)) {
861      tree[i] = SynthFindOrCreateMlTree(table, dd, ofuncs[i], 1, 0,
862                                        &ref, verbosity);
863      if (!tree[i])
864        return(1);
865    } else {
866      tree[i] = SynthLookupMlTable(table, dd, ofuncs[i], 1, verbosity);
867      if (tree[i]) {
868        if (MlTree_IsComplement(tree[i]) || tree[i]->top)
869          ref = 1;
870        else
871          SynthUpdateRefOfParent(tree[i]);
872      }
873      else if (UseFuncDivisor) {
874        /* Try to divide by existing functions. The smaller
875         * functions are factored first to increase the probability
876         * of success of this step. Both phases of the divisor are
877         * tried.
878         */
879        for (j = k - 1; j >= 0; j--) {
880          tree[i] = (* factoring_func)(dd, table, ofuncs[i], 0, &ref,
881                                       tree[out_order[j]], 0, NULL, verbosity);
882          if (tree[i]) {
883            SynthSetSharedFlag(dd, tree[out_order[j]]);
884            break;
885          } else if (noMemoryFlag == 1)
886            return(1);
887          else {
888            tree[i] = (* factoring_func)(dd, table, ofuncs[i], 0,
889                                 &ref, tree[out_order[j]], 1, NULL, verbosity);
890            if (tree[i]) {
891              SynthSetSharedFlag(dd, tree[out_order[j]]);
892              break;
893            } else if (noMemoryFlag == 1)
894              return(1);
895          }
896        }
897      }
898    }
899    /* Division by other functions did not work. Find a brand-new
900     * factorization.
901     */
902    if (!tree[i]) {
903      tree[i] = (* factoring_func)(dd, table, ofuncs[i], 0,
904                                   &ref, NULL, 0, NULL, verbosity);
905      if (!tree[i])
906        return(1);
907    }
908    /* Compute the complement ZDD node of ofuncs[i], if not exist.
909     * This is to increase sharing.
910     */
911    tmp_tree = tree[i];
912    tree[i] = SynthCheckAndMakeComplement(dd, table, tree[i], &comp_flag,
913                                          verbosity);
914    if (!tree[i])
915      return(1);
916    else if (tree[i] != tmp_tree) {
917      ref = 1;
918      if (comp_flag)
919        tree[i] = MlTree_Not(tree[i]);
920    }
921
922    /* When the tree already exists, create a new tree and copy all
923     * contents, and set the field 'ref' to 1. This is for the
924     * purpose of avoiding duplicate literal counting.
925     */
926    if (ref) {
927      int       comp_flag;
928
929      comp_flag = 0;
930      if (MlTree_IsComplement(tree[i])) {
931        tree[i] = MlTree_Not(tree[i]);
932        comp_flag = 1;
933      }
934      tmp_tree = ALLOC(MlTree, sizeof(MlTree));
935      memcpy((void *)tmp_tree, (void *)tree[i], sizeof(MlTree));
936      tree[i] = tmp_tree;
937      tree[i]->ref = 1;
938      tree[i]->comp = comp_flag;
939    }
940    tree[i]->top = 1;
941    bdd_ref(tree[i]->node);
942
943    nml = SynthCountMlLiteral(dd, tree[i], 1);
944
945    if (verbosity) {
946      SynthPrintMlTreeWithName(net, dd, tree[i], "result : ");
947      fprintf(vis_stdout, "**** %d (#literal = %d) ****\n", i, nml);
948      if (verbosity > 1)
949        SynthWriteEqn(stdout, net, dd, tree[i], ofuncs, combOutNames[i], 1);
950    }
951
952    if (VerifyTreeMode) {
953      SynthVerifyTree(dd, tree[i], 1);
954      SynthVerifyMlTable(dd, table);
955    }
956  }
957
958  flag = SynthPostFactoring(dd, table, factoring_func, verbosity);
959
960  if (VerifyTreeMode) {
961    bdd_node *tmp;
962
963    for (i = 0; i < no; i++) {
964      if (tree[i]->comp)
965        tmp = tree[i]->complement;
966      else
967        tmp = tree[i]->node;
968      if (tmp != ofuncs[i]) {
969        (void) fprintf(vis_stdout,
970                       "** synth error: Different zdds in [%s].\n",
971                       combOutNames[i]);
972      }
973      SynthVerifyTree(dd, tree[i], 1);
974    }
975  }
976
977  return(flag);
978}
Note: See TracBrowser for help on using the repository browser.