VIS
|
#include "partInt.h"
Go to the source code of this file.
Functions | |
static int | CommandBuildPartitionMdds (Hrc_Manager_t **hmgr, int argc, char **argv) |
static int | CommandPrintPartition (Hrc_Manager_t **hmgr, int argc, char **argv) |
static int | CommandPrintPartitionStats (Hrc_Manager_t **hmgr, int argc, char **argv) |
static void | TimeOutHandle (void) |
void | Part_Init (void) |
void | Part_End (void) |
void | PartNameFree (lsGeneric name) |
Variables | |
static char rcsid[] | UNUSED = "$Id: partCmd.c,v 1.22 2009/04/11 01:47:18 fabio Exp $" |
static jmp_buf | timeOutEnv |
static int CommandBuildPartitionMdds | ( | Hrc_Manager_t ** | hmgr, |
int | argc, | ||
char ** | argv | ||
) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Implements the build_partition_mdds command.]
Description [The data structure needed to store the information related to the partitioning process will be stored in a graph_t structure that will become part of the network. This procedure checks if the network has already registered this application. If not, a new structure is allocated. After this process, depending on the type of method specified in the command line, the specific routine is executed. The user may set the specific flag partition_method
as the default to be used whenever no method is specified in the command line. If no flag is defined, the frontier
method will be used.]
CommandName [build_partition_mdds]
CommandSynopsis [build a partition of MDDs for the flattened network]
CommandArguments [\[-h\] \[-i\] \[-n <list>\] \[-s <num>\] \[-t <seconds>\] \[-v\] \[<method>\]]
CommandDescription [Build the MDDs of a flattened network. Depending on the method
selected, the MDDs for the combinational outputs (COs) are built in terms of either the combinational inputs (CIs) or in terms of some subset of intermediate nodes of the network. The MDDs built are stored in a DAG called a "partition". The vertices of a partition correspond to the CIs, COs, and any intermediate nodes used. Each vertex has a multi-valued function (represented by MDDs) expressing the function of the corresponding network node in terms of the partition vertices in its transitive fanin. Hence, the MDDs of the partition represent a partial collapsing of the network.
This command must be preceded by the commands flatten_hierarchy
and static_order
. The partition built is stored with the network for use by other commands, such as simulate
, compute_reach
, model_check
, etc. This command has no affect when invoked on a network that already has a partition. To remove the existing partition of a network, reinvoke flatten_hierarchy
.
The choice of method
determines which intermediate nodes are used. The inout
method represents one extreme where no intermediate nodes are used, and total
represents the other extreme where every node in the network has a corresponding vertex in the partition. If no method
is specified on the command line, then the value of the flag partition_method
is used (this flag is set by the command set partition_method
), unless it does not have a value, in which case the forntier
method is used. The different methods available are:
inout
Expresses the combinational outputs in terms of the combinational inputs.
total
The partition built is isomorphic to the combinational part of the network. The function of each node is expressed in terms of its immediate fanins. If the -i
is used the function attached to each vertex is computed as a function of the combinational inputs.
partial
Builds a partition using the intermediate nodes specified with the -n
option or the -f
option.
frontier
(default) Builds a partition creating vertices for the intermediate nodes as needed in order to control the BDD size. The threshold value for the BDD size can be set by the parameter "partition_threshold". This method encompasses both "inout" (set partition_threshold parameter to infinity) and "total" (set partition_threshold parameter to 0).
boundary
Builds a partition in a fashion that preserves all nodes that are Input/Output nodes of any hnode in the hierarchy rooted at the current hnode.
Command options:
Print the command usage.
Build the multi-valued functions of each partition vertex in terms of the combinational inputs, rather than in terms of its transitive fanin vertices.
Used in conjunction with the partial
method. List
is a comma separated list of network nodes to use as intermediate nodes in the partition.
Level of severity of a post-computation check applied to the partition data structure (0 by default, meaning no check).
Time in seconds allowed to build the partition. If the computation time goes above that limit, the process of building the partition is aborted. The default is no limit.
Turn on the verbosity.
]
SideEffects [Registers in the network the partition application with the key specified by PART_NETWORK_APPL_KEY]
SeeAlso [Ntk_NetworkAddApplInfo]
Definition at line 206 of file partCmd.c.
{ static Part_PartitionMethod method; static boolean inTermsOfLeaves; lsList nodeList = lsCreate(); graph_t *partition; static int verbose; static int sanityCheck; static int timeOutPeriod; int c; int length; char *methodString; char *modelName; Hrc_Node_t *currentNode; Ntk_Network_t *network = Ntk_HrcManagerReadCurrentNetwork(*hmgr); char *nodeName; char *tmpNodeName; char *realName; FILE *nodeFile; static boolean fileUsed; fileUsed = FALSE; inTermsOfLeaves = FALSE; verbose = 0; sanityCheck = 0; timeOutPeriod = 0; nodeFile = NIL(FILE); util_getopt_reset(); while ((c = util_getopt(argc, argv, "f:hvin:s:t:")) != EOF) { switch(c) { case 'f': fileUsed = TRUE; nodeFile = Cmd_FileOpen(util_optarg, "r", &realName, 1); FREE(realName); if (nodeFile == NIL(FILE)){ (void)fprintf(vis_stderr,"Cannot open %s\n", util_optarg); lsDestroy(nodeList, (void (*)(lsGeneric))0); return 1; } else{ tmpNodeName = ALLOC(char, 512); while(fscanf(nodeFile, "%s\n", tmpNodeName) != EOF){ if(*tmpNodeName != '#'){ nodeName = ALLOC(char, strlen(tmpNodeName) + 2); sprintf(nodeName, "%s", tmpNodeName); lsNewEnd(nodeList, (lsGeneric)nodeName, NIL(lsHandle)); } } FREE(tmpNodeName); } break; case 'h': goto usage; case 'i': inTermsOfLeaves = TRUE; break; case 'v': verbose = 1; break; case 's': sanityCheck = atoi(util_optarg); break; case 't': timeOutPeriod = atoi(util_optarg); break; case 'n': length = strlen(util_optarg); for(c = 0; c < length; c++) { if (util_optarg[c] == ',') { util_optarg[c] = 0; } /* End of if */ } /* End of for */ c = 0; while (c < length) { lsNewEnd(nodeList, &util_optarg[c], NIL(lsHandle)); while (util_optarg[c++] != 0); } /* End of while */ break; default: goto usage; } } if (argc == util_optind) { /* No method specified. Choosing default */ methodString = Cmd_FlagReadByName("partition_method"); if (methodString == NIL(char)) { methodString = "default"; } } else { methodString = argv[util_optind]; } if (strcmp(methodString,"inout") == 0) { method = Part_InOut_c; if (lsLength(nodeList) != 0) { (void) fprintf(vis_stderr, "Ignoring provided list of nodes in <inout>"); (void) fprintf(vis_stderr, " method\n"); } /* End of if */ if (inTermsOfLeaves) { (void) fprintf(vis_stderr, "Ignoring -i flag in the <inout> method\n"); } /* End of if */ } else if (strcmp(methodString,"partial") == 0) { method = Part_Partial_c; /* Make sure a list of nodes has been provided */ if (lsLength(nodeList) == 0) { (void) fprintf(vis_stderr, "Method <partial> requires a non-empty list"); (void) fprintf(vis_stderr, " of nodes\n"); lsDestroy(nodeList, (void (*)(lsGeneric))0); goto usage; } /* End of if */ } else if (strcmp(methodString,"total") == 0) { method = Part_Total_c; if (lsLength(nodeList) != 0) { (void) fprintf(vis_stderr, "Ignoring provided list of nodes in <total>"); (void) fprintf(vis_stderr, " method\n"); } /* End of if */ } else if (strcmp(methodString,"frontier") == 0) { method = Part_Frontier_c; } else if (strcmp(methodString,"boundary") == 0) { method = Part_Boundary_c; } else if (strcmp(methodString, "fine") == 0) { method = Part_Fine_c; } else if (strcmp(methodString, "default") == 0) { method = Part_Default_c; } else { goto usage; } /* Check if the network has been read in */ if (network == NIL(Ntk_Network_t)) { lsDestroy(nodeList, (void (*)(lsGeneric))0); return 1; } /* Check if the network has the variables ordered */ if (Ord_NetworkTestAreVariablesOrdered(network, Ord_InputAndLatch_c) == FALSE) { (void) fprintf(vis_stdout, "The MDD variables have not been ordered. Use static_order.\n"); lsDestroy(nodeList, (void (*)(lsGeneric))0); return 1; } /* Check if there is already a partition attached to the network */ partition = (graph_t *) Ntk_NetworkReadApplInfo(network, PART_NETWORK_APPL_KEY); /* If there is, just return. */ if (partition != NIL(graph_t)) { (void) fprintf(vis_stderr, "partition already built; reinvoke "); (void) fprintf(vis_stderr, "flatten_hierarchy to remove the current partition\n"); return 1; } /* Read the name of the model to be passed to Part_NetworkCreatePartition */ currentNode = Hrc_ManagerReadCurrentNode(*hmgr); modelName = Hrc_NodeReadModelName(currentNode); /* Set the timeout */ if (timeOutPeriod > 0) { (void) signal(SIGALRM, (void(*)(int))TimeOutHandle); (void) alarm(timeOutPeriod); if (setjmp(timeOutEnv) > 0) { (void) fprintf(vis_stdout, "Partition: timeout occurred after "); (void) fprintf(vis_stdout, "%d seconds\n", timeOutPeriod); alarm(0); /* Partial clean up */ lsDestroy(nodeList, (void (*)(lsGeneric))0); return 1; } } /* * Execute the partition algorithm. The two nil pointers is to indicate * that the graph must represent the complete network. */ partition = Part_NetworkCreatePartition(network, currentNode, modelName, (lsList)0, (lsList)0, NIL(mdd_t), method, nodeList, inTermsOfLeaves, verbose, sanityCheck); /* Register the partition in the network if any */ Ntk_NetworkAddApplInfo(network, PART_NETWORK_APPL_KEY, (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback, (void *) partition); /* Deactivate the alarm */ alarm(0); /* Clean up */ if(fileUsed){ lsDestroy(nodeList, PartNameFree); } else{ lsDestroy(nodeList, (void (*)(lsGeneric))0); } return 0; usage: (void) fprintf(vis_stderr, "usage: build_partition_mdds [options] [method]\n"); (void) fprintf(vis_stderr, "Options:\n"); (void) fprintf(vis_stderr, " -h\t\tprint the command usage\n"); (void) fprintf(vis_stderr, " -i\t\tBuild the functions in the partition in terms of the\n"); (void) fprintf(vis_stderr, " \t\tcombinational inputs of the system. This option is redundant if\n"); (void) fprintf(vis_stderr, " \t\tthe inout partition is chosen.\n"); (void) fprintf(vis_stderr, " -n <list>\tComma separated list of network nodes to preserve in the\n"); (void) fprintf(vis_stderr, " \tpartitioning. It only matters if the partial method has been\n"); (void) fprintf(vis_stderr, " \tselected.\n"); (void) fprintf(vis_stderr, " -f <file>\tSpecifies the file containing names of network nodes\n"); (void) fprintf(vis_stderr, " \tto preserve while partitioning. This option matters only \n"); (void) fprintf(vis_stderr, " \tif the partial method has been selected. Each node name must\n"); (void) fprintf(vis_stderr, " \tbe listed on a new line. Comments in <file> must begin with '#'.\n"); (void) fprintf(vis_stderr, " -s <num>\tLevel of severity check applied after computation. 0 being no\n"); (void) fprintf(vis_stderr, " \t\tcheck, 1 begin simple check and >1 being exhaustive check.\n"); (void) fprintf(vis_stderr, " -t <sec>\tTime in seconds allowed to build the partition. If the\n"); (void) fprintf(vis_stderr, " \tcomputation time goes above that limit, the process of building\n"); (void) fprintf(vis_stderr, " \tthe partition is aborted.\n"); (void) fprintf(vis_stderr, " -v\t\tverbose\n"); (void) fprintf(vis_stderr, "Methods\n"); (void) fprintf(vis_stderr, " inout\tIt represents the network with one MDD for\n"); (void) fprintf(vis_stderr, " \teach combinational output as a function of the combinational\n"); (void) fprintf(vis_stderr, " \tinputs\n"); (void) fprintf(vis_stderr, " total\tPartitions the network preserving its structure. Every node in\n"); (void) fprintf(vis_stderr, " \tthe network will produce a vertex in the partition graph. The\n"); (void) fprintf(vis_stderr, " \tflag -i explained above controls the support of\n"); (void) fprintf(vis_stderr, " \tthe functions attached to the vertices.\n"); (void) fprintf(vis_stderr, " frontier\tThe default method. Partitions the network creating vertices for intermediate nodes\n"); (void) fprintf(vis_stderr, " \tas necessary to control the BDD size. The threshold value of the\n"); (void) fprintf(vis_stderr, " \tBDD can be specified by partition_threshold.\n"); (void) fprintf(vis_stderr, " partial\tPartitions the network preserving certain nodes specified with\n"); (void) fprintf(vis_stderr, " \tthe option -n or -f.\n"); (void) fprintf(vis_stderr, " boundary\tPartitions the network preserving all nodes that are \n"); (void) fprintf(vis_stderr, " \tsubcircuit IOs.\n"); lsDestroy(nodeList, (void (*)(lsGeneric))0); return 1; /* Error exit */ } /* End of CommandBuildPartitionMdds */
static int CommandPrintPartition | ( | Hrc_Manager_t ** | hmgr, |
int | argc, | ||
char ** | argv | ||
) | [static] |
Function********************************************************************
Synopsis [Command level routine to write a file in dot format of the partition DAG.]
SideEffects []
SeeAlso [CommandBuildPartitionMdds]
CommandName [print_partition]
CommandSynopsis [print the "dot" format describing the partition graph]
CommandArguments [\[-h\] <file>]
CommandDescription [Write a file in the format taken by the tool dot
. Dot is a tool that, given a description of a graph in a certain format, produces a postscript print of the graph. For more information about dot
look in http://www.research.att.com/sw/tools/graphviz.
If no argument is specified on the command line, the output is written to the standard output.
Command options:
Print the command usage.
Name of file where the partition is to be written in "dot" format.
]
Definition at line 520 of file partCmd.c.
{ FILE *fp; int c, status; graph_t *partition; Ntk_Network_t *network = Ntk_HrcManagerReadCurrentNetwork(*hmgr); util_getopt_reset(); while ((c = util_getopt(argc,argv,"h")) != EOF){ switch(c){ case 'h': goto usage; default: goto usage; } } /* Check if the network has been read in */ if (network == NIL(Ntk_Network_t)) { return 1; } /* Check if there is a partition attached to the network */ partition = (graph_t *) Ntk_NetworkReadApplInfo(network, PART_NETWORK_APPL_KEY); if (partition == NIL(graph_t)) { (void) fprintf(vis_stderr, "No partition has been created for this network.\n"); return 1; } if (argc == 1) { fp = vis_stdout; } else if (argc == 2) { fp = Cmd_FileOpen(*(++argv), "w", NIL(char *), /* silent */ 1); if (fp == NIL(FILE)) { (void) fprintf(vis_stderr, "Cannot write to %s\n", *argv); return 1; } } else { goto usage; } error_init(); status = PartPartitionPrint(fp, partition); (void) fprintf(vis_stderr, "%s", error_string()); fflush(fp); /* If we opened a file before, close it */ if (argc == 2) { (void) fclose(fp); } return (status ? 0 : 1); usage: (void) fprintf(vis_stderr, "usage: print_partition [-h] [file]\n"); (void) fprintf(vis_stderr, " -h\t\tprint the command usage\n"); return 1; } /* End of CommandPrintPartition */
static int CommandPrintPartitionStats | ( | Hrc_Manager_t ** | hmgr, |
int | argc, | ||
char ** | argv | ||
) | [static] |
Function********************************************************************
Synopsis [Command level routine to print some stats of the partition DAG.]
SideEffects []
SeeAlso [CommandBuildPartitionMdds]
CommandName [print_partition_stats]
CommandSynopsis [print statistics about the partition graph]
CommandArguments [\[-h\] \[-n\]]
CommandDescription [Print statistics about the partition currently attached to the network, such as:
Method used to build the partition. Number of sink vertices. Number of source vertices. Total number of vertices. Number of shared MDD nodes used to represent the functions.
Command options:
Print the command usage.
Print the name of the network nodes represented by vertices in the partition.
]
Definition at line 624 of file partCmd.c.
{ int c; graph_t *partition; Ntk_Network_t *network = Ntk_HrcManagerReadCurrentNetwork(*hmgr); boolean printNodeNames = FALSE; util_getopt_reset(); while ((c = util_getopt(argc,argv,"hn")) != EOF){ switch(c){ case 'n': printNodeNames = TRUE; break; case 'h': goto usage; default: goto usage; } } /* Check if the network has been read in */ if (network == NIL(Ntk_Network_t)) { return 1; } /* Check if there is a partition attached to the network */ partition = (graph_t *) Ntk_NetworkReadApplInfo(network, PART_NETWORK_APPL_KEY); if (partition == NIL(graph_t)) { (void) fprintf(vis_stderr, "No partition has been created for this network.\n"); return 1; } /* Print the statistics to vis_stdout */ Part_PartitionPrintStats(vis_stdout, partition, printNodeNames); return 0; usage: (void) fprintf(vis_stderr, "usage: print_partition_stats [-h] [-n]\n"); (void) fprintf(vis_stderr, " -h\t\tprint the command usage\n"); (void) fprintf(vis_stderr, " -n\t\tprint names of network nodes "); (void) fprintf(vis_stderr, "represented by vertices\n"); return 1; } /* End of CommandPrintPartitionStats */
void Part_End | ( | void | ) |
void Part_Init | ( | void | ) |
AutomaticEnd Function********************************************************************
Synopsis [Initializes the partitioning package.]
SideEffects []
SeeAlso [Part_End]
Definition at line 62 of file partCmd.c.
{ Cmd_CommandAdd("build_partition_mdds", CommandBuildPartitionMdds, 0/* doesn't change network */); Cmd_CommandAdd("print_partition", CommandPrintPartition, 0/* doesn't change network */); Cmd_CommandAdd("print_partition_stats", CommandPrintPartitionStats, 0/* doesn't change network*/); } /* End of Part_Init */
void PartNameFree | ( | lsGeneric | name | ) |
Function********************************************************************
Synopsis [This frees a given char *]
Description [This function frees the memory assocated with a char * that is given as input]
SideEffects [ ]
SeeAlso []
Definition at line 475 of file partCmd.c.
{ FREE(name); }
static void TimeOutHandle | ( | void | ) | [static] |
Function********************************************************************
Synopsis [required]
Description [optional]
SideEffects [required]
SeeAlso [optional]
Definition at line 685 of file partCmd.c.
{ longjmp(timeOutEnv, 1); } /* End of TimeOutHandle */
jmp_buf timeOutEnv [static] |
char rcsid [] UNUSED = "$Id: partCmd.c,v 1.22 2009/04/11 01:47:18 fabio Exp $" [static] |
CFile***********************************************************************
FileName [partCmd.c]
PackageName [part]
Synopsis [Command interface for the partition package.]
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.]