source: vis_dev/vis-2.3/src/baig/baigBddSweep.c @ 104

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

vis2.3
  • Property svn:executable set to *
File size: 22.2 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [baigBddSweep.c]
4
5  PackageName [baig]
6
7  Synopsis    [Functions to find functional equivalent node index using bdd sweeping.]
8
9  Author      [HoonSang Jin]
10
11  Copyright [ This file was created at the University of Colorado at
12  Boulder.  The University of Colorado at Boulder makes no warranty
13  about the suitability of this software for any purpose.  It is
14  presented on an AS IS basis.]
15
16******************************************************************************/
17
18#include "maig.h"
19#include "ntk.h"
20#include "cmd.h"
21#include "baig.h"
22#include "baigInt.h"
23#include "heap.h"
24#include "ntmaig.h"
25#include "ord.h"
26
27static char rcsid[] UNUSED = "$Id: baigBddSweep.c,v 1.13 2005/05/18 18:11:42 jinh Exp $";
28
29/*---------------------------------------------------------------------------*/
30/* Constant declarations                                                     */
31/*---------------------------------------------------------------------------*/
32
33
34/*---------------------------------------------------------------------------*/
35/* Stucture declarations                                                     */
36/*---------------------------------------------------------------------------*/
37
38
39/*---------------------------------------------------------------------------*/
40/* Type declarations                                                         */
41/*---------------------------------------------------------------------------*/
42
43
44/*---------------------------------------------------------------------------*/
45/* Variable declarations                                                     */
46/*---------------------------------------------------------------------------*/
47
48/*---------------------------------------------------------------------------*/
49/* Macro declarations                                                        */
50/*---------------------------------------------------------------------------*/
51
52
53/**AutomaticStart*************************************************************/
54
55/*---------------------------------------------------------------------------*/
56/* Static function prototypes                                                */
57/*---------------------------------------------------------------------------*/
58
59static int SweepBddCompare(const char *x, const char *y);
60static int SweepBddHash(char *x, int size);
61
62/**AutomaticEnd***************************************************************/
63
64
65/*---------------------------------------------------------------------------*/
66/* Definition of exported functions                                          */
67/*---------------------------------------------------------------------------*/
68void bAig_BuildAigBFSManner( Ntk_Network_t *network, mAig_Manager_t *manager, st_table *leaves, int sweep);
69void bAig_BddSweepMain(Ntk_Network_t *network, array_t *nodeArray);
70void bAig_BddSweepForceMain(Ntk_Network_t *network, array_t *nodeArray);
71
72/**Function********************************************************************
73
74  Synopsis    [Compare function for BDD sweeping]
75
76  Description [Compare function for BDD sweeping]
77
78  SideEffects []
79
80  SeeAlso     []
81
82******************************************************************************/
83static int
84SweepBddCompare(const char *x, const char *y)
85{
86  return(bdd_ptrcmp((bdd_t *)x, (bdd_t *)y));
87}
88
89/**Function********************************************************************
90
91  Synopsis    [Hashing function for BDD sweeping]
92
93  Description [Hashing function for BDD sweeping]
94
95  SideEffects []
96
97  SeeAlso     []
98
99******************************************************************************/
100static int
101SweepBddHash(char *x, int size)
102{
103
104  return(bdd_ptrhash((bdd_t *)x, size));
105}
106
107/**Function********************************************************************
108
109  Synopsis    [BDD sweeping for aig nodes]
110
111  Description [BDD sweeping for aig nodes rooted at latch data inputs and
112               primary outputs]
113
114  SideEffects []
115
116  SeeAlso     []
117
118******************************************************************************/
119void
120bAig_BddSweepMain(Ntk_Network_t *network, array_t *nodeArray)
121{
122  array_t *mVarList, *bVarList;
123  bdd_t *bdd, *func;
124  int bddIdIndex;
125  int i, count, sizeLimit, mvfSize;
126  int maxSize, curSize;
127  array_t *tnodeArray;
128  lsGen gen;
129  st_generator *gen1;
130  Ntk_Node_t *node;
131  bAigEdge_t v;
132  MvfAig_Function_t  *mvfAig;
133  mAig_Manager_t *manager;
134  mdd_manager *mgr;
135  st_table *node2MvfAigTable;
136  st_table * bdd2vertex;
137  mAigMvar_t mVar;
138  mAigBvar_t bVar;
139  int index1, mAigId;
140
141
142  manager = Ntk_NetworkReadMAigManager(network);
143
144  mgr = Ntk_NetworkReadMddManager(network);
145  if(mgr == 0) {
146    Ord_NetworkOrderVariables(network, Ord_RootsByDefault_c, 
147            Ord_NodesByDefault_c, FALSE, Ord_InputAndLatch_c, 
148            Ord_Unassigned_c, 0, 0);
149    mgr = Ntk_NetworkReadMddManager(network);
150  }
151  node2MvfAigTable = 
152      (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
153
154  bdd2vertex = st_init_table(SweepBddCompare, SweepBddHash);
155
156  sizeLimit = 500;
157  maxSize = manager->nodesArraySize;
158
159  tnodeArray = 0;
160  if(nodeArray == 0) {
161    bVarList = mAigReadBinVarList(manager);
162    mVarList = mAigReadMulVarList(manager);
163    tnodeArray = array_alloc(bAigEdge_t, 0);
164    Ntk_NetworkForEachLatch(network, gen, node) { 
165      node = Ntk_LatchReadDataInput(node);
166      st_lookup(node2MvfAigTable, node, &mvfAig);
167      mvfSize = array_n(mvfAig);
168      for(i=0; i<mvfSize; i++){
169        v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, i));
170        array_insert_last(bAigEdge_t, tnodeArray, v);
171      }
172
173      mAigId = Ntk_NodeReadMAigId(node);
174      mVar = array_fetch(mAigMvar_t, mVarList, mAigId);
175      for(i=0, index1=mVar.bVars; i<mVar.encodeLength; i++) {
176        bVar = array_fetch(mAigBvar_t, bVarList, index1++);
177        v = bVar.node;
178        v = bAig_GetCanonical(manager, v);
179        array_insert_last(bAigEdge_t, tnodeArray, v);
180      }
181    }
182    Ntk_NetworkForEachPrimaryOutput(network, gen, node) { 
183      st_lookup(node2MvfAigTable, node, &mvfAig);
184      mvfSize = array_n(mvfAig);
185      for(i=0; i<mvfSize; i++){
186        v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, i));
187        array_insert_last(bAigEdge_t, tnodeArray, v);
188      }
189    }
190  }
191
192  count = bAigNodeID(manager->nodesArraySize);
193  for(i=0; i<count; i++) {
194    manager->bddIdArray[i] = -1;
195    manager->bddArray[i] = 0;
196  }
197  manager->bddArray[0] = bdd_zero(mgr);
198
199  bddIdIndex = 0;
200  for(i=bAigNodeSize; i<manager->nodesArraySize; i+=bAigNodeSize) {
201    if(leftChild(i) != 2)       continue;
202    bdd = bdd_get_variable(mgr, bddIdIndex);
203    manager->bddIdArray[bAigNodeID(i)] = bddIdIndex;
204    manager->bddArray[bAigNodeID(i)] = bdd;
205    bddIdIndex++;
206  }
207
208  if(nodeArray) {
209    for(i=0; i<array_n(nodeArray); i++) {
210      v = array_fetch(bAigEdge_t, nodeArray, i);
211      v = bAig_GetCanonical(manager, v);
212      bAig_BddSweepSub(manager, mgr, v, bdd2vertex, sizeLimit, &bddIdIndex);
213    }
214  }
215  else {
216    for(i=0; i<array_n(tnodeArray); i++) {
217      v = array_fetch(bAigEdge_t, tnodeArray, i);
218      v = bAig_GetCanonical(manager, v);
219      bAig_BddSweepSub(manager, mgr, v, bdd2vertex, sizeLimit, &bddIdIndex);
220    }
221    array_free(tnodeArray);
222  }
223 
224  count = bAigNodeID(manager->nodesArraySize);
225  for(i=0; i<count; i++) {
226    if(manager->bddArray[i])    {
227      bdd_free(manager->bddArray[i]);
228      manager->bddArray[i] = 0;
229    }
230  }
231
232  st_foreach_item(bdd2vertex, gen1, &func, &v) {
233    bdd_free(func);
234  }
235  st_free_table(bdd2vertex);
236
237  count = bAigNodeID(manager->nodesArraySize);
238  curSize = 0;
239  for(i=0; i<count; i++) {
240    if(bAigGetPassFlag(manager, i*bAigNodeSize)) {
241      curSize++;
242    }
243  }
244  /*
245  fprintf(vis_stdout, "NOTICE : Before %d after %d used %d\n",
246          maxSize/bAigNodeSize, count, (maxSize-curSize)/bAigNodeSize);
247  fflush(vis_stdout);
248  */
249  return;
250
251}
252
253/**Function********************************************************************
254
255  Synopsis    [Auxiliary function for BDD sweeping]
256
257  Description [Auxiliary function for BDD sweeping]
258
259  SideEffects []
260
261  SeeAlso     []
262
263******************************************************************************/
264void
265bAig_BddSweepSub(
266        bAig_Manager_t *manager, 
267        mdd_manager *mgr, 
268        bAigEdge_t v, 
269        st_table *bdd2vertex,
270        int sizeLimit,
271        int *newBddIdIndex)
272{
273  bAigEdge_t left, right, oldV, nv;
274  bdd_t *leftBdd, *rightBdd;
275  bdd_t *func, *nfunc, *funcBar, *newBdd;
276  int newId, size;
277
278  if(v == 0 || v == 1)  return;
279  if(manager->bddArray[bAigNodeID(v)]) {
280    return;
281  }
282
283  left = leftChild(v);
284  right = rightChild(v);
285  left = bAig_GetCanonical(manager, left);
286  right = bAig_GetCanonical(manager, right);
287
288  if(left == 2 && right == 2) {
289    return;
290  }
291
292  bAig_BddSweepSub(manager, mgr, left, bdd2vertex, sizeLimit, newBddIdIndex);
293  bAig_BddSweepSub(manager, mgr, right, bdd2vertex, sizeLimit, newBddIdIndex);
294
295  v = bAig_GetCanonical(manager, v);
296  if(manager->bddArray[bAigNodeID(v)]) {
297    return;
298  }
299
300  left = leftChild(v);
301  right = rightChild(v);
302  left = bAig_GetCanonical(manager, left);
303  right = bAig_GetCanonical(manager, right);
304
305  leftBdd = manager->bddArray[bAigNodeID(left)];
306  rightBdd = manager->bddArray[bAigNodeID(right)];
307
308  if(leftBdd == 0) {
309    bAig_BddSweepSub(manager, mgr, left, bdd2vertex, sizeLimit, newBddIdIndex);
310    left = bAig_GetCanonical(manager, left);
311    leftBdd = manager->bddArray[bAigNodeID(left)];
312  }
313
314  if(rightBdd == 0) {
315    bAig_BddSweepSub(manager, mgr, right, bdd2vertex, sizeLimit, newBddIdIndex);
316    right = bAig_GetCanonical(manager, right);
317    rightBdd = manager->bddArray[bAigNodeID(right)];
318  }
319
320  /**
321  bAig_VerifyBddArray(manager, leftBdd, left);
322  bAig_VerifyBddArray(manager, rightBdd, right);
323  **/
324
325  if(leftBdd == 0 || rightBdd == 0) {
326    fprintf(vis_stdout, 
327            "ERROR : all the nodes should have bdd node at this moment\n");
328  }
329
330  func = bdd_and(leftBdd, rightBdd, 
331             !bAig_IsInverted(left), !bAig_IsInverted(right));
332
333  if(bAig_IsInverted(v))        {
334    funcBar = bdd_not(func);
335    nfunc = funcBar;
336  }
337  else {
338    nfunc = bdd_dup(func);
339  }
340
341  if(st_lookup(bdd2vertex, nfunc, &oldV)) {
342    bAig_Merge(manager, oldV, v);
343  }
344  else {
345    funcBar = bdd_not(nfunc);
346    if(st_lookup(bdd2vertex, funcBar, &oldV)) {
347      bAig_Merge(manager, bAig_Not(oldV), v);
348    }
349    bdd_free(funcBar);
350  }
351  bdd_free(nfunc);
352
353  v = bAig_NonInvertedEdge(v);
354  nv = bAig_GetCanonical(manager, v);
355  v = nv;
356
357  if(manager->bddArray[bAigNodeID(v)] == 0) {
358    size = bdd_size(func);
359    if(size > sizeLimit) {
360      newId = *newBddIdIndex;
361      (*newBddIdIndex) ++;
362      newBdd = bdd_get_variable(mgr, newId);
363      manager->bddIdArray[bAigNodeID(v)] = newId;
364      bdd_free(func);
365      func = newBdd;
366      manager->bddArray[bAigNodeID(v)] = func;
367      st_insert(bdd2vertex, (char *)bdd_dup(func), (char *)bAig_NonInvertedEdge(v));
368    }
369    else {
370      if(bAig_IsInverted(v)) {
371        funcBar = bdd_not(func);
372        manager->bddArray[bAigNodeID(v)] = funcBar;
373        st_insert(bdd2vertex, (char *)func, (char *)v);
374      }
375      else {
376        manager->bddArray[bAigNodeID(v)] = func;
377        st_insert(bdd2vertex, (char *)bdd_dup(func), (char *)v);
378      }
379    }
380  }
381  else  bdd_free(func);
382
383}
384
385/**Function********************************************************************
386
387  Synopsis    [Build aig nodes in breath first manner]
388
389  Description [Build aig nodes in breath first manner]
390
391  SideEffects []
392
393  SeeAlso     []
394
395******************************************************************************/
396void
397bAig_BuildAigBFSManner(
398        Ntk_Network_t *network, 
399        mAig_Manager_t *manager, 
400        st_table *leaves,
401        int sweep)
402{
403array_t *nodeArray, *result;
404lsGen gen1;
405int iter, maxLevel, level;
406int i, j, k;
407bAigEdge_t v;
408Ntk_Node_t *node, *fanin, *fanout;
409st_table *node2mvfAigTable;
410array_t *curArray, *nextArray, *tmpArray;
411array_t *levelArray, *clevelArray;
412MvfAig_Function_t  *mvfAig;
413int mvfSize;
414st_generator *gen;
415
416  Ntk_NetworkForEachNode(network, gen1, node) {
417    Ntk_NodeSetUndef(node, (void *)0);
418  }
419
420  curArray = array_alloc(Ntk_Node_t *, 0);
421  st_foreach_item(leaves, gen, &node, &fanout) {
422    array_insert_last(Ntk_Node_t *, curArray, node);
423    Ntk_NodeSetUndef(node, (void *)1);
424  }
425
426  levelArray = array_alloc(array_t *, 10);
427  nextArray = array_alloc(Ntk_Node_t *, 0);
428  iter = 0;
429  while(1) {
430    clevelArray = array_alloc(array_t *, 10);
431    array_insert_last(array_t *, levelArray, clevelArray);
432    for(i=0; i<array_n(curArray); i++) {
433      node = array_fetch(Ntk_Node_t *, curArray, i);
434      Ntk_NodeForEachFanout(node, j, fanout) { 
435
436        level = (int)(long)Ntk_NodeReadUndef(fanout);
437        if(level > 0)   continue;
438
439        maxLevel = 0;
440        Ntk_NodeForEachFanin(fanout, k, fanin) {
441          level = (int)(long)Ntk_NodeReadUndef(fanin);
442          if(level == 0) {
443            maxLevel = 0;
444            break;
445          }
446          else if(level > maxLevel) {
447            maxLevel = level;
448          }
449        }
450
451        if(maxLevel > 0) {
452          Ntk_NodeSetUndef(fanout, (void *)(long)(maxLevel+1));
453          array_insert_last(Ntk_Node_t *, nextArray, fanout);
454          array_insert_last(Ntk_Node_t *, clevelArray, fanout);
455        }
456      }
457    }
458   
459    curArray->num = 0;
460    tmpArray = curArray;
461    curArray = nextArray;
462    nextArray = tmpArray;
463    if(curArray->num == 0)      break;
464
465    iter++;
466  }
467
468  Ntk_NetworkForEachNode(network, gen1, node) {
469    Ntk_NodeSetUndef(node, (void *)0);
470  }
471
472  for(i=0; i<array_n(levelArray); i++) {
473    clevelArray = array_fetch(array_t *, levelArray, i);
474    result = ntmaig_NetworkBuildMvfAigs(network, clevelArray, leaves);
475    MvfAig_FunctionArrayFree(result);
476    node2mvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(
477            network, MVFAIG_NETWORK_APPL_KEY);
478
479    if(i < 50 && sweep) {
480      nodeArray = array_alloc(bAigEdge_t, 0);
481      for(j=0; j<array_n(clevelArray); j++) {
482        node = array_fetch(Ntk_Node_t *, clevelArray, j);
483        st_lookup(node2mvfAigTable, node, &mvfAig);
484        mvfSize = array_n(mvfAig);
485        for(k=0; k<mvfSize; k++){
486          v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, k));
487          array_insert_last(bAigEdge_t, nodeArray, v);
488        }
489      }
490
491      bAig_BddSweepForceMain(network, nodeArray);
492 
493      for(j=0; j<array_n(clevelArray); j++) {
494        node = array_fetch(Ntk_Node_t *, clevelArray, j);
495        st_lookup(node2mvfAigTable, node, &mvfAig);
496        mvfSize = array_n(mvfAig);
497        for(k=0; k<mvfSize; k++){
498          v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, k));
499          array_insert(bAigEdge_t, nodeArray, v, k);
500        }
501      }
502      array_free(nodeArray);
503    }
504
505    array_free(clevelArray);
506  }
507  array_free(levelArray);
508}
509
510
511/**Function********************************************************************
512
513  Synopsis    [BDD sweeping ]
514
515  Description [BDD sweeping ]
516
517  SideEffects []
518
519  SeeAlso     []
520
521******************************************************************************/
522void
523bAig_BddSweepForceMain(Ntk_Network_t *network, array_t *nodeArray)
524{
525  array_t *mVarList, *bVarList;
526  bdd_t *bdd, *func;
527  int bddIdIndex;
528  int i, count, sizeLimit, mvfSize;
529  int maxSize, curSize;
530  array_t *tnodeArray;
531  lsGen gen;
532  st_generator *gen1;
533  Ntk_Node_t *node;
534  bAigEdge_t v;
535  MvfAig_Function_t  *mvfAig;
536  mAig_Manager_t *manager;
537  mdd_manager *mgr;
538  st_table *node2MvfAigTable;
539  st_table * bdd2vertex;
540  mAigMvar_t mVar;
541  mAigBvar_t bVar;
542  int index1, mAigId;
543  int newmask, resetNewmask;
544  int usedAig;
545
546
547  manager = Ntk_NetworkReadMAigManager(network);
548
549  mgr = Ntk_NetworkReadMddManager(network);
550  if(mgr == 0) {
551    Ord_NetworkOrderVariables(network, Ord_RootsByDefault_c, 
552            Ord_NodesByDefault_c, FALSE, Ord_InputAndLatch_c, 
553            Ord_Unassigned_c, 0, 0);
554    mgr = Ntk_NetworkReadMddManager(network);
555  }
556  node2MvfAigTable = 
557      (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
558
559  bdd2vertex = st_init_table(SweepBddCompare, SweepBddHash);
560
561  sizeLimit = 500;
562  maxSize = manager->nodesArraySize;
563
564  tnodeArray = 0;
565  if(nodeArray == 0) {
566    bVarList = mAigReadBinVarList(manager);
567    mVarList = mAigReadMulVarList(manager);
568    tnodeArray = array_alloc(bAigEdge_t, 0);
569    Ntk_NetworkForEachLatch(network, gen, node) { 
570      node = Ntk_LatchReadDataInput(node);
571      st_lookup(node2MvfAigTable, node, &mvfAig);
572      mvfSize = array_n(mvfAig);
573      for(i=0; i<mvfSize; i++){
574        v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, i));
575        array_insert_last(bAigEdge_t, tnodeArray, v);
576      }
577
578      mAigId = Ntk_NodeReadMAigId(node);
579      mVar = array_fetch(mAigMvar_t, mVarList, mAigId);
580      for(i=0, index1=mVar.bVars; i<mVar.encodeLength; i++) {
581        bVar = array_fetch(mAigBvar_t, bVarList, index1++);
582        v = bVar.node;
583        v = bAig_GetCanonical(manager, v);
584        array_insert_last(bAigEdge_t, tnodeArray, v);
585      }
586    }
587    Ntk_NetworkForEachPrimaryOutput(network, gen, node) { 
588      st_lookup(node2MvfAigTable, node, &mvfAig);
589      mvfSize = array_n(mvfAig);
590      for(i=0; i<mvfSize; i++){
591        v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, i));
592        array_insert_last(bAigEdge_t, tnodeArray, v);
593      }
594    }
595  }
596
597  count = bAigNodeID(manager->nodesArraySize);
598  for(i=0; i<count; i++) {
599    manager->bddIdArray[i] = -1;
600    manager->bddArray[i] = 0;
601  }
602  manager->bddArray[0] = bdd_zero(mgr);
603
604  bddIdIndex = 0;
605  for(i=bAigNodeSize; i<manager->nodesArraySize; i+=bAigNodeSize) {
606    if(leftChild(i) != 2)       continue;
607    bdd = bdd_get_variable(mgr, bddIdIndex);
608    manager->bddIdArray[bAigNodeID(i)] = bddIdIndex;
609    manager->bddArray[bAigNodeID(i)] = bdd;
610    bddIdIndex++;
611  }
612
613  if(nodeArray) {
614    for(i=0; i<array_n(nodeArray); i++) {
615      v = array_fetch(bAigEdge_t, nodeArray, i);
616      v = bAig_GetCanonical(manager, v);
617      bAig_BddSweepForceSub(manager, mgr, v, bdd2vertex, sizeLimit, &bddIdIndex);
618    }
619  }
620  else {
621    for(i=0; i<array_n(tnodeArray); i++) {
622      v = array_fetch(bAigEdge_t, tnodeArray, i);
623      v = bAig_GetCanonical(manager, v);
624      bAig_BddSweepForceSub(manager, mgr, v, bdd2vertex, sizeLimit, &bddIdIndex);
625    }
626  }
627 
628  count = bAigNodeID(manager->nodesArraySize);
629  for(i=0; i<count; i++) {
630    if(manager->bddArray[i])    {
631      bdd_free(manager->bddArray[i]);
632      manager->bddArray[i] = 0;
633    }
634  }
635
636  st_foreach_item(bdd2vertex, gen1, &func, &v) {
637    bdd_free(func);
638  }
639  st_free_table(bdd2vertex);
640
641  count = bAigNodeID(manager->nodesArraySize);
642  curSize = 0;
643  for(i=0; i<count; i++) {
644    if(bAigGetPassFlag(manager, i*bAigNodeSize)) {
645      curSize++;
646    }
647  }
648
649
650  newmask = 0x00000100;
651  resetNewmask = 0xfffffeff;
652  if(tnodeArray) {
653  for(i=0; i<array_n(tnodeArray); i++) {
654    v = array_fetch(int, tnodeArray, i);
655    bAig_SetMaskTransitiveFanin(manager, v, newmask);
656  }
657
658  usedAig = 0;
659  for(i=bAigNodeSize; i<manager->nodesArraySize; i+=bAigNodeSize) {
660    if(flags(i) & newmask)      usedAig++;
661  }
662
663  for(i=0; i<array_n(tnodeArray); i++) {
664    v = array_fetch(int, tnodeArray, i);
665    bAig_ResetMaskTransitiveFanin(manager, v, newmask, resetNewmask);
666  }
667  array_free(tnodeArray);
668  fprintf(vis_stdout, "NOTICE : Before %d after %d used %d\n", 
669          maxSize/bAigNodeSize, count, usedAig);
670  fflush(vis_stdout);
671  }
672
673}
674
675/**Function********************************************************************
676
677  Synopsis    [Auxilary function BDD sweeping ]
678
679  Description [Auxilary function BDD sweeping ]
680
681  SideEffects []
682
683  SeeAlso     []
684
685******************************************************************************/
686void
687bAig_BddSweepForceSub(
688        bAig_Manager_t *manager, 
689        mdd_manager *mgr, 
690        bAigEdge_t v, 
691        st_table *bdd2vertex,
692        int sizeLimit,
693        int *newBddIdIndex)
694{
695  bAigEdge_t left, right, oldV, nv;
696  bdd_t *leftBdd, *rightBdd;
697  bdd_t *func, *nfunc, *funcBar, *newBdd;
698  int newId, size;
699
700  if(v == 0 || v == 1)  return;
701  if(manager->bddArray[bAigNodeID(v)]) {
702    return;
703  }
704
705
706  left = leftChild(v);
707  right = rightChild(v);
708  left = bAig_GetCanonical(manager, left);
709  right = bAig_GetCanonical(manager, right);
710
711  if(left == 2 && right == 2) {
712    return;
713  }
714
715  bAig_BddSweepForceSub(manager, mgr, left, bdd2vertex, sizeLimit, newBddIdIndex);
716  bAig_BddSweepForceSub(manager, mgr, right, bdd2vertex, sizeLimit, newBddIdIndex);
717
718  v = bAig_GetCanonical(manager, v);
719  if(manager->bddArray[bAigNodeID(v)]) {
720    return;
721  }
722
723  left = leftChild(v);
724  right = rightChild(v);
725  left = bAig_GetCanonical(manager, left);
726  right = bAig_GetCanonical(manager, right);
727
728  leftBdd = manager->bddArray[bAigNodeID(left)];
729  rightBdd = manager->bddArray[bAigNodeID(right)];
730
731  if(leftBdd == 0) {
732    bAig_BddSweepForceSub(manager, mgr, left, bdd2vertex, sizeLimit, newBddIdIndex);
733    left = bAig_GetCanonical(manager, left);
734    leftBdd = manager->bddArray[bAigNodeID(left)];
735  }
736
737  if(rightBdd == 0) {
738    bAig_BddSweepForceSub(manager, mgr, right, bdd2vertex, sizeLimit, newBddIdIndex);
739    right = bAig_GetCanonical(manager, right);
740    rightBdd = manager->bddArray[bAigNodeID(right)];
741  }
742
743  /**
744  bAig_VerifyBddArray(manager, leftBdd, left);
745  bAig_VerifyBddArray(manager, rightBdd, right);
746  **/
747
748  if(leftBdd == 0 || rightBdd == 0) {
749    fprintf(vis_stdout, 
750            "ERROR : all the nodes should have bdd node at this moment\n");
751  }
752
753  func = bdd_and(leftBdd, rightBdd, 
754             !bAig_IsInverted(left), !bAig_IsInverted(right));
755
756  if(bAig_IsInverted(v))        {
757    funcBar = bdd_not(func);
758    nfunc = funcBar;
759  }
760  else {
761    nfunc = bdd_dup(func);
762  }
763
764  if(st_lookup(bdd2vertex, nfunc, &oldV)) {
765    bAig_Merge(manager, oldV, v);
766  }
767  else {
768    funcBar = bdd_not(nfunc);
769    if(st_lookup(bdd2vertex, funcBar, &oldV)) {
770      bAig_Merge(manager, bAig_Not(oldV), v);
771    }
772    bdd_free(funcBar);
773  }
774  bdd_free(nfunc);
775
776  v = bAig_NonInvertedEdge(v);
777  nv = bAig_GetCanonical(manager, v);
778  v = nv;
779
780  if(manager->bddArray[bAigNodeID(v)] == 0) {
781    size = bdd_size(func);
782    if(size > sizeLimit) {
783      newId = *newBddIdIndex;
784      (*newBddIdIndex) ++;
785      newBdd = bdd_get_variable(mgr, newId);
786      manager->bddIdArray[bAigNodeID(v)] = newId;
787      bdd_free(func);
788      func = newBdd;
789      manager->bddArray[bAigNodeID(v)] = func;
790      st_insert(bdd2vertex, (char *)bdd_dup(func), (char *)bAig_NonInvertedEdge(v));
791    }
792    else {
793      if(bAig_IsInverted(v)) {
794        funcBar = bdd_not(func);
795        manager->bddArray[bAigNodeID(v)] = funcBar;
796        st_insert(bdd2vertex, (char *)func, (char *)v);
797      }
798      else {
799        manager->bddArray[bAigNodeID(v)] = func;
800        st_insert(bdd2vertex, (char *)bdd_dup(func), (char *)v);
801      }
802    }
803  }
804  else  bdd_free(func);
805
806  return;
807}
Note: See TracBrowser for help on using the repository browser.