/**CFile************************************************************************ FileName [partPart.c] PackageName [part] Synopsis [Routines to initialize the command build_partition_mdds, create and delete internal data structures of the partition, and print information about the partition.] Author [Abelardo Pardo] Copyright [This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.] ******************************************************************************/ #include "partInt.h" static char rcsid[] UNUSED = "$Id: partPart.c,v 1.45 2009/04/11 01:47:18 fabio Exp $"; /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ static void PrintVertexDescription(FILE *fp, vertex_t *vertexPtr, int order); /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Deletes the graph created for the partition and all the information attached to it.] SideEffects [] SeeAlso [PartPartitionInfoFree PartVertexInfoFree] ******************************************************************************/ void Part_PartitionFree( graph_t *partition) { /* Delete the graph information */ g_free(partition, PartPartitionInfoFree, PartVertexInfoFree, (void (*)(gGeneric))0); } /* End of Part_PartitionFree */ /**Function******************************************************************** Synopsis [Call-back function to free a partition.] Description [This function will be stored in the network together with the pointer to the structure. Whenever the network deletes the partitioning information, this function is called and it will deallocate the partition and the information attached to it.] SideEffects [] SeeAlso [Ntk_NetworkAddApplInfo] ******************************************************************************/ void Part_PartitionFreeCallback( void *data) { Part_PartitionFree((graph_t *) data); } /* End of Part_PartitionFreeCallback */ /**Function******************************************************************** Synopsis [Finds a vertex in the graph with a certain name.] Description [Given a name, it returns a pointer to a vertex structure if there is a vertex with that name in the partition. Otherwise it returns a NULL pointer.] SideEffects [] SeeAlso [PartPartitionInfo] ******************************************************************************/ vertex_t * Part_PartitionFindVertexByName( graph_t *partition, char *name) { vertex_t *result = NIL(vertex_t); st_table *table = PartPartitionReadNameToVertex(partition); if (table != NIL(st_table)) { st_lookup(table, name, &result); } /* End of if */ return result; } /* End of Part_PartitionFindVertexByName */ /**Function******************************************************************** Synopsis [Finds a vertex in the graph with a certain MddId.] Description [Given a MddId, it returns a pointer to a vertex structure if there is a vertex with that mddId in the partition. Otherwise it returns a NULL pointer.] SideEffects [] SeeAlso [PartVertexInfo] ******************************************************************************/ vertex_t * Part_PartitionFindVertexByMddId( graph_t *partition, int mddId) { vertex_t *result = NIL(vertex_t); st_table *table = PartPartitionReadMddIdToVertex(partition); if (table != NIL(st_table)) { st_lookup(table, (char *)(long)mddId, &result); } /* End of if */ return result; } /* End of Part_PartitionFindVertexByMddId */ /**Function******************************************************************** Synopsis [Returns the name of the entity from which the partition was created.] SideEffects [] SeeAlso [PartPartitionInfo] ******************************************************************************/ char * Part_PartitionReadName( graph_t *partition) { return PartPartitionReadName(partition); } /* End of Part_PartitionReadName */ /**Function******************************************************************** Synopsis [Returns the method which was used to create the partition graph.] SideEffects [] SeeAlso [PartPartitionInfo] ******************************************************************************/ Part_PartitionMethod Part_PartitionReadMethod( graph_t *partition) { Part_PartitionMethod method; method = PartPartitionReadMethod(partition); if (method == Part_Default_c) method = Part_Frontier_c; return(method); } /* End of Part_PartitionReadMethod */ /**Function******************************************************************** Synopsis [Returns the partition method as a string.] Description [Returns the method stored in the partition as a new string. The caller of the function has the responsibility of freeing the string. The possible values of the string are: "Inputs-Outputs", "Total", "Partial" or "Frontier".] SideEffects [] SeeAlso [Part_PartitionPrintStats] ******************************************************************************/ char * Part_PartitionObtainMethodAsString( graph_t *partition) { char *resultString; assert(partition != NIL(graph_t)); switch(PartPartitionReadMethod(partition)) { case Part_Total_c: resultString = util_strsav("Total"); break; case Part_Partial_c: resultString = util_strsav("Partial"); break; case Part_InOut_c: resultString = util_strsav("Inputs-Outputs"); break; case Part_Frontier_c: case Part_Default_c: resultString = util_strsav("Frontier"); break; case Part_Boundary_c: resultString = util_strsav("Boundary"); break; case Part_Fine_c: resultString = util_strsav("Fine"); break; default: fail("Unexpected Partition method."); } return resultString; } /* End of Part_PartitionObtainMethodAsString */ /**Function******************************************************************** Synopsis [Function to read the manager attached to the partition.] SideEffects [] SeeAlso [PartPartitionInfo] ******************************************************************************/ mdd_manager * Part_PartitionReadMddManager( graph_t *partition) { return PartPartitionReadMddManager(partition); } /* End of Part_PartitionReadMddManager */ /**Function******************************************************************** Synopsis [Returns the type of a vertex.] SideEffects [] SeeAlso [PartVertexInfo Part_VertexType] ******************************************************************************/ Part_VertexType Part_VertexReadType( vertex_t *vertexPtr) { return PartVertexReadType(vertexPtr); } /* End of Part_VertexReadType */ /**Function******************************************************************** Synopsis [Reads the name attached to a vertex.] SideEffects [] SeeAlso [PartVertexInfo] ******************************************************************************/ char * Part_VertexReadName( vertex_t *vertexPtr) { return PartVertexReadName(vertexPtr); } /* End of Part_VertexReadName */ /**Function******************************************************************** Synopsis [Reads the clusterMembers field of a vertex.] Description [This function does not make sure that the vertex is of clustered type. It is the responsibility of the caller to guarantee that.] SideEffects [] SeeAlso [PartVertexInfo] ******************************************************************************/ array_t * Part_VertexReadClusterMembers( vertex_t *vertexPtr) { return PartVertexReadClusterMembers(vertexPtr); } /* End of Part_VertexReadClusterMembers */ /**Function******************************************************************** Synopsis [Reads the multi-valued function attached to a vertex.] Description [This function does not make sure that the vertex is of single type. It is the responsibility of the caller to guarantee that.] SideEffects [] SeeAlso [PartVertexInfo] ******************************************************************************/ Mvf_Function_t * Part_VertexReadFunction( vertex_t *vertexPtr) { return PartVertexReadFunction(vertexPtr); } /* End of Part_VertexReadFunction */ /**Function******************************************************************** Synopsis [Sets the multi-valued function of a vertex.] SideEffects [] SeeAlso [PartVertexInfo] ******************************************************************************/ void Part_VertexSetFunction( vertex_t *vertexPtr, Mvf_Function_t *mvf) { assert(PartVertexReadType(vertexPtr) != Part_VertexCluster_c); PartVertexSetFunction(vertexPtr, mvf); } /* End of Part_VertexSetFunction */ /**Function******************************************************************** Synopsis [Reads the MddId attached to a vertex.] SideEffects [] SeeAlso [PartVertexInfo] ******************************************************************************/ int Part_VertexReadMddId( vertex_t *vertexPtr) { return PartVertexReadMddId(vertexPtr); } /* End of Part_VertexReadMddId */ /**Function******************************************************************** Synopsis [Test of a vertex is member of a cluster.] SideEffects [] SeeAlso [PartVertexInfo Part_VertexReadType] ******************************************************************************/ boolean Part_VertexTestIsClustered( vertex_t *vertexPtr) { return PartVertexTestIsClustered(vertexPtr); } /* End of Part_VertexTestIsClustered */ /**Function******************************************************************** Synopsis [Executes the selected partitioning method.] Description [Given a network, and a method, the function creates a partition by using the specified method. This function may be called from any point in the code to create a partition. In particular, the command partition uses this function to create the partition and store it in the network.

The function receives two lists of pointers to network nodes, the roots and the leaves. The function will create the partition of the subnetwork between the root and the leave nodes. As a special case, if both lists are passed NIL values, the root and leave lists default to combinational outputs and combinational inputs respectively. The parameter careSet specifies which minterms in the input space are considered. The nodes parameter is an optional list of nodes that may be specified in case the partial method is used. It represents the set of nodes in the network to be preserved when building the partition. The boolean variable inTermsOfLeaves is valid only in the case of the total method and provides the option of creating the functions attached to the vertices in terms of the combinational inputs or in terms of their immediate fanin. Two additional parameters are provided to control the verbosity and the intensity of the sanity check applied to the computation.

This function is called by the command build_partition_mdds which has a time-out option. In the event of the execution time going over the time out, the control is returned to the prompt and all the memory allocated by the internal procedures is leaked.] SideEffects [] SeeAlso [part.h] ******************************************************************************/ graph_t * Part_NetworkCreatePartition( Ntk_Network_t *network, Hrc_Node_t *hnode, char *name, lsList rootList, lsList leaveList, mdd_t *careSet, Part_PartitionMethod method, lsList nodes, boolean inTermsOfLeaves, int verbose, int sanityCheck) { graph_t *partition; long lap = 0; if (verbose) { lap = util_cpu_time(); } /* End of if */ /* Create the new graph to represent the partition */ partition = g_alloc(); partition->user_data = (gGeneric)PartPartitionInfoCreate(name, Ntk_NetworkReadMddManager(network), method); switch (method) { case Part_Partial_c: if (verbose) { (void) fprintf(vis_stdout, "Partitioning the system by the Partial"); (void) fprintf(vis_stdout, " method\n"); } /* End of if */ PartPartitionPartial(network, partition, rootList, leaveList, careSet, nodes, inTermsOfLeaves); break; case Part_Boundary_c: if (verbose) { (void) fprintf(vis_stdout, "Partitioning the system by the Boundary"); (void) fprintf(vis_stdout, " method\n"); } /* End of if */ PartPartitionBoundary(network, hnode, partition, rootList, leaveList, careSet, inTermsOfLeaves); break; case Part_Total_c: if (verbose) { (void) fprintf(vis_stdout, "Partitioning the circuit by the Total"); (void) fprintf(vis_stdout, " method\n"); } /* End of if */ PartPartitionTotal(network, partition, rootList, leaveList, careSet, inTermsOfLeaves); break; case Part_Frontier_c: case Part_Default_c: if (verbose) { (void) fprintf(vis_stdout, "Partitioning the circuit by the Frontier"); (void) fprintf(vis_stdout, " method\n"); } /* End of if */ PartPartitionFrontier(network, partition, rootList, leaveList, careSet); break; case Part_Fine_c: if (verbose) { (void) fprintf(vis_stdout, "Partitioning the circuit for the fine-grain"); (void) fprintf(vis_stdout, " method\n"); } /* End of if */ PartPartitionFineGrain(network, partition, careSet); break; case Part_InOut_c: if (verbose) { (void) fprintf(vis_stdout, "Partitioning the circuit by the"); (void) fprintf(vis_stdout, " Input-Output method\n"); } /* End of if */ PartPartitionInputsOutputs(network, partition, rootList, leaveList, careSet); break; default: (void) fprintf(vis_stdout, "Partition method not implemented yet\n"); break; } if (sanityCheck >0) { PartPartitionSanityCheck(partition, sanityCheck); } if (verbose) { (void) fprintf(vis_stdout, "%.2f (secs) spent in partitioning.\n", (util_cpu_time() - lap)/1000.0); } /* End of if */ return partition; } /* End of Part_NetworkCreatePartition */ /**Function******************************************************************** Synopsis [Creates a duplicate of a partition.] SideEffects [] SeeAlso [PartVertexInfo, PartPartitionInfo] ******************************************************************************/ graph_t * Part_PartitionDuplicate( graph_t *partition) { graph_t *result; lsGen gen; vertex_t *fromVertex; vertex_t *toVertex; edge_t *edgePtr; result = g_alloc(); result->user_data = (gGeneric)PartPartitionInfoCreate(PartPartitionReadName(partition), PartPartitionReadMddManager(partition), PartPartitionReadMethod(partition)); foreach_vertex(partition, gen, fromVertex) { char *name; int mddId; name = PartVertexReadName(fromVertex); mddId = PartVertexReadMddId(fromVertex); toVertex = g_add_vertex(result); st_insert(PartPartitionReadNameToVertex(result), name, (char *)toVertex); if (mddId != NTK_UNASSIGNED_MDD_ID) { st_insert(PartPartitionReadMddIdToVertex(result), (char *)(long)mddId, (char *)toVertex); } /* End of if */ if (PartVertexReadType(fromVertex) == Part_VertexSingle_c) { Mvf_Function_t *mdd; mdd = Mvf_FunctionDuplicate(PartVertexReadFunction(fromVertex)); toVertex->user_data = (gGeneric)PartVertexInfoCreateSingle(name, mdd, mddId); } if (PartVertexReadType(fromVertex) == Part_VertexCluster_c) { toVertex->user_data = (gGeneric)PartVertexInfoCreateCluster(name, Part_VertexReadClusterMembers(fromVertex)); } } foreach_edge(partition, gen, edgePtr) { vertex_t *fromVertexCopy; vertex_t *toVertexCopy; fromVertex = g_e_source(edgePtr); toVertex = g_e_dest(edgePtr); st_lookup(PartPartitionReadNameToVertex(result), PartVertexReadName(fromVertex), &fromVertexCopy); st_lookup(PartPartitionReadNameToVertex(result), PartVertexReadName(toVertex), &toVertexCopy); g_add_edge(fromVertexCopy, toVertexCopy); } return result; } /* End of Part_PartitionDuplicate */ /**Function******************************************************************** Synopsis [Create reduced partition according to given CTL formulae] Comments [Combinational root and leave nodes are combinational support nodes of given CTL properties.] SideEffects [] SeeAlso [] ******************************************************************************/ graph_t * Part_PartCreatePartitionWithCTL( Hrc_Manager_t **hmgr, Part_PartitionMethod method, int verbose, int sanityCheck, boolean inTermsOfLeaves, array_t *ctlArray, array_t *fairArray) { return Part_PartCreatePartitionWithCtlAndLtl(hmgr, method, verbose, sanityCheck, inTermsOfLeaves, ctlArray, NIL(array_t), fairArray); } /**Function******************************************************************** Synopsis [Create reduced partition according to given CTL formulae] Comments [Combinational root and leave nodes are combinational support nodes of given CTL properties.] SideEffects [] SeeAlso [] ******************************************************************************/ graph_t * Part_PartCreatePartitionWithCtlAndLtl( Hrc_Manager_t **hmgr, Part_PartitionMethod method, int verbose, int sanityCheck, boolean inTermsOfLeaves, array_t *ctlArray, array_t *ltlArray, array_t *fairArray) { char *modelName; Hrc_Node_t *currentNode; graph_t *partition; lsList latchInputList; lsGen gen; Ntk_Node_t *node; Ntk_Network_t *network = Ntk_HrcManagerReadCurrentNetwork(*hmgr); latchInputList = lsCreate(); currentNode = Hrc_ManagerReadCurrentNode(*hmgr); modelName = Hrc_NodeReadModelName(currentNode); if (method != Part_InOut_c){ return NIL(graph_t); } PartGetLatchInputListFromCtlAndLtl(network, ctlArray, ltlArray, fairArray, latchInputList, FALSE); Ntk_NetworkForEachCombOutput(network, gen, node){ if (Ntk_NodeTestIsLatchInitialInput(node)){ lsNewEnd(latchInputList, (lsGeneric)node, LS_NH); } } /* * Execute the partition algorithm. If rootList and leaveList are null, * graph includes all network nodes */ partition = Part_NetworkCreatePartition(network, currentNode, modelName, latchInputList, (lsList)0, NIL(mdd_t), method, (lsList)0, inTermsOfLeaves, verbose, sanityCheck); lsDestroy(latchInputList, (void (*)(lsGeneric))0); return partition; } /**Function******************************************************************** Synopsis [Change partition to include new vertex in root list] Comments [Current partition in increased to include all next state functions for all members in rootList.] SideEffects [] SeeAlso [] ******************************************************************************/ int Part_PartitionChangeRoots( Ntk_Network_t *network, graph_t *partition, lsList rootList, int verbosity) { if (Part_PartitionReadMethod(partition) != Part_InOut_c){ return 0; } return PartPartitionInOutChangeRoots(network, partition, rootList, verbosity); } /**Function******************************************************************** Synopsis [Reads the partition attached to a network.] SideEffects [] SeeAlso [CommandBuildPartitionMdds] ******************************************************************************/ graph_t * Part_NetworkReadPartition( Ntk_Network_t *network) { return (graph_t *)Ntk_NetworkReadApplInfo(network, PART_NETWORK_APPL_KEY); } /* End of Part_NetworkReadPartition */ /**Function******************************************************************** Synopsis [Adds a vertex to the partition representing a set of vertices.] SideEffects [] SeeAlso [PartVertexInfo] ******************************************************************************/ vertex_t * Part_PartitionCreateClusterVertex( graph_t *partition, char *name, array_t *arrayOfVertices) { vertex_t *newVertex; newVertex = g_add_vertex(partition); newVertex->user_data = (gGeneric)PartVertexInfoCreateCluster(name, arrayOfVertices); return(newVertex); } /* End of Part_PartitionCreateClusterVertex */ /**Function******************************************************************** Synopsis [ Partition by adding vertices for the nodes in rootList and leaveList. A node in leaveList may already have a corresponding vertex in the partition graph -- Only creating the new vertex if not exists. Nodes in rootList should NOT have existing vertices in the partition graph. (The caller should guarantee this) This routine is for the use in the 'ltl' package. We assume the partition method is Part_Frontier_c.] SideEffects [partition might be changed.] SeeAlso [PartPartitionFrontier] ******************************************************************************/ void Part_UpdatePartitionFrontier( Ntk_Network_t *network, graph_t *partition, lsList rootList, lsList leaveList, mdd_t *careSet) { PartUpdateFrontier(network, partition, rootList, leaveList, careSet); } /**Function******************************************************************** Synopsis [Removes a cluster vertex from the partition.] SideEffects [] SeeAlso [PartVertexInfo] ******************************************************************************/ void Part_VertexInfoFreeCluster( vertex_t *vertexPtr) { if (PartVertexReadType(vertexPtr) == Part_VertexCluster_c) { g_delete_vertex(vertexPtr, PartVertexInfoFree, (void (*)(gGeneric))0); } /* End of then */ else { (void) fprintf(vis_stderr, "Warning -- Inconsistent vertex deletion in"); (void) fprintf(vis_stderr, " partition package\n"); } } /* End of Part_VertexInfoFreeCluster */ /**Function******************************************************************** Synopsis [Test if the functions attached to a set of vertices in the partition are completely specified.] Description [Given a set of vertices (roots) build their functions in terms of a second set of vertices (leaves) and test if the functions are completely specified.] SideEffects [] SeeAlso [Part_PartitionTestDeterministic] ******************************************************************************/ boolean Part_PartitionTestCompletelySp( graph_t *partition, array_t *roots, st_table *leaves) { array_t *mvfFunctions; vertex_t *vertexPtr; Mvf_Function_t *functionPtr; boolean result = TRUE; int i; char *vertexName; mvfFunctions = Part_PartitionCollapse(partition, roots, leaves, NIL(mdd_t)); arrayForEachItem(Mvf_Function_t *, mvfFunctions, i, functionPtr) { vertexPtr = array_fetch(vertex_t *, roots, i); vertexName = PartVertexReadName(vertexPtr); if (!Mvf_FunctionTestIsCompletelySpecified(functionPtr)) { error_append("Vertex "); error_append(vertexName); error_append(" is not completely specified\n"); result = FALSE; } /* End of if */ /* We don't need the Mvf_Function any more, so we delete it */ Mvf_FunctionFree(functionPtr); } /* Clean up*/ array_free(mvfFunctions); return result; } /* End of Part_PartitionTestCompletelySp */ /**Function******************************************************************** Synopsis [Test if the functions attached to a set of vertices in the partition are deterministic.] Description [Given a set of vertices (roots) build their functions in terms of a second set of vertices (leaves) and test if the functions are deterministic.] SideEffects [] SeeAlso [Part_PartitionTestCompletelySp] ******************************************************************************/ boolean Part_PartitionTestDeterministic( graph_t *partition, array_t *roots, st_table *leaves) { array_t *mvfFunctions; vertex_t *vertexPtr; Mvf_Function_t *functionPtr; boolean result = TRUE; int i; char *vertexName; mvfFunctions = Part_PartitionCollapse(partition, roots, leaves, NIL(mdd_t)); arrayForEachItem(Mvf_Function_t *, mvfFunctions, i, functionPtr) { vertexPtr = array_fetch(vertex_t *, roots, i); vertexName = PartVertexReadName(vertexPtr); if (!Mvf_FunctionTestIsDeterministic(functionPtr)) { error_append("Vertex "); error_append(vertexName); error_append(" is non-deterministic\n"); result = FALSE; } /* End of if */ /* We don't need the Mvf_Function any more, so we delete it */ Mvf_FunctionFree(functionPtr); } /* Clean up*/ array_free(mvfFunctions); return result; } /* End of Part_PartitionTestDeterministic */ /**Function******************************************************************** Synopsis [Create latch input nodes list from CTL properties and fairness constraints] Comments [] SideEffects [latchInputList is changed] SeeAlso [] ******************************************************************************/ int Part_PartitionGetLatchInputListFromCTL( Ntk_Network_t *network, array_t *ctlArray, array_t *fairArray, lsList latchInputList) { return PartGetLatchInputListFromCTL( network, ctlArray, fairArray, latchInputList); } /**Function******************************************************************** Synopsis [Create latch input nodes list from CTL properties and fairness constraints] Comments [] SideEffects [latchInputList is changed] SeeAlso [] ******************************************************************************/ int Part_PartitionGetLatchInputListFromCtlAndLtl( Ntk_Network_t *network, array_t *ctlArray, array_t *ltlArray, array_t *fairArray, lsList latchInputList, boolean stopAtLatch) { return PartGetLatchInputListFromCtlAndLtl( network, ctlArray, ltlArray, fairArray, latchInputList, stopAtLatch); } /**Function******************************************************************** Synopsis [Prints statistics about the partition DAG.] Comments [If the parameter printNodeNames is true, the function prints names of the network nodes represented by vertices in the partition graph.] SideEffects [] SeeAlso [PartPartitionInfo] ******************************************************************************/ void Part_PartitionPrintStats( FILE *fp, graph_t *partition, boolean printNodeNames) { lsList vertexList = g_get_vertices(partition); vertex_t *vertexPtr; array_t *functions; Mvf_Function_t* vertexFunction; mdd_t *mddPtr; lsGen gen; char *methodName; int numVertices = lsLength(vertexList); int numSources; int numSinks; int i; /* Obtain the method name as a string */ methodName = Part_PartitionObtainMethodAsString(partition); /* * Count the number of sources and sinks and at the same time store all the * bdd_t of every vertex in a common array to compute the shared size. */ numSources = 0; numSinks = 0; functions = array_alloc(mdd_t *, 0); if (printNodeNames) { (void) fprintf(fp, "Network nodes represented as vertices in the "); (void) fprintf(fp, "partition:\n"); } foreach_vertex(partition, gen, vertexPtr) { if (lsLength(g_get_in_edges(vertexPtr)) == 0) { numSources++; } /* End of if */ if (lsLength(g_get_out_edges(vertexPtr)) == 0) { numSinks++; } /* End of if */ if (PartVertexReadType(vertexPtr) == Part_VertexSingle_c) { if (printNodeNames) { if (PartVertexReadName(vertexPtr) != NIL(char)) { (void) fprintf(fp, "%s\n", PartVertexReadName(vertexPtr)); } } vertexFunction = PartVertexReadFunction(vertexPtr); if (vertexFunction != NIL(Mvf_Function_t)) { Mvf_FunctionForEachComponent(vertexFunction, i, mddPtr) { array_insert_last(mdd_t *, functions, mddPtr); } } /* End of if */ } /* End of if */ } /* foreach_vertex*/ /* Print results */ (void)fprintf(fp, "Method %s, %d sinks, %d sources,", methodName, numSinks, numSources); (void)fprintf(fp, " %d total vertices,", numVertices); (void)fprintf(fp, " %ld mdd nodes\n", bdd_size_multiple(functions)); /* Clean up */ FREE(methodName); array_free(functions); return; } /* End of Part_PartitionPrintStats */ /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Initializes the information attached to the graph of the partition.] Description [Allocates the memory needed for the information attached to the graph structure.] SideEffects [] SeeAlso [PartPartitionInfo PartPartitionInfoFree] ******************************************************************************/ PartPartitionInfo_t * PartPartitionInfoCreate( char *name, mdd_manager *manager, Part_PartitionMethod method) { PartPartitionInfo_t *recordPartition = ALLOC(PartPartitionInfo_t, 1); recordPartition->name = util_strsav(name); recordPartition->method = method; recordPartition->mddManager = manager; recordPartition->nameToVertex = st_init_table(strcmp,st_strhash); recordPartition->mddIdToVertex = st_init_table(st_numcmp, st_numhash); return recordPartition; } /* End of PartPartitionInfoCreate */ /**Function******************************************************************** Synopsis [Deallocates the user information in the graph.] Description [Deallocates the user information in the graph. Does not free the MDD manager associated with the partition.] SideEffects [] SeeAlso [PartPartitionInfoCreate] ******************************************************************************/ void PartPartitionInfoFree( gGeneric partitionInfo) { if (((PartPartitionInfo_t *)partitionInfo)->name != NIL(char)) { FREE(((PartPartitionInfo_t *)partitionInfo)->name); } st_free_table(((PartPartitionInfo_t *)partitionInfo)->nameToVertex); st_free_table(((PartPartitionInfo_t *)partitionInfo)->mddIdToVertex); FREE(partitionInfo); } /* End of PartPartitionInfoFree */ /**Function******************************************************************** Synopsis [Initializes the information attached to a single vertex.] SideEffects [] SeeAlso [PartVertexInfo] ******************************************************************************/ PartVertexInfo_t * PartVertexInfoCreateSingle( char *name, Mvf_Function_t *mvf, int mddId) { PartVertexInfo_t *result; result = ALLOC(PartVertexInfo_t, 1); result->type = Part_VertexSingle_c; result->name = util_strsav(name); result->functionality.mvf = mvf; result->mddId = mddId; result->isClustered = 0; return result; } /* End of PartVertexInfoCreateSingle */ /**Function******************************************************************** Synopsis [Creates a cluster vertex in the partition.] SideEffects [] SeeAlso [PartVertexInfo] ******************************************************************************/ PartVertexInfo_t * PartVertexInfoCreateCluster( char *name, array_t *vertexArray) { PartVertexInfo_t *result; vertex_t *auxPtr; int i; /* Make sure all the nodes are simple nodes */ for(i = 0; i < array_n(vertexArray); i++) { auxPtr = array_fetch(vertex_t *, vertexArray, i); if (PartVertexReadType(auxPtr) == Part_VertexCluster_c) { fail("Only one level of hierarchy allowed in the partition"); } /* End of if */ if (PartVertexTestIsClustered(auxPtr)) { fail("Partition: Clustering vertex already member of another cluster"); } /* End of then */ else { PartVertexSetIsClustered(auxPtr, 1); } } /* End of for */ result = ALLOC(PartVertexInfo_t, 1); result->type = Part_VertexCluster_c; result->name = util_strsav(name); result->functionality.clusterMembers = array_dup(vertexArray); result->mddId = NTK_UNASSIGNED_MDD_ID; result->isClustered = 0; return result; } /* End of PartVertexInfoCreateCluster */ /**Function******************************************************************** Synopsis [Deallocates the user information attached to a vertex.] SideEffects [] SeeAlso [PartVertexInfo] ******************************************************************************/ void PartVertexInfoFree( gGeneric vertexInfo ) { if (((PartVertexInfo_t *)vertexInfo)->type == Part_VertexSingle_c) { /* Free the function attached to the node if any */ if (((PartVertexInfo_t *)vertexInfo)->functionality.mvf != NIL(Mvf_Function_t)) { Mvf_FunctionFree(((PartVertexInfo_t *)vertexInfo)->functionality.mvf); } /* End of if */ } /* End of then */ else { if (((PartVertexInfo_t *)vertexInfo)->functionality.clusterMembers != NIL(array_t)) { array_free(((PartVertexInfo_t *)vertexInfo)->functionality.clusterMembers); } /* End of if */ } /* End of if-then-else */ if (((PartVertexInfo_t *)vertexInfo)->name != NIL(char)) { FREE(((PartVertexInfo_t *)vertexInfo)->name); } FREE(vertexInfo); } /* End of PartVertexInfoFree */ /**Function******************************************************************** Synopsis [Verifies that the information in the nameToVertex table of a graph is consistent.] SideEffects [] SeeAlso [PartPartitionInfo] ******************************************************************************/ void PartPartitionSanityCheck( graph_t *partition, int intensity) { st_table *table; lsList vertexList = g_get_vertices(partition); lsGen lgen; vertex_t *vertex, *rvertex; /* Consistency in the nameToVertex table */ table = PartPartitionReadNameToVertex(partition); /* * The number of elements in the nameToVertex table and the number * of vertices agrees */ if (lsLength(g_get_vertices(partition)) != st_count(table)) { (void) fprintf(vis_stderr, "Warning -- NameToVertex table incomplete in "); (void) fprintf(vis_stderr, " graph\n"); if (intensity > 1) { (void) fprintf(vis_stderr, " %d vertices in the graph and %d entries", lsLength(g_get_vertices(partition)), st_count(table)); (void) fprintf(vis_stderr, " in the nameToVertex table\n"); } /* End of if */ } /* End of if */ lsForEachItem(vertexList, lgen, vertex) { char *name = PartVertexReadName(vertex); if (!st_lookup(table, name, &rvertex) || strcmp(PartVertexReadName(vertex),PartVertexReadName(rvertex)) != 0) { (void) fprintf(vis_stderr, "Warning -- Inconsistency detected in"); (void) fprintf(vis_stderr, " the partition data-base\n"); } } /* Consistency in the mddIdToVertexTable */ table = PartPartitionReadMddIdToVertex(partition); lsForEachItem(vertexList, lgen, vertex) { int mddId = PartVertexReadMddId(vertex); if((mddId != NTK_UNASSIGNED_MDD_ID) && (!st_lookup(table, (char *)(long)mddId, &rvertex) || PartVertexReadMddId(vertex) != PartVertexReadMddId(rvertex))) { (void) fprintf(vis_stderr, "Warning -- Inconsistency detected in the"); (void) fprintf(vis_stderr, " partition data-base\n"); } } /* * Make sure that the mdd Id NTK_UNASSIGNED_MDD_ID does not appear in the * mddIdToVertex node. */ table = PartPartitionReadMddIdToVertex(partition); if (st_is_member(table, (char *) NTK_UNASSIGNED_MDD_ID)) { (void) fprintf(vis_stderr, "Warning -- Inconsistency detected in the"); (void) fprintf(vis_stderr, " partition data-base\n"); } /* End of if */ /* Check the Mvfs in the vertices of the partition.*/ if (intensity > 1) { lsForEachItem(vertexList, lgen, vertex) { Mvf_Function_t *function = PartVertexReadFunction(vertex); int i; (void) fprintf(vis_stderr, "Vertex: %s, mddId: %d, Clustered: %c\n", PartVertexReadName(vertex), PartVertexReadMddId(vertex), (PartVertexReadType(vertex) == Part_VertexCluster_c)?'t':'f'); for(i = 0; i < Mvf_FunctionReadNumComponents(function); i ++) { mdd_t *unit = Mvf_FunctionObtainComponent(function, i); boolean x; if (intensity > 2) { (void) fprintf(vis_stderr, "BDD_T: %lx, %lx\n", (unsigned long) bdd_get_node(unit, &x), (unsigned long) mdd_get_manager(unit)); } } /* End of for */ } } /* End of if */ /* ToDo: Check for redundant name in the list of vertices */ } /* End of PartPartitionSanityCheck */ /**Function******************************************************************** Synopsis [Computes the support of an array of mdds.] Description [Computes the support of a multi-valued function. It is just the union of the supports of every component of the function.] Comment [The reason why is it returned in a table is because it's very likely that questions such as, "is certain Id part of the support ?" will happen.] SideEffects [] SeeAlso [PartVertexCreateFaninEdges] ******************************************************************************/ st_table * PartCreateFunctionSupportTable( Mvf_Function_t *mvf) { mdd_manager *mddManager; /* Manager for the MDDs */ array_t *support; st_table *mddSupport = st_init_table(st_numcmp, st_numhash); int numComponents = Mvf_FunctionReadNumComponents(mvf); int j, k; mdd_t *unit; assert(numComponents!= 0); mddManager = Mvf_FunctionReadMddManager(mvf); /* * compute the support of an mdd as the union of supports of every * function component */ for(j = 0; j < numComponents; j++) { unit = Mvf_FunctionReadComponent(mvf, j); support = mdd_get_support(mddManager, unit); /* For every element of its support */ for(k = 0; k < array_n(support); k++) { st_insert(mddSupport, (char *)(long)array_fetch(int, support, k), (char *)0); } /* End of for */ array_free(support); } /* End of for */ return mddSupport; } /* End of PartCreateFunctionSupportTable */ /**Function******************************************************************** Synopsis [Creates fanin edges of a vertex based on MDD support.] Description [Computes the support of the function attached to a vertex and adds to the graph the edges from the vertices representing those variables to the given vertex.] SideEffects [] ******************************************************************************/ void PartPartitionCreateVertexFaninEdges( graph_t *partition, vertex_t *vertexPtr) { vertex_t *fromVertex; Mvf_Function_t *vertexFunction; st_table *support; st_table *mddIdToVertex; st_generator *stGen; long mddId; mddIdToVertex = PartPartitionReadMddIdToVertex(partition); vertexFunction = PartVertexReadFunction(vertexPtr); support = PartCreateFunctionSupportTable(vertexFunction); /* Create the edges for every element in support */ st_foreach_item(support, stGen, &mddId, NULL) { st_lookup(mddIdToVertex, (char *)mddId, &fromVertex); /* Make sure no self loops are created */ if (fromVertex != vertexPtr) { g_add_edge(fromVertex, vertexPtr); } /* End of if */ } st_free_table(support); } /* End of PartPartitionCreateVertexFaninEdges */ /**Function******************************************************************** Synopsis [Prints information about the Partition through standard output.] Description [ The format used for printing is dot, a tool for graph visualization developed at AT&T. It can be obtained from http://www.research.att.com/orgs/ssr/book/reuse. The function receives as a parameter a file pointer in case the print wants to be redirected. This function is used by the command routine CommandPrintPartition.] SideEffects [] ******************************************************************************/ int PartPartitionPrint( FILE *fp, graph_t *partition) { lsGen gen; /* To iterate over edges */ edge_t *edgePtr; /* Will hold the edge being processed */ vertex_t *fromVertex; /* Will hold the vertex source of the edge */ vertex_t *toVertex; /* Will hold the destination of the edge */ st_table *vertexToId; /* To lookup the ordinal of a vertex */ time_t now = time(0); struct tm *nowStructPtr = localtime(& now); char *nowTxt = asctime(nowStructPtr); char *partitionName = PartPartitionReadName(partition); int vertexId; int clusterId; /* * Write out the header for the output file. */ (void) fprintf(fp, "# %s\n", Vm_VisReadVersion()); (void) fprintf(fp, "# partition name: %s\n", partitionName); (void) fprintf(fp, "# generated: %s", nowTxt); (void) fprintf(fp, "#\n"); (void) fprintf(fp, "# Partition with %d vertices and %d edges\n", lsLength(g_get_vertices(partition)), lsLength(g_get_edges(partition))); (void) fprintf(fp, "digraph \"%s\" {\n rotate=90;\n", partitionName); (void) fprintf(fp, " margin=0.5;\n label=\"%s\";\n", partitionName); (void) fprintf(fp, " size=\"10,7.5\";\n ratio=\"fill\";\n"); vertexToId = st_init_table(st_ptrcmp, st_ptrhash); vertexId = 0; clusterId = 0; foreach_vertex(partition, gen, fromVertex) { if (PartVertexReadType(fromVertex) == Part_VertexCluster_c) { array_t *members = PartVertexReadClusterMembers(fromVertex); vertex_t *auxPtr; int i; (void) fprintf(fp, " subgraph cluster%d {\n", clusterId++); (void) fprintf(fp, " label = \"%s\";\n", PartVertexReadName(fromVertex)); arrayForEachItem(vertex_t *, members, i, auxPtr) { (void) fprintf(fp, " "); st_insert(vertexToId, (char *)auxPtr, (char *)(long)vertexId); PrintVertexDescription(fp, auxPtr, vertexId++); } (void) fprintf(fp, " }\n"); } /* End of then */ else if (!PartVertexTestIsClustered(fromVertex)) { st_insert(vertexToId, (char *)fromVertex, (char *)(long)vertexId); PrintVertexDescription(fp, fromVertex, vertexId++); } } foreach_edge(partition, gen, edgePtr) { fromVertex = g_e_source(edgePtr); toVertex = g_e_dest(edgePtr); st_lookup_int(vertexToId, (char *)fromVertex, &vertexId); (void) fprintf(fp, " node%d -> ", vertexId); st_lookup_int(vertexToId, (char *)toVertex, &vertexId); (void) fprintf(fp, "node%d;\n", vertexId); } /* End of foreach_edge */ (void) fprintf(fp, "}\n"); st_free_table(vertexToId); return 1; } /* End of PartPartitionPrint */ /**Function******************************************************************** Synopsis [Create latch nodes list and leave nodes list form CTL properties and fairness constraints] Comments [] SideEffects [] SeeAlso [] ******************************************************************************/ int PartGetLatchInputListFromCTL( Ntk_Network_t *network, array_t *ctlArray, array_t *fairArray, lsList latchInputList) { return PartGetLatchInputListFromCtlAndLtl(network, ctlArray, NIL(array_t), fairArray, latchInputList, FALSE); } /**Function******************************************************************** Synopsis [Create latch inputs list form properties and fairness constraints] Comments [Return all the Cone-Of-Influence nodes if stopAtLatch is FALSE; otherwise, return only the nodes up to the immediate support.] SideEffects [] SeeAlso [] ******************************************************************************/ int PartGetLatchInputListFromCtlAndLtl( Ntk_Network_t *network, array_t *ctlArray, array_t *ltlArray, array_t *fairArray, lsList latchInputList, boolean stopAtLatch) { int i; Ctlp_Formula_t *ctlFormula; Ctlsp_Formula_t *ltlFormula; st_table *formulaNodes; st_generator *stGen; array_t *nodeArray; array_t *formulaCombNodes; Ntk_Node_t *node; formulaNodes = st_init_table( st_ptrcmp, st_ptrhash ); if ( formulaNodes == NIL(st_table)){ return 0; } /* * Extract nodes in CTL/LTL properties */ if ( ctlArray != NIL(array_t)){ arrayForEachItem( Ctlp_Formula_t *, ctlArray, i, ctlFormula ) { Mc_NodeTableAddCtlFormulaNodes( network, ctlFormula, formulaNodes ); } } if ( ltlArray != NIL(array_t)){ arrayForEachItem( Ctlsp_Formula_t *, ltlArray, i, ltlFormula ) { Mc_NodeTableAddLtlFormulaNodes( network, ltlFormula, formulaNodes ); } } /* * Extract nodes in fairness properties */ if ( fairArray != NIL(array_t)){ arrayForEachItem( Ctlp_Formula_t *, fairArray, i, ctlFormula ) { Mc_NodeTableAddCtlFormulaNodes( network, ctlFormula, formulaNodes ); } } nodeArray = array_alloc( Ntk_Node_t *, 0 ); st_foreach_item( formulaNodes, stGen, &node, NULL) { array_insert_last( Ntk_Node_t *, nodeArray, node ); } st_free_table( formulaNodes ); /* * Get all combinational support nodes in network from formula nodes */ formulaCombNodes = Ntk_NodeComputeCombinationalSupport( network, nodeArray, stopAtLatch ); array_free(nodeArray); /* * Root list includes latch data input nodes */ arrayForEachItem( Ntk_Node_t *, formulaCombNodes, i, node ) { if ( Ntk_NodeTestIsLatch( node ) ) { Ntk_Node_t *tempNode = Ntk_LatchReadDataInput( node ); lsNewEnd(latchInputList, (lsGeneric)tempNode, LS_NH); } } array_free(formulaCombNodes); return 1; } /**Function******************************************************************** Synopsis [Create latch nodes list form properties and fairness constraints] Comments [Return all the Cone-Of-Influence nodes if stopAtLatch is FALSE; otherwise, return only the nodes up to the immediate support.] SideEffects [] SeeAlso [] ******************************************************************************/ int PartGetLatchListFromCtlAndLtl( Ntk_Network_t *network, array_t *ctlArray, array_t *ltlArray, array_t *fairArray, lsList latchInputList, boolean stopAtLatch) { int i; Ctlp_Formula_t *ctlFormula; Ctlsp_Formula_t *ltlFormula; st_table *formulaNodes; st_generator *stGen; array_t *nodeArray; array_t *formulaCombNodes; Ntk_Node_t *node; formulaNodes = st_init_table( st_ptrcmp, st_ptrhash ); if ( formulaNodes == NIL(st_table)){ return 0; } /* * Extract nodes in CTL/LTL properties */ if ( ctlArray != NIL(array_t)){ arrayForEachItem( Ctlp_Formula_t *, ctlArray, i, ctlFormula ) { Mc_NodeTableAddCtlFormulaNodes( network, ctlFormula, formulaNodes ); } } if ( ltlArray != NIL(array_t)){ arrayForEachItem( Ctlsp_Formula_t *, ltlArray, i, ltlFormula ) { Mc_NodeTableAddLtlFormulaNodes( network, ltlFormula, formulaNodes ); } } /* * Extract nodes in fairness properties */ if ( fairArray != NIL(array_t)){ arrayForEachItem( Ctlp_Formula_t *, fairArray, i, ctlFormula ) { Mc_NodeTableAddCtlFormulaNodes( network, ctlFormula, formulaNodes ); } } nodeArray = array_alloc( Ntk_Node_t *, 0 ); st_foreach_item( formulaNodes, stGen, &node, NULL) { array_insert_last( Ntk_Node_t *, nodeArray, node ); } st_free_table( formulaNodes ); /* * Get all combinational support nodes in network from formula nodes */ formulaCombNodes = Ntk_NodeComputeCombinationalSupport( network, nodeArray, stopAtLatch ); array_free(nodeArray); /* * Root list includes latch data input nodes */ arrayForEachItem( Ntk_Node_t *, formulaCombNodes, i, node ) { if ( Ntk_NodeTestIsLatch( node ) ) { lsNewEnd(latchInputList, (lsGeneric)node, LS_NH); } } array_free(formulaCombNodes); return 1; } /*---------------------------------------------------------------------------*/ /* Definition of static functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Prints the declaration of a vertex in dot format.] SideEffects [] SeeAlso [Part_PartitionPrint] ******************************************************************************/ static void PrintVertexDescription( FILE *fp, vertex_t *vertexPtr, int order) { char *name = PartVertexReadName(vertexPtr); (void) fprintf(fp, " node%d [label=", order); if (name != NIL(char)) { (void) fprintf(fp, "\"%s\"", name); } else { (void) fprintf(fp, "\"None\""); } (void) fprintf(fp, "]; \n"); } /* End of PrintVertexDescription */