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

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

vis2.3

File size: 49.0 KB
Line 
1/**CFile************************************************************************
2
3  FileName    [partPart.c]
4
5  PackageName [part]
6
7  Synopsis [Routines to initialize the command <em>build_partition_mdds</em>,
8  create and delete internal data structures of the partition, and print
9  information about the partition.]
10
11  Author      [Abelardo Pardo]
12
13  Copyright   [This file was created at the University of Colorado at
14  Boulder.  The University of Colorado at Boulder makes no warranty
15  about the suitability of this software for any purpose.  It is
16  presented on an AS IS basis.]
17
18******************************************************************************/
19
20#include "partInt.h"
21
22static char rcsid[] UNUSED = "$Id: partPart.c,v 1.45 2009/04/11 01:47:18 fabio Exp $";
23
24/**AutomaticStart*************************************************************/
25
26/*---------------------------------------------------------------------------*/
27/* Static function prototypes                                                */
28/*---------------------------------------------------------------------------*/
29
30static void PrintVertexDescription(FILE *fp, vertex_t *vertexPtr, int order);
31
32/**AutomaticEnd***************************************************************/
33
34/*---------------------------------------------------------------------------*/
35/* Definition of exported functions                                          */
36/*---------------------------------------------------------------------------*/
37
38/**Function********************************************************************
39
40  Synopsis [Deletes the graph created for the partition and all the information
41  attached to it.]
42
43  SideEffects []
44
45  SeeAlso     [PartPartitionInfoFree PartVertexInfoFree]
46
47******************************************************************************/
48void
49Part_PartitionFree(
50   graph_t *partition)
51{
52  /* Delete the graph information */
53  g_free(partition, PartPartitionInfoFree, PartVertexInfoFree,
54         (void (*)(gGeneric))0);
55} /* End of Part_PartitionFree */
56
57
58/**Function********************************************************************
59
60  Synopsis    [Call-back function to free a partition.]
61
62  Description [This function will be stored in the network together with the
63  pointer to the structure. Whenever the network deletes the partitioning
64  information, this function is called and it will deallocate the partition and
65  the information attached to it.]
66
67  SideEffects []
68
69  SeeAlso     [Ntk_NetworkAddApplInfo]
70
71******************************************************************************/
72void
73Part_PartitionFreeCallback(
74   void *data)
75{
76  Part_PartitionFree((graph_t *) data);
77} /* End of Part_PartitionFreeCallback */
78
79/**Function********************************************************************
80
81  Synopsis    [Finds a vertex in the graph with a certain name.]
82
83  Description [Given a name, it returns a pointer to a vertex structure if
84  there is a vertex with that name in the partition. Otherwise it returns a
85  NULL pointer.]
86
87  SideEffects []
88
89  SeeAlso     [PartPartitionInfo]
90
91******************************************************************************/
92vertex_t *
93Part_PartitionFindVertexByName(
94  graph_t *partition,
95  char *name)
96{
97  vertex_t *result = NIL(vertex_t);
98  st_table *table = PartPartitionReadNameToVertex(partition);
99
100  if (table != NIL(st_table)) {
101    st_lookup(table, name, &result);
102  } /* End of if */
103
104  return result;
105} /* End of Part_PartitionFindVertexByName */
106
107/**Function********************************************************************
108
109  Synopsis    [Finds a vertex in the graph with a certain MddId.]
110
111  Description [Given a MddId, it returns a pointer to a vertex structure if
112  there is a vertex with that mddId in the partition. Otherwise it returns a
113  NULL pointer.]
114
115  SideEffects []
116
117  SeeAlso     [PartVertexInfo]
118
119******************************************************************************/
120vertex_t *
121Part_PartitionFindVertexByMddId(
122  graph_t *partition,
123  int mddId)
124{
125  vertex_t *result = NIL(vertex_t);
126  st_table *table = PartPartitionReadMddIdToVertex(partition);
127
128  if (table != NIL(st_table)) {
129    st_lookup(table, (char *)(long)mddId, &result);
130  } /* End of if */
131
132  return result;
133} /* End of Part_PartitionFindVertexByMddId */
134
135/**Function********************************************************************
136
137  Synopsis [Returns the name of the entity from which the partition
138  was created.]
139
140  SideEffects []
141
142  SeeAlso     [PartPartitionInfo]
143
144******************************************************************************/
145char *
146Part_PartitionReadName(
147   graph_t *partition)
148{
149  return PartPartitionReadName(partition);
150} /* End of Part_PartitionReadName */
151
152/**Function********************************************************************
153
154  Synopsis [Returns the method which was used to create the partition graph.]
155
156  SideEffects []
157
158  SeeAlso     [PartPartitionInfo]
159
160******************************************************************************/
161Part_PartitionMethod
162Part_PartitionReadMethod(
163  graph_t *partition)
164{
165  Part_PartitionMethod  method;
166
167  method = PartPartitionReadMethod(partition);
168  if (method == Part_Default_c)
169    method = Part_Frontier_c;
170  return(method);
171} /* End of Part_PartitionReadMethod */
172
173/**Function********************************************************************
174
175  Synopsis    [Returns the partition method as a string.]
176
177  Description [Returns the method stored in the partition as a new
178  string. The caller of the function has the responsibility of freeing
179  the string. The possible values of the string are: "Inputs-Outputs",
180  "Total", "Partial" or "Frontier".]
181
182  SideEffects []
183
184  SeeAlso     [Part_PartitionPrintStats]
185
186******************************************************************************/
187char *
188Part_PartitionObtainMethodAsString(
189  graph_t *partition)
190{
191  char *resultString;
192
193  assert(partition != NIL(graph_t));
194
195  switch(PartPartitionReadMethod(partition)) {
196    case Part_Total_c:
197      resultString = util_strsav("Total");
198      break;
199    case Part_Partial_c:
200      resultString = util_strsav("Partial");
201      break;
202    case Part_InOut_c:
203      resultString = util_strsav("Inputs-Outputs");
204      break;
205    case Part_Frontier_c:
206    case Part_Default_c:
207      resultString = util_strsav("Frontier");
208      break;
209    case Part_Boundary_c:
210      resultString = util_strsav("Boundary");
211      break;
212    case Part_Fine_c:
213      resultString = util_strsav("Fine");
214      break;
215    default:
216      fail("Unexpected Partition method.");
217  }
218
219  return resultString;
220} /* End of Part_PartitionObtainMethodAsString */
221
222/**Function********************************************************************
223
224  Synopsis    [Function to read the manager attached to the partition.]
225
226  SideEffects []
227
228  SeeAlso     [PartPartitionInfo]
229
230******************************************************************************/
231mdd_manager *
232Part_PartitionReadMddManager(
233  graph_t *partition)
234{
235  return PartPartitionReadMddManager(partition);
236} /* End of Part_PartitionReadMddManager */
237
238/**Function********************************************************************
239
240  Synopsis    [Returns the type of a vertex.]
241
242  SideEffects []
243
244  SeeAlso     [PartVertexInfo Part_VertexType]
245
246******************************************************************************/
247Part_VertexType
248Part_VertexReadType(
249  vertex_t *vertexPtr)
250{
251  return PartVertexReadType(vertexPtr);
252} /* End of Part_VertexReadType */
253
254/**Function********************************************************************
255
256  Synopsis    [Reads the name attached to a vertex.]
257
258  SideEffects []
259
260  SeeAlso     [PartVertexInfo]
261
262******************************************************************************/
263char *
264Part_VertexReadName(
265  vertex_t *vertexPtr)
266{
267  return PartVertexReadName(vertexPtr);
268} /* End of Part_VertexReadName */
269
270/**Function********************************************************************
271
272  Synopsis    [Reads the clusterMembers field  of a vertex.]
273
274  Description [This function does not make sure that the vertex is of clustered
275  type. It is the responsibility of the caller to guarantee that.]
276
277  SideEffects []
278
279  SeeAlso     [PartVertexInfo]
280
281******************************************************************************/
282array_t *
283Part_VertexReadClusterMembers(
284  vertex_t *vertexPtr)
285{
286  return PartVertexReadClusterMembers(vertexPtr);
287} /* End of Part_VertexReadClusterMembers */
288
289/**Function********************************************************************
290
291  Synopsis    [Reads the multi-valued function attached to a vertex.]
292
293  Description [This function does not make sure that the vertex is of single
294  type.  It is the responsibility of the caller to guarantee that.]
295
296  SideEffects []
297
298  SeeAlso     [PartVertexInfo]
299
300******************************************************************************/
301Mvf_Function_t *
302Part_VertexReadFunction(
303  vertex_t *vertexPtr)
304{
305    return PartVertexReadFunction(vertexPtr);
306} /* End of Part_VertexReadFunction */
307
308
309/**Function********************************************************************
310
311  Synopsis    [Sets the multi-valued function of a vertex.]
312
313  SideEffects []
314
315  SeeAlso     [PartVertexInfo]
316
317******************************************************************************/
318void
319Part_VertexSetFunction(
320  vertex_t *vertexPtr,
321  Mvf_Function_t *mvf)
322{
323  assert(PartVertexReadType(vertexPtr) != Part_VertexCluster_c);
324
325  PartVertexSetFunction(vertexPtr, mvf);
326} /* End of Part_VertexSetFunction */
327
328
329/**Function********************************************************************
330
331  Synopsis    [Reads the MddId attached to a vertex.]
332
333  SideEffects []
334
335  SeeAlso     [PartVertexInfo]
336
337******************************************************************************/
338int
339Part_VertexReadMddId(
340  vertex_t *vertexPtr)
341{
342    return PartVertexReadMddId(vertexPtr);
343} /* End of Part_VertexReadMddId */
344
345/**Function********************************************************************
346
347  Synopsis    [Test of a vertex is member of a cluster.]
348
349  SideEffects []
350
351  SeeAlso     [PartVertexInfo Part_VertexReadType]
352
353******************************************************************************/
354boolean
355Part_VertexTestIsClustered(
356  vertex_t *vertexPtr)
357{
358  return PartVertexTestIsClustered(vertexPtr);
359} /* End of Part_VertexTestIsClustered */
360
361/**Function********************************************************************
362
363  Synopsis    [Executes the selected partitioning method.]
364
365  Description [Given a network, and a method, the function creates a partition
366  by using the specified method. This function may be called from any point in
367  the code to create a partition.  In particular, the command partition uses
368  this function to create the partition and store it in the network.<p>
369
370  The function receives two lists of pointers to network nodes, the roots and
371  the leaves. The function will create the partition of the subnetwork between
372  the root and the leave nodes. As a special case, if both lists are passed NIL
373  values, the root and leave lists default to combinational outputs and
374  combinational inputs respectively.
375
376  The parameter <tt>careSet</tt> specifies which minterms in the input space are
377  considered.
378
379  The <tt>nodes</tt> parameter is an optional list of nodes that may be
380  specified in case the <tt>partial</tt> method is used. It represents the set
381  of nodes in the network to be preserved when building the partition. The
382  boolean variable <tt>inTermsOfLeaves</tt> is valid only in the case of
383  the <tt>total</tt> method and provides the option of creating the functions
384  attached to the vertices in terms of the combinational inputs or in terms of
385  their immediate fanin.  Two additional parameters are provided to control the
386  verbosity and the intensity of the sanity check applied to the computation.<p>
387
388  This function is called by the command build_partition_mdds which has a
389  time-out option.  In the event of the execution time going over the time out,
390  the control is returned to the prompt and all the memory allocated by the
391  internal procedures is leaked.]
392
393  SideEffects []
394
395  SeeAlso     [part.h]
396
397******************************************************************************/
398graph_t *
399Part_NetworkCreatePartition(
400  Ntk_Network_t *network,
401  Hrc_Node_t *hnode,
402  char *name,
403  lsList rootList,
404  lsList leaveList,
405  mdd_t *careSet,
406  Part_PartitionMethod method,
407  lsList nodes,
408  boolean inTermsOfLeaves,
409  int verbose,
410  int sanityCheck)
411{
412  graph_t    *partition;
413  long       lap = 0;
414
415  if (verbose) {
416    lap = util_cpu_time();
417  } /* End of if */
418
419  /* Create the new graph to represent the partition */
420  partition = g_alloc();
421  partition->user_data =
422    (gGeneric)PartPartitionInfoCreate(name,
423                                      Ntk_NetworkReadMddManager(network),
424                                      method);
425
426  switch (method) {
427    case Part_Partial_c:
428      if (verbose) {
429        (void) fprintf(vis_stdout, "Partitioning the system by the Partial");
430        (void) fprintf(vis_stdout, " method\n");
431      } /* End of if */
432      PartPartitionPartial(network, partition, rootList, leaveList, careSet,
433                           nodes, inTermsOfLeaves);
434      break;
435    case Part_Boundary_c:
436      if (verbose) {
437        (void) fprintf(vis_stdout, "Partitioning the system by the Boundary");
438        (void) fprintf(vis_stdout, " method\n");
439      } /* End of if */
440      PartPartitionBoundary(network, hnode, partition, rootList, leaveList, careSet,
441                           inTermsOfLeaves);
442      break;
443    case Part_Total_c:
444      if (verbose) {
445        (void) fprintf(vis_stdout, "Partitioning the circuit by the Total");
446        (void) fprintf(vis_stdout, " method\n");
447      } /* End of if */
448      PartPartitionTotal(network, partition, rootList, leaveList, careSet,
449                         inTermsOfLeaves);
450      break;
451    case Part_Frontier_c:
452    case Part_Default_c:
453      if (verbose) {
454        (void) fprintf(vis_stdout, "Partitioning the circuit by the Frontier");
455        (void) fprintf(vis_stdout, " method\n");
456      } /* End of if */
457      PartPartitionFrontier(network, partition, rootList, leaveList, careSet);
458      break;
459    case Part_Fine_c:
460      if (verbose) {
461        (void) fprintf(vis_stdout, "Partitioning the circuit for the fine-grain");
462        (void) fprintf(vis_stdout, " method\n");
463      } /* End of if */
464      PartPartitionFineGrain(network, partition, careSet);
465      break;
466    case Part_InOut_c:
467      if (verbose) {
468        (void) fprintf(vis_stdout, "Partitioning the circuit by the");
469        (void) fprintf(vis_stdout, " Input-Output method\n");
470      } /* End of if */
471      PartPartitionInputsOutputs(network, partition, rootList,
472                                 leaveList, careSet);
473      break;
474    default:
475      (void) fprintf(vis_stdout, "Partition method not implemented yet\n");
476      break;
477  }
478
479  if (sanityCheck >0) {
480    PartPartitionSanityCheck(partition, sanityCheck);
481  }
482
483  if (verbose) {
484    (void) fprintf(vis_stdout, "%.2f (secs) spent in partitioning.\n",
485                   (util_cpu_time() - lap)/1000.0);
486  } /* End of if */
487
488  return partition;
489} /* End of Part_NetworkCreatePartition */
490
491/**Function********************************************************************
492
493  Synopsis    [Creates a duplicate of a partition.]
494
495  SideEffects []
496
497  SeeAlso     [PartVertexInfo, PartPartitionInfo]
498
499******************************************************************************/
500graph_t *
501Part_PartitionDuplicate(
502  graph_t *partition)
503{
504  graph_t          *result;
505  lsGen            gen;
506  vertex_t         *fromVertex;
507  vertex_t         *toVertex;
508  edge_t           *edgePtr;
509
510  result = g_alloc();
511  result->user_data =
512    (gGeneric)PartPartitionInfoCreate(PartPartitionReadName(partition),
513                                      PartPartitionReadMddManager(partition),
514                                      PartPartitionReadMethod(partition));
515  foreach_vertex(partition, gen, fromVertex) {
516    char *name;
517    int  mddId;
518
519    name = PartVertexReadName(fromVertex);
520    mddId = PartVertexReadMddId(fromVertex);
521    toVertex = g_add_vertex(result);
522
523    st_insert(PartPartitionReadNameToVertex(result), name, (char *)toVertex);
524
525    if (mddId != NTK_UNASSIGNED_MDD_ID) {
526      st_insert(PartPartitionReadMddIdToVertex(result), (char *)(long)mddId,
527                (char *)toVertex);
528    } /* End of if */
529
530    if (PartVertexReadType(fromVertex) == Part_VertexSingle_c) {
531      Mvf_Function_t *mdd;
532
533      mdd = Mvf_FunctionDuplicate(PartVertexReadFunction(fromVertex));
534      toVertex->user_data = (gGeneric)PartVertexInfoCreateSingle(name, mdd,
535                                                                 mddId);
536    }
537    if (PartVertexReadType(fromVertex) == Part_VertexCluster_c) {
538      toVertex->user_data =
539        (gGeneric)PartVertexInfoCreateCluster(name, Part_VertexReadClusterMembers(fromVertex));
540    }
541  }
542
543  foreach_edge(partition, gen, edgePtr) {
544    vertex_t *fromVertexCopy;
545    vertex_t *toVertexCopy;
546
547    fromVertex = g_e_source(edgePtr);
548    toVertex = g_e_dest(edgePtr);
549
550    st_lookup(PartPartitionReadNameToVertex(result),
551              PartVertexReadName(fromVertex), &fromVertexCopy);
552    st_lookup(PartPartitionReadNameToVertex(result),
553              PartVertexReadName(toVertex), &toVertexCopy);
554
555    g_add_edge(fromVertexCopy, toVertexCopy);
556  }
557
558  return result;
559} /* End of Part_PartitionDuplicate */
560
561
562/**Function********************************************************************
563
564  Synopsis    [Create reduced partition according to given CTL formulae]
565
566  Comments    [Combinational root and leave nodes are combinational support
567  nodes of given CTL properties.]
568
569  SideEffects []
570
571  SeeAlso     []
572
573******************************************************************************/
574graph_t *
575Part_PartCreatePartitionWithCTL(
576  Hrc_Manager_t **hmgr,
577  Part_PartitionMethod method,
578  int verbose,
579  int sanityCheck,
580  boolean inTermsOfLeaves,
581  array_t *ctlArray,
582  array_t *fairArray)
583{
584  return Part_PartCreatePartitionWithCtlAndLtl(hmgr, method, verbose,
585                                               sanityCheck, inTermsOfLeaves,
586                                               ctlArray, NIL(array_t),
587                                               fairArray);
588}
589
590/**Function********************************************************************
591
592  Synopsis    [Create reduced partition according to given CTL formulae]
593
594  Comments    [Combinational root and leave nodes are combinational support
595  nodes of given CTL properties.]
596
597  SideEffects []
598
599  SeeAlso     []
600
601******************************************************************************/
602graph_t *
603Part_PartCreatePartitionWithCtlAndLtl(
604  Hrc_Manager_t **hmgr,
605  Part_PartitionMethod method,
606  int verbose,
607  int sanityCheck,
608  boolean inTermsOfLeaves,
609  array_t *ctlArray,
610  array_t *ltlArray,
611  array_t *fairArray)
612{
613  char          *modelName;
614  Hrc_Node_t    *currentNode;
615  graph_t       *partition;
616  lsList        latchInputList;
617  lsGen         gen;
618  Ntk_Node_t    *node;
619  Ntk_Network_t *network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
620
621  latchInputList = lsCreate();
622  currentNode = Hrc_ManagerReadCurrentNode(*hmgr);
623  modelName = Hrc_NodeReadModelName(currentNode);
624
625  if (method != Part_InOut_c){
626    return NIL(graph_t);
627  }
628
629  PartGetLatchInputListFromCtlAndLtl(network, ctlArray, ltlArray, fairArray,
630                                     latchInputList, FALSE);
631
632  Ntk_NetworkForEachCombOutput(network, gen, node){
633    if (Ntk_NodeTestIsLatchInitialInput(node)){
634      lsNewEnd(latchInputList, (lsGeneric)node, LS_NH);
635    }
636  }
637
638  /*
639   * Execute the partition algorithm. If rootList and leaveList are null,
640   * graph includes all network nodes
641   */
642  partition = Part_NetworkCreatePartition(network, currentNode, modelName,
643                 latchInputList, (lsList)0, NIL(mdd_t), method, (lsList)0,
644                 inTermsOfLeaves, verbose, sanityCheck);
645
646  lsDestroy(latchInputList, (void (*)(lsGeneric))0);
647  return partition;
648}
649
650
651/**Function********************************************************************
652
653  Synopsis    [Change partition to include new vertex in root list]
654
655  Comments    [Current partition in increased to include all next state
656  functions for all members in rootList.]
657
658  SideEffects []
659
660  SeeAlso     []
661
662******************************************************************************/
663int
664Part_PartitionChangeRoots(
665  Ntk_Network_t *network,
666  graph_t *partition,
667  lsList  rootList,
668  int verbosity)
669{
670  if (Part_PartitionReadMethod(partition) != Part_InOut_c){
671    return 0;
672  }
673
674  return
675   PartPartitionInOutChangeRoots(network, partition, rootList, verbosity);
676}
677
678
679/**Function********************************************************************
680
681  Synopsis    [Reads the partition attached to a network.]
682
683  SideEffects []
684
685  SeeAlso     [CommandBuildPartitionMdds]
686
687******************************************************************************/
688graph_t *
689Part_NetworkReadPartition(
690  Ntk_Network_t *network)
691{
692  return (graph_t *)Ntk_NetworkReadApplInfo(network, PART_NETWORK_APPL_KEY);
693} /* End of Part_NetworkReadPartition */
694
695
696/**Function********************************************************************
697
698  Synopsis    [Adds a vertex to the partition representing a set of vertices.]
699
700  SideEffects []
701
702  SeeAlso     [PartVertexInfo]
703
704******************************************************************************/
705vertex_t *
706Part_PartitionCreateClusterVertex(
707  graph_t *partition,
708  char *name,
709  array_t *arrayOfVertices)
710{
711  vertex_t *newVertex;
712
713  newVertex = g_add_vertex(partition);
714  newVertex->user_data = (gGeneric)PartVertexInfoCreateCluster(name,
715                                                               arrayOfVertices);
716
717  return(newVertex);
718
719} /* End of Part_PartitionCreateClusterVertex */
720
721/**Function********************************************************************
722
723  Synopsis    [ Partition by adding vertices for the nodes in rootList
724  and leaveList.  A node in leaveList may already have a corresponding
725  vertex in the partition graph -- Only creating the new vertex if not exists.
726  Nodes in rootList should NOT have existing vertices in the partition graph.
727  (The caller should guarantee this)
728
729  This routine is for the use in the 'ltl' package. We assume the partition
730  method is Part_Frontier_c.]
731
732  SideEffects [partition might be changed.]
733
734  SeeAlso     [PartPartitionFrontier]
735
736******************************************************************************/
737void
738Part_UpdatePartitionFrontier(
739  Ntk_Network_t *network,
740  graph_t *partition,
741  lsList  rootList,
742  lsList  leaveList,
743  mdd_t   *careSet)
744{
745  PartUpdateFrontier(network, partition, rootList, leaveList, careSet);
746}
747
748/**Function********************************************************************
749
750  Synopsis    [Removes a cluster vertex from the partition.]
751
752  SideEffects []
753
754  SeeAlso     [PartVertexInfo]
755
756******************************************************************************/
757void
758Part_VertexInfoFreeCluster(
759  vertex_t *vertexPtr)
760{
761  if (PartVertexReadType(vertexPtr) == Part_VertexCluster_c) {
762    g_delete_vertex(vertexPtr, PartVertexInfoFree, (void (*)(gGeneric))0);
763  } /* End of then */
764  else {
765    (void) fprintf(vis_stderr, "Warning -- Inconsistent vertex deletion in");
766    (void) fprintf(vis_stderr, " partition package\n");
767  }
768} /* End of Part_VertexInfoFreeCluster */
769
770/**Function********************************************************************
771
772  Synopsis [Test if the functions attached to a set of vertices in the
773  partition are completely specified.]
774
775  Description [Given a set of vertices (roots) build their functions in terms
776  of a second set of vertices (leaves) and test if the functions are
777  completely specified.]
778
779  SideEffects []
780
781  SeeAlso     [Part_PartitionTestDeterministic]
782
783******************************************************************************/
784boolean
785Part_PartitionTestCompletelySp(
786  graph_t *partition,
787  array_t *roots,
788  st_table *leaves)
789{
790  array_t *mvfFunctions;
791  vertex_t *vertexPtr;
792  Mvf_Function_t *functionPtr;
793  boolean result = TRUE;
794  int i;
795  char *vertexName;
796
797  mvfFunctions = Part_PartitionCollapse(partition, roots, leaves, NIL(mdd_t));
798
799  arrayForEachItem(Mvf_Function_t *, mvfFunctions, i, functionPtr) {
800    vertexPtr = array_fetch(vertex_t *, roots, i);
801    vertexName = PartVertexReadName(vertexPtr);
802    if (!Mvf_FunctionTestIsCompletelySpecified(functionPtr)) {
803      error_append("Vertex ");
804      error_append(vertexName);
805      error_append(" is not completely specified\n");
806      result = FALSE;
807    } /* End of if */
808
809    /* We don't need the Mvf_Function any more, so we delete it */
810    Mvf_FunctionFree(functionPtr);
811  }
812
813  /* Clean up*/
814  array_free(mvfFunctions);
815
816  return result;
817} /* End of Part_PartitionTestCompletelySp */
818
819/**Function********************************************************************
820
821  Synopsis    [Test if the functions attached to a set of vertices in the
822  partition are deterministic.]
823
824  Description [Given a set of vertices (roots) build their functions in terms
825  of a second set of vertices (leaves) and test if the functions are
826  deterministic.]
827
828  SideEffects []
829
830  SeeAlso     [Part_PartitionTestCompletelySp]
831
832******************************************************************************/
833boolean
834Part_PartitionTestDeterministic(
835  graph_t *partition,
836  array_t *roots,
837  st_table *leaves)
838{
839  array_t *mvfFunctions;
840  vertex_t *vertexPtr;
841  Mvf_Function_t *functionPtr;
842  boolean result = TRUE;
843  int i;
844  char *vertexName;
845
846  mvfFunctions = Part_PartitionCollapse(partition, roots, leaves, NIL(mdd_t));
847
848  arrayForEachItem(Mvf_Function_t *, mvfFunctions, i, functionPtr) {
849    vertexPtr = array_fetch(vertex_t *, roots, i);
850    vertexName = PartVertexReadName(vertexPtr);
851    if (!Mvf_FunctionTestIsDeterministic(functionPtr)) {
852      error_append("Vertex ");
853      error_append(vertexName);
854      error_append(" is non-deterministic\n");
855      result = FALSE;
856    } /* End of if */
857
858    /* We don't need the Mvf_Function any more, so we delete it */
859    Mvf_FunctionFree(functionPtr);
860  }
861
862  /* Clean up*/
863  array_free(mvfFunctions);
864
865  return result;
866} /* End of Part_PartitionTestDeterministic */
867
868/**Function********************************************************************
869
870  Synopsis    [Create latch input nodes list from CTL properties and fairness
871  constraints]
872
873  Comments    []
874
875  SideEffects [latchInputList is changed]
876
877  SeeAlso     []
878
879******************************************************************************/
880int
881Part_PartitionGetLatchInputListFromCTL(
882  Ntk_Network_t *network,
883  array_t *ctlArray,
884  array_t *fairArray,
885  lsList  latchInputList)
886{
887  return PartGetLatchInputListFromCTL( network, ctlArray, fairArray,
888                                       latchInputList);
889}
890
891/**Function********************************************************************
892
893  Synopsis    [Create latch input nodes list from CTL properties and fairness
894  constraints]
895
896  Comments    []
897
898  SideEffects [latchInputList is changed]
899
900  SeeAlso     []
901
902******************************************************************************/
903int
904Part_PartitionGetLatchInputListFromCtlAndLtl(
905  Ntk_Network_t *network,
906  array_t *ctlArray,
907  array_t *ltlArray,
908  array_t *fairArray,
909  lsList  latchInputList,
910  boolean stopAtLatch)
911{
912  return PartGetLatchInputListFromCtlAndLtl( network, ctlArray, ltlArray,
913                                             fairArray,
914                                             latchInputList, stopAtLatch);
915}
916
917/**Function********************************************************************
918
919  Synopsis    [Prints statistics about the partition DAG.]
920
921  Comments    [If the parameter printNodeNames is true, the function prints
922  names of the network nodes represented by vertices in the partition graph.]
923
924  SideEffects []
925
926  SeeAlso     [PartPartitionInfo]
927
928******************************************************************************/
929void
930Part_PartitionPrintStats(
931  FILE *fp,
932  graph_t *partition,
933  boolean printNodeNames)
934{
935  lsList vertexList = g_get_vertices(partition);
936  vertex_t *vertexPtr;
937  array_t *functions;
938  Mvf_Function_t* vertexFunction;
939  mdd_t *mddPtr;
940  lsGen gen;
941  char *methodName;
942  int numVertices = lsLength(vertexList);
943  int numSources;
944  int numSinks;
945  int i;
946
947  /* Obtain the method name as a string */
948  methodName = Part_PartitionObtainMethodAsString(partition);
949
950  /*
951   * Count the number of sources and sinks and at the same time store all the
952   * bdd_t of every vertex in a common array to compute the shared size.
953   */
954  numSources = 0;
955  numSinks = 0;
956  functions = array_alloc(mdd_t *, 0);
957  if (printNodeNames) {
958    (void) fprintf(fp, "Network nodes represented as vertices in the ");
959    (void) fprintf(fp, "partition:\n");
960  }
961  foreach_vertex(partition, gen, vertexPtr) {
962    if (lsLength(g_get_in_edges(vertexPtr)) == 0) {
963      numSources++;
964    } /* End of if */
965    if (lsLength(g_get_out_edges(vertexPtr)) == 0) {
966      numSinks++;
967    } /* End of if */
968    if (PartVertexReadType(vertexPtr) == Part_VertexSingle_c) {
969      if (printNodeNames) {
970        if (PartVertexReadName(vertexPtr) != NIL(char)) {
971          (void) fprintf(fp, "%s\n", PartVertexReadName(vertexPtr));
972        }
973      }
974      vertexFunction = PartVertexReadFunction(vertexPtr);
975      if (vertexFunction != NIL(Mvf_Function_t)) {
976        Mvf_FunctionForEachComponent(vertexFunction, i, mddPtr) {
977          array_insert_last(mdd_t *, functions, mddPtr);
978        }
979      } /* End of if */
980    } /* End of if */
981  } /* foreach_vertex*/
982
983  /* Print results */
984  (void)fprintf(fp, "Method %s, %d sinks, %d sources,", methodName, numSinks, numSources);
985  (void)fprintf(fp, " %d total vertices,", numVertices);
986  (void)fprintf(fp, " %ld mdd nodes\n", bdd_size_multiple(functions));
987
988  /* Clean up */
989  FREE(methodName);
990  array_free(functions);
991
992  return;
993} /* End of Part_PartitionPrintStats */
994
995/*---------------------------------------------------------------------------*/
996/* Definition of internal functions                                          */
997/*---------------------------------------------------------------------------*/
998
999/**Function********************************************************************
1000
1001  Synopsis [Initializes the information attached to the graph of the
1002  partition.]
1003
1004  Description [Allocates the memory needed for the information attached to the
1005  graph structure.]
1006
1007  SideEffects []
1008
1009  SeeAlso     [PartPartitionInfo PartPartitionInfoFree]
1010
1011******************************************************************************/
1012PartPartitionInfo_t *
1013PartPartitionInfoCreate(
1014  char *name,
1015  mdd_manager *manager,
1016  Part_PartitionMethod method)
1017{
1018  PartPartitionInfo_t *recordPartition = ALLOC(PartPartitionInfo_t, 1);
1019
1020  recordPartition->name          = util_strsav(name);
1021  recordPartition->method        = method;
1022  recordPartition->mddManager    = manager;
1023  recordPartition->nameToVertex  = st_init_table(strcmp,st_strhash);
1024  recordPartition->mddIdToVertex = st_init_table(st_numcmp, st_numhash);
1025
1026  return recordPartition;
1027} /* End of PartPartitionInfoCreate */
1028
1029/**Function********************************************************************
1030
1031  Synopsis [Deallocates the user information in the graph.]
1032
1033  Description [Deallocates the user information in the graph. Does not free the
1034  MDD manager associated with the partition.]
1035
1036  SideEffects []
1037
1038  SeeAlso     [PartPartitionInfoCreate]
1039
1040******************************************************************************/
1041void
1042PartPartitionInfoFree(
1043  gGeneric partitionInfo)
1044{
1045  if (((PartPartitionInfo_t *)partitionInfo)->name != NIL(char)) {
1046    FREE(((PartPartitionInfo_t *)partitionInfo)->name);
1047  }
1048
1049  st_free_table(((PartPartitionInfo_t *)partitionInfo)->nameToVertex);
1050  st_free_table(((PartPartitionInfo_t *)partitionInfo)->mddIdToVertex);
1051
1052  FREE(partitionInfo);
1053} /* End of PartPartitionInfoFree */
1054
1055/**Function********************************************************************
1056
1057  Synopsis [Initializes the information attached to a single vertex.]
1058
1059  SideEffects []
1060
1061  SeeAlso     [PartVertexInfo]
1062
1063******************************************************************************/
1064PartVertexInfo_t *
1065PartVertexInfoCreateSingle(
1066  char *name,
1067  Mvf_Function_t *mvf,
1068  int mddId)
1069{
1070  PartVertexInfo_t *result;
1071
1072  result                    = ALLOC(PartVertexInfo_t, 1);
1073  result->type              = Part_VertexSingle_c;
1074  result->name              = util_strsav(name);
1075  result->functionality.mvf = mvf;
1076  result->mddId             = mddId;
1077  result->isClustered       = 0;
1078
1079  return result;
1080} /* End of PartVertexInfoCreateSingle */
1081
1082/**Function********************************************************************
1083
1084  Synopsis    [Creates a cluster vertex in the partition.]
1085
1086  SideEffects []
1087
1088  SeeAlso     [PartVertexInfo]
1089
1090******************************************************************************/
1091PartVertexInfo_t *
1092PartVertexInfoCreateCluster(
1093  char *name,
1094  array_t *vertexArray)
1095{
1096  PartVertexInfo_t *result;
1097  vertex_t *auxPtr;
1098  int i;
1099
1100  /* Make sure all the nodes are simple nodes */
1101  for(i = 0; i < array_n(vertexArray); i++) {
1102    auxPtr = array_fetch(vertex_t *, vertexArray, i);
1103    if (PartVertexReadType(auxPtr) == Part_VertexCluster_c) {
1104      fail("Only one level of hierarchy allowed in the partition");
1105    } /* End of if */
1106    if (PartVertexTestIsClustered(auxPtr)) {
1107      fail("Partition: Clustering vertex already member of another cluster");
1108    } /* End of then */
1109    else {
1110      PartVertexSetIsClustered(auxPtr, 1);
1111    }
1112  } /* End of for */
1113
1114  result                               = ALLOC(PartVertexInfo_t, 1);
1115  result->type                         = Part_VertexCluster_c;
1116  result->name                         = util_strsav(name);
1117  result->functionality.clusterMembers = array_dup(vertexArray);
1118
1119  result->mddId                        = NTK_UNASSIGNED_MDD_ID;
1120  result->isClustered                  = 0;
1121
1122  return result;
1123} /* End of PartVertexInfoCreateCluster */
1124
1125/**Function********************************************************************
1126
1127  Synopsis [Deallocates the user information attached to a vertex.]
1128
1129  SideEffects []
1130
1131  SeeAlso     [PartVertexInfo]
1132
1133******************************************************************************/
1134void
1135PartVertexInfoFree(
1136  gGeneric vertexInfo
1137   )
1138{
1139  if (((PartVertexInfo_t *)vertexInfo)->type == Part_VertexSingle_c) {
1140    /* Free the function attached to the node if any */
1141    if (((PartVertexInfo_t *)vertexInfo)->functionality.mvf !=
1142        NIL(Mvf_Function_t)) {
1143      Mvf_FunctionFree(((PartVertexInfo_t *)vertexInfo)->functionality.mvf);
1144    } /* End of if */
1145  } /* End of then */
1146  else {
1147    if (((PartVertexInfo_t *)vertexInfo)->functionality.clusterMembers !=
1148        NIL(array_t)) {
1149      array_free(((PartVertexInfo_t *)vertexInfo)->functionality.clusterMembers);
1150    } /* End of if */
1151  } /* End of if-then-else */
1152
1153  if (((PartVertexInfo_t *)vertexInfo)->name != NIL(char)) {
1154    FREE(((PartVertexInfo_t *)vertexInfo)->name);
1155  }
1156
1157  FREE(vertexInfo);
1158} /* End of PartVertexInfoFree */
1159
1160/**Function********************************************************************
1161
1162  Synopsis [Verifies that the information in the nameToVertex table of
1163  a graph is consistent.]
1164
1165  SideEffects []
1166
1167  SeeAlso     [PartPartitionInfo]
1168
1169******************************************************************************/
1170void
1171PartPartitionSanityCheck(
1172  graph_t *partition,
1173  int intensity)
1174{
1175  st_table *table;
1176  lsList vertexList = g_get_vertices(partition);
1177  lsGen lgen;
1178  vertex_t *vertex, *rvertex;
1179
1180  /* Consistency in the nameToVertex table */
1181  table = PartPartitionReadNameToVertex(partition);
1182
1183  /*
1184   * The number of elements in the nameToVertex table and the number
1185   * of vertices agrees
1186   */
1187  if (lsLength(g_get_vertices(partition)) != st_count(table)) {
1188    (void) fprintf(vis_stderr, "Warning -- NameToVertex table incomplete in ");
1189    (void) fprintf(vis_stderr, " graph\n");
1190    if (intensity > 1) {
1191      (void) fprintf(vis_stderr, "  %d vertices in the graph and %d entries",
1192                     lsLength(g_get_vertices(partition)),
1193                     st_count(table));
1194      (void) fprintf(vis_stderr, " in the nameToVertex table\n");
1195    } /* End of if */
1196  } /* End of if */
1197
1198  lsForEachItem(vertexList, lgen, vertex) {
1199    char *name = PartVertexReadName(vertex);
1200    if (!st_lookup(table, name, &rvertex) ||
1201        strcmp(PartVertexReadName(vertex),PartVertexReadName(rvertex)) != 0) {
1202      (void) fprintf(vis_stderr, "Warning -- Inconsistency detected in");
1203      (void) fprintf(vis_stderr, " the partition data-base\n");
1204    }
1205  }
1206
1207  /* Consistency in the mddIdToVertexTable */
1208  table = PartPartitionReadMddIdToVertex(partition);
1209  lsForEachItem(vertexList, lgen, vertex) {
1210    int mddId = PartVertexReadMddId(vertex);
1211    if((mddId != NTK_UNASSIGNED_MDD_ID) &&
1212       (!st_lookup(table, (char *)(long)mddId, &rvertex) ||
1213        PartVertexReadMddId(vertex) != PartVertexReadMddId(rvertex))) {
1214      (void) fprintf(vis_stderr, "Warning -- Inconsistency detected in the");
1215      (void) fprintf(vis_stderr, " partition data-base\n");
1216    }
1217  }
1218
1219  /*
1220   * Make sure that the mdd Id NTK_UNASSIGNED_MDD_ID does not appear in the
1221   * mddIdToVertex node.
1222   */
1223  table = PartPartitionReadMddIdToVertex(partition);
1224  if (st_is_member(table, (char *) NTK_UNASSIGNED_MDD_ID)) {
1225    (void) fprintf(vis_stderr, "Warning -- Inconsistency detected in the");
1226    (void) fprintf(vis_stderr, " partition data-base\n");
1227  } /* End of if */
1228
1229  /* Check the Mvfs in the vertices of the partition.*/
1230  if (intensity > 1) {
1231    lsForEachItem(vertexList, lgen, vertex) {
1232      Mvf_Function_t *function = PartVertexReadFunction(vertex);
1233      int i;
1234
1235      (void) fprintf(vis_stderr, "Vertex: %s, mddId: %d, Clustered: %c\n",
1236                     PartVertexReadName(vertex),
1237                     PartVertexReadMddId(vertex),
1238                     (PartVertexReadType(vertex) == Part_VertexCluster_c)?'t':'f');
1239      for(i = 0; i < Mvf_FunctionReadNumComponents(function); i ++) {
1240        mdd_t *unit = Mvf_FunctionObtainComponent(function, i);
1241        boolean x;
1242
1243        if (intensity > 2) {
1244          (void) fprintf(vis_stderr, "BDD_T: %lx, %lx\n",
1245                         (unsigned long) bdd_get_node(unit, &x),
1246                         (unsigned long) mdd_get_manager(unit));
1247        }
1248      } /* End of for */
1249    }
1250  } /* End of if */
1251
1252  /* ToDo: Check for redundant name in the list of vertices */
1253} /* End of PartPartitionSanityCheck */
1254
1255/**Function********************************************************************
1256
1257  Synopsis    [Computes the support of an array of mdds.]
1258
1259  Description [Computes the support of a multi-valued function. It is
1260  just the union of the supports of every component of the function.]
1261
1262  Comment [The reason why is it returned in a table is because it's very likely
1263  that questions such as, "is certain Id part of the support ?"  will happen.]
1264
1265  SideEffects []
1266
1267  SeeAlso     [PartVertexCreateFaninEdges]
1268
1269******************************************************************************/
1270st_table *
1271PartCreateFunctionSupportTable(
1272  Mvf_Function_t *mvf)
1273{
1274  mdd_manager  *mddManager;        /* Manager for the MDDs */
1275  array_t      *support;
1276  st_table     *mddSupport = st_init_table(st_numcmp, st_numhash);
1277  int          numComponents = Mvf_FunctionReadNumComponents(mvf);
1278  int          j, k;
1279  mdd_t        *unit;
1280
1281  assert(numComponents!= 0);
1282
1283  mddManager = Mvf_FunctionReadMddManager(mvf);
1284
1285  /*
1286   * compute the support of an mdd as the union of supports of every
1287   * function component
1288   */
1289  for(j = 0; j < numComponents; j++) {
1290    unit = Mvf_FunctionReadComponent(mvf, j);
1291    support = mdd_get_support(mddManager, unit);
1292
1293    /* For every element of its support */
1294    for(k = 0; k < array_n(support); k++) {
1295      st_insert(mddSupport, (char *)(long)array_fetch(int, support, k), (char *)0);
1296    } /* End of for */
1297    array_free(support);
1298  } /* End of for */
1299
1300  return mddSupport;
1301} /* End of PartCreateFunctionSupportTable */
1302
1303/**Function********************************************************************
1304
1305  Synopsis [Creates fanin edges of a vertex based on MDD support.]
1306
1307  Description [Computes the support of the function attached to a vertex and
1308  adds to the graph the edges from the vertices representing those variables
1309  to the given vertex.]
1310
1311  SideEffects []
1312
1313******************************************************************************/
1314void
1315PartPartitionCreateVertexFaninEdges(
1316  graph_t  *partition,
1317  vertex_t *vertexPtr)
1318{
1319  vertex_t       *fromVertex;
1320  Mvf_Function_t *vertexFunction;
1321  st_table       *support;
1322  st_table       *mddIdToVertex;
1323  st_generator   *stGen;
1324  long            mddId;
1325
1326  mddIdToVertex = PartPartitionReadMddIdToVertex(partition);
1327  vertexFunction = PartVertexReadFunction(vertexPtr);
1328  support = PartCreateFunctionSupportTable(vertexFunction);
1329
1330  /* Create the edges for every element in support */
1331  st_foreach_item(support, stGen, &mddId, NULL) {
1332    st_lookup(mddIdToVertex, (char *)mddId, &fromVertex);
1333    /* Make sure no self loops are created */
1334    if (fromVertex != vertexPtr) {
1335      g_add_edge(fromVertex, vertexPtr);
1336    } /* End of if */
1337  }
1338
1339  st_free_table(support);
1340} /* End of PartPartitionCreateVertexFaninEdges */
1341
1342/**Function********************************************************************
1343
1344  Synopsis [Prints information about the Partition through standard output.]
1345
1346  Description [ The format used for printing is <b>dot</b>, a tool for
1347  graph visualization developed at AT&T. It can be obtained from <a
1348  href="http://www.research.att.com/orgs/ssr/book/reuse">
1349  http://www.research.att.com/orgs/ssr/book/reuse</a>. The function
1350  receives as a parameter a file pointer in case the print wants to be
1351  redirected. This function is used by the command routine
1352  CommandPrintPartition.]
1353
1354  SideEffects []
1355
1356******************************************************************************/
1357int
1358PartPartitionPrint(
1359  FILE *fp,
1360  graph_t *partition)
1361{
1362  lsGen      gen;           /* To iterate over edges */
1363  edge_t     *edgePtr;      /* Will hold the edge being processed */
1364  vertex_t   *fromVertex;   /* Will hold the vertex source of the edge */
1365  vertex_t   *toVertex;     /* Will hold the destination of the edge */
1366  st_table   *vertexToId;   /* To lookup the ordinal of a vertex */
1367  time_t      now           = time(0);
1368  struct tm  *nowStructPtr  = localtime(& now);
1369  char       *nowTxt        = asctime(nowStructPtr);
1370  char       *partitionName = PartPartitionReadName(partition);
1371  int        vertexId;
1372  int        clusterId;
1373
1374  /*
1375   * Write out the header for the output file.
1376   */
1377
1378  (void) fprintf(fp, "# %s\n", Vm_VisReadVersion());
1379  (void) fprintf(fp, "# partition name: %s\n", partitionName);
1380  (void) fprintf(fp, "# generated: %s", nowTxt);
1381  (void) fprintf(fp, "#\n");
1382
1383  (void) fprintf(fp, "# Partition with %d vertices and %d edges\n",
1384                 lsLength(g_get_vertices(partition)),
1385                 lsLength(g_get_edges(partition)));
1386
1387  (void) fprintf(fp, "digraph \"%s\" {\n  rotate=90;\n", partitionName);
1388  (void) fprintf(fp, "  margin=0.5;\n  label=\"%s\";\n", partitionName);
1389  (void) fprintf(fp, "  size=\"10,7.5\";\n  ratio=\"fill\";\n");
1390
1391
1392  vertexToId = st_init_table(st_ptrcmp, st_ptrhash);
1393
1394  vertexId = 0;
1395  clusterId = 0;
1396  foreach_vertex(partition, gen, fromVertex) {
1397    if (PartVertexReadType(fromVertex) == Part_VertexCluster_c) {
1398      array_t *members = PartVertexReadClusterMembers(fromVertex);
1399      vertex_t *auxPtr;
1400      int i;
1401
1402      (void) fprintf(fp, "  subgraph cluster%d {\n", clusterId++);
1403      (void) fprintf(fp, "    label = \"%s\";\n",
1404                     PartVertexReadName(fromVertex));
1405      arrayForEachItem(vertex_t *, members, i, auxPtr) {
1406        (void) fprintf(fp, "  ");
1407        st_insert(vertexToId, (char *)auxPtr, (char *)(long)vertexId);
1408        PrintVertexDescription(fp, auxPtr, vertexId++);
1409      }
1410      (void) fprintf(fp, "  }\n");
1411    } /* End of then */
1412    else if (!PartVertexTestIsClustered(fromVertex)) {
1413      st_insert(vertexToId, (char *)fromVertex, (char *)(long)vertexId);
1414      PrintVertexDescription(fp, fromVertex, vertexId++);
1415    }
1416
1417  }
1418
1419  foreach_edge(partition, gen, edgePtr) {
1420    fromVertex = g_e_source(edgePtr);
1421    toVertex = g_e_dest(edgePtr);
1422
1423    st_lookup_int(vertexToId, (char *)fromVertex, &vertexId);
1424    (void) fprintf(fp, "  node%d -> ", vertexId);
1425
1426    st_lookup_int(vertexToId, (char *)toVertex, &vertexId);
1427    (void) fprintf(fp, "node%d;\n", vertexId);
1428  } /* End of foreach_edge */
1429
1430  (void) fprintf(fp, "}\n");
1431
1432  st_free_table(vertexToId);
1433
1434  return 1;
1435} /* End of PartPartitionPrint */
1436
1437
1438/**Function********************************************************************
1439
1440  Synopsis    [Create latch nodes list and leave nodes list form
1441  CTL properties and fairness constraints]
1442
1443  Comments    []
1444
1445  SideEffects []
1446
1447  SeeAlso     []
1448
1449******************************************************************************/
1450int
1451PartGetLatchInputListFromCTL(
1452  Ntk_Network_t *network,
1453  array_t *ctlArray,
1454  array_t *fairArray,
1455  lsList  latchInputList)
1456{
1457  return PartGetLatchInputListFromCtlAndLtl(network, ctlArray, NIL(array_t),
1458                                            fairArray, latchInputList,
1459                                            FALSE);
1460}
1461
1462/**Function********************************************************************
1463
1464  Synopsis [Create latch inputs list form properties and fairness
1465  constraints]
1466
1467  Comments [Return all the Cone-Of-Influence nodes if stopAtLatch is
1468  FALSE; otherwise, return only the nodes up to the immediate
1469  support.]
1470
1471  SideEffects []
1472
1473  SeeAlso     []
1474
1475******************************************************************************/
1476int
1477PartGetLatchInputListFromCtlAndLtl(
1478  Ntk_Network_t *network,
1479  array_t *ctlArray,
1480  array_t *ltlArray,
1481  array_t *fairArray,
1482  lsList  latchInputList,
1483  boolean stopAtLatch)
1484{
1485  int i;
1486  Ctlp_Formula_t  *ctlFormula;
1487  Ctlsp_Formula_t *ltlFormula;
1488  st_table *formulaNodes;
1489  st_generator *stGen;
1490  array_t *nodeArray;
1491  array_t *formulaCombNodes;
1492  Ntk_Node_t *node;
1493
1494
1495  formulaNodes = st_init_table( st_ptrcmp, st_ptrhash );
1496
1497  if ( formulaNodes == NIL(st_table)){
1498    return 0;
1499  }
1500
1501 /*
1502  * Extract nodes in CTL/LTL properties
1503  */
1504  if ( ctlArray != NIL(array_t)){
1505    arrayForEachItem( Ctlp_Formula_t *, ctlArray, i, ctlFormula ) {
1506      Mc_NodeTableAddCtlFormulaNodes( network, ctlFormula, formulaNodes );
1507    }
1508  }
1509  if ( ltlArray != NIL(array_t)){
1510    arrayForEachItem( Ctlsp_Formula_t *, ltlArray, i, ltlFormula ) {
1511      Mc_NodeTableAddLtlFormulaNodes( network, ltlFormula, formulaNodes );
1512    }
1513  }
1514
1515 /*
1516  * Extract nodes in fairness properties
1517  */
1518  if ( fairArray != NIL(array_t)){
1519    arrayForEachItem( Ctlp_Formula_t *, fairArray, i, ctlFormula ) {
1520      Mc_NodeTableAddCtlFormulaNodes( network, ctlFormula, formulaNodes );
1521    }
1522  }
1523
1524  nodeArray = array_alloc( Ntk_Node_t *, 0 );
1525  st_foreach_item( formulaNodes, stGen, &node, NULL) {
1526    array_insert_last( Ntk_Node_t *, nodeArray, node );
1527  }
1528
1529  st_free_table( formulaNodes );
1530
1531 /*
1532  * Get all combinational support nodes in network from formula nodes
1533  */
1534  formulaCombNodes = Ntk_NodeComputeCombinationalSupport( network,
1535                     nodeArray, stopAtLatch );
1536  array_free(nodeArray);
1537 /*
1538  * Root list includes latch data input nodes
1539  */
1540  arrayForEachItem( Ntk_Node_t *, formulaCombNodes, i, node ) {
1541    if ( Ntk_NodeTestIsLatch( node ) ) {
1542      Ntk_Node_t *tempNode = Ntk_LatchReadDataInput( node );
1543      lsNewEnd(latchInputList, (lsGeneric)tempNode, LS_NH);
1544    }
1545  }
1546
1547  array_free(formulaCombNodes);
1548
1549  return 1;
1550}
1551
1552/**Function********************************************************************
1553
1554  Synopsis [Create latch nodes list form properties and fairness
1555  constraints]
1556
1557  Comments [Return all the Cone-Of-Influence nodes if stopAtLatch is
1558  FALSE; otherwise, return only the nodes up to the immediate
1559  support.]
1560
1561  SideEffects []
1562
1563  SeeAlso     []
1564
1565******************************************************************************/
1566int
1567PartGetLatchListFromCtlAndLtl(
1568  Ntk_Network_t *network,
1569  array_t *ctlArray,
1570  array_t *ltlArray,
1571  array_t *fairArray,
1572  lsList  latchInputList,
1573  boolean stopAtLatch)
1574{
1575  int i;
1576  Ctlp_Formula_t  *ctlFormula;
1577  Ctlsp_Formula_t *ltlFormula;
1578  st_table *formulaNodes;
1579  st_generator *stGen;
1580  array_t *nodeArray;
1581  array_t *formulaCombNodes;
1582  Ntk_Node_t *node;
1583
1584
1585  formulaNodes = st_init_table( st_ptrcmp, st_ptrhash );
1586
1587  if ( formulaNodes == NIL(st_table)){
1588    return 0;
1589  }
1590
1591 /*
1592  * Extract nodes in CTL/LTL properties
1593  */
1594  if ( ctlArray != NIL(array_t)){
1595    arrayForEachItem( Ctlp_Formula_t *, ctlArray, i, ctlFormula ) {
1596      Mc_NodeTableAddCtlFormulaNodes( network, ctlFormula, formulaNodes );
1597    }
1598  }
1599  if ( ltlArray != NIL(array_t)){
1600    arrayForEachItem( Ctlsp_Formula_t *, ltlArray, i, ltlFormula ) {
1601      Mc_NodeTableAddLtlFormulaNodes( network, ltlFormula, formulaNodes );
1602    }
1603  }
1604
1605 /*
1606  * Extract nodes in fairness properties
1607  */
1608  if ( fairArray != NIL(array_t)){
1609    arrayForEachItem( Ctlp_Formula_t *, fairArray, i, ctlFormula ) {
1610      Mc_NodeTableAddCtlFormulaNodes( network, ctlFormula, formulaNodes );
1611    }
1612  }
1613
1614  nodeArray = array_alloc( Ntk_Node_t *, 0 );
1615  st_foreach_item( formulaNodes, stGen, &node, NULL) {
1616    array_insert_last( Ntk_Node_t *, nodeArray, node );
1617  }
1618
1619  st_free_table( formulaNodes );
1620
1621 /*
1622  * Get all combinational support nodes in network from formula nodes
1623  */
1624  formulaCombNodes = Ntk_NodeComputeCombinationalSupport( network,
1625                     nodeArray, stopAtLatch );
1626  array_free(nodeArray);
1627 /*
1628  * Root list includes latch data input nodes
1629  */
1630  arrayForEachItem( Ntk_Node_t *, formulaCombNodes, i, node ) {
1631    if ( Ntk_NodeTestIsLatch( node ) ) {
1632      lsNewEnd(latchInputList, (lsGeneric)node, LS_NH);
1633    }
1634  }
1635
1636  array_free(formulaCombNodes);
1637
1638  return 1;
1639}
1640
1641/*---------------------------------------------------------------------------*/
1642/* Definition of static functions                                            */
1643/*---------------------------------------------------------------------------*/
1644
1645
1646/**Function********************************************************************
1647
1648  Synopsis    [Prints the declaration of a vertex in dot format.]
1649
1650  SideEffects []
1651
1652  SeeAlso     [Part_PartitionPrint]
1653
1654******************************************************************************/
1655static void
1656PrintVertexDescription(
1657  FILE *fp,
1658  vertex_t *vertexPtr,
1659  int order)
1660{
1661  char *name = PartVertexReadName(vertexPtr);
1662
1663  (void) fprintf(fp, "  node%d [label=", order);
1664  if (name != NIL(char)) {
1665    (void) fprintf(fp, "\"%s\"", name);
1666  }
1667  else {
1668    (void) fprintf(fp, "\"None\"");
1669  }
1670  (void) fprintf(fp, "]; \n");
1671} /* End of PrintVertexDescription */
Note: See TracBrowser for help on using the repository browser.