derived attributes: list of derived attributes of the node
See the ntk documentation for more information on types and attributes. The
following is an example describing information associated with a node.
small.latch_in: mdd=2, combinational; data-input comb-output
The flattened name of the node is "small.latch_in", its MDD id is 2, it is
of type combinational, and it is both a data input to a latch, and a
combinational output.
Command options:
- -f
- Print the fanins and fanouts of each node.
- -h
- Print the command usage.
- -t
- Print table statistics for those nodes having tables.
]
SideEffects []
******************************************************************************/
static int
CommandPrintNetwork(
Hrc_Manager_t ** hmgr,
int argc,
char ** argv)
{
int c;
boolean printIo = FALSE; /* default */
boolean printTableStats = FALSE; /* default */
Ntk_Network_t *network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
/*
* Parse the command line.
*/
util_getopt_reset();
while ((c = util_getopt(argc, argv, "fth")) != EOF) {
switch (c) {
case 'f':
printIo = TRUE;
break;
case 't':
printTableStats = TRUE;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if (network == NIL(Ntk_Network_t)) {
return 1;
}
Ntk_NetworkPrint(vis_stdout, network, printIo, printTableStats);
return 0; /* normal exit */
usage:
(void) fprintf(vis_stderr, "usage: print_network [-f] [-h] [-t]\n");
(void) fprintf(vis_stderr, " -f print fanins and fanouts of nodes\n");
(void) fprintf(vis_stderr, " -h print the command usage\n");
(void) fprintf(vis_stderr, " -t print table stats of nodes having tables\n");
return 1; /* error exit */
}
/**Function********************************************************************
Synopsis [Implements the print_network_dot command.]
CommandName [print_network_dot]
CommandSynopsis [print a dot description of the flattened network]
CommandArguments [\[-h\] <file_name>]
CommandDescription [Write a file in the format taken by the tool dot
depicting the topology of the network. Dot is a tool that given a description
of a graph in a certain format it produces a postscript print of the
graph. For more information about dot look in
http://www.research.att.com/orgs/ssr/book/reuse. Once a dot file is
produced with this command, the shell command dot -Tps
>.ps will produce the postscript file depicting the network.
If no argument is specified on the command line, the description is written
to the standard output.
Command options:
- -h
- Print the command usage.
]
SideEffects []
******************************************************************************/
static int
CommandPrintNetworkDot(
Hrc_Manager_t ** hmgr,
int argc,
char ** argv)
{
FILE *fp;
int c, status;
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;
}
if (argc == 1) {
fp = 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 = Ntk_NetworkPrintDot(fp, network);
(void) fprintf(vis_stderr, "%s", error_string());
fflush(fp);
if (fp != stdout) {
(void) fclose(fp);
}
return (status ? 0 : 1);
usage:
(void) fprintf(vis_stderr, "usage: print_network_dot [-h] [file]\n");
(void) fprintf(vis_stderr, " -h\t\tprint the command usage\n");
return 1;
}
/**Function********************************************************************
Synopsis [Write a (flattened) network in blif-MV format.]
CommandName [write_network_blif_mv]
CommandSynopsis [write a blif-MV description of the flattened network]
CommandArguments [\[-h\] \[-p\] <file_name>]
CommandDescription [Write a file in Blif-MV format describing the
network.
If no argument is specified on the command line, the description is written
to the vis standard output.
Command options:
- -h
- Print the command usage.
- -p
- Promote pseudo inputs to primary inputs.
]
SideEffects []
******************************************************************************/
static int
CommandWriteNetworkBlifMv(
Hrc_Manager_t ** hmgr,
int argc,
char ** argv)
{
FILE *fp;
int c;
boolean promotePseudo = FALSE;
Ntk_Network_t *network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
/* Check whether the network has been created. */
if (network == NIL(Ntk_Network_t)) {
return 1;
}
util_getopt_reset();
while ((c = util_getopt(argc,argv,"hp")) != EOF){
switch(c){
case 'h':
goto usage;
case 'p':
promotePseudo = TRUE;
argv++;
argc--;
break;
default:
goto usage;
}
}
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();
Ntk_NetworkWriteBlifMv(fp, network, promotePseudo);
(void) fprintf(vis_stderr, "%s", error_string());
fflush(fp);
if (fp != vis_stdout) {
(void) fclose(fp);
}
return 1;
usage:
(void) fprintf(vis_stderr, "usage: write_network_blif_mv [-h] [file]\n");
(void) fprintf(vis_stderr, " -h\t\tprint the command usage\n");
(void) fprintf(vis_stderr, " -p\t\tpromote pseudo inputs to primary inputs\n");
return 1;
} /* CommandWriteNetworkBlifMv */
/**Function********************************************************************
Synopsis [Implements the flatten_hierarchy command.]
CommandName [flatten_hierarchy]
CommandSynopsis [create a flattened network]
CommandArguments [\[-a <file>\] \[-b\] \[-h\] \[-s\] \[-v #\]]
CommandDescription [Creates a flattened network from a hierarchical
description. The flattened network encompasses everything from the
current node of the hierarchy (reached by the command cd),
down to and including the leaves. It creates a view with the
hierarchy removed, but retains the multi-level logic structure. The
resulting flattened network is stored with the current node. Every
table in the flattened network is checked whether it is completely
specified and deterministic. This is the starting point for
verification related commands.
A limited form of abstraction can be done by providing a list of variables
to treat as primary inputs. See the information under <file>
below.
The verification part of VIS requires the functions specified by the BLIF-MV
tables to be completely specified and deterministic. These conditions are
checked during the flattening process; if a table is found that is
incompletely specified or is nondeterministic, then an error message is
written and a flattened network is not created. The exception to this
rule is tables specifying "pseudo inputs"; these are tables with no inputs,
and a single output that can take more than one value. Such tables are
generated by vl2mv to model the "$ND" construct in Verilog.
If this command is invoked a second time from the same point in the
hierarchy, the previous network is deleted and a new one is created. This
is the tactic to follow if you want to change some aspect of the current
network, such as MDD variable ordering or image_method.
Command options:
- -a <file>
- A file containing names of variables, used to specify which variables
to abstract. The name of a variable is the full hierarchical path name,
starting from just after the current hierarchy node (i.e., if the current
node is foo, and you want to refer to variable x in foo, then just use x).
A variable should appear at most once in the file. Each variable name
should appear at the beginning of a new line, with no white space preceding
it. The end of a variable name is marked by white space, and any other text
on the rest of the line is ignored. Any line starting with "#" or white
space is ignored. A sample file is shown here.
# variables to abstract to model check liveness property
choosing0
p0.pc
For each variable x appearing in the file, a new primary input node named
x$ABS is created to drive all the nodes that were previously driven by x.
Hence, the node x will not have any fanouts; however, x and its transitive
fanins will remain in the network.
Abstracting a net effectively allows it to take any value in its range, at
every clock cycle. This mechanism can be used to perform manual
abstractions. The variables to abstract should not affect the correctness
of the property being checked. This usually simplifies the network, and
permits some verification tasks to complete that would not otherwise. Note,
however, that by increasing the behavior of the system, false negatives are
possible when checking universal properties, and false positives are
possible when checking existential properties.
A convenient way of generating the hierarchical variable names is by using
the write_order command. Note that abstracting next state variables has no
effect.
- -b
- This option has no effect any longer.
- -h
- Print the command usage.
- -s
- Do not perform a sweep.
- -v #
- Print debug information.
-
0: (default) Nothing is printed out.
>= 2: Prints the variables read from the input file.
]
SideEffects []
******************************************************************************/
static int
CommandFlattenHierarchy(
Hrc_Manager_t ** hmgr,
int argc,
char ** argv)
{
int c;
Ntk_Network_t *network;
char *fileName = NIL(char);
int verbose = 0; /* default */
int sweep = 1;
lsList varNameList = (lsList) NULL;
Hrc_Node_t *currentNode = Hrc_ManagerReadCurrentNode(*hmgr);
/*
* Parse the command line.
*/
util_getopt_reset();
while ((c = util_getopt(argc, argv, "a:bhsv:")) != EOF) {
switch (c) {
case 'a':
fileName = util_optarg;
break;
case 'b':
break;
case 'h':
goto usage;
case 's':
sweep = 0;
break;
case 'v':
verbose = atoi(util_optarg);
break;
default:
goto usage;
}
}
if (currentNode == NIL(Hrc_Node_t)) {
(void) fprintf(vis_stdout, "The hierarchy manager is empty. Read in design.\n");
return 1;
}
/*
* Process the file containing the variable names.
*/
if (fileName != NIL(char)) {
FILE *fp = Cmd_FileOpen(fileName, "r", NIL(char *), 0);
if (fp == NIL(FILE)) {
return 1;
}
else {
boolean status;
error_init();
status = FileReadNameList(fp, &varNameList, verbose);
(void) fclose(fp);
if (status == FALSE) {
(void) fprintf(vis_stderr, "Error reading variable name file:\n");
(void) fprintf(vis_stderr, "%s", error_string());
(void) fprintf(vis_stderr, "Cannot perform flatten_hierarchy.\n");
return 1;
}
}
}
/*
* If a network already exists, delete it. Then create the new one, and
* register it with the hrcNode.
*/
network = (Ntk_Network_t *) Hrc_NodeReadApplInfo(currentNode,
NTK_HRC_NODE_APPL_KEY);
if (network != NIL(Ntk_Network_t)) {
(void) fprintf(vis_stdout, "Deleting current network and creating new one.\n");
Hrc_NodeFreeApplInfo(currentNode, NTK_HRC_NODE_APPL_KEY);
}
error_init();
network = Ntk_HrcNodeConvertToNetwork(currentNode, TRUE, varNameList);
/* Clean up the varNameList. */
if (varNameList != (lsList) NULL) {
lsGen gen;
char *varName;
lsForEachItem(varNameList, gen, varName) {
FREE(varName);
}
(void) lsDestroy(varNameList, (void (*) (lsGeneric)) NULL);
}
/* sweep network */
if (network != NIL(Ntk_Network_t) && sweep ==1) {
Ntk_NetworkSweep(network, verbose);
}
if (network == NIL(Ntk_Network_t)) {
(void) fprintf(vis_stderr, "%s", error_string());
(void) fprintf(vis_stderr, "Cannot perform flatten_hierarchy.\n");
return 1;
}
Hrc_NodeAddApplInfo(currentNode, NTK_HRC_NODE_APPL_KEY,
(Hrc_ApplInfoFreeFn) Ntk_NetworkFreeCallback,
(Hrc_ApplInfoChangeFn) NULL, /* not currently used by hrc */
(void *) network);
return 0; /* normal exit */
usage:
(void) fprintf(vis_stderr, "usage: flatten_hierarchy [-a file] [-b] [-h] [-s] [-v #]\n");
(void) fprintf(vis_stderr, " -a file variables to abstract\n");
(void) fprintf(vis_stderr, " -b not used any longer\n");
(void) fprintf(vis_stderr, " -h print the command usage\n");
(void) fprintf(vis_stderr, " -s do not perform a sweep\n");
(void) fprintf(vis_stderr, " -v # verbosity level\n");
return 1; /* error exit */
}
/**Function********************************************************************
Synopsis [Implements the test_network_acyclic command.]
CommandName [test_network_acyclic]
CommandSynopsis [determine whether the network is acyclic]
CommandArguments [\[-h\]]
CommandDescription [If the flattened network has a combinational
cycle, then prints information about one of the cycles. If no cycles are
present, then it prints a message to this effect.
Command options:
- -h
- Print the command usage.
]
SideEffects []
******************************************************************************/
static int
CommandTestNetworkAcyclic(
Hrc_Manager_t ** hmgr,
int argc,
char ** argv)
{
int c;
Ntk_Network_t *network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
/*
* Parse the command line.
*/
util_getopt_reset();
while ((c = util_getopt(argc, argv, "h")) != EOF) {
switch (c) {
case 'h':
goto usage;
default:
goto usage;
}
}
if (network == NIL(Ntk_Network_t)) {
return 1;
}
error_init();
if (Ntk_NetworkTestIsAcyclic(network) == 0) {
(void) fprintf(vis_stdout, "Combinational cycle found: ");
(void) fprintf(vis_stdout, "%s", error_string());
(void) fprintf(vis_stdout, "\n");
}
else {
(void) fprintf(vis_stdout, "Network has no combinational cycles\n");
}
return 0; /* normal exit */
usage:
(void) fprintf(vis_stderr, "usage: test_network_acyclic [-h]\n");
(void) fprintf(vis_stderr, " -h print the command usage\n");
return 1; /* error exit */
}
/**Function********************************************************************
Synopsis [Implements the init_verify command.]
CommandName [init_verify]
CommandSynopsis [create and initialize a flattened network for verification]
CommandArguments [\[-b\] \[-h\]]
CommandDescription [This command initializes the system for verification,
and is equivalent to the command sequence flatten_hierarchy;
static_order; build_partition_mdds. If a command returns an error
condition, then the sequence is aborted. After init_verify has
successfully executed, various commands can be invoked, like
model_check, compute_reach, simulate,
print_network_stats, and seq_verify.
Please note that init_verify does not enable dynamic variable
reordering. Sometimes, though, this is needed to complete building
the partitions, and one has to initialize the verification by hand.
Similarly, it may be wise to turn on dynamic variable reordering after
init, so that further commands complete more easily. See the help page
for dynamic_var_ordering.
Command options:
- -b
- This option has no effect any longer.
- -h
- Print the command usage.
]
SideEffects []
******************************************************************************/
static int
CommandInitVerify(
Hrc_Manager_t ** hmgr,
int argc,
char ** argv)
{
int c;
Hrc_Node_t *currentNode = Hrc_ManagerReadCurrentNode(*hmgr);
/*
* Parse the command line.
*/
util_getopt_reset();
while ((c = util_getopt(argc, argv, "bh")) != EOF) {
switch (c) {
case 'b':
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if (currentNode == NIL(Hrc_Node_t)) {
(void) fprintf(vis_stdout, "The hierarchy manager is empty. Read in design.\n");
return 1;
}
/*
* Call the commands one-by-one, returning upon the first error.
*/
if (Cmd_CommandExecute(hmgr, "flatten_hierarchy")) {
return 1;
}
if (Cmd_CommandExecute(hmgr, "static_order")) {
return 1;
}
if (Cmd_CommandExecute(hmgr, "build_partition_mdds")) {
return 1;
}
return 0; /* normal exit */
usage:
(void) fprintf(vis_stderr, "usage: init_verify [-b] [-h]\n");
(void) fprintf(vis_stderr, " -b not used any longer.\n");
(void) fprintf(vis_stderr, " -h print the command usage\n");
return 1; /* error exit */
}
/**Function********************************************************************
Synopsis [Implements the network_sweep command.]
CommandName [network_sweep]
CommandSynopsis [sweeps the network to ensure that deterministic constants
are removed]
CommandArguments [\[-h\]\[-v\]]
CommandDescription [This function performs a sweep on the given
Ntk_Network_t. It propagates all the deterministic constant nodes, and
removes all buffer nodes. It modifies the network.
Command options:
- -h
- Print the command usage.
- -v
- Print debug information.
]
SideEffects []
******************************************************************************/
static int
CommandNetworkSweep(
Hrc_Manager_t ** hmgr,
int argc,
char ** argv)
{
int c;
Ntk_Network_t *network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
int verbosity = 0;
/*
* Parse the command line.
*/
util_getopt_reset();
while ((c = util_getopt(argc, argv, "hv")) != EOF) {
switch (c) {
case 'h':
goto usage;
case 'v':
verbosity = 1;
break;
default:
goto usage;
}
}
if (network == NIL(Ntk_Network_t)) {
return 1;
}
Ntk_NetworkSweep(network, verbosity);
return 0;
usage:
(void) fprintf(vis_stderr, "usage: network_sweep [-h][-v]\n");
(void) fprintf(vis_stderr, " -h print the command usage\n");
(void) fprintf(vis_stderr, " -v print debug information\n");
return 1; /* error exit */
}
/**Function********************************************************************
Synopsis [Returns a list of names corresponding to the names in a file.]
Description [Parses a file and builds a name list corresponding to the names
found in the first "column" of each line of the file. Any line starting
with the comment character '#' or white space is ignored. No checks are
made to see if the names are well-formed in any respect. If a problem is
found while parsing the file (e.g. name length exceeded), then a message is
written to error_string, the partial name list is freed, and the function
returns FALSE; otherwise, it returns TRUE, and a pointer to a list is
returned.]
Comment [The parser consists of 3 states. See the documentation
accompanying the #defines defining the state names. This code was adapted
from Ord_FileReadNodeList.]
SideEffects []
******************************************************************************/
static boolean
FileReadNameList(
FILE * fp,
lsList * nameList /* of char *, for return */,
int verbose)
{
int c;
int state;
int curPosition = 0;
char *name;
char string[MAX_NAME_LENGTH];
boolean returnFlag = TRUE;
*nameList = lsCreate();
state = STATE_TEST;
while ((c = fgetc(fp)) != EOF) {
switch (state) {
case STATE_TEST:
/* At start of a new line. */
if (c == '#') {
/* Line starting with comment character; wait for newline */
state = STATE_WAIT;
}
else if ((c == ' ') || (c == '\t')) {
/* Line starting with white space; wait for newline */
state = STATE_WAIT;
}
else if (c == '\n') {
/* Line starting with newline; go to next line */
state = STATE_TEST;
}
else {
/* Assume starting a name. */
curPosition = 0;
string[curPosition++] = c;
state = STATE_IN;
}
break;
case STATE_WAIT:
/*
* Waiting for the newline character.
*/
state = (c == '\n') ? STATE_TEST : STATE_WAIT;
break;
case STATE_IN:
/*
* Parsing a name. If white space reached, then terminate the
* name and process it. Else, continue parsing.
*/
if ((c == ' ') || (c == '\n') || (c == '\t')) {
string[curPosition] = '\0';
name = util_strsav(string);
if (verbose > 1) {
(void) fprintf(vis_stdout, "Reading name: %s\n", name);
}
(void) lsNewEnd(*nameList, (lsGeneric) name, LS_NH);
state = (c == '\n') ? STATE_TEST : STATE_WAIT;
}
else {
string[curPosition++] = c;
if (curPosition >= MAX_NAME_LENGTH) {
error_append("maximum name length exceeded");
returnFlag = FALSE;
}
state = STATE_IN; /* redundant, but be explicit */
}
break;
default:
fail("unrecognized state");
}
}
/*
* Handle case where EOF terminates a name.
*/
if (state == STATE_IN) {
string[curPosition] = '\0';
name = util_strsav(string);
if (verbose > 1) {
(void) fprintf(vis_stdout, "Reading name: %s\n", name);
}
(void) lsNewEnd(*nameList, (lsGeneric) name, LS_NH);
}
if (returnFlag) {
return TRUE;
}
else {
(void) lsDestroy(*nameList, (void (*) (lsGeneric)) NULL);
return FALSE;
}
}