[14] | 1 | /**CHeaderFile***************************************************************** |
---|
| 2 | |
---|
| 3 | FileName [part.h] |
---|
| 4 | |
---|
| 5 | PackageName [part] |
---|
| 6 | |
---|
| 7 | Synopsis [Partition of a system and creation of MDDs.] |
---|
| 8 | |
---|
| 9 | Description [Once the description of a system has been read, and the ordering |
---|
| 10 | of the variables has been assigned, the partition package creates an |
---|
| 11 | abstracted view of the system in which only information in terms of MDDs is |
---|
| 12 | stored. The MDDs belong to the MDD manager of the system. Different options |
---|
| 13 | may be considered when creating this abstracted view. If the system is |
---|
| 14 | described as a network there are several options to create this partition. As |
---|
| 15 | a first choice, the system may be considered as a set of functions |
---|
| 16 | representing the combinational outputs as functions of the combinational |
---|
| 17 | inputs. In general, the latch functions may be specified as functions of any |
---|
| 18 | intermediate variables. These intermediate variables are themselves functions |
---|
| 19 | of other variables, and ultimately the dependency on the combinational inputs |
---|
| 20 | is achieved. The structure to represent these arbitrary dependencies is a |
---|
| 21 | DAG. The combinational inputs of the network will be represented as |
---|
| 22 | vertices. Every other function (either representing a latch or any other |
---|
| 23 | intermediate node) is represented as a vertex with in-coming edges from the |
---|
| 24 | vertices representing the function's domain. Hence, the vertices representing |
---|
| 25 | the combinational inputs will not have any in-coming edges, and conversely, |
---|
| 26 | the vertices representing the combinational outputs will not have any fanout |
---|
| 27 | edges.<p> |
---|
| 28 | |
---|
| 29 | The partition may have two types of vertices, called single and |
---|
| 30 | clustered. Single vertices are the ones that represent, for example, nodes in |
---|
| 31 | a network. Clustered vertices are used solely for the purpose of grouping |
---|
| 32 | single vertices into disjoint sets. No clustered vertex can be member of a |
---|
| 33 | clustered vertex, and every single vertex may be a member of a unique clustered |
---|
| 34 | vertex. The edges of the graph are connecting only single vertices. Functions |
---|
| 35 | are provided to access the list of vertices represented by a clustered vertex |
---|
| 36 | as well as for testing the type of a vertex.<p> |
---|
| 37 | |
---|
| 38 | A partition is the central input to the image computation |
---|
| 39 | package. However, it is important to note that there is no network-specific |
---|
| 40 | information stored in the partition data structure itself. Hence, it is |
---|
| 41 | possible that another application (i.e. besides the network application) |
---|
| 42 | could create a partition, and use that partition as input to the image |
---|
| 43 | computation package.] |
---|
| 44 | |
---|
| 45 | Author [Abelardo Pardo] |
---|
| 46 | |
---|
| 47 | Copyright [This file was created at the University of Colorado at |
---|
| 48 | Boulder. The University of Colorado at Boulder makes no warranty |
---|
| 49 | about the suitability of this software for any purpose. It is |
---|
| 50 | presented on an AS IS basis.] |
---|
| 51 | |
---|
| 52 | Revision [$Id: part.h,v 1.33 2009/04/11 01:47:18 fabio Exp $] |
---|
| 53 | |
---|
| 54 | ******************************************************************************/ |
---|
| 55 | |
---|
| 56 | #ifndef _PART |
---|
| 57 | #define _PART |
---|
| 58 | |
---|
| 59 | #include "ntk.h" |
---|
| 60 | |
---|
| 61 | /*---------------------------------------------------------------------------*/ |
---|
| 62 | /* Constant declarations */ |
---|
| 63 | /*---------------------------------------------------------------------------*/ |
---|
| 64 | #define PART_NETWORK_APPL_KEY "Part_NetworkApplKey" |
---|
| 65 | |
---|
| 66 | /*---------------------------------------------------------------------------*/ |
---|
| 67 | /* Structure declarations */ |
---|
| 68 | /*---------------------------------------------------------------------------*/ |
---|
| 69 | |
---|
| 70 | /**Enum************************************************************************ |
---|
| 71 | |
---|
| 72 | Synopsis [Different methods of partitioning a system.] |
---|
| 73 | |
---|
| 74 | SeeAlso [PartPartitionInputsOutputs PartPartitionTotal |
---|
| 75 | PartPartitionPartial] |
---|
| 76 | |
---|
| 77 | ******************************************************************************/ |
---|
| 78 | typedef enum { |
---|
| 79 | Part_Default_c, /* Default partition. (Right now Outputs as function of |
---|
| 80 | * inputs) */ |
---|
| 81 | Part_InOut_c, /* Outputs as function of inputs */ |
---|
| 82 | Part_Total_c, /* Replicates the system's structure */ |
---|
| 83 | Part_Partial_c, /* Preserves certain user-provided nodes */ |
---|
| 84 | Part_Frontier_c, |
---|
| 85 | Part_Boundary_c, /* partition nodes are subckt IOs */ |
---|
| 86 | Part_Fine_c /* partition nodes are subckt IOs */ |
---|
| 87 | } Part_PartitionMethod; |
---|
| 88 | |
---|
| 89 | /**Enum************************************************************************ |
---|
| 90 | |
---|
| 91 | Synopsis [Type of vertex in the partition.] |
---|
| 92 | |
---|
| 93 | Description [There are two types of vertices in the partition: single and |
---|
| 94 | clustered. A single vertex represents itself and it may have a multi-valued |
---|
| 95 | function and a MddId attached to it. A clustered vertex represents a set of |
---|
| 96 | single vertices. The only information stored in this type of vertex is the |
---|
| 97 | list of single vertices being represented by the cluster. Only one level of |
---|
| 98 | hierarchy is allowed, that is, clustered vertices may only represent single |
---|
| 99 | vertices. Every single vertex may only be represented by a unique clustered |
---|
| 100 | vertex. In other words, a vertex representing a cluster of vertices cannot be |
---|
| 101 | a member of another cluster.] |
---|
| 102 | |
---|
| 103 | SeeAlso [PartVertexInfo] |
---|
| 104 | |
---|
| 105 | ******************************************************************************/ |
---|
| 106 | typedef enum { |
---|
| 107 | Part_VertexCluster_c, /* Vertex represents a cluster of vertices */ |
---|
| 108 | Part_VertexSingle_c /* Vertex represents itself */ |
---|
| 109 | } Part_VertexType; |
---|
| 110 | |
---|
| 111 | /**Enum************************************************************************ |
---|
| 112 | |
---|
| 113 | Synopsis [ Methods of Breaking for State Space Decomposition ] |
---|
| 114 | |
---|
| 115 | SeeAlso [] |
---|
| 116 | |
---|
| 117 | ******************************************************************************/ |
---|
| 118 | typedef enum{ |
---|
| 119 | Part_BSRR_s, /* static round robin seed choice */ |
---|
| 120 | Part_BFix_v /* fixed order vertex choice */ |
---|
| 121 | } Part_BMethod; |
---|
| 122 | |
---|
| 123 | /**Enum************************************************************************ |
---|
| 124 | |
---|
| 125 | Synopsis [ Method of Correlation calculation. ] |
---|
| 126 | |
---|
| 127 | Description [ Correlation is calculated by ratio of minterm count of XOR. |
---|
| 128 | If BDD function is not available or try to avoid using MDD operation, |
---|
| 129 | correaltion can be calculated by second method. Then, support set is |
---|
| 130 | generated from network and correlation is simply the ration of common support |
---|
| 131 | to union of two support sets.] |
---|
| 132 | |
---|
| 133 | SeeAlso [] |
---|
| 134 | |
---|
| 135 | ******************************************************************************/ |
---|
| 136 | typedef enum{ |
---|
| 137 | Part_CorrelationWithBDD, /* correlation is based on BDD correlation */ |
---|
| 138 | Part_CorrelationWithSupport, /* correlation is based on support */ |
---|
| 139 | Part_CorrelationDefault |
---|
| 140 | } Part_CMethod; |
---|
| 141 | |
---|
| 142 | /*---------------------------------------------------------------------------*/ |
---|
| 143 | /* Type declarations */ |
---|
| 144 | /*---------------------------------------------------------------------------*/ |
---|
| 145 | typedef struct PartSubsystemInfo Part_SubsystemInfo_t; |
---|
| 146 | typedef struct PartSubsystem Part_Subsystem_t; |
---|
| 147 | |
---|
| 148 | /*---------------------------------------------------------------------------*/ |
---|
| 149 | /* Variable declarations */ |
---|
| 150 | /*---------------------------------------------------------------------------*/ |
---|
| 151 | |
---|
| 152 | |
---|
| 153 | /*---------------------------------------------------------------------------*/ |
---|
| 154 | /* Macro declarations */ |
---|
| 155 | /*---------------------------------------------------------------------------*/ |
---|
| 156 | |
---|
| 157 | |
---|
| 158 | /**AutomaticStart*************************************************************/ |
---|
| 159 | |
---|
| 160 | /*---------------------------------------------------------------------------*/ |
---|
| 161 | /* Function prototypes */ |
---|
| 162 | /*---------------------------------------------------------------------------*/ |
---|
| 163 | |
---|
| 164 | EXTERN void Part_Init(void); |
---|
| 165 | EXTERN void Part_End(void); |
---|
| 166 | EXTERN array_t * Part_PartitionBuildFunctions(graph_t *partition, array_t *roots, array_t *leaves, mdd_t *careSet); |
---|
| 167 | EXTERN array_t * Part_PartitionCollapse(graph_t *partition, array_t *roots, st_table *leaves, mdd_t *careSet); |
---|
| 168 | EXTERN array_t * Part_PartGroupVeriticesBasedOnHierarchy(Ntk_Network_t *network, array_t *latchDataInputNames); |
---|
| 169 | EXTERN array_t * Part_PartCreateSubsystems(Part_SubsystemInfo_t *subInfo, array_t *arrayOfLatchNames, array_t *arrayOfGroupIndex); |
---|
| 170 | EXTERN array_t * Part_PartCreateSubsystemsWithCTL(Part_SubsystemInfo_t *subInfo, array_t *ctlArray, array_t *fairArray,boolean dynamicIncrease,boolean dynamicAndDependency); |
---|
| 171 | EXTERN array_t * Part_PartCreateSubsystemsWithCtlAndLtl(Part_SubsystemInfo_t *subInfo, array_t *ctlArray, array_t *ltlArray, array_t *fairArray,boolean dynamicIncrease,boolean dynamicAndDependency,boolean strictBound); |
---|
| 172 | EXTERN st_table * Part_PartitionSubsystemReadVertexTable(Part_Subsystem_t *partitionedSubsystem); |
---|
| 173 | EXTERN array_t * Part_PartitionSubsystemReadFanIn(Part_Subsystem_t *partitionedSubsystem); |
---|
| 174 | EXTERN array_t * Part_PartitionSubsystemReadFanOut(Part_Subsystem_t *partitionedSubsystem); |
---|
| 175 | EXTERN Part_SubsystemInfo_t * Part_PartitionSubsystemInfoInit(Ntk_Network_t *network); |
---|
| 176 | EXTERN void Part_PartitionSubsystemInfoFree(Part_SubsystemInfo_t *partSubInfo); |
---|
| 177 | EXTERN void Part_PartitionSubsystemFree(Part_Subsystem_t *partSubsystem); |
---|
| 178 | EXTERN void Part_PartitionSubsystemInfoSetNetwork(Part_SubsystemInfo_t *subInfo, Ntk_Network_t *network); |
---|
| 179 | EXTERN void Part_PartitionSubsystemInfoSetBreakingMethod(Part_SubsystemInfo_t *subInfo, Part_BMethod bMethod); |
---|
| 180 | EXTERN void Part_PartitionSubsystemInfoSetBound(Part_SubsystemInfo_t *subInfo, int bound); |
---|
| 181 | EXTERN void Part_PartitionSubsystemInfoSetThreshold(Part_SubsystemInfo_t *subInfo, float threshold); |
---|
| 182 | EXTERN void Part_PartitionSubsystemInfoSetVerbosity(Part_SubsystemInfo_t *subInfo, int verbosity); |
---|
| 183 | EXTERN void Part_PartitionSubsystemInfoSetCorrelationMethod(Part_SubsystemInfo_t *subInfo, Part_CMethod corMethod); |
---|
| 184 | EXTERN void Part_PartitionSubsystemInfoSetAffinityFactor( Part_SubsystemInfo_t *subInfo, float affinity); |
---|
| 185 | EXTERN Part_Subsystem_t * Part_PartCreateSingleSubSystem( array_t *arrayOfNodes, Ntk_Network_t *network); |
---|
| 186 | EXTERN graph_t * Part_CreatePartitionFromMvfs(mdd_manager *manager, st_table *nameToMvf, st_table *nameToId, st_table *leafTable, char *partName); |
---|
| 187 | EXTERN graph_t * Part_NetworkCreatePartitionFromMvfs(Ntk_Network_t *network, st_table *nameToMvf); |
---|
| 188 | EXTERN void Part_PartitionFree(graph_t *partition); |
---|
| 189 | EXTERN void Part_PartitionFreeCallback(void *data); |
---|
| 190 | EXTERN vertex_t * Part_PartitionFindVertexByName(graph_t *partition, char *name); |
---|
| 191 | EXTERN vertex_t * Part_PartitionFindVertexByMddId(graph_t *partition, int mddId); |
---|
| 192 | EXTERN char * Part_PartitionReadName(graph_t *partition); |
---|
| 193 | EXTERN Part_PartitionMethod Part_PartitionReadMethod(graph_t *partition); |
---|
| 194 | EXTERN char * Part_PartitionObtainMethodAsString(graph_t *partition); |
---|
| 195 | EXTERN mdd_manager * Part_PartitionReadMddManager(graph_t *partition); |
---|
| 196 | EXTERN Part_VertexType Part_VertexReadType(vertex_t *vertexPtr); |
---|
| 197 | EXTERN char * Part_VertexReadName(vertex_t *vertexPtr); |
---|
| 198 | EXTERN array_t * Part_VertexReadClusterMembers(vertex_t *vertexPtr); |
---|
| 199 | EXTERN Mvf_Function_t * Part_VertexReadFunction(vertex_t *vertexPtr); |
---|
| 200 | EXTERN void Part_VertexSetFunction(vertex_t *vertexPtr, Mvf_Function_t *mvf); |
---|
| 201 | EXTERN int Part_VertexReadMddId(vertex_t *vertexPtr); |
---|
| 202 | EXTERN boolean Part_VertexTestIsClustered(vertex_t *vertexPtr); |
---|
| 203 | EXTERN 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); |
---|
| 204 | EXTERN graph_t * Part_PartitionDuplicate(graph_t *partition); |
---|
| 205 | EXTERN graph_t * Part_NetworkReadPartition(Ntk_Network_t *network); |
---|
| 206 | EXTERN vertex_t * Part_PartitionCreateClusterVertex(graph_t *partition, char *name, array_t *arrayOfVertices); |
---|
| 207 | EXTERN void Part_UpdatePartitionFrontier(Ntk_Network_t *network, graph_t *partition, lsList rootList, lsList leaveList, mdd_t *careSet); |
---|
| 208 | EXTERN void Part_VertexInfoFreeCluster(vertex_t *vertexPtr); |
---|
| 209 | EXTERN boolean Part_PartitionTestCompletelySp(graph_t *partition, array_t *roots, st_table *leaves); |
---|
| 210 | EXTERN boolean Part_PartitionTestDeterministic(graph_t *partition, array_t *roots, st_table *leaves); |
---|
| 211 | EXTERN graph_t * Part_PartCreatePartitionWithCTL(Hrc_Manager_t ** hmgr, Part_PartitionMethod method, int verbose, int sanityCheck, boolean inTermsOfLeaves, array_t *ctlArray, array_t *fairArray); |
---|
| 212 | EXTERN 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); |
---|
| 213 | EXTERN int Part_PartitionChangeRoots(Ntk_Network_t *network, graph_t *partition, lsList rootList, int verbosity); |
---|
| 214 | EXTERN void Part_PartitionPrintStats(FILE *fp, graph_t *partition, boolean printNodeNames); |
---|
| 215 | EXTERN int Part_PartitionGetLatchInputListFromCTL(Ntk_Network_t *network, array_t *ctlArray, array_t *fairArray, lsList latchInputList); |
---|
| 216 | EXTERN int Part_PartitionGetLatchInputListFromCtlAndLtl(Ntk_Network_t *network, array_t *ctlArray, array_t *ltlArray, array_t *fairArray, lsList latchInputList, boolean stopAtLatch); |
---|
| 217 | EXTERN void Part_PartitionReadOrCreateBnvs(Ntk_Network_t *network, st_table *coiLatchTable, st_table *coiBnvTable); |
---|
| 218 | EXTERN void PartPartitionFineGrain( Ntk_Network_t *network, graph_t *partition, mdd_t *careSet); |
---|
| 219 | EXTERN int Part_CheckLeafNodeCondition(Ntk_Node_t *node, st_table *leafTable, int fanoutFreeLimit, int numVariableLimit); |
---|
| 220 | EXTERN int Img_CutCalcTransitiveFanin(st_table *table, st_table *ownTable, Ntk_Node_t *node, Ntk_Node_t *fanin, int limit); |
---|
| 221 | EXTERN Ntk_Node_t * Part_GetFaninFreeLogic(Ntk_Node_t *node); |
---|
| 222 | EXTERN Ntk_Node_t * Part_GetFanoutFreeLogic(Ntk_Node_t *node); |
---|
| 223 | EXTERN void Part_PartitionWithExistingBnvs(Ntk_Network_t *network, graph_t *partition, st_table *coiBnvTable, st_table *absLatchTable, st_table *absBnvTable); |
---|
| 224 | |
---|
| 225 | /**AutomaticEnd***************************************************************/ |
---|
| 226 | |
---|
| 227 | #endif /* _PART */ |
---|