source: vis_dev/vis-2.3/src/res/resCompose.c @ 53

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

vis2.3

File size: 46.8 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [resCompose.c]
4
5  PackageName [res]
6
7  Synopsis [This file contains all relevant procedures for the composition of
8  the nodes of the circuit into the residue Add.]
9
10  Author      [Kavita Ravi    <ravi@boulder.colorado.edu> and
11               Abelardo Pardo <abel@boulder.colorado.edu>]
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 "resInt.h"
20
21static char rcsid[] UNUSED = "$Id: resCompose.c,v 1.30 2005/04/18 05:00:14 fabio Exp $";
22
23/*---------------------------------------------------------------------------*/
24/* Constant declarations                                                     */
25/*---------------------------------------------------------------------------*/
26
27/*---------------------------------------------------------------------------*/
28/* Structure declarations                                                    */
29/*---------------------------------------------------------------------------*/
30
31/*---------------------------------------------------------------------------*/
32/* Type declarations                                                         */
33/*---------------------------------------------------------------------------*/
34
35/*---------------------------------------------------------------------------*/
36/* Variable declarations                                                     */
37/*---------------------------------------------------------------------------*/
38long Res_composeTime;
39long Res_shuffleTime;
40long Res_smartVarTime;
41long Res_orderTime;
42
43/*---------------------------------------------------------------------------*/
44/* Macro declarations                                                        */
45/*---------------------------------------------------------------------------*/
46
47/**AutomaticStart*************************************************************/
48
49/*---------------------------------------------------------------------------*/
50/* Static function prototypes                                                */
51/*---------------------------------------------------------------------------*/
52
53static void UpdateUnassignedNodesWithNewIds(lsList orderList, array_t *newIdArray);
54static lsList CreateNodeAndFaninOrderList(array_t *currentLayer);
55static lsList ListAppend(Ntk_Node_t *nodePtr, lsList newList, lsList faninList);
56static int IdCompare(const void *obj1, const void *obj2);
57static int IdListCompare(lsGeneric item1, lsGeneric item2);
58static lsList CreateFaninVarSetList(array_t *currentLayer, st_table *faninTable);
59static bdd_node * ComposeLayer(bdd_manager *ddManager, bdd_node *residueDd, array_t *currentLayer, bdd_node **functionArray);
60static Mvf_Function_t * NodeBuildConstantMvf(Ntk_Node_t * node, mdd_manager *mddMgr);
61
62/**AutomaticEnd***************************************************************/
63
64
65/*---------------------------------------------------------------------------*/
66/* Definition of exported functions                                          */
67/*---------------------------------------------------------------------------*/
68
69
70/*---------------------------------------------------------------------------*/
71/* Definition of internal functions                                          */
72/*---------------------------------------------------------------------------*/
73
74 
75/**Function********************************************************************
76
77  Synopsis [Return a referenced BDD for the function of a node.]
78
79  Description [Return a referenced BDD for the function of a node. This
80  procedure uses the Ntm call but frees the rest of the MDD structure and
81  returns the bdd only. The arguments to this function are the network to which
82  this node belongs, the node whose bdd is required and the type of fanin
83  support its BDDs need to be in terms of.]
84
85  SideEffects   []
86
87  SeeAlso            [Res_NetworkResidueVerify]
88
89******************************************************************************/
90bdd_node *
91BuildBDDforNode(Ntk_Network_t *network,
92                Ntk_Node_t *nodePtr,
93                int fanin)
94{
95  bdd_node *function;
96  st_table *leaves;
97  array_t *mvfArray;
98  Mvf_Function_t *nodeFunction;
99  Ntk_Node_t *faninNodePtr;
100  lsGen netGen;
101  array_t *root;
102  int j;
103  mdd_manager *mddMgr;
104
105  /* if it is a constant, build the mvf for it */
106  if( Ntk_NodeTestIsConstant(nodePtr) == 1) {
107    mddMgr = (mdd_manager *)Ntk_NetworkReadMddManager(network);
108    nodeFunction = NodeBuildConstantMvf(nodePtr, mddMgr);
109  } else if (Ntk_NodeTestIsCombInput(nodePtr)) {
110    /* the Bdd for a latch input is itself */
111    mddMgr = (mdd_manager *)Ntk_NetworkReadMddManager(network);
112    nodeFunction = Mvf_FunctionCreateFromVariable(mddMgr, Ntk_NodeReadMddId(nodePtr));
113  } else {
114
115    /* Set the root to build the Mvf */
116    root = array_alloc(Ntk_Node_t *, 1);
117    array_insert(Ntk_Node_t *, root, 0, nodePtr);
118   
119    /* Set the leaves depending on the fanin flag*/
120    leaves = st_init_table(st_ptrcmp, st_ptrhash);
121    if (fanin == IMMEDIATE_FANIN) {
122      Ntk_NodeForEachFanin(nodePtr, j, faninNodePtr) {
123        st_insert(leaves, (char *)faninNodePtr, (char *)NTM_UNUSED);
124      }
125    } else if (fanin == PRIMARY_INPUTS) {
126      Ntk_NetworkForEachCombInput(network, netGen, nodePtr) {
127        st_insert(leaves, (char *)nodePtr, (char *)NTM_UNUSED);
128      }
129    }
130       
131    /* Effectively compute the function (We are not using don't cares)*/
132    mvfArray = Ntm_NetworkBuildMvfs(network, root, leaves, NIL(mdd_t));
133    st_free_table(leaves);
134    array_free(root);
135   
136    nodeFunction = array_fetch(Mvf_Function_t *, mvfArray, 0);
137    /* since we built the MDD for only one root */
138    array_free(mvfArray);
139  } /* end of else if not a latch output */
140  /*
141   * The function above returned a Mvf_Function_t, but since we are
142   * working with binary nodes (so far), we do not need the Mvf
143   * representation, therefore we only keep one single Bdd and deallocate
144   * all the memory attached to the rest of the Mvf.
145   */
146  function = (bdd_node *)bdd_extract_node_as_is(Mvf_FunctionReadComponent(nodeFunction, 1));
147  if (function != NULL) {
148    bdd_ref(function);
149  }
150 
151  /* Clean up */
152  Mvf_FunctionFree(nodeFunction);
153  return (function);
154}
155
156
157/**Function********************************************************************
158
159  Synopsis [Procedure to compose the network into the residue ADD.]
160
161  Description [Procedure to compose the network into the residue ADD.  Assume
162  here that the output nodes are labeled with the same ids as the vars in the
163  initial residue dd. The variable manager has to be initialized for smart
164  variable allocation. First the variable manager is updated with the output
165  node Ids. Starting from the last layer, the nodes in each layer are ordered
166  with their fanins such that the nodes being composed in are always above
167  their fanin. This list is given to the variable manager to update the Ids in
168  use, provide available Ids for the unassigned nodes and allocate new
169  variables in both the variable and Dd manager. The variable manager then
170  marks all the node and fanin ids in use and returns an id array for the
171  unassigned nodes, reusing the ids whenever possible. It is also responsible
172  for creating an inverse permutation array with the current layer nodes and
173  their fanins in the order of the list and nodes unrelated at the bottom. The
174  unassigned nodes are updated with the ID array. The inverse permutation array
175  is fed to a CUDD procedure that moves the Ids to the required levels. Once
176  this order is achieved, composition is performed depending on the method
177  specified. Since the variable allocation procedure assumes that nodes with
178  unassigned IDs need to be filled with the holes closest to them, the ID on
179  each node is cleared after composition. This also makes it cleaner. The
180  variable manager is freed at the end of the procedure. The result of the
181  composition is the new residue Dd and is used for composition of the next
182  layer. The procedure returns the residue Dd in terms of the primary
183  inputs. The arguments to this function are the network to which the layers
184  belong, the layer array structure and the residue DD into which the circuit
185  needs to be composed into.This assumes that the residue DD has as many
186  variables as the number of outputs and the Ids of the variables starts with
187  0.]
188
189  SideEffects []
190
191  SeeAlso     [ResidueVerification]
192
193******************************************************************************/
194bdd_node *
195ComposeLayersIntoResidue(Ntk_Network_t *network, 
196                         array_t *layerArray, 
197                         bdd_node *residueDd,
198                         array_t *outputArray)
199{
200  bdd_manager *ddManager;                 /* Dd Manager */
201  bdd_node *newResidueDd = NIL(bdd_node); /* final composed Dd */
202  bdd_node *currentDd;                   /* local copy of residue Dd to
203                                          * perform composition
204                                          */
205  lsList outputList, orderList;          /* output and layer+fanin node
206                                          * list fed to the ordering procedure
207                                          */
208  lsHandle nodeHandle;                   /* handle for node list */ 
209  int *invPermArray;                     /* inverse permutation array
210                                          * for the Dd manager
211                                          */
212  array_t *newIdArray;                   /* array with new Ids to be
213                                          * assigned to each node
214                                          */
215  Ntk_Node_t *nodePtr;                   /* variable to store node pointer */
216  array_t *currentLayer;                 /* current layer of nodes */
217  int numNodes;                          /* number of nodes in current layer */
218  bdd_node **functionArray;              /* array of Adds of the current nodes
219                                          * in terms of their fanin
220                                          */
221                                         
222  bdd_node *functionBdd;                 /* Bdds of current layer nodes */
223  char *flagValue;                       /* string that stores flag values */
224  int verbose;                           /* verbosity level */
225  int j, k;                              /* iterators */
226  int layerIndex, nodeIndex;             /* iterators */
227  long tempTime, thisComposeTime;        /* local time measurement variables */
228  long thisSmartVarTime, thisOrderTime;  /* local time measurement variables */
229  long thisShuffleTime;                  /* local time measurement variables */
230  int unassignedValue;                   /* NTK_UNASSIGNED_MDD_ID value holder */
231 
232  /* initialize local time measurement variables */
233  tempTime = 0;
234  thisSmartVarTime = 0;
235  thisOrderTime = 0;
236  thisShuffleTime = 0;
237  thisComposeTime = 0;
238  unassignedValue =  NTK_UNASSIGNED_MDD_ID;
239 
240  /* make a local copy of the residue Dd to compose the network into */
241  bdd_ref(currentDd = residueDd);
242 
243  /* read verbosity flag */
244  verbose = 0;
245  flagValue = Cmd_FlagReadByName("residue_verbosity");
246  if (flagValue != NIL(char)) {
247    verbose = atoi(flagValue);
248  }
249 
250  ddManager = (bdd_manager *)Ntk_NetworkReadMddManager(network);
251  /* initialize the variable manager that keeps track of what variables
252   * are in use in residue verification.
253   */
254  ResResidueInitializeVariableManager(bdd_num_vars(ddManager));
255 
256  /* assume the pos are labeled before they come here each time */
257  outputList = lsCreate();
258
259  /* outputs do not need to be ordered as the node ids are already
260   * assigned. Here this list is created just so that the variable
261   * manager can be updated
262   */
263
264  arrayForEachItem(Ntk_Node_t *, outputArray, j, nodePtr) {
265    lsNewEnd(outputList, (lsGeneric)nodePtr, (lsHandle *)&nodeHandle);
266  }
267 
268  newIdArray = array_alloc(int, 0);
269  tempTime = util_cpu_time();
270  /* update the variable manager with the output node ids */
271  invPermArray = ResResidueVarAllocate(ddManager, outputList, newIdArray);
272  if (invPermArray == NIL(int)) {
273    error_append("Unable to update variable manager\n");
274    array_free(newIdArray);
275    ResResidueFreeVariableManager();
276    return NULL;
277  } /* end of error */
278  thisSmartVarTime += util_cpu_time() - tempTime;
279  FREE(invPermArray);
280  array_free(newIdArray);
281  lsDestroy(outputList, (void (*)(lsGeneric))0);
282
283  /* start the main loop for composition of layers into the residue Add */
284  for(layerIndex = 0; layerIndex < array_n(layerArray); layerIndex++) {
285    /* fetch each layer */
286    currentLayer = ResLayerFetchIthLayer(layerArray, layerIndex);
287    numNodes = ResLayerNumNodes(currentLayer);
288    if (verbose >= 3) {
289      fprintf(vis_stdout, "Layer %d being composed", layerIndex);
290      fprintf(vis_stdout, " with %d nodes\n", numNodes);
291    }
292
293    /* create the order of the nodes in the layer and their fanin
294     * for composition
295     */
296    tempTime = util_cpu_time();
297    orderList = CreateNodeAndFaninOrderList(currentLayer);
298    thisOrderTime +=  util_cpu_time() - tempTime;
299
300    /* assign new Ids if required and create the corresponding variables
301     * in the manager
302     */
303    newIdArray = array_alloc(int, 0);
304    tempTime = util_cpu_time();
305    invPermArray = ResResidueVarAllocate(ddManager, orderList, newIdArray);
306    if (invPermArray == NIL(int)) {
307      error_append("Unable to update variable manager\n");
308      bdd_recursive_deref(ddManager, currentDd);
309      array_free(newIdArray);
310      ResResidueFreeVariableManager();
311      return NULL;
312    } /* end of error */
313    thisSmartVarTime += util_cpu_time() - tempTime;
314
315    /* assign Ids to unassigned fanin nodes */
316    if (array_n(newIdArray)) {
317      UpdateUnassignedNodesWithNewIds(orderList, newIdArray);
318    }
319    array_free(newIdArray);
320    lsDestroy(orderList, (void (*)(lsGeneric))0);
321   
322    /* shuffle the IDs */
323    tempTime = util_cpu_time();
324    (void) bdd_shuffle_heap(ddManager, invPermArray);
325    thisShuffleTime += util_cpu_time() - tempTime;
326    FREE(invPermArray);
327   
328    /* array initialized for dd nodes of the current layer */
329    tempTime = util_cpu_time();
330    functionArray = ALLOC(bdd_node *, numNodes);
331    LayerForEachNode(currentLayer, nodeIndex, nodePtr) {
332
333      /* build the BDD for the function of each node */
334      functionBdd = BuildBDDforNode(network, nodePtr, IMMEDIATE_FANIN);
335      if (functionBdd == NULL) { /* error */
336        error_append("Unable to build function for node ");
337        error_append(Ntk_NodeReadName(nodePtr));
338        error_append("\n");
339        for (k = 0; k < nodeIndex; k++) {
340          bdd_recursive_deref(ddManager, functionArray[k]);
341        }
342        FREE(functionArray);
343        bdd_recursive_deref(ddManager, currentDd);
344        ResResidueFreeVariableManager();
345        return NULL;
346      } /* end of error */
347
348      /* Convert to ADD */
349      bdd_ref(functionArray[nodeIndex] = bdd_bdd_to_add(ddManager, functionBdd));
350      bdd_recursive_deref(ddManager, functionBdd);
351      if (functionArray[nodeIndex] == NULL) { /* error */
352        error_append("Unable to build add from bdd for node ");
353        error_append(Ntk_NodeReadName(nodePtr));
354        error_append("\n");
355        for (k = 0; k < nodeIndex; k++) {
356          bdd_recursive_deref(ddManager, functionArray[k]);
357        }
358        FREE(functionArray);
359        bdd_recursive_deref(ddManager, currentDd);
360        ResResidueFreeVariableManager();
361        return NULL;
362      } /* end of error */
363    } /* end of iterating over each node in a layer */
364    /* compose the array into the residue ADD */
365
366    /* Perform the actual composition of current layer */
367    tempTime = util_cpu_time();
368    newResidueDd = ComposeLayer(ddManager, currentDd,  currentLayer, functionArray);
369    thisComposeTime += util_cpu_time() - tempTime;
370    /* free old residue Dd */
371    bdd_recursive_deref(ddManager, currentDd);
372    if (newResidueDd == NULL) { /* error */
373      error_append("Unable to do composition for layer\n");
374      for (k = 0; k < numNodes; k++) {
375        bdd_recursive_deref(ddManager, functionArray[k]);
376      }
377      FREE(functionArray);
378      ResResidueFreeVariableManager();
379      return NULL;
380    } /* end of error */
381    currentDd = newResidueDd;
382    if (verbose >= 3) {
383      mdd_t *fnMddT;
384      int size;
385      bdd_ref(currentDd);
386      fnMddT = bdd_construct_bdd_t(ddManager, currentDd);
387      size = bdd_size(fnMddT);
388      bdd_free(fnMddT);
389      fprintf(vis_stdout, "Layer %d has %d nodes\n", layerIndex,
390              size);
391    }
392   
393    /* free function array */
394    for (j = 0; j < numNodes; j++) {
395      bdd_recursive_deref(ddManager, functionArray[j]);
396    }
397    FREE(functionArray);
398   
399    /*  free ids of nodes just composed */
400    ResResidueVarDeallocate(currentLayer);
401    /* reset node Ids of the composed layer */
402    LayerForEachNode(currentLayer, j, nodePtr) {
403      if (!Ntk_NodeTestIsCombInput(nodePtr)) {
404        Ntk_NodeSetMddId(nodePtr, unassignedValue);
405      }
406    }
407  } /* end of iterating over the layers */
408
409  /* free the variable manager */
410  ResResidueFreeVariableManager();
411  if (verbose >= 1) {
412    (void) fprintf(vis_stdout, "ADD Compose Time = %.3f\n",(thisComposeTime)/1000.0);
413    (void) fprintf(vis_stdout, "Smart variable allocation time = %.3f\n", (thisSmartVarTime)/1000.0);
414    (void) fprintf(vis_stdout, "Shuffle time = %.3f\n", (thisShuffleTime)/1000.0);
415    (void) fprintf(vis_stdout, "Order time = %.3f\n", (thisOrderTime)/1000.0);
416  }
417  /* update global time variables */
418  Res_composeTime += thisComposeTime;
419  Res_smartVarTime += thisSmartVarTime;
420  Res_shuffleTime += thisShuffleTime;
421  Res_orderTime += thisOrderTime;
422
423  /* return the composed residue Dd in terms of the primary inputs */
424  return(newResidueDd);
425 
426} /* End of ComposeLayersIntoResidue */
427
428/*---------------------------------------------------------------------------*/
429/* Definition of static functions                                            */
430/*---------------------------------------------------------------------------*/
431
432/**Function********************************************************************
433
434  Synopsis  [Updates unassigned nodes in list with mdd ids in the array.]
435
436  Description [Updates unassigned nodes in list with mdd ids in the array. The
437  procedure steps through all nodes in a list and assigns them an id from the
438  array. The parameters to this procedure are the list of nodes, some of which
439  may not have assigned IDs and the array containing new Ids ready to be
440  assigned to the nodes.]
441 
442  SideEffects   []
443
444  SeeAlso            [ComposeLayersIntoResidue]
445
446******************************************************************************/
447static void
448UpdateUnassignedNodesWithNewIds(lsList orderList,   
449                                array_t *newIdArray) 
450{
451  int i, id;
452  lsGen listGen;
453  Ntk_Node_t *nodePtr;
454  char *flagValue;
455  int verbose;
456 
457  verbose = 0;
458  flagValue = Cmd_FlagReadByName("residue_verbosity");
459  if (flagValue != NIL(char)) {
460    verbose = atoi(flagValue);
461  }
462
463  /* step through each item in the list to find nodes with unassigned Ids */
464  i = 0;
465  lsForEachItem(orderList, listGen, nodePtr) {
466    if (Ntk_NodeReadMddId(nodePtr) == NTK_UNASSIGNED_MDD_ID) {
467      id = array_fetch(int, newIdArray, i);
468      Ntk_NodeSetMddId(nodePtr, id);
469      i++;
470      if (verbose >= 4) {
471        fprintf(vis_stdout, "Id %d being assigned to node %s\n", id,
472                Ntk_NodeReadName(nodePtr));
473      }
474    }
475  }
476  assert(i == array_n(newIdArray));
477  return;
478} /* End of UpdateUnassignedNodesWithNewIds */
479
480
481/**Function********************************************************************
482
483  Synopsis  [Creates a list of the nodes of layer and the fanin nodes
484  of the layer.]
485
486  Description [Creates a list of the nodes of a layer and the order in which
487  they should appear in the dd manager for the composition process.  The main
488  idea is to be as efficient in composition as possible. This requires nodes
489  with overlapping support to be together, nodes being above their fanins in
490  the dd order (to perform fewer ITE calls) and nodes being composed in at the
491  top of the DD. This requires shuffling of the nodes in the layer to the top
492  and their fanins below them.  Shuffling is done by sifting and is an
493  expensive operation. Hence the motivation to keep the shuffles to as few as
494  possible. So we start with layer where the nodes are sorted according to
495  their level in the dd manager. It is a greedy heuristic that tries to
496  minimize the sifting.  Next the nodes with overlapping support are brought
497  together. Finally the fanin Nodes are sorted according to their levels too
498  and inserted below the last (in the order) node of their fanout. The
499  procedure returns the final sorted list of the nodes in the layer and their
500  fanin. Note: It is assumed that the current layer has Ids assigned to
501  it. This implies that the Primary outputs need special assignment of Ids and
502  every other node automatically gets assigned Ids since they appear in the
503  transitive fanin of some output. The function takes as an argument the layer
504  to be ordered.]
505 
506  SideEffects   []
507
508  SeeAlso            [ComposeLayersIntoResidue]
509
510******************************************************************************/
511static lsList
512CreateNodeAndFaninOrderList(array_t *currentLayer) 
513{
514  st_table *faninTable;       /* table to store fanin */
515  lsList layerList;           /* list of nodes in layer */
516  lsList faninVarSetList;     /* list of support corresponding to layer
517                               * nodes.
518                               */
519  lsList newList;             /* ordered list of nodes and fanins */
520  lsGen listGen;              /* generator to step through list */
521  lsGen layerGen, faninGen;   /* generators to step through lists */
522  int totalFanins;/* variable to store total number of fanins
523                               * of this layer
524                               */
525  int intersect;              /* number of elements in the intersection
526                               * of support.
527                               */
528  int i, j, faninIndex;       /* iterators */
529  Ntk_Node_t *nodePtr;        /* node pointer variables */
530  Ntk_Node_t *faninNodePtr;   /* node pointer variables */
531  Ntk_Node_t *nextNodePtr;    /* node pointer variables */
532  lsHandle nodeHandle;        /* handle for ls procedure */
533  lsHandle varSetHandle;      /* handle for ls procedure */
534  lsHandle newNodeHandle;     /* handle for ls procedure */
535  lsHandle maxIntersectNodeHandle;   /* handle for ls procedure */
536  lsHandle maxIntersectVarSetHandle; /* handle for ls procedure */
537  var_set_t *currVarSet;      /* support of current node */
538  var_set_t *varSetIntersect; /* intersection of support between 2 nodes */
539  var_set_t *nextVarSet;      /* support of next node */
540  array_t *faninArray;        /* array of fanin of a node read from network */
541  lsList faninList;           /* list of fanins of current layer */
542  int nodeIndex;              /* iterator */
543  int verbose;                /* verbosity level */
544  char *flagValue;            /* string to read flag value */
545 
546  verbose = 0;
547  flagValue = Cmd_FlagReadByName("residue_verbosity");
548  if (flagValue != NIL(char)) {
549    verbose = atoi(flagValue);
550  }
551
552  /* sort current layer by position in the dd manager for least number
553   * of shuffles
554   */
555  LayerSort(currentLayer, IdCompare);
556  /* create a list to be able to order the list and later manipulation */
557  layerList = lsCreate();
558  if (verbose >= 4) {
559    fprintf(vis_stdout, "Nodes in this layer are: ");
560  }
561  LayerForEachNode(currentLayer, i, nodePtr) {
562    lsNewEnd(layerList, (lsGeneric)nodePtr, (lsHandle *)&nodeHandle);
563    if (verbose >= 4) {
564      fprintf(vis_stdout, "%s ",Ntk_NodeReadName(nodePtr));
565    }
566  }
567  if (verbose >= 4) {
568    fprintf(vis_stdout, "\n");
569  }
570
571  /* insert all fanins in a table with a unique index. This is to identify
572   * each fanin as a support variable
573   */
574  faninIndex = 0;
575  faninTable = st_init_table(st_ptrcmp, st_ptrhash);
576
577  LayerForEachNode(currentLayer, nodeIndex, nodePtr) {
578    Ntk_NodeForEachFanin(nodePtr, j, faninNodePtr) {
579      /* here constants are omitted, so that they are not assigned an
580       * Id. The other case to be avoided is when the node in consideration
581       * is a latch output i.e. a combinational input. Hence it is not
582       * desirable that the latch data input and latch initial input
583       * be considered as its fanin.
584       */
585      if ((!st_is_member(faninTable, (char *)faninNodePtr)) &&
586        (!(Ntk_NodeTestIsConstant(faninNodePtr) ||
587        (Ntk_NodeTestIsLatch(nodePtr) &&
588         (Ntk_NodeTestIsLatchDataInput(faninNodePtr) ||
589          Ntk_NodeTestIsLatchInitialInput(faninNodePtr)))))) {
590        st_insert(faninTable, (char *)faninNodePtr,
591                  (char *)(long)faninIndex);
592        faninIndex++;
593      }
594    }
595  }
596  /* keep a count of the total number of fanins to this layer */
597  totalFanins = faninIndex;
598 
599  /* Create fanin var set for each node */
600  faninVarSetList = CreateFaninVarSetList(currentLayer, faninTable);
601  st_free_table(faninTable);
602
603  /* Main sorting part: Like Insertion Sort*/
604  /* initialize to first item from both layer and fanin lists */
605  /* starting here, find the list element in the list with max overlap
606   * with this element. Here each node in the layer is brought up
607   * neighbor
608   */
609  (void) lsFirstItem(faninVarSetList, &currVarSet, &varSetHandle);
610  (void) lsFirstItem(layerList, &nodePtr, &nodeHandle);
611  (void) lsRemoveItem(nodeHandle, &nodePtr);
612  (void) lsRemoveItem(varSetHandle, &currVarSet);
613 
614  /* insert first item in new list */
615  newList = lsCreate();
616  lsNewEnd(newList, (lsGeneric)nodePtr, (lsHandle *)&newNodeHandle);
617 
618  /* create var set for checking overlap of support */
619  varSetIntersect = var_set_new(totalFanins);
620  /* done when all the nodes in the layerList have been transferred
621   * to new list. In each iteration of this list, the node with max
622   * support overlap with the current node is taken out of the list
623   * and added to the new list. Its corresponding var set is also
624   * removed, the current var set is freed and the new var set is
625   * set to the current var set. The var set list has to be manipulated
626   * simultaneously to keep the correspondence between the node list
627   * and its support list.
628   */
629  while(lsLength(newList) != ResLayerNumNodes(currentLayer)) { /* while not done */
630    /* create generators to step through list */
631    faninGen = lsStart(faninVarSetList);
632    layerGen = lsStart(layerList);
633    /* initialize */
634    intersect = 0;
635    maxIntersectNodeHandle = NULL;
636    maxIntersectVarSetHandle = NULL;
637    while (lsNext(layerGen, &nextNodePtr, &nodeHandle) != LS_NOMORE) {
638      /* clear result var set */
639      var_set_clear(varSetIntersect);
640      /* position var set corresponding to node in layer list */
641      lsNext(faninGen, &nextVarSet, &varSetHandle);
642      /* get support overlap */
643      varSetIntersect = var_set_and(varSetIntersect, currVarSet, nextVarSet);
644      /* check if current overlap is larger than current max */
645      if (var_set_n_elts(varSetIntersect) > intersect) {
646        /* record current position */
647        intersect = var_set_n_elts(varSetIntersect);
648        maxIntersectNodeHandle = nodeHandle;
649        maxIntersectVarSetHandle = varSetHandle;
650      }
651    } /* end of iterating over layer list */
652
653    /* destroy Generator */
654    (void) lsFinish(layerGen);
655    (void) lsFinish(faninGen);
656    /* free current var set */
657    var_set_free(currVarSet);
658    /* process differently if there was overlap and if there wasn't */
659    if (maxIntersectNodeHandle == NULL) {
660      /* support overlap was zero with the rest of the nodes */
661      /* set current item to first in the lists */
662      (void) lsFirstItem(faninVarSetList, &nextVarSet, &maxIntersectVarSetHandle);
663      (void) lsFirstItem(layerList, &nextNodePtr, &maxIntersectNodeHandle);
664    }
665   
666    /* remove max support overlap item from the lists */
667    (void) lsRemoveItem(maxIntersectNodeHandle, &nextNodePtr);
668    (void) lsRemoveItem(maxIntersectVarSetHandle, &nextVarSet);
669   
670    /* add node to the new list */
671    lsNewEnd(newList, (lsGeneric)nextNodePtr, (lsHandle *)&newNodeHandle);
672    /* move current item to the new item */
673    currVarSet = nextVarSet;
674
675  }
676  /* Clean up */
677  var_set_free(varSetIntersect);
678  var_set_free(currVarSet);
679  lsDestroy(faninVarSetList, (void (*)(lsGeneric))0);
680  lsDestroy(layerList, (void (*)(lsGeneric))0);
681  /* end of sorting part */
682 
683  /* insert nodes in new order in the current layer */
684  i = 0;
685  lsForEachItem(newList, listGen, nodePtr) {
686    LayerAddNodeAtIthPosition(currentLayer, i, nodePtr);
687    i++;
688  }
689  assert(lsLength(newList) == array_n(currentLayer));
690
691  /* keep track of running update of the fanins included */
692  faninTable = st_init_table(st_ptrcmp, st_ptrhash);
693  /* insert fanin nodes after the last node in the order */
694  nodeIndex = ResLayerNumNodes(currentLayer)-1;
695  /* while nodes exist that have to be processed and all fanins haven't
696   * been processed, repeat
697   */
698  while ((nodeIndex >= 0) || (st_count(faninTable) != totalFanins)) {
699    nodePtr = LayerFetchIthNode(currentLayer, nodeIndex);
700    faninArray = Ntk_NodeReadFanins(nodePtr);
701    /* create a fanin list to append to the nodeList */
702    faninList = lsCreate();
703    arrayForEachItem(Ntk_Node_t *, faninArray, i, faninNodePtr) {
704      /* only include those fanins that haven't appeared yet. Also
705       * exclude the cases where the node is a constant and it is
706       * a latch data/initial input. You don't want to compose a
707       * latch output i.e. a combinational input with the latch input.
708       */
709      if ((!st_is_member(faninTable, (char *)faninNodePtr)) &&
710          (!(Ntk_NodeTestIsConstant(faninNodePtr) ||
711             (Ntk_NodeTestIsLatch(nodePtr) &&
712              (Ntk_NodeTestIsLatchDataInput(faninNodePtr) ||
713               Ntk_NodeTestIsLatchInitialInput(faninNodePtr)))))) {
714        lsNewEnd(faninList, (lsGeneric)faninNodePtr, (lsHandle *)&nodeHandle);
715        st_insert(faninTable, (char *)faninNodePtr, NIL(char));
716        /* done when all fanins have been processed */
717        if (st_count(faninTable) == totalFanins) break;
718      }
719    }
720    /* if list is not empty add fanin behind the node */
721    if (lsLength(faninList)) { 
722      /* sort fanins by their level in the ddmanager */
723      lsSort(faninList, IdListCompare);
724      /* append the fanin list to the node list */
725      newList = ListAppend(nodePtr, newList, faninList);
726    }
727    lsDestroy(faninList, (void (*)(lsGeneric))0);
728    nodeIndex--;
729
730  } /* end of while fanin nodes need to be processed and nodes
731     * are present in layer */
732  st_free_table(faninTable);
733  assert(lsLength(newList) == (array_n(currentLayer) + totalFanins));
734
735  return(newList);
736} /* End of CreateNodeAndFaninOrderList */
737
738
739/**Function********************************************************************
740
741  Synopsis  [Procedure to add fanin nodes below a particular node.]
742
743  Description [ Procedure to add fanin nodes below a particular node.  Finds
744  the node in the list after which fanin list is to be added.  Adds nodes in
745  the fanin list to the new list. This procedure takes as arguments the nodePtr
746  after which the fanins are to be inserted, the collated list where the fanins
747  should be inserted and a list of fanins. The updated list is returned.]
748
749  SideEffects   [New list is added to.]
750
751  SeeAlso            [CreateNodeAndFaninOrderList]
752
753******************************************************************************/
754static lsList
755ListAppend(Ntk_Node_t *nodePtr, 
756           lsList newList,     
757           lsList faninList)   
758{
759  lsGen layerGen, newGen, faninGen;
760  Ntk_Node_t *currNodePtr, *faninNodePtr;
761  lsHandle nodeHandle, faninNodeHandle;
762  lsStatus status;
763 
764  layerGen = lsEnd(newList);
765  /* find the spot to insert fanin List */
766  while(lsPrev(layerGen, &currNodePtr, &nodeHandle) != LS_NOMORE) {
767    if (nodePtr == currNodePtr) {
768      /* when spot found, insert fanin list */
769      newGen = lsGenHandle(nodeHandle, &currNodePtr, LS_AFTER);
770      lsForEachItem(faninList, faninGen, faninNodePtr) {
771        status = lsInAfter(newGen, (lsGeneric)faninNodePtr, (lsHandle *)&faninNodeHandle);
772        if (status != LS_OK) {
773          error_append("Something wrong with fanin list to be appended\n");
774          status = lsFinish(layerGen);
775          status = lsFinish(newGen);
776          status = lsFinish(faninGen);
777          return NULL;
778        }
779      } /* end of iterating through the fanin list */
780      /* done as fanin list has been inserted */
781      lsFinish(newGen);
782      break;
783    } /* end of if node found  in the list */
784  } /* end of stepping through the new list */
785 
786  /* Clean up generators */
787  lsFinish(layerGen);
788 
789  /* return modified list */
790  return (newList);
791}/* End of ListAppend */
792   
793
794/**Function********************************************************************
795
796  Synopsis  [ Compares the Ids of 2 nodes.]
797
798  Description [Compares the Ids of 2 nodes. It is a procedure fed to array
799  sort.]
800 
801  SideEffects   []
802
803  SeeAlso            [CreateNodeAndFaninOrderList]
804
805******************************************************************************/
806static int
807IdCompare(const void *obj1,
808          const void *obj2)
809{
810  Ntk_Node_t *nodePtr1, *nodePtr2;
811  int id1 , id2;
812  int level1, level2;
813  Ntk_Network_t *network;
814  bdd_manager *ddManager;
815 
816  nodePtr1 = *(Ntk_Node_t **)obj1;
817  nodePtr2 = *(Ntk_Node_t **)obj2;
818  id1 = Ntk_NodeReadMddId((Ntk_Node_t *)nodePtr1);
819  id2 = Ntk_NodeReadMddId((Ntk_Node_t *)nodePtr2);
820  /* if unassigned Ids return the value before reading the
821   * position . If equal return -1.
822   */
823  if ((id1 == NTK_UNASSIGNED_MDD_ID) || (id2 == NTK_UNASSIGNED_MDD_ID)) {
824    if (id1 == NTK_UNASSIGNED_MDD_ID) {
825      return -1;
826    } else {
827      return 1;
828    }
829  }
830
831  network = Ntk_NodeReadNetwork(nodePtr1);
832  ddManager = (bdd_manager *)Ntk_NetworkReadMddManager(network);
833  level1 = bdd_get_level_from_id(ddManager, id1);
834  level2 = bdd_get_level_from_id(ddManager, id2);
835  if (level1 > level2) {
836    return 1;
837  } else if (level1 == level2) {
838    return 0;
839  } else {
840    return -1;
841  }
842} /* End of IdCompare */
843
844/**Function********************************************************************
845
846  Synopsis  [Compares the Ids of 2 nodes.]
847
848  Description [Compares the Ids of 2 nodes. it is fed to s list sort routine. ]
849 
850  SideEffects   []
851
852  SeeAlso            [CreateNodeAndFaninOrderList]
853
854******************************************************************************/
855static int
856IdListCompare(lsGeneric item1,
857              lsGeneric item2)
858{
859  Ntk_Node_t *nodePtr1, *nodePtr2;
860  int id1 , id2;
861  int level1, level2;
862  Ntk_Network_t *network;
863  bdd_manager *ddManager;
864
865 
866  nodePtr1 = (Ntk_Node_t *)item1;
867  nodePtr2 = (Ntk_Node_t *)item2;
868  id1 = Ntk_NodeReadMddId((Ntk_Node_t *)nodePtr1);
869  id2 = Ntk_NodeReadMddId((Ntk_Node_t *)nodePtr2);
870  /* if unassigned Ids return the value before reading the
871   * position . If equal return -1.
872   */
873  if ((id1 == NTK_UNASSIGNED_MDD_ID) || (id2 == NTK_UNASSIGNED_MDD_ID)) {
874    if (id1 == NTK_UNASSIGNED_MDD_ID) {
875      return -1;
876    } else {
877      return 1;
878    }
879  }
880  network = Ntk_NodeReadNetwork(nodePtr1);
881  ddManager = (bdd_manager *)Ntk_NetworkReadMddManager(network);
882  level1 = bdd_get_level_from_id(ddManager, id1);
883  level2 = bdd_get_level_from_id(ddManager, id2);
884  if (level1 > level2) {
885    return 1;
886  } else if (level1 == level2) {
887    return 0;
888  } else {
889    return -1;
890  }
891} /* End of IdListCompare */
892
893
894/**Function********************************************************************
895
896  Synopsis  [Creates a list of var set of support for each node in layer.]
897
898  Description [ Creates a list of var set of support for each node in layer.
899  For each node in the layer, create a var set of support based on the fanin
900  index stored in the fanin table. Returns a list of var sets. Takes as
901  arguments the current layer whose support sets need to be formed and a table
902  with the fanin and their unique IDs.]
903 
904  SideEffects   []
905
906  SeeAlso            [CreateNodeAndFaninOrderList]
907
908******************************************************************************/
909static lsList
910CreateFaninVarSetList(array_t *currentLayer, 
911                      st_table *faninTable) 
912{
913  Ntk_Node_t *nodePtr, *faninNodePtr;  /* variables to store nodes */
914  array_t *faninArray;                 /* array of fanin of nodes */
915  lsList faninVarSetList;              /* list of var set representing
916                                        * support of nodes in layer
917                                        */
918  var_set_t *currVarSet;               /* var set indicating current
919                                        * node support
920                                        */
921  lsHandle varSetHandle;               /* handle for ls procedure */
922  int totalFanins;                     /* total number of fanins of this
923                                        * layer.
924                                        */
925  int i, j, faninIndex;                /* iterators */
926
927
928 
929  totalFanins = (int)st_count(faninTable);
930  faninVarSetList = lsCreate();
931  /* create var-set of support for each node in this layer */
932  arrayForEachItem(Ntk_Node_t *, currentLayer, i, nodePtr) {
933    faninArray = Ntk_NodeReadFanins(nodePtr);
934    currVarSet = var_set_new(totalFanins);
935    /* if the above node is a constant, the var set will be empty
936     * also if it a latch output(comb. input), then the var set will
937     * be empty.
938     */
939    arrayForEachItem(Ntk_Node_t *, faninArray, j, faninNodePtr) {
940      /* process only those fanins in the table, i.e. no constants
941       * no latch inputs (combinational outputs) are fanins to this array
942       */
943      if (st_lookup_int(faninTable, (char *)faninNodePtr, &faninIndex)) {
944        /* these aren't supposed to be here */
945        assert(!((Ntk_NodeTestIsConstant(faninNodePtr) ||
946                  (Ntk_NodeTestIsLatch(nodePtr) &&
947                   (Ntk_NodeTestIsLatchDataInput(faninNodePtr) ||
948                    Ntk_NodeTestIsLatchInitialInput(faninNodePtr))))));
949        /* set the bit in the support according to the index the fanin
950         * was assigned
951         */
952        var_set_set_elt(currVarSet, faninIndex);
953      } /* end of if is in the fanin table (has no constants and no
954         * latch data or initial input.
955         */
956    } /* end of if present in fanin table */
957    /* insert var set in fanin var set list */
958    lsNewEnd(faninVarSetList, (lsGeneric)currVarSet, (lsHandle *)&varSetHandle);
959  }
960  return (faninVarSetList);
961} /* End of CreateFaninVarSetList */
962
963/**Function********************************************************************
964
965  Synopsis [Procedure that does the actual composition of a layer into the
966  residue add.]
967
968  Description [ Procedure that does the actual composition of a layer into the
969  residue add depending on the method specified. Note for vector composition,
970  this procedure assumes that currentLayer is sorted according to the levels
971  and according to common support. This is done in
972  CreateNodeAndFaninOrderList. The procedure takes as arguments the DD manager,
973  the residue DD, the current layer that needs to be composed in and the array
974  of the function BDDs of the nodes to be composed in (in 1-to-1 correspondence
975  with the current layer. The procedure returns the composed Dd.]
976 
977  SideEffects   []
978
979  SeeAlso            [ComposeLayersIntoResidue]
980
981******************************************************************************/
982static bdd_node *
983ComposeLayer(bdd_manager *ddManager,   
984             bdd_node *residueDd,       
985             array_t *currentLayer,   
986             bdd_node **functionArray) 
987{
988  Ntk_Node_t *nodePtr;          /* variable to store nodes */
989  char *flagValue;              /* string to read flag value */
990  ResCompositionMethod method;  /* type of composition to be performed */
991  int i, j, layerIndex;                     /* iterators */
992  int nodeId;                   /* current node id */
993  bdd_node **composeVector;       /* vector required for composition */
994  bdd_node *new_ = NIL(bdd_node), *andDd,*yDd, *nodeReln, *currentDd; /* temporary Dds */
995  int maxLayerSize;             /* max size of layers */
996  int first, last;              /* first and last positions of the array */
997 
998  /* read the type of composition to be performed, default is vector
999   * composition.
1000   */
1001  flagValue = Cmd_FlagReadByName("residue_composition_method");
1002  if (flagValue == NIL(char)) {
1003    method = ResDefaultComposeMethod_c;
1004  } else if (strcmp(flagValue, "vector") == 0) {
1005      method = ResVector_c;
1006  } else if (strcmp(flagValue, "onegate") == 0) {
1007    method =  ResOneGateAtATime_c;
1008  } else if (strcmp(flagValue, "preimage") == 0) {
1009    method = ResPreimageComputation_c;
1010  } else if (strcmp(flagValue, "superG") == 0) {
1011    method = ResSuperG_c;
1012  } else {
1013    fprintf(vis_stderr, 
1014            "** res warning: Unknown composition method, %s, resorting to default.\n", 
1015            flagValue);
1016    method = ResDefaultComposeMethod_c;
1017  } 
1018
1019  switch(method) {
1020
1021  case ResVector_c:
1022  case ResSuperG_c:
1023    {
1024      /* read the flag for maximum value of layer size */
1025      flagValue = Cmd_FlagReadByName("residue_layer_size");
1026      if (flagValue == NIL(char)) {
1027        maxLayerSize = ResLayerNumNodes(currentLayer); 
1028      } else {
1029        maxLayerSize = atoi(flagValue);
1030      }
1031      /* if max layer size is within 5 nodes of the length of the
1032       * size of the array, resize it to the size of the array
1033       */
1034      if (maxLayerSize + 5 >= ResLayerNumNodes(currentLayer)) {
1035        maxLayerSize = ResLayerNumNodes(currentLayer);
1036      }
1037
1038      /* initialize a vector with projection functions */
1039      composeVector = ALLOC(bdd_node *, bdd_num_vars(ddManager));
1040      for(i = 0; (unsigned) i < bdd_num_vars(ddManager); i++) {
1041        bdd_ref(composeVector[i] = bdd_add_ith_var(ddManager, i));
1042        if (composeVector[i] == NIL(bdd_node)) { /* error */
1043          error_append("Something wrong in obtaining projection functions");
1044          for(j = 0; j < i; j++) {
1045            bdd_recursive_deref(ddManager, composeVector[j]);
1046          }
1047          return NIL(bdd_node);
1048        } /* end of if error */
1049      }
1050      /* break this layer up into sub-layers to ease composition
1051       * process. Hence the composition will be performed for several
1052       * subarrays.
1053       */
1054      /* start at the end of the layer */
1055      layerIndex = ResLayerNumNodes(currentLayer);
1056      /* make a local copy */
1057      bdd_ref(currentDd = residueDd);
1058      do {
1059        /* extract sublayers in the size of maxLayerSize starting from the
1060         * end of the layer or a smaller sub-layer (leftover) in the end
1061         */
1062
1063        /* record last+1 position of the sub-layer in the current layer */
1064        last = layerIndex;
1065
1066        /* record the position of the beginning of this sub-layer */ 
1067        first = (last < maxLayerSize) ? 0 : (last - maxLayerSize);
1068
1069        /* iterate through the layer to find the sublayer */
1070        while(layerIndex  > first) { /* extract sub-layer */
1071          layerIndex--;
1072          nodePtr = LayerFetchIthNode(currentLayer, layerIndex);
1073          nodeId = Ntk_NodeReadMddId(nodePtr);
1074          bdd_recursive_deref(ddManager, composeVector[nodeId]);
1075          /* plug in the functions of the nodes in the layer instead of
1076           * the projection functions
1077           */
1078          bdd_ref(composeVector[nodeId] = functionArray[layerIndex]);
1079        }
1080
1081        /* perform composition */
1082        if (method == ResVector_c) {
1083          bdd_ref(new_ = bdd_add_vector_compose(ddManager, currentDd, composeVector));
1084        } else {
1085          bdd_ref(new_ = bdd_add_nonsim_compose(ddManager, currentDd, composeVector));
1086        }
1087
1088        /* free old copy and use new to compose in the next sub-layer, if any */
1089        bdd_recursive_deref(ddManager, currentDd);
1090        currentDd = new_;
1091       
1092        if (new_ == NULL) { /* error */
1093          error_append("NULL Dd returned on vector or superG compose\n");
1094          break;
1095        } /* end of error */
1096
1097        /* undo the compose vector changes for this sub-array to
1098         * prepare it for the next subarray. Replace the function of
1099         * nodes with the projection functions
1100         */
1101        for (i = first; i < last; i++) {
1102          nodePtr = LayerFetchIthNode(currentLayer, i);
1103          nodeId = Ntk_NodeReadMddId(nodePtr);
1104          bdd_recursive_deref(ddManager, composeVector[nodeId]);
1105          bdd_ref(composeVector[nodeId] = bdd_add_ith_var(ddManager, nodeId));
1106        }
1107      } while(layerIndex  > 0);
1108
1109      /* clean up */
1110      for(i = 0; (unsigned) i < bdd_num_vars(ddManager); i++) {
1111        bdd_recursive_deref(ddManager, composeVector[i]);
1112      }
1113      FREE(composeVector);
1114      break;
1115    } /* end of cases: ResVector_c, ResSuperG_c */
1116  case ResOneGateAtATime_c:
1117    {
1118      /* duplicate  as current Dd gets freed later */
1119      bdd_ref(currentDd = residueDd);
1120      /* compose the nodes in one at a time */
1121      LayerForEachNode(currentLayer, i, nodePtr) {
1122        nodeId = Ntk_NodeReadMddId(nodePtr);
1123        bdd_ref(new_ = bdd_add_compose(ddManager, currentDd, functionArray[i],
1124                                       nodeId));
1125        bdd_recursive_deref(ddManager, currentDd);
1126        if (new_ == NULL) { /* error */
1127          error_append("NULL Dd returned on single gate compose, node: ");
1128          error_append(Ntk_NodeReadName(nodePtr));
1129          error_append("\n");
1130          return NULL;
1131        } /* end of error */
1132        currentDd = new_;
1133      }
1134      break;
1135    } /* end of case Res_OneGateAtATime_c */
1136  case ResPreimageComputation_c:
1137    {
1138      /* duplicate  as current Dd gets freed later */
1139      bdd_ref(currentDd = residueDd);
1140      /* form the y_i \equiv f_i(x) relation, this would be wrong
1141       * if the node appeared again in the circuit. But here it is
1142       * correct due to the one time rule
1143       */
1144      LayerForEachNode(currentLayer, i, nodePtr) {
1145        nodeId = Ntk_NodeReadMddId(nodePtr);
1146        /* find the var for this node */
1147        bdd_ref(yDd = bdd_add_ith_var(ddManager, nodeId));
1148        if (yDd == NULL) { /* error */
1149          error_append("Null Dd returned on preimage compose- y_i stage. ");
1150          error_append("Node: ");
1151          error_append(Ntk_NodeReadName(nodePtr));
1152          bdd_recursive_deref(ddManager, currentDd);
1153          error_append("\n");
1154          return NULL;
1155        } /* end of error */
1156        /* construct the relation */
1157        bdd_ref(nodeReln = bdd_add_apply(ddManager, bdd_add_xnor, yDd, functionArray[i]));
1158
1159        if (nodeReln == NULL) { /* error */
1160          error_append("Null Dd returned on preimage compose - node reln stage");
1161          error_append("Node: ");
1162          error_append(Ntk_NodeReadName(nodePtr));
1163          bdd_recursive_deref(ddManager, yDd);
1164          bdd_recursive_deref(ddManager, currentDd);
1165          error_append("\n");
1166          return NULL;
1167        } /* end of error */
1168        /* perform the and of the and-abstract */
1169        bdd_ref(andDd = bdd_add_apply(ddManager, bdd_add_times, currentDd, nodeReln));
1170        bdd_recursive_deref(ddManager, currentDd);
1171        bdd_recursive_deref(ddManager, nodeReln);
1172        if (andDd == NULL) { /* error */
1173          error_append("Null Dd returned on preimage compose - and dd stage");
1174          error_append("Node: ");
1175          error_append(Ntk_NodeReadName(nodePtr));
1176          error_append("\n");
1177          bdd_recursive_deref(ddManager, yDd);
1178          return NULL;
1179        } /* end of error */
1180        /* perform the abstract of the and-abstract */
1181        bdd_ref(new_ = bdd_add_exist_abstract(ddManager, andDd, yDd));
1182        bdd_recursive_deref(ddManager, andDd);
1183        bdd_recursive_deref(ddManager, yDd);
1184        if (new_ == NULL) { /* error */
1185          error_append("Null Dd returned on preimage compose - and dd stage");
1186          error_append("Node: ");
1187          error_append((char *)Ntk_NodeReadName(nodePtr));
1188          error_append("\n");
1189          return NULL;
1190        } /* end of error */
1191        currentDd = new_;
1192      }
1193      break;
1194    } /* end of case Res_PreimageComputation_c */
1195  } /* end of switch(method) */
1196 
1197  /* return the new composed Dd */
1198  return new_;
1199} /* End of ComposeLayersIntoResidue */
1200 
1201
1202/**Function********************************************************************
1203
1204  Synopsis [Builds MVF for a node with no inputs, and only one row in its
1205  table.]
1206
1207  Description [Builds MVF for a constant, then node should be a constant,
1208  combinational node.  In this case, an MVF is built with a single component
1209  (indexed by the value of node) is one, and all other components are zero.]
1210
1211  SideEffects []
1212
1213******************************************************************************/
1214static Mvf_Function_t *
1215NodeBuildConstantMvf(
1216  Ntk_Node_t * node,
1217  mdd_manager *mddMgr)
1218{
1219  int             value        = 0; /* initialized to stop lint complaining */
1220  mdd_t          *oneMdd       = mdd_one(mddMgr);
1221  Var_Variable_t *variable     = Ntk_NodeReadVariable(node);
1222  int             numVarValues = Var_VariableReadNumValues(variable);
1223  Mvf_Function_t *mvf          = Mvf_FunctionAlloc(mddMgr, numVarValues);
1224  int          outputIndex = Ntk_NodeReadOutputIndex(node);
1225  Tbl_Table_t *table       = Ntk_NodeReadTable(node);
1226
1227  assert(Ntk_NodeTestIsConstant(node));
1228  value = Tbl_TableReadConstValue(table, outputIndex);
1229  assert(value != -1);
1230 
1231  Mvf_FunctionAddMintermsToComponent(mvf, value, oneMdd);
1232  mdd_free(oneMdd);
1233  return mvf;
1234}
Note: See TracBrowser for help on using the repository browser.