source: vis_dev/vis-2.3/src/part/partFrontier.c

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

vis2.3

File size: 51.2 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [partFrontier.c]
4
5  PackageName [part]
6
7  Synopsis [Implements the partition of the network based on the strategy of
8  creating a node whenever the size of the BDD representing the functionality
9  of the node increases the threshold value.]
10
11  Description [The network is composed of an arbitrary set of nodes each of
12  them implementing some simple function.  This method will create a graph such
13  that every vertex in that graph represents a node in the network.  Each node
14  in the primary he result
15  is a graph with exactly the same topology as the network and such that every
16  node has an MddId and a corresponding function.]
17
18  SeeAlso     [part.h]
19
20  Author      [Rajeev K. Ranjan, Chao Wang]
21
22  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
23  All rights reserved.
24
25  Permission is hereby granted, without written agreement and without license
26  or royalty fees, to use, copy, modify, and distribute this software and its
27  documentation for any purpose, provided that the above copyright notice and
28  the following two paragraphs appear in all copies of this software.
29
30  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
31  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
32  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
33  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
34
35  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
36  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
37  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
38  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
39  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
40******************************************************************************/
41#include "partInt.h"
42
43static char rcsid[] UNUSED = "$Id: partFrontier.c,v 1.25 2005/05/11 20:50:32 jinh Exp $";
44
45/*---------------------------------------------------------------------------*/
46/* Constant declarations                                                     */
47/*---------------------------------------------------------------------------*/
48
49
50/*---------------------------------------------------------------------------*/
51/* Stucture declarations                                                     */
52/*---------------------------------------------------------------------------*/
53
54/*---------------------------------------------------------------------------*/
55/* Type declarations                                                         */
56/*---------------------------------------------------------------------------*/
57
58
59/*---------------------------------------------------------------------------*/
60/* Variable declarations                                                     */
61/*---------------------------------------------------------------------------*/
62
63/*---------------------------------------------------------------------------*/
64/* Macro declarations                                                        */
65/*---------------------------------------------------------------------------*/
66
67
68/**AutomaticStart*************************************************************/
69
70/*---------------------------------------------------------------------------*/
71/* Static function prototypes                                                */
72/*---------------------------------------------------------------------------*/
73
74static void PartitionCreateEdges(graph_t *partition);
75static Mvf_Function_t * NodeBuildMvf(Ntk_Node_t * node, st_table * nodeToMvfTable);
76static Mvf_Function_t * NodeBuildMvf2(Ntk_Node_t * node, st_table * nodeToMvfTable, st_table *faninNumberTable);
77static Mvf_Function_t * NodeBuildPseudoInputMvf(Ntk_Node_t * node);
78static void PrintPartitionRecursively(vertex_t *vertex, st_table *vertexTable, int indent);
79
80/**AutomaticEnd***************************************************************/
81
82
83/*---------------------------------------------------------------------------*/
84/* Definition of exported functions                                          */
85/*---------------------------------------------------------------------------*/
86
87/**Function********************************************************************
88
89  Synopsis    [Read or create the Boolean network variables (BNVs).]
90
91  Description [Read or create the Boolean network variables. If the
92  partition is available, find the BNVs directly inside the
93  graph. Otherwise, sweep the network with the Frontier partition
94  method, and selectively insert BNVs. In both cases, the BNVs are put
95  into the hash table coiBnvTable.]
96
97  SideEffects []
98
99******************************************************************************/
100void 
101Part_PartitionReadOrCreateBnvs(
102  Ntk_Network_t *network,
103  st_table *coiLatchTable,
104  st_table *coiBnvTable)
105{
106  graph_t    *partition;
107  lsGen      lsgen;
108  vertex_t   *vertex;
109  long       mddId;
110  Ntk_Node_t *node;
111
112  /* if the partition is not available, sweep the network  */
113  partition = Part_NetworkReadPartition(network);
114  if (partition == NIL(graph_t)) {
115    PartInsertBnvs(network, coiLatchTable, coiBnvTable);
116    return;
117  }
118
119  /* otherwise, go through the vertices */
120  foreach_vertex(partition, lsgen, vertex) {
121    mddId = PartVertexReadMddId(vertex);
122    if (mddId == -1) continue;
123
124    node = Ntk_NetworkFindNodeByMddId(network, mddId);
125    assert(node != NIL(Ntk_Node_t));
126
127    if ( !Ntk_NodeTestIsCombInput(node) &&
128         Ntk_NodeReadNumFanouts(node)!=0 )
129      st_insert(coiBnvTable, (char *)node, NIL(char));
130  }
131 
132}
133
134/**Function********************************************************************
135
136  Synopsis    [Read or create the Boolean network variables (BNVs).]
137
138  Description [Read or create the Boolean network variables. If the
139  partition is available, find the BNVs directly inside the
140  graph. Otherwise, sweep the network with the Frontier partition
141  method, and selectively insert BNVs. In both cases, the BNVs are put
142  into the hash table coiBnvTable.]
143
144  SideEffects []
145
146******************************************************************************/
147void
148Part_PartitionWithExistingBnvs(
149  Ntk_Network_t *network,
150  graph_t *partition,
151  st_table *coiBnvTable,
152  st_table *absLatchTable,
153  st_table *absBnvTable)
154{
155
156  PartPartitionWithExistingBnvs(network, partition, coiBnvTable, 
157                                absLatchTable, absBnvTable);
158}
159
160/*---------------------------------------------------------------------------*/
161/* Definition of internal functions                                          */
162/*---------------------------------------------------------------------------*/
163
164/**Function********************************************************************
165
166  Synopsis [Creates the graph representing the combinational outputs
167  as functions of the combinational inputs as well as possibly some
168  intermediate variables.]
169
170  Description [The idea behind this partition method is representing
171  the functionality of combinational outputs in terms of combinational
172  inputs as well as some intermediate variables. Using intermediate
173  variables helps in controlling size of the BDDs for the combinational
174  outputs. These intermediate variables themselves may depend on other
175  intermediate variables and priamry inputs. Ultimately, the
176  functionality is realized in terms of combinational inputs alone.
177
178  The procedure works as follows:
179
180  i) First a topological order of the nodes is computed.
181  ii) A table mapping node to mvf is initialized for combinational
182  inputs.
183  iii) The functionality of nodes is computed in topological order in
184  terms of the fanin functions.
185  iii) If the bdd size of the mvf for a node exceeds the given bdd size
186  limit (set by partition_threshold), and the node has non-zero
187  fanouts, an mdd variable corresponding to that node is created and
188  node-mvf table is updated appropriately.
189  iv) For all the nodes in the fanouts of that node, the given node is
190  treated as primary input.
191  ]
192 
193
194  SideEffects [Partition is changed.]
195
196  SeeAlso     [Part_NetworkCreatePartition PartPartitionTotal PartPartitionInputsOutputs]
197
198******************************************************************************/
199void
200PartPartitionFrontier(Ntk_Network_t *network,
201                      graph_t *partition,
202                      lsList  rootList,
203                      lsList  leaveList,
204                      mdd_t   *careSet)
205{
206  Ntk_Node_t    *node;           /* Pointer to iterate over nodes */
207  lsGen         gen;                /* To iterate over lists */
208  vertex_t      *vertex;          /* Destination of the edge being added */
209  char          *name;              /* Name of the node being processed */
210  int           mddId;              /* Id of the node being processed */
211  int           i;
212  mdd_manager   *mddManager = PartPartitionReadMddManager(partition);
213  /* nodeToMvfTable maps a node to the mvf in the form that is needed to build
214     mvfs for the fanouts of the node.  I.e., a cutpoint node is mapped to an
215     mdd for a new variable. */
216  st_table *nodeToMvfTable = st_init_table(st_ptrcmp, st_ptrhash);
217  st_table *leafNodesTable = st_init_table(st_ptrcmp, st_ptrhash);
218  st_table *topoNodeTable;
219  Ntk_Node_t *fanoutNode;
220  array_t *rootNodesArray;
221  long fanoutNumber = 0;
222  Mvf_Function_t *nodeMvf; 
223  long bddSize;
224  int sizeThreshold;
225  lsList topologicalNodeList;
226  lsGen lsgen;
227  st_generator *stgen;
228  char *flagValue =  Cmd_FlagReadByName("partition_threshold");
229
230  if (flagValue == NIL(char)){
231    sizeThreshold = 1000; /* the default value */
232  }
233  else {
234    sizeThreshold = atoi(flagValue);
235  }
236
237  /* Put combinational inputs in the leafNodesTable. */
238  if (leaveList == (lsList)0) {
239    Ntk_NetworkForEachCombInput(network, gen, node) {
240      st_insert(leafNodesTable, (char *)node, (char *) (long) (-1) );
241    }
242  } /* End of then */ 
243  else {
244    lsForEachItem(leaveList, gen, node) {
245      st_insert(leafNodesTable, (char *)node, (char *) (long) (-1) );
246    }
247  } /* End of if-then-else */
248
249 
250  /* Take the nodes in rootList as the roots */
251  if (rootList == (lsList)0) {
252    rootNodesArray = array_alloc(Ntk_Node_t *, 
253                               Ntk_NetworkReadNumCombOutputs(network));
254    i = 0;
255    Ntk_NetworkForEachCombOutput(network, gen, node) {
256      array_insert(Ntk_Node_t *, rootNodesArray, i++, node);
257    }
258
259  } /* End of then */ 
260  else {
261    rootNodesArray = array_alloc(Ntk_Node_t *, lsLength(rootList));
262    i = 0;
263    lsForEachItem(rootList, gen, node) {
264      array_insert(Ntk_Node_t *, rootNodesArray, i++, node);
265    }
266  } /* End of if-then-else */
267
268  /* Get an array of nodes sorted in topological order */
269  topologicalNodeList = Ntk_NetworkComputeTopologicalOrder(network,
270                                                           rootNodesArray,
271                                                           leafNodesTable);   
272
273  /* For each node, compute the number of its fanouts */
274  topoNodeTable = st_init_table(st_ptrcmp, st_ptrhash);
275  lsForEachItem(topologicalNodeList, lsgen, node){
276    st_insert(topoNodeTable, (char *)node, NIL(char));
277  }
278  lsForEachItem(topologicalNodeList, lsgen, node){
279    fanoutNumber = 0;
280    Ntk_NodeForEachFanout(node, i, fanoutNode) {
281      if (st_is_member(topoNodeTable, fanoutNode) &&
282          !st_is_member(leafNodesTable, fanoutNode))
283        fanoutNumber++;
284    }
285    st_insert(topoNodeTable, node, (char *) fanoutNumber);
286  }
287
288  /* For each leaf nodes, create a vertex in the partition, create the mvf, and
289   * a mapping of name to vertex, and mddId to vertex.
290   */
291  st_foreach_item(leafNodesTable, stgen, &node, NULL) {
292    if (!st_lookup(topoNodeTable, node, &fanoutNumber)) {
293      continue;
294    }
295    mddId = Ntk_NodeReadMddId(node);
296    assert(mddId != NTK_UNASSIGNED_MDD_ID);
297    vertex = g_add_vertex(partition);
298    name  = Ntk_NodeReadName(node);
299    st_insert(PartPartitionReadNameToVertex(partition), name, vertex);
300    st_insert(PartPartitionReadMddIdToVertex(partition), (char *)(long)mddId,
301              vertex); 
302
303    if (Ntk_NodeTestIsPseudoInput(node)){
304      nodeMvf = NodeBuildPseudoInputMvf(node);
305    }
306    else {
307      nodeMvf = Mvf_FunctionCreateFromVariable(mddManager,mddId);
308    }
309
310    if (fanoutNumber <= 0) {
311      st_insert(nodeToMvfTable, (char *)node, NIL(char));
312    }else
313      st_insert(nodeToMvfTable, (char *)node, 
314                (char *)Mvf_FunctionDuplicate(nodeMvf));
315
316    vertex->user_data = (gGeneric)PartVertexInfoCreateSingle(name, nodeMvf,
317                                                             mddId);
318  }
319
320  st_free_table(leafNodesTable);
321 
322
323  fflush(vis_stdout);
324
325  /* Go through the topologicalNodeList
326   * a. If the node is of combinational input type, continue.
327   *
328   * b. Otherwise, Build the Mdd for this node, in terms of the function of the
329   *    fanin nodes in. If the Mdd size exceeds the threshold, create an Mdd ID
330   *    for this node.
331   */
332
333  lsForEachItem(topologicalNodeList, lsgen, node){
334    if (st_is_member(nodeToMvfTable, (char *)node)) continue;
335
336    nodeMvf = NodeBuildMvf2(node, nodeToMvfTable, topoNodeTable);
337    bddSize = bdd_size_multiple(nodeMvf);
338
339    if ((bddSize <= sizeThreshold) && !Ntk_NodeTestIsCombOutput(node)) {
340      st_insert(nodeToMvfTable, node, nodeMvf);
341      continue;
342    }
343
344    /* node either is a primary output, or has an mvf exceeding the
345     * threshold.
346     */
347    st_lookup(topoNodeTable, node, &fanoutNumber);
348    if ( (bddSize > sizeThreshold) &&  fanoutNumber > 0 ) {
349      if ((mddId = Ntk_NodeReadMddId(node)) == -1){
350        Ord_NetworkAssignMddIdForNode(network, node);
351        mddId = Ntk_NodeReadMddId(node);
352      }
353      st_insert(nodeToMvfTable, node,
354                Mvf_FunctionCreateFromVariable(mddManager,mddId));
355    }else {
356      if (fanoutNumber <= 0) {
357        st_insert(nodeToMvfTable, node, NIL(char));
358      }else
359        st_insert(nodeToMvfTable, (char *)node, 
360                  (char *)Mvf_FunctionDuplicate(nodeMvf));
361    }
362
363    vertex = g_add_vertex(partition);
364    name  = Ntk_NodeReadName(node);
365    mddId = Ntk_NodeReadMddId(node);
366    st_insert(PartPartitionReadNameToVertex(partition), name, (char *)vertex);
367    vertex->user_data = (gGeneric)PartVertexInfoCreateSingle(name, nodeMvf, 
368                                                             mddId);
369    if (mddId != -1){
370      st_insert(PartPartitionReadMddIdToVertex(partition),
371                (char *)(long)mddId, (char *)vertex);
372    }
373  }/* for each member of topologicalNodeList */
374 
375
376  /* sanity check */
377  st_foreach_item(nodeToMvfTable, stgen, &node, &nodeMvf) {
378#if 0
379    if (nodeMvf != NIL(Mvf_Function_t)) {
380      int chk = st_lookup(topoNodeTable, node, &fanoutNumber);
381      Ntk_NodeForEachFanout(node, i, fanoutNode) {
382        fprintf(vis_stdout, "\nunclean node %s   =>   %s",
383                Ntk_NodeReadName(node),
384                Ntk_NodeReadName(fanoutNode));
385        if (Ntk_NodeTestIsLatch(fanoutNode))
386          fprintf(vis_stdout, "\t(latch)");
387      }
388    }
389#else
390    assert (nodeMvf == NIL(Mvf_Function_t)) ;
391#endif
392  }
393
394  PartitionCreateEdges(partition);
395  array_free(rootNodesArray);
396  st_free_table(nodeToMvfTable);
397  st_free_table(topoNodeTable);
398  lsDestroy(topologicalNodeList, (void (*)(lsGeneric))0);
399}
400
401#if 0
402void
403PartPartitionFrontierOld(Ntk_Network_t *network,
404                      graph_t *partition,
405                      lsList  rootList,
406                      lsList  leaveList,
407                      mdd_t   *careSet)
408{
409  Ntk_Node_t    *node;           /* Pointer to iterate over nodes */
410  lsGen         gen;                /* To iterate over lists */
411  vertex_t      *vertex;          /* Destination of the edge being added */
412  char          *name;              /* Name of the node being processed */
413  int           mddId;              /* Id of the node being processed */
414  int           i;
415  mdd_manager   *mddManager = PartPartitionReadMddManager(partition);
416  /* nodeToMvfTable maps a node to the mvf in the form that is needed to build
417     mvfs for the fanouts of the node.  I.e., a cutpoint node is mapped to an
418     mdd for a new variable. */
419  st_table *nodeToMvfTable = st_init_table(st_ptrcmp, st_ptrhash);
420  st_table *leafNodesTable = st_init_table(st_ptrcmp, st_ptrhash);
421  array_t *rootNodesArray;
422  Mvf_Function_t *nodeMvf;
423  long bddSize;
424  int sizeThreshold;
425  lsList topologicalNodeList;
426  lsGen lsgen;
427  st_generator *stgen;
428  char *flagValue =  Cmd_FlagReadByName("partition_threshold");
429  if (flagValue == NIL(char)){
430    sizeThreshold = 1000; /* the default value */
431  }
432  else {
433    sizeThreshold = atoi(flagValue);
434  }
435
436  /* Put combinational inputs in the leafNodesTable. */
437  if (leaveList == (lsList)0) {
438    Ntk_NetworkForEachCombInput(network, gen, node) {
439      st_insert(leafNodesTable, (char *)node, (char *) (long) (-1) );
440    }
441  } /* End of then */
442  else {
443    lsForEachItem(leaveList, gen, node) {
444      st_insert(leafNodesTable, (char *)node, (char *) (long) (-1) );
445    }
446  } /* End of if-then-else */
447
448  /*
449   * For each leaf nodes, create a vertex in the partition, create the mvf, and
450   * a mapping of name to vertex, and mddId to vertex.
451   */
452  st_foreach_item(leafNodesTable, stgen, &node, NULL){
453    mddId = Ntk_NodeReadMddId(node);
454    assert(mddId != NTK_UNASSIGNED_MDD_ID);
455    vertex = g_add_vertex(partition);
456    name  = Ntk_NodeReadName(node);
457    st_insert(PartPartitionReadNameToVertex(partition), name, (char *)vertex);
458    st_insert(PartPartitionReadMddIdToVertex(partition), (char *)(long)mddId,
459              (char *)vertex);
460    if (Ntk_NodeTestIsPseudoInput(node)){
461      nodeMvf = NodeBuildPseudoInputMvf(node);
462    }
463    else {
464      nodeMvf = Mvf_FunctionCreateFromVariable(mddManager,mddId);
465    }
466    st_insert(nodeToMvfTable, (char *)node, (char *)nodeMvf);
467    vertex->user_data = (gGeneric)PartVertexInfoCreateSingle(name, nodeMvf,
468                                                             mddId);
469  }
470
471 
472  /* Take the nodes in rootList as the roots */
473  if (rootList == (lsList)0) {
474    rootNodesArray = array_alloc(Ntk_Node_t *,
475                               Ntk_NetworkReadNumCombOutputs(network));
476    i = 0;
477    Ntk_NetworkForEachCombOutput(network, gen, node) {
478      array_insert(Ntk_Node_t *, rootNodesArray, i++, node);
479    }
480  } /* End of then */
481  else {
482    rootNodesArray = array_alloc(Ntk_Node_t *, lsLength(rootList));
483    i = 0;
484    lsForEachItem(rootList, gen, node) {
485      array_insert(Ntk_Node_t *, rootNodesArray, i++, node);
486    }
487  } /* End of if-then-else */
488
489 
490
491  /* Get an array of nodes sorted in topological order */
492  topologicalNodeList = Ntk_NetworkComputeTopologicalOrder(network,
493                                                           rootNodesArray,
494                                                           leafNodesTable);   
495 
496  st_free_table(leafNodesTable);
497 
498
499  /* Go through the topologicalNodeList
500   * a. If the node is of combinational input type, continue.
501   *
502   * b. Otherwise, Build the Mdd for this node, in terms of the function of the
503   *    fanin nodes in. If the Mdd size exceeds the threshold, create an Mdd ID
504   *    for this node.
505   */
506
507  lsForEachItem(topologicalNodeList, lsgen, node){
508    if (st_is_member(nodeToMvfTable, (char *)node)) continue;
509    nodeMvf = NodeBuildMvf(node, nodeToMvfTable);
510    bddSize = bdd_size_multiple(nodeMvf);
511    if ((bddSize <= sizeThreshold) &&
512        (Ntk_NodeTestIsCombOutput(node) == 0)){
513      st_insert(nodeToMvfTable, (char *)node, (char *)nodeMvf);
514      continue;
515    }
516    /* node either is a primary output, or has an mvf exceeding the
517       threshold. */
518    vertex = g_add_vertex(partition);
519    name  = Ntk_NodeReadName(node);
520    st_insert(PartPartitionReadNameToVertex(partition), name,
521              (char *)vertex);
522    if ((bddSize > sizeThreshold) &&
523        (Ntk_NodeReadNumFanouts(node) != 0)){
524      if ((mddId = Ntk_NodeReadMddId(node)) == -1){
525        Ord_NetworkAssignMddIdForNode(network, node);
526        mddId = Ntk_NodeReadMddId(node);
527      }
528      st_insert(nodeToMvfTable, (char *)node,
529                (char *)Mvf_FunctionCreateFromVariable(mddManager,mddId));
530    }
531    else {
532      /* Small mvf, or no fanout */
533      st_insert(nodeToMvfTable, (char *)node, (char *)nodeMvf);
534    }
535    mddId = Ntk_NodeReadMddId(node);
536    vertex->user_data = (gGeneric)PartVertexInfoCreateSingle(name,
537                                                             nodeMvf,
538                                                             mddId);
539    if (mddId != -1){
540      st_insert(PartPartitionReadMddIdToVertex(partition),
541                (char *)(long)mddId, (char *)vertex);
542    }
543  }/* for each member of topologicalNodeList */
544 
545  /*
546   * Free the Mvfs in nodeToMvfTable not associated with vertices in the
547   * partition.  The mvfs of inputs are always in the partition; hence,
548   * their mvfs should always be preserved.  For outputs, we have to free
549   * the mvf in nodeToMvfTable if the output is also a cutpoint, because in
550   * this case the mvf in the partition vertex and the one in the
551   * nodeToMvfTable are different.
552   */
553
554  lsForEachItem(topologicalNodeList, gen, node){
555    if (!Ntk_NodeTestIsCombInput(node)){
556      if(!Ntk_NodeTestIsCombOutput(node)){
557        st_lookup(nodeToMvfTable, node, &nodeMvf);
558        assert(nodeMvf != NIL(Mvf_Function_t));
559        Mvf_FunctionFree(nodeMvf);
560      } else {
561        Mvf_Function_t *vertexMvf;
562       
563        name =  Ntk_NodeReadName(node);
564        vertex = Part_PartitionFindVertexByName(partition, name);
565        st_lookup(nodeToMvfTable, node, &nodeMvf);
566        vertexMvf = PartVertexReadFunction(vertex);
567        assert(nodeMvf != NIL(Mvf_Function_t) &&
568               vertexMvf != NIL(Mvf_Function_t));
569        if(vertexMvf != nodeMvf){
570          Mvf_FunctionFree(nodeMvf);
571        }
572      }
573    }/* not input */
574  }/* for each node */
575
576  PartitionCreateEdges(partition);
577  array_free(rootNodesArray);
578  st_free_table(nodeToMvfTable);
579  lsDestroy(topologicalNodeList, (void (*)(lsGeneric))0);
580}
581#endif
582
583/**Function********************************************************************
584
585  Synopsis [Creates the graph representing the combinational outputs
586  as functions of the combinational inputs as well as possibly some
587  intermediate variables.]
588
589  Description [The same as PartPartitionFrontier, but only add vertices for
590  nodes that are not in partition. This function can be used to update the
591  partition after more network nodes are added.]
592 
593  SideEffects [Partition is changed.]
594
595  SeeAlso     [PartPartitionFrontier]
596
597******************************************************************************/
598void
599PartUpdateFrontier(Ntk_Network_t *network,
600                   graph_t *partition,
601                   lsList  rootList,
602                   lsList  leaveList,
603                   mdd_t   *careSet)
604{
605  Ntk_Node_t    *node;           /* Pointer to iterate over nodes */
606  lsGen         gen;                /* To iterate over lists */
607  vertex_t      *vertex;          /* Destination of the edge being added */
608  char          *name;              /* Name of the node being processed */
609  int           mddId;              /* Id of the node being processed */
610  int           i, flag;
611  mdd_manager   *mddManager = PartPartitionReadMddManager(partition);
612  /* nodeToMvfTable maps a node to the mvf in the form that is needed to build
613     mvfs for the fanouts of the node.  I.e., a cutpoint node is mapped to an
614     mdd for a new variable. */
615  st_table *nodeToMvfTable = st_init_table(st_ptrcmp, st_ptrhash);
616  st_table *leafNodesTable = st_init_table(st_ptrcmp, st_ptrhash);
617  array_t *rootNodesArray;
618  Mvf_Function_t *nodeMvf; 
619  long bddSize;
620  int sizeThreshold;
621  lsList topologicalNodeList;
622  lsGen lsgen;
623  st_generator *stgen;
624  char *flagValue =  Cmd_FlagReadByName("partition_threshold");
625 
626  if (flagValue == NIL(char)){
627    sizeThreshold = 1000; /* the default value */
628  }
629  else {
630    sizeThreshold = atoi(flagValue);
631  }
632
633  /* Put combinational inputs in the leafNodesTable. */
634  if (leaveList == (lsList)0) {
635    Ntk_NetworkForEachCombInput(network, gen, node) {
636      st_insert(leafNodesTable, (char *)node, (char *) (long) (-1) );
637    }
638  } /* End of then */ 
639  else {
640    lsForEachItem(leaveList, gen, node) {
641      st_insert(leafNodesTable, (char *)node, (char *) (long) (-1) );
642    }
643  } /* End of if-then-else */
644
645  /*
646   * For each leaf nodes, create a vertex in the partition, create the mvf, and
647   * a mapping of name to vertex, and mddId to vertex.
648   * Notices that: if a vertex exists in the partition, use it instead of
649   * creating a new one.
650   */
651  st_foreach_item(leafNodesTable, stgen, &node, NULL){
652    mddId = Ntk_NodeReadMddId(node);
653    name  = Ntk_NodeReadName(node);
654    assert(mddId != NTK_UNASSIGNED_MDD_ID);
655    flag = st_lookup(PartPartitionReadNameToVertex(partition), 
656                     name, &vertex);
657    if (flag) {
658      nodeMvf = ((PartVertexInfo_t *)(vertex->user_data))->functionality.mvf;
659      st_insert(nodeToMvfTable, node, nodeMvf);
660      /*
661      name = Ntk_NodeReadName(node);
662      fprintf(vis_stdout, "warning: node %s already in the partition\n",
663              name);
664      */
665    }else {
666      vertex = g_add_vertex(partition);
667      st_insert(PartPartitionReadNameToVertex(partition), name, (char *)vertex);
668      st_insert(PartPartitionReadMddIdToVertex(partition), (char *)(long)mddId,
669                (char *)vertex); 
670      if (Ntk_NodeTestIsPseudoInput(node)){
671        nodeMvf = NodeBuildPseudoInputMvf(node);
672      }else {
673        nodeMvf = Mvf_FunctionCreateFromVariable(mddManager,mddId);
674      }
675      st_insert(nodeToMvfTable, (char *)node, (char *)nodeMvf);
676      vertex->user_data = (gGeneric)PartVertexInfoCreateSingle(name, nodeMvf,
677                                                               mddId);
678    }
679  }
680 
681  /* Take the nodes in rootList as the roots */
682  if (rootList == (lsList)0) {
683    rootNodesArray = array_alloc(Ntk_Node_t *, 
684                               Ntk_NetworkReadNumCombOutputs(network));
685    i = 0;
686    Ntk_NetworkForEachCombOutput(network, gen, node) {
687      name = Ntk_NodeReadName(node);
688      if ( !st_is_member(PartPartitionReadNameToVertex(partition), name) )
689        array_insert(Ntk_Node_t *, rootNodesArray, i++, node);
690    }
691  } /* End of then */ 
692  else {
693    rootNodesArray = array_alloc(Ntk_Node_t *, lsLength(rootList));
694    i = 0;
695    lsForEachItem(rootList, gen, node) {
696      name = Ntk_NodeReadName(node);
697      if ( !st_is_member(PartPartitionReadNameToVertex(partition), name) )
698        array_insert(Ntk_Node_t *, rootNodesArray, i++, node);
699    }
700  } /* End of if-then-else */
701
702 
703
704  /* Get an array of nodes sorted in topological order */
705  topologicalNodeList = Ntk_NetworkComputeTopologicalOrder(network,
706                                                           rootNodesArray,
707                                                           leafNodesTable);   
708 
709  st_free_table(leafNodesTable);
710 
711
712  /* Go through the topologicalNodeList
713   * a. If the node is of combinational input type, continue.
714   *
715   * b. Otherwise, Build the Mdd for this node, in terms of the function of the
716   *    fanin nodes in. If the Mdd size exceeds the threshold, create an Mdd ID
717   *    for this node.
718   */
719
720  lsForEachItem(topologicalNodeList, lsgen, node){
721    if (st_is_member(nodeToMvfTable, node)) continue;
722    name = Ntk_NodeReadName(node);
723    flag = st_lookup(PartPartitionReadNameToVertex(partition), 
724                     name, &vertex);
725    if (flag) {
726      mddId = Ntk_NodeReadMddId(node);
727      if (mddId != -1)
728        st_insert(nodeToMvfTable, node,
729                  (char *)Mvf_FunctionCreateFromVariable(mddManager,mddId));
730      else {
731        nodeMvf = PartVertexReadFunction(vertex);
732        st_insert(nodeToMvfTable, node, nodeMvf);
733      }
734      continue;
735    }
736    nodeMvf = NodeBuildMvf(node, nodeToMvfTable);
737    bddSize = bdd_size_multiple(nodeMvf);
738    if ((bddSize <= sizeThreshold) &&
739        (Ntk_NodeTestIsCombOutput(node) == 0)){
740      st_insert(nodeToMvfTable, (char *)node, (char *)nodeMvf);
741      continue;
742    }
743    /* node either is a primary output, or has an mvf exceeding the
744       threshold. */
745    vertex = g_add_vertex(partition);
746    name  = Ntk_NodeReadName(node);
747    st_insert(PartPartitionReadNameToVertex(partition), name,
748              (char *)vertex);
749    if ((bddSize > sizeThreshold) &&
750        (Ntk_NodeReadNumFanouts(node) != 0)){
751      if ((mddId = Ntk_NodeReadMddId(node)) == -1){
752        Ord_NetworkAssignMddIdForNode(network, node);
753        mddId = Ntk_NodeReadMddId(node);
754      }
755      st_insert(nodeToMvfTable, (char *)node,
756                (char *)Mvf_FunctionCreateFromVariable(mddManager,mddId));
757    }
758    else {
759      /* Small mvf, or no fanout */
760      st_insert(nodeToMvfTable, (char *)node, (char *)nodeMvf);
761    }
762    mddId = Ntk_NodeReadMddId(node);
763    vertex->user_data = (gGeneric)PartVertexInfoCreateSingle(name,
764                                                             nodeMvf, 
765                                                             mddId);
766    if (mddId != -1){
767      st_insert(PartPartitionReadMddIdToVertex(partition),
768                (char *)(long)mddId, (char *)vertex);
769    }
770  }/* for each member of topologicalNodeList */
771 
772  /*
773   * Free the Mvfs in nodeToMvfTable not associated with vertices in the
774   * partition.  The mvfs of inputs are always in the partition; hence,
775   * their mvfs should always be preserved.  For outputs, we have to free
776   * the mvf in nodeToMvfTable if the output is also a cutpoint, because in
777   * this case the mvf in the partition vertex and the one in the
778   * nodeToMvfTable are different.
779   */
780
781  lsForEachItem(topologicalNodeList, gen, node){ 
782    if (!Ntk_NodeTestIsCombInput(node)){
783      if(!Ntk_NodeTestIsCombOutput(node)){ 
784        st_lookup(nodeToMvfTable, node, &nodeMvf); 
785        assert(nodeMvf != NIL(Mvf_Function_t)); 
786        Mvf_FunctionFree(nodeMvf);
787      } else {
788        Mvf_Function_t *vertexMvf;
789       
790        name =  Ntk_NodeReadName(node);
791        vertex = Part_PartitionFindVertexByName(partition, name);
792        st_lookup(nodeToMvfTable, node, &nodeMvf);
793        vertexMvf = PartVertexReadFunction(vertex);
794        assert(nodeMvf != NIL(Mvf_Function_t) &&
795               vertexMvf != NIL(Mvf_Function_t));
796        if(vertexMvf != nodeMvf){
797          Mvf_FunctionFree(nodeMvf);
798        }
799      }
800    }/* not input */
801  }/* for each node */
802
803  PartitionCreateEdges(partition);
804  array_free(rootNodesArray);
805  st_free_table(nodeToMvfTable);
806  lsDestroy(topologicalNodeList, (void (*)(lsGeneric))0);
807}
808
809/**Function********************************************************************
810
811  Synopsis [Selectively insert Boolean network variables.]
812
813  Description [Selectively insert Boolean network varibles using the
814  Frontier partition method---every time the BDD size exceeds the
815  partition threshold, a boolean network variable is inserted.
816
817  The added boolean network variables are inserted into the coiBnvTable. ]
818 
819
820  SideEffects []
821
822  SeeAlso     [PartPartitionFrontier]
823
824******************************************************************************/
825void
826PartInsertBnvs(
827  Ntk_Network_t *network,
828  st_table *coiLatchTable,
829  st_table *coiBnvTable)
830{
831  mdd_manager    *mddManager = Ntk_NetworkReadMddManager(network);
832  st_table       *nodeToMvfTable = st_init_table(st_ptrcmp, st_ptrhash);
833  st_table       *leafNodesTable = st_init_table(st_ptrcmp, st_ptrhash);
834  lsList         topologicalNodeList;
835  st_table       *topoNodeTable;
836  array_t        *rootNodesArray;
837  Ntk_Node_t     *fanoutNode, *node;
838  Mvf_Function_t *nodeMvf; 
839  long           bddSize, sizeThreshold, fanoutNumber, mddId;
840  int            i;
841  lsGen          lsgen;
842  st_generator   *stgen;
843  char           *flagValue;
844
845  flagValue =  Cmd_FlagReadByName("partition_threshold");
846  if (flagValue == NIL(char)){
847    sizeThreshold = 1000; /* the default value */
848  }
849  else {
850    sizeThreshold = atoi(flagValue);
851  }
852
853  /* Put latch data inputs in the rootNodesArray */
854  rootNodesArray = array_alloc(Ntk_Node_t *, 0);
855  st_foreach_item(coiLatchTable, stgen, &node, NULL) {
856    array_insert_last(Ntk_Node_t *, rootNodesArray, 
857                      Ntk_LatchReadDataInput(node));
858    array_insert_last(Ntk_Node_t *, rootNodesArray, 
859                      Ntk_LatchReadInitialInput(node));
860  }
861
862  /* Put combinational inputs, as well as the existing coiBnvs, in the
863   * leafNodesTable. */
864  Ntk_NetworkForEachCombInput(network, lsgen, node) {
865    st_insert(leafNodesTable, node, (char *) (long) (-1) );
866  }
867  st_foreach_item(coiBnvTable, stgen, &node, NULL) {
868    st_insert(leafNodesTable, node, (char *) (long) (-1) );
869  }
870 
871  /* Get an array of nodes sorted in topological order */
872  topologicalNodeList = Ntk_NetworkComputeTopologicalOrder(network,
873                                                           rootNodesArray,
874                                                           leafNodesTable);   
875
876  /* For each node, compute the number of fanouts */
877  topoNodeTable = st_init_table(st_ptrcmp, st_ptrhash);
878  lsForEachItem(topologicalNodeList, lsgen, node){
879    st_insert(topoNodeTable, (char *)node, NIL(char));
880  }
881  lsForEachItem(topologicalNodeList, lsgen, node){
882    fanoutNumber = 0;
883    Ntk_NodeForEachFanout(node, i, fanoutNode) {
884      if (st_is_member(topoNodeTable, (char *)fanoutNode) &&
885          !st_is_member(leafNodesTable, (char *)fanoutNode) )
886        fanoutNumber++;
887    }
888    st_insert(topoNodeTable, (char *)node, (char *)fanoutNumber);
889  }
890
891  /* assign mddIds to latches if necessary */
892  /* chao: this may be too slow! */
893  /* chao: this order may not be as good as static_order */
894  lsForEachItem(topologicalNodeList, lsgen, node){
895    if (Ntk_NodeTestIsInput(node)) {
896      Ord_NetworkAssignMddIdForNode(network, node);
897    }else if (Ntk_NodeTestIsLatch(node)) {
898      Ord_NetworkAssignMddIdForNode(network, node);
899      Ord_NetworkAssignMddIdForNode(network, Ntk_NodeReadShadow(node));
900    }
901  }
902  st_foreach_item(coiLatchTable, stgen, &node, NULL) {
903    Ord_NetworkAssignMddIdForNode(network, node);
904    Ord_NetworkAssignMddIdForNode(network, Ntk_NodeReadShadow(node));
905  }
906
907  /* create nodeMvf for leaf nodes */
908  st_foreach_item(leafNodesTable, stgen, &node, NULL) {
909    if (!st_lookup(topoNodeTable, node, &fanoutNumber)) {
910      continue;
911    }
912    mddId = Ntk_NodeReadMddId(node);
913    assert(mddId != NTK_UNASSIGNED_MDD_ID);
914
915    if (Ntk_NodeTestIsPseudoInput(node)){
916      nodeMvf = NodeBuildPseudoInputMvf(node);
917    }
918    else {
919      nodeMvf = Mvf_FunctionCreateFromVariable(mddManager,mddId);
920    }
921
922    if (fanoutNumber <= 0) {
923      Mvf_FunctionFree(nodeMvf);
924      st_insert(nodeToMvfTable, (char *)node, NIL(char));
925    }
926    else
927      st_insert(nodeToMvfTable, (char *)node, (char *)nodeMvf);
928  }
929
930  st_free_table(leafNodesTable);
931
932
933  /* Go through the topologicalNodeList
934   * a. If the node is of combinational input type, continue.
935   *
936   * b. Otherwise, Build the Mdd for this node, in terms of the function of the
937   *    fanin nodes in. If the Mdd size exceeds the threshold, create an Mdd ID
938   *    for this node.
939   */
940  lsForEachItem(topologicalNodeList, lsgen, node){
941    if (st_is_member(nodeToMvfTable, node)) 
942      continue;
943
944    nodeMvf = NodeBuildMvf2(node, nodeToMvfTable, topoNodeTable);
945    bddSize = bdd_size_multiple(nodeMvf);
946    st_lookup(topoNodeTable, node, &fanoutNumber);
947
948    if ((bddSize <= sizeThreshold) && !Ntk_NodeTestIsCombOutput(node)) {
949      assert(fanoutNumber > 0);
950      st_insert(nodeToMvfTable, node, nodeMvf);
951      continue;
952    }
953    /* node either is a primary output, or has an mvf exceeding the
954       threshold. */
955    if ((bddSize > sizeThreshold) && fanoutNumber > 0) {
956                                   /*(Ntk_NodeReadNumFanouts(node) != 0)) { */
957      /* ADD A bnv !!! */
958      st_insert(coiBnvTable, (char *)node, NIL(char));
959
960      if ((mddId = Ntk_NodeReadMddId(node)) == -1){
961        Ord_NetworkAssignMddIdForNode(network, node);
962        mddId = Ntk_NodeReadMddId(node);
963      }
964
965      st_insert(nodeToMvfTable, (char *)node,
966                (char *)Mvf_FunctionCreateFromVariable(mddManager,mddId));
967      Mvf_FunctionFree(nodeMvf);
968    }else {
969      if (fanoutNumber <= 0) {
970        Mvf_FunctionFree(nodeMvf);
971        st_insert(nodeToMvfTable, node, NIL(char));
972      }
973      else
974        st_insert(nodeToMvfTable, node, (char *)nodeMvf);
975    }
976
977  }/* for each member of topologicalNodeList */
978 
979  /* sanity check */
980  st_foreach_item(nodeToMvfTable, stgen, &node, &nodeMvf) {
981#if 0
982    if (nodeMvf != NIL(Mvf_Function_t)) {
983      st_lookup(topoNodeTable, node, &fanoutNumber);
984      fprintf(vis_stdout, "\nunclean node = %s, fanout# = %d",
985              Ntk_NodeReadName(node), fanoutNumber);
986    }
987#else
988    assert (nodeMvf == NIL(Mvf_Function_t));
989#endif
990  }
991
992  array_free(rootNodesArray);
993  st_free_table(nodeToMvfTable);
994  st_free_table(topoNodeTable);
995  lsDestroy(topologicalNodeList, (void (*)(lsGeneric))0);
996}
997
998/**Function********************************************************************
999
1000  Synopsis [Update the partition with the given set of internal nodes.]
1001
1002  Description [Update the partition with the given set of internal
1003  nodes. Insert intermediate variables, or Boolean Network Variables
1004  (BNVs) only for the given set of internal nodes
1005  (coiBnvTable). Intermediate variables (or Bnvs) that do not appear
1006  in absBnvTable will not be included in the partition---they will be
1007  treated as inputs.]
1008
1009  SideEffects []
1010
1011  SeeAlso     [PartPartitionFrontier PartPartitionInsertBnvs]
1012
1013******************************************************************************/
1014void
1015PartPartitionWithExistingBnvs(
1016  Ntk_Network_t *network,
1017  graph_t *partition,
1018  st_table *coiBnvTable,
1019  st_table *absLatchTable,
1020  st_table *absBnvTable)
1021{
1022  mdd_manager    *mddManager = PartPartitionReadMddManager(partition);
1023  st_table       *nodeToMvfTable = st_init_table(st_ptrcmp, st_ptrhash);
1024  st_table       *leafNodesTable = st_init_table(st_ptrcmp, st_ptrhash);
1025  array_t        *rootNodesArray, *combNodesArray;
1026  lsList         topologicalNodeList;
1027  st_table       *topoNodeTable;
1028  Ntk_Node_t     *fanoutNode, *node;
1029  Mvf_Function_t *nodeMvf; 
1030  vertex_t       *vertex;         
1031  long           mddId, fanoutNumber;
1032  char           *name;           
1033  lsGen          lsgen;
1034  st_generator   *stgen;
1035  int            i;
1036
1037  /* Put latch data inputs in the rootNodesArray */
1038  rootNodesArray = array_alloc(Ntk_Node_t *, 0);
1039  st_foreach_item(absLatchTable, stgen, &node, NULL) {
1040    array_insert_last(Ntk_Node_t *, rootNodesArray, 
1041                      Ntk_LatchReadDataInput(node));
1042    array_insert_last(Ntk_Node_t *, rootNodesArray, 
1043                      Ntk_LatchReadInitialInput(node));
1044  }
1045
1046  /* Put also latch initial inputs in the rootNodesArray */
1047  combNodesArray = Ntk_NodeComputeTransitiveFaninNodes(network,
1048                                                       rootNodesArray,
1049                                                       TRUE, TRUE);
1050  arrayForEachItem(Ntk_Node_t *, combNodesArray, i, node) {
1051    if ( Ntk_NodeTestIsLatch(node) && 
1052         !st_is_member(absLatchTable, (char *)node) )
1053      array_insert_last(Ntk_Node_t *, rootNodesArray, 
1054                        Ntk_LatchReadInitialInput(node));
1055  }
1056  array_free(combNodesArray);
1057
1058
1059  /* Put combinational inputs in the leafNodesTable. */
1060  Ntk_NetworkForEachCombInput(network, lsgen, node) {
1061    st_insert(leafNodesTable, (char *)node, (char *) (long) (-1) );
1062  }
1063  /* Put BNVs that are not in absBnvTable in the leafNodesTable */
1064  st_foreach_item(coiBnvTable, stgen, &node, NULL) {
1065    if (!st_is_member(absBnvTable, (char *)node))
1066      st_insert(leafNodesTable, node, (char *) (long) (-1) );
1067  }
1068
1069  /* Get an array of nodes sorted in topological order  */
1070  topologicalNodeList = Ntk_NetworkComputeTopologicalOrder(network,
1071                                                           rootNodesArray,
1072                                                           leafNodesTable);
1073
1074  /* For each node, compute the number of fanouts */
1075  topoNodeTable = st_init_table(st_ptrcmp, st_ptrhash);
1076  lsForEachItem(topologicalNodeList, lsgen, node){
1077    st_insert(topoNodeTable, (char *)node, NIL(char));
1078  }
1079  lsForEachItem(topologicalNodeList, lsgen, node){
1080    fanoutNumber = 0;
1081    Ntk_NodeForEachFanout(node, i, fanoutNode) {
1082      if (st_is_member(topoNodeTable, (char *)fanoutNode) &&
1083          !st_is_member(leafNodesTable, (char *)fanoutNode))
1084        fanoutNumber++;
1085    }
1086    st_insert(topoNodeTable, (char *)node, (char *)fanoutNumber);
1087   }
1088
1089  /* Create partition vertices for the leaves
1090   */
1091  st_foreach_item(leafNodesTable, stgen, &node, NULL){
1092    if (!st_lookup(topoNodeTable, node, &fanoutNumber))
1093      continue;
1094    mddId = Ntk_NodeReadMddId(node);
1095    if (mddId == NTK_UNASSIGNED_MDD_ID) {
1096        /* it is a input sign under the fanin cone of the initialInput
1097         * of some invisible latches */
1098        assert(Ntk_NodeTestIsInput(node));
1099        Ord_NetworkAssignMddIdForNode(network, node);
1100        mddId = Ntk_NodeReadMddId(node);
1101    }
1102    /*assert(mddId != NTK_UNASSIGNED_MDD_ID);*/
1103    vertex = g_add_vertex(partition);
1104    name  = Ntk_NodeReadName(node);
1105    st_insert(PartPartitionReadNameToVertex(partition), name, (char *)vertex);
1106    st_insert(PartPartitionReadMddIdToVertex(partition), (char *)(long)mddId,
1107              (char *)vertex); 
1108    if (Ntk_NodeTestIsPseudoInput(node)){
1109      nodeMvf = NodeBuildPseudoInputMvf(node);
1110    }
1111    else {
1112      nodeMvf = Mvf_FunctionCreateFromVariable(mddManager,mddId);
1113    }
1114
1115    if (fanoutNumber <= 0) 
1116      st_insert(nodeToMvfTable, (char *)node, NIL(char));
1117    else
1118      st_insert(nodeToMvfTable, (char *)node, 
1119                (char *)Mvf_FunctionDuplicate(nodeMvf));
1120
1121    vertex->user_data = (gGeneric)PartVertexInfoCreateSingle(name, nodeMvf,
1122                                                             mddId);
1123  }
1124
1125  /* Go through the topologicalNodeList, and build Mdds for nodes in
1126   * the absBnvTable
1127   */
1128  lsForEachItem(topologicalNodeList, lsgen, node){
1129    if (st_is_member(nodeToMvfTable, (char *)node)) continue;
1130
1131    nodeMvf = NodeBuildMvf2(node, nodeToMvfTable, topoNodeTable);
1132
1133    if ( !st_is_member(absBnvTable,(char *)node) && 
1134         !Ntk_NodeTestIsCombOutput(node)) {
1135      st_insert(nodeToMvfTable, (char *)node, (char *)nodeMvf);
1136      continue; 
1137    }
1138   
1139    /* node is either a primary output, or a boolean network var */
1140    vertex = g_add_vertex(partition);
1141    name  = Ntk_NodeReadName(node);
1142    st_insert(PartPartitionReadNameToVertex(partition), name, (char *)vertex);
1143
1144    if (st_is_member(absBnvTable,node)) {
1145      /* ADD a bnv !!! */
1146      mddId = Ntk_NodeReadMddId(node);
1147      assert(mddId != -1);
1148      st_insert(nodeToMvfTable, node,
1149                (char *)Mvf_FunctionCreateFromVariable(mddManager,mddId));
1150    }else {
1151      st_lookup(topoNodeTable, node, &fanoutNumber);
1152      if (fanoutNumber <= 0) 
1153        st_insert(nodeToMvfTable, node, NIL(char));
1154      else
1155        st_insert(nodeToMvfTable, node, 
1156                  (char *)Mvf_FunctionDuplicate(nodeMvf));
1157    }
1158
1159    mddId = Ntk_NodeReadMddId(node);
1160    vertex->user_data = (gGeneric)PartVertexInfoCreateSingle(name, nodeMvf, 
1161                                                             mddId);
1162    if (mddId != -1){
1163      st_insert(PartPartitionReadMddIdToVertex(partition),
1164                (char *)(long)mddId, (char *)vertex);
1165    }
1166  }/* for each member of topologicalNodeList */
1167
1168  /* sanity check */
1169  st_foreach_item(nodeToMvfTable, stgen, &node, &nodeMvf) {
1170#if 1
1171    if (nodeMvf != NIL(Mvf_Function_t)) {
1172      st_lookup(topoNodeTable, node, &fanoutNumber);
1173      fprintf(vis_stdout, "\nunclean node = %s, fanout# = %ld",
1174              Ntk_NodeReadName(node), fanoutNumber);
1175    }
1176#else
1177    assert(nodeMvf == NIL(Mvf_Function_t));
1178#endif
1179  }
1180
1181  PartitionCreateEdges(partition);
1182  array_free(rootNodesArray);
1183  st_free_table(nodeToMvfTable);
1184  st_free_table(topoNodeTable);
1185  st_free_table(leafNodesTable);
1186  lsDestroy(topologicalNodeList, (void (*)(lsGeneric))0);
1187}
1188
1189
1190/**Function********************************************************************
1191
1192  Synopsis    [Prints the integers from a symbol table.]
1193
1194  Description [Prints the integers from a symbol table.]
1195
1196  SideEffects []
1197
1198******************************************************************************/
1199void
1200PartPrintPartition(graph_t *partition)
1201{
1202  vertex_t *vertex;
1203  lsList vertexList = g_get_vertices(partition);
1204  lsGen gen;
1205  st_table *vertexTable = st_init_table(st_ptrcmp, st_ptrhash);
1206  fprintf(vis_stdout,"******* Printing Partition *********\n");
1207  lsForEachItem(vertexList, gen, vertex){
1208    PrintPartitionRecursively(vertex,vertexTable,0);
1209  }
1210  fprintf(vis_stdout,"******* End Printing Partition *********\n");
1211  st_free_table(vertexTable);
1212}
1213
1214 
1215/*---------------------------------------------------------------------------*/
1216/* Definition of static functions                                            */
1217/*---------------------------------------------------------------------------*/
1218
1219/**Function********************************************************************
1220
1221  Synopsis    [Creates edges in the graph corresponding to a partition.]
1222
1223  Description [Creates edges in the graph corresponding to a
1224  partition. An edge exists between node i and node j, if node j is in
1225  the support of functionality of node i.]
1226
1227  SideEffects [Partition is changed.]
1228
1229  SeeAlso     []
1230
1231******************************************************************************/
1232static void
1233PartitionCreateEdges(graph_t *partition)
1234{
1235  lsList vertexList;
1236  lsGen gen;
1237  vertex_t *toVertex;
1238  edge_t *edge;
1239
1240  /* this will be executed only when used inside PartitionUpdateFrontier */
1241  foreach_edge(partition, gen, edge) {
1242    g_delete_edge(edge, (void(*)(gGeneric))0);
1243  }
1244
1245  vertexList = g_get_vertices(partition);
1246
1247  lsForEachItem(vertexList, gen, toVertex) {
1248    st_table     *mddSupport; /* To store the support of the Mvf_Function */
1249    st_generator *stGen;      /* To iterate over the MddIds of the support */
1250    vertex_t     *fromVertex; /* Will hold the current vertex in the support */
1251    Mvf_Function_t *mddFunction;
1252    long          mddId;
1253   
1254    mddFunction = PartVertexReadFunction(toVertex);
1255    mddSupport = PartCreateFunctionSupportTable(mddFunction);
1256    st_foreach_item(mddSupport, stGen, &mddId, NULL) {
1257      st_lookup(PartPartitionReadMddIdToVertex(partition), (char *) mddId,
1258                &fromVertex); 
1259      /*
1260       * Add the edge to the graph. Make sure a self loop is not added. The
1261       * self loop may be produced by a mdd that has in its support the same
1262       * variables that represent the mddId of the node.
1263       */
1264      if (fromVertex != toVertex) {
1265        g_add_edge(fromVertex, toVertex);
1266      }
1267    }
1268    st_free_table(mddSupport);
1269  } 
1270}
1271
1272/**Function********************************************************************
1273
1274  Synopsis    [Builds the functionality of a node, given the
1275  functionality of its fanins.]
1276
1277  Description [The nodeToMvfTable must contain the functionality of
1278  all the fanins of the node.]
1279
1280  SideEffects [none.]
1281
1282  SeeAlso     []
1283
1284******************************************************************************/
1285static Mvf_Function_t *
1286NodeBuildMvf(Ntk_Node_t * node, st_table * nodeToMvfTable)
1287{
1288  int i;
1289  Mvf_Function_t *resultMvf;
1290  Ntk_Node_t *faninNode;
1291  array_t *faninMvfs = array_alloc(Mvf_Function_t *,
1292                                            Ntk_NodeReadNumFanins(node));
1293  mdd_manager *mddMgr = Ntk_NetworkReadMddManager(Ntk_NodeReadNetwork(node)); 
1294  int columnIndex = Ntk_NodeReadOutputIndex(node);
1295  Tbl_Table_t *table = Ntk_NodeReadTable(node);
1296 
1297  Ntk_NodeForEachFanin(node, i, faninNode) {
1298    Mvf_Function_t *tmpMvf;
1299    st_lookup(nodeToMvfTable, faninNode, &tmpMvf); 
1300    assert(tmpMvf);
1301    array_insert(Mvf_Function_t *, faninMvfs, i, tmpMvf);
1302  }
1303 
1304  resultMvf = Tbl_TableBuildMvfFromFanins(table, columnIndex,
1305                                          faninMvfs, mddMgr);   
1306 
1307  /* Don't free the MVFs themselves, but just free the array. */
1308  array_free(faninMvfs);
1309  return resultMvf;
1310}
1311   
1312/**Function********************************************************************
1313
1314  Synopsis    [Builds the functionality of a node, given the
1315  functionality of its fanins.]
1316
1317  Description [The nodeToMvfTable must contain the functionality of
1318  all the fanins of the node. When the faninNumber counter is
1319  decreased to 0, free the corresponding MVF in the nodeToMvfTable.]
1320
1321  SideEffects [none.]
1322
1323  SeeAlso     []
1324
1325******************************************************************************/
1326static Mvf_Function_t *
1327NodeBuildMvf2(
1328  Ntk_Node_t * node, 
1329  st_table * nodeToMvfTable,
1330  st_table * faninNumberTable)
1331{
1332  long faninNumber;
1333  int i;
1334  Mvf_Function_t *resultMvf;
1335  Ntk_Node_t *faninNode;
1336  array_t *faninMvfs = array_alloc(Mvf_Function_t *,
1337                                   Ntk_NodeReadNumFanins(node));
1338  mdd_manager *mddMgr = Ntk_NetworkReadMddManager(Ntk_NodeReadNetwork(node)); 
1339  int columnIndex = Ntk_NodeReadOutputIndex(node);
1340  Tbl_Table_t *table = Ntk_NodeReadTable(node);
1341 
1342  Ntk_NodeForEachFanin(node, i, faninNode) {
1343    Mvf_Function_t *tmpMvf;
1344    st_lookup(nodeToMvfTable, faninNode, &tmpMvf); 
1345    assert(tmpMvf);
1346    array_insert(Mvf_Function_t *, faninMvfs, i, tmpMvf);
1347  }
1348 
1349  resultMvf = Tbl_TableBuildMvfFromFanins(table, columnIndex,
1350                                          faninMvfs, mddMgr);   
1351 
1352  /* Don't free the MVFs themselves, but just free the array. */
1353  array_free(faninMvfs);
1354
1355  /* if the fanin node is no longer useful, remove its Mvfs */
1356  Ntk_NodeForEachFanin(node, i, faninNode) {
1357    st_lookup(faninNumberTable, faninNode, &faninNumber);
1358    assert(faninNumber > 0);
1359    faninNumber--;
1360    st_insert(faninNumberTable, faninNode, (char *)faninNumber);
1361
1362    if (faninNumber <= 0) {
1363      Mvf_Function_t *tmpMvf;
1364      st_lookup(nodeToMvfTable, faninNode, &tmpMvf); 
1365      Mvf_FunctionFree(tmpMvf);
1366      st_insert(nodeToMvfTable, faninNode, NIL(char));
1367    }
1368  }
1369
1370  return resultMvf;
1371}
1372   
1373     
1374
1375/**Function********************************************************************
1376
1377  Synopsis    [Builds MVF for a node that is a pseudo input.]
1378
1379  Description [Builds MVF for a node that is a pseudo input.  This node has a
1380  single output and no inputs. Its table has several row entries.  We build an
1381  MVF whose components correspond exactly to possible table outputs.]
1382
1383  SideEffects []
1384
1385  Comment [Although pseudo inputs, constants, and internal nodes all have
1386  tables, a single procedure cannot be used to build their MVF.  A pseudo
1387  input MVF is built in terms of its mddId, whereas a constant or internal is
1388  not.  A constant or pseudo input doesn't have any inputs, whereas an
1389  internal does.]
1390 
1391  SeeAlso     [Tbl_TableBuildMvfForNonDetConstant]
1392
1393******************************************************************************/
1394static Mvf_Function_t *
1395NodeBuildPseudoInputMvf(
1396  Ntk_Node_t * node)
1397{
1398  mdd_manager  *mddMgr = Ntk_NetworkReadMddManager(Ntk_NodeReadNetwork(node));
1399  int          mddId = Ntk_NodeReadMddId( node );
1400  int          columnIndex = Ntk_NodeReadOutputIndex( node );
1401  Tbl_Table_t  *table = Ntk_NodeReadTable( node );
1402  Mvf_Function_t *mvf = Tbl_TableBuildNonDetConstantMvf(table, columnIndex,
1403                                                        mddId, mddMgr);
1404
1405  mdd_t *vMdd, *tMdd, *rMdd;
1406  int lIndex, needProcess, i;
1407
1408  rMdd = mdd_zero(mddMgr);
1409  needProcess = 0;
1410  lIndex = 0;
1411  for(i=0; i<mvf->num; i++) {
1412    vMdd = array_fetch(mdd_t *, mvf, i);
1413    if(mdd_equal(vMdd, rMdd)) {
1414      needProcess = 1;
1415    }
1416    else {
1417      lIndex = i;
1418    }
1419  }
1420  if(needProcess) {
1421    for(i=0; i<lIndex; i++) {
1422      vMdd = array_fetch(mdd_t *, mvf, i);
1423      tMdd = mdd_or(vMdd, rMdd, 1, 1);
1424      mdd_free(rMdd);
1425      rMdd = tMdd;
1426    }
1427    vMdd = array_fetch(mdd_t *, mvf, lIndex);
1428    mdd_free(vMdd);
1429    tMdd = mdd_not(rMdd);
1430    mdd_free(rMdd);
1431    array_insert(mdd_t *, mvf, lIndex, tMdd);
1432  }
1433  else {
1434    mdd_free(rMdd);
1435  }
1436
1437  return mvf;
1438}
1439
1440
1441/**Function********************************************************************
1442
1443  Synopsis    [Prints the integers from a symbol table.]
1444
1445  Description [Prints the integers from a symbol table.]
1446
1447  SideEffects []
1448
1449******************************************************************************/
1450static void
1451PrintPartitionRecursively(vertex_t *vertex, st_table *vertexTable, int
1452                          indent)
1453{
1454  int i;
1455  lsList faninEdges;
1456  lsGen gen;
1457  vertex_t *faninVertex;
1458  edge_t *faninEdge;
1459 
1460  if (st_is_member(vertexTable, (char *)vertex)) return;
1461  st_insert(vertexTable, (char *)vertex, NIL(char));
1462  for(i=0; i<= indent; i++) fprintf(vis_stdout," ");
1463  fprintf(vis_stdout,"%s %d\n", Part_VertexReadName(vertex),
1464          Part_VertexReadMddId(vertex)); 
1465  faninEdges = g_get_in_edges(vertex);
1466  if (lsLength(faninEdges) == 0) return;
1467  lsForEachItem(faninEdges, gen, faninEdge){
1468    faninVertex = g_e_source(faninEdge);
1469    PrintPartitionRecursively(faninVertex, vertexTable,indent+2);
1470  }
1471}
1472
Note: See TracBrowser for help on using the repository browser.