#include "resInt.h"
Include dependency graph for resCmd.c:
Go to the source code of this file.
Functions | |
| static int | CommandResVerify (Hrc_Manager_t **hmgr, int argc, char **argv) |
| static void | TimeOutHandle (void) |
| static st_table * | ReadMatchingPairs (char *fileName, Ntk_Network_t *ntk1, Ntk_Network_t *ntk2) |
| static array_t * | ReadOutputOrder (char *fileName, Ntk_Network_t *ntk1) |
| static array_t * | GenerateDefaultOutputOrder (Ntk_Network_t *specNetwork) |
| static int | CheckForMultiValueNode (Ntk_Network_t *network) |
| void | Res_Init (void) |
| void | Res_End (void) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: resCmd.c,v 1.58 2010/04/10 00:38:26 fabio Exp $" |
| static jmp_buf | timeOutEnv |
Function Documentation
| static int CheckForMultiValueNode | ( | Ntk_Network_t * | network | ) | [static] |
Function********************************************************************
Synopsis [Checks if the network contains any multi-valued node .]
Description [Checks if the network contains any multi-valued node. Returns 0, if none exist and 1 if there are any]
SideEffects []
SeeAlso [CommandResVerify]
Definition at line 1113 of file resCmd.c.
{
lsGen listGen;
Ntk_Node_t *nodePtr;
Var_Variable_t * var;
Ntk_NetworkForEachNode(network, listGen, nodePtr) {
var = Ntk_NodeReadVariable(nodePtr);
if ((Var_VariableReadNumValues(var) > 2) ||
(!Var_VariableTestIsEnumerative(var))) {
return 1;
}
}
return 0;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static int CommandResVerify | ( | Hrc_Manager_t ** | hmgr, |
| int | argc, | ||
| char ** | argv | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Implements the res_verify command.]
CommandName [res_verify]
CommandSynopsis [Verifies a combinational circuit using residue arithmetic.]
CommandArguments [\[-b\] \[-d <n>\] \[-h\] -i <filename> \[-m <filename>\] \[-n <filename>\] {-o <filename> | -O} \[-s <filename>\] \[-t <timeOut>\] ]
CommandDescription [This command performs residue verification between two networks. The method used is based on residue arithmetic and the Chinese Remainder theorem; it is described in [1\] ftp://vlsi.colorado.edu/pub/fmcad96.ps. Verification is performed by interpreting the outputs of the circuits as integers and verifying the residues of the outputs with respect to a set of moduli. The choice of moduli is directed by the Chinese Remainder Theorem in order to prove equivalence of the two circuits. This method works well with multipliers and possibly other arithmetic circuits (due to its dependence on residue arithmetic). For the same reason, it is necessary to specify an output order which determines how the outputs are interpreted as integers. Discretion should be exercised in applying this method to general combinational circuits.
Residue verification is available only if vis is linked with the cu BDD package. (This is the default.) It reads both blif and blif-mv files. However, it does NOT support multi-valued variables. Residue verification is primarily for combinational verification, but may be applied to sequential circuits with the same state encoding. The latch outputs are then considered to be combinational inputs of the circuits and the latch inputs and reset are considered to be combinational outputs of the circuits.
There are two ways to perform residue verification in this package. As a first option, two files describing two networks, the specification and the implementation, (in the same format, blif or blif-mv, see option -b) are given in the command line; the procedure tries to verify the equivalence of the combinational outputs as functions of the combinational inputs.
vis> res_verify -o network.order -i network1.blif -s network2.blif
In this case both networks are read in, flattened and the verification is performed between the combinational outputs of both networks. The -i option denotes the implementation file and the -s option denotes the specification file. The -o option specifies the order of outputs for the circuits (See Command Options below for detailed explanation).
A second way to perform the verification is as follows. The specification network is taken from a hierarchy already read into VIS. Then the res_verify command compares that specification against an implementation network obtained from the file in the command line. Any previous verification, performed with the specification, can be used towards the next verification task only if the same implementation circuit is being verified against and the same number of outputs have been directly verified with sucess in the previous attempt. The typical sequence of commands given to perform such task would be:
vis> read_blifmv network1.mv
vis> flatten_hierarchy
vis> res_verify -o network.order -i network2.mv
If the hierarchy has been read but no flattened network exists at the current node, the command will return without doing anything.
If one of the networks used is the one in the current node in the hierarchy, then the information regarding the verification process will be stored in that network.
Note: It is important to keep the specification distinct from the implementation because most parameters specified for the res_verify command are with respect to the specification. For example, the output order is specified with respect to the specification. The file that is read in first in the second format, is considered to be the specification.
There is an option to directly verify some outputs by building the BDDs for the corresponding outputs of the 2 circuits. In that case, if the user wants to use an initial ordering, the only way to do it is the second method and reading in the network, one may specify the initial order using static order.
The command does not repeat residue verification if the same specification-implementation pair have been verified with success and the same number of directly verified outputs have been verified in the previous attempt.
Relevant flags to be set using the set command:
- residue_verbosity
Default is 0, turns on verbosity to the desired level between 0 and 5.
- residue_ignore_direct_verified_outputs
Default 0 (FALSE). If 1, then ignores directly verified outputs during residue verification.
- residue_top_var
Default "msb". The 2 possible values are "msb" and lsb"; this puts the most/least significant bit near the top or bottom of the residue decision diagram.
- residue_autodyn_residue_verif
Default 0 (FALSE). If 1, turns on dynamic reordering during residue verification.
- residue_residue_dyn_method
Default "groupsift". Specifies the method for dynamic reordering during residue verification. Other methods supported are "same" (same as before), "none", "random", "randompivot", "sift", "siftconverge", "symmsiftconverge", "symmsift", "window2", "window3", "window4", "window2converge", "window3converge", "window4converge", "groupsift", "groupsiftconverge", "anneal", "genetic", "linear", "linearconverge", "exact".
- residue_autodyn_direct_verif
Default 0 (FALSE). If 1, turns on dynamic reordering during direct verification.
- residue_direct_dyn_method
Default "groupsift". Specifies the method for dynamic reordering during direct verification. Other methods supported are "same" (same as before), "none", "random", "randompivot", "sift", "siftconverge", "symmsiftconverge", "symmsift", "window2", "window3", "window4", "window2converge", "window3converge", "window4converge", "groupsift", "groupsiftconverge", "anneal", "genetic", "linear", "linearconverge", "exact".
- residue_layer_schedule
Default "alap". This is a flag to specify the layering strategy of the networks. The 2 options are "asap" (as soon as possible) and "alap" (as late as possible).
- residue_layer_size
Default largest layer size in network. Specifies the maximum layer size that can be composed in (relevant for vector composition only).
- residue_composition_method
Default "vector". Specifies the composition method to be used in composing the network into the residue ADD. The options are "vector", "onegate", "preimage" and "superG".
Command Options:
- -b
If this option is specified, the specification and the implementation files read are considered to be in blif-mv format. Default is blif format.
- -d n
This option specifies the number of outputs to be directly verified. That is, for
nleast significant outputs of the circuit, this command performs like comb_verify. The actual outputs are read off the output order array. Since the output order array is specified starting with the MSB, the number of directly verified outputs will be a chunk of the bottom part of the output order array. The option "-d all" sets the number of directly verified outputs to the number of combinational outputs in the circuit i.e., all outputs are directly verified. The direct verification for small BDD sizes is faster and overall reduces the number of primes to be used in residue verification. In general, one output is checked at a time against the corresponding output of the other network and consequently , this method may be fast and use less memory resources.
IMPORTANT: It is possible to specify an initial order for the direct verification. This is done by reading in the specification file and using static_order to specify the initial order. The implementation will get the same order as the specification. When specifying the initial order, one must be careful not to specify the -s option in the res_verify command. The -s option reads in the specification file again and the initial order is lost.- -h
Print the command usage.
- -i <filename>
Implementation network to perform verification against. The file must be in blif format unless
-bis specified, in which case the file is taken to be in blif-mv format. The blif format is the default.- -m <filename>
Optional file name specifying the matching pair of output names between the two networks. If not specified, it is assumed that all outputs have identical names. This option is useful when verifying two circuits whose output names do not match. The file will give pairs of the form
name1 name2to be considered as corresponding outputs in the verification process. In each pair,name1may belong to the specification andname2to the implementation or vice-versa. The matching procedure is not capable of dealing with some special situations. For example, when two outputs, one of each network have the same name, they must correspond to the same output. Partial orders may not be specified.- -n <filename>
Optional file name specifying the matching pair of input names between the two networks. If not specified, it is assumed that all inputs have identical names. This option is useful when verifying two circuits whose input names do not match. The file will give pairs of the form
name1 name2to be considered as corresponding inputs in the verification process. In each pair,name1may belong to the specification andname2to the implementation or vice-versa. The matching procedure is not capable of dealing with some special situations. For example, when two inputs, one of each network have the same name, they must correspond to the same input. Partial orders may not be specified.- -o <filename>
Required file specifying output order, starting with the MSB. The file must be a list of output names separated by spaces. The list must belong to the specification network and must contain a full order i.e., must contain all the combinational output names. It is advisable to use the -o option as far as possible to specify the order of the outputs.See also -O option.
- -O
This option specifies whether the
res_verifycommand should generate a default order for the outputs. If the -o option is not used, this option must be specified. The default order generated is random and is NOT the same as the input files. The set of outputs for the output order may be generated by using the print_network command to write the network into a file and extract the node name from the lines containing the word "comb-output". The set of outputs can then be ordered as required.
It is advisable to use the -o option as far as possible to specify the order of the outputs. The -o option overrides the -O option. See also -o option.- -s <filename>
Specification network. This network will be taken as the specification of the circuit. The result of the computation will be stored in this network. If this network is not provided, the current node of the hierarchy will be taken. The file must contain a blif description of a circuit unless the option
-bis specified, in which case the file is considered in blif-mv format. If two networks are specified in the command line, both of them must have the same format, either blif or blif-mv. The blif format is the default.- -t <timeOut >
Execution time in seconds allowed for verification before aborting. The default is no limit.
]
SideEffects [It registers the information about the verification in the specification if this is the current node in the hierarchy manager.]
SeeAlso [Res_NetworkResidueVerify]
Definition at line 393 of file resCmd.c.
{
static int timeOutPeriod; /* CPU seconds allowed */
static array_t *outputOrderArray; /* required to specify the outputs
* starting with MSB first */
static Hrc_Manager_t *implHmgr; /* Auxiliary hierarchy manager */
static Hrc_Manager_t *specHmgr; /* Auxiliary hierarchy manager */
static Hrc_Node_t *currentNode; /* node in the hierarchy */
static Ntk_Network_t *specNetwork; /* spec network */
static Ntk_Network_t *implNetwork; /* implementation network */
static st_table *inputMatch; /* List of pairs of input name match */
static st_table *outputMatch; /* List of pairs of output name match */
int outputsToVerifyDirectly; /* number of outputs to
* directly verify
*/
int c; /* To process the command line options */
/* Flush previous verification if any */
int success; /* Outcome of the verification */
int status; /* Status of the call to the function */
char *specFileName; /* File to read the specification from */
char *impFileName; /* File to read the implementation from */
char *fileMatchOut; /* File specifying the output matching */
char *fileMatchIn; /* File specifying the input matching */
char *fileOutputOrder; /*file name that contains the order of
outputs starting with MSB */
boolean isInBlifMv; /* Format to be read in */
st_generator *stGen; /* generator to step through the table */
char *key, *value; /* variables for the st_table */
int i;
int defaultOutputOrder; /* flag to indicate default order to
* be taken, if no output order file
* is specified
*/
char *strptr; /* variable to hold return value
* of strtol
*/
int allFlag;
if (bdd_get_package_name() != CUDD) {
fprintf(vis_stdout, "** res error: Residue Verification is available with the CUDD package only.\n");
return 0;
}
/* Default values for some variables */
timeOutPeriod = 0;
allFlag = 1;
outputsToVerifyDirectly = 0;
outputOrderArray = NIL(array_t);
implHmgr = NIL(Hrc_Manager_t);
specHmgr = NIL(Hrc_Manager_t);
currentNode = NIL(Hrc_Node_t);
specNetwork = NIL(Ntk_Network_t);
implNetwork = NIL(Ntk_Network_t);
inputMatch = NIL(st_table);
outputMatch = NIL(st_table);
impFileName = NIL(char);
specFileName = NIL(char);
isInBlifMv = FALSE;
fileMatchOut = NIL(char);
fileMatchIn = NIL(char);
status = 1;
fileOutputOrder = NIL(char);
defaultOutputOrder = 0;
/*
* Parse command line options.
*/
util_getopt_reset();
while ((c = util_getopt(argc, argv, "bd:hi:m:n:o:Os:t:")) != EOF) {
switch(c) {
case 'b':
isInBlifMv = TRUE;
break;
case 'd':
/* number of outputs to verify directly */
/* outputsToVerifyDirectly = atoi(util_optarg); */
outputsToVerifyDirectly = (int)strtol(util_optarg, &strptr, 0);
allFlag = strcmp(util_optarg, "all");
break;
case 'h':
goto usage;
case 'i':
impFileName = util_optarg;
break;
case 'm':
fileMatchOut = util_optarg;
break;
case 'n':
fileMatchIn = util_optarg;
break;
case 'o':
fileOutputOrder = util_optarg;
break;
case 'O':
defaultOutputOrder = 1;
break;
case 's':
specFileName = util_optarg;
break;
case 't':
timeOutPeriod = atoi(util_optarg);
break;
default:
goto usage;
}
}
/* Obtain the Specification network either from file or hierarchy manager */
if (specFileName != NIL(char)) {
/* Read blif or blif-mv depending on the flag */
error_init();
if (isInBlifMv) {
FILE *fp; /* Used to read from files */
/* Open the file */
fp = Cmd_FileOpen(specFileName, "r", NIL(char *), TRUE);
if (fp != NULL) {
specHmgr = Io_BlifMvRead(fp, NIL(Hrc_Manager_t),
0, /* No Cannonical */
0, /* No incremental */
0 /* No verbosity */);
fclose(fp);
} else {
fprintf(vis_stderr, "** res error: Specification file required(may not exist in path)\n");
goto usage;
}
} /* End of then */
else {
specHmgr = Io_BlifRead(specFileName, 0 /* No verbosity */);
} /* End of if-then-else */
/* Check if the read has been performed correctly */
if (specHmgr == NIL(Hrc_Manager_t)) {
(void) fprintf(vis_stderr, "%s", error_string());
(void) fprintf(vis_stderr, "Cannot read blif file %s.\n", impFileName);
goto cleanup;
}
/* Hierarchy manager successfully created */
error_init();
currentNode = Hrc_ManagerReadCurrentNode(specHmgr);
specNetwork = Ntk_HrcNodeConvertToNetwork(currentNode, TRUE, (lsList)0);
if (specNetwork == NIL(Ntk_Network_t)) {
(void) fprintf(vis_stderr, "%s", error_string());
(void) fprintf(vis_stderr, "Cannot perform flatten_hierarchy.\n");
goto cleanup;
}
} else {
/* Check if any circuit has been read in */
currentNode = Hrc_ManagerReadCurrentNode(*hmgr);
if (currentNode == NIL(Hrc_Node_t)) {
(void) fprintf(vis_stderr, "The hierarchy manager is empty. ");
(void) fprintf(vis_stderr, "Read in design.\n");
goto cleanup;
}
/* Check if the network has been created with flatten_hierarchy */
specNetwork = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
if (specNetwork == NIL(Ntk_Network_t)) {
goto cleanup;
} /* End of if */
}
/* Obtain the implementation network from file */
if (impFileName != NIL(char)) {
/* Read blif or blif-mv depending on the flag */
error_init();
if (isInBlifMv) {
FILE *fp; /* Used to read from files */
/* Open the file */
fp = Cmd_FileOpen(impFileName, "r", NIL(char *), TRUE);
if (fp != NULL) {
implHmgr = Io_BlifMvRead(fp, NIL(Hrc_Manager_t),
0, /* No Cannonical */
0, /* No incremental */
0 /* No verbosity */);
fclose(fp);
} else {
fprintf(vis_stderr, "** res error: Implementation file required(may not exist in path)\n");
goto usage;
}
} else { /* End of then */
implHmgr = Io_BlifRead(impFileName, 0 /* No verbosity */);
} /* End of if-then-else */
/* Check if the read has been performed correctly */
if (implHmgr == NIL(Hrc_Manager_t)) {
(void) fprintf(vis_stderr, "%s", error_string());
(void) fprintf(vis_stderr, "Cannot read blif file %s.\n", impFileName);
goto cleanup;
}
/* Hierarchy manager successfully created */
error_init();
currentNode = Hrc_ManagerReadCurrentNode(implHmgr);
implNetwork = Ntk_HrcNodeConvertToNetwork(currentNode, TRUE, NULL);
if (implNetwork == NIL(Ntk_Network_t)) {
(void) fprintf(vis_stderr, "%s", error_string());
(void) fprintf(vis_stderr, "Cannot perform flatten_hierarchy.\n");
goto cleanup;
}
}
else {
/* The option -1 has not been provided in the command line */
goto usage;
}
/* At this point both networks have been built */
/* Check that no node in the two network is multi-valued */
if (CheckForMultiValueNode(specNetwork)) {
fprintf(vis_stderr, "** res error: Specification has multivalued network\n");
fprintf(vis_stderr, "** res error: Residue verification does not support multi-valued variables, variables have to be binary.\n");
goto cleanup;
}
if (CheckForMultiValueNode(implNetwork)) {
fprintf(vis_stderr, "** res error: Implementation has multivalued network\n");
fprintf(vis_stderr, "** res error: Residue verification does not support multi-valued variables, variables have to be binary.\n");
goto cleanup;
}
/* Check that both networks have the same number of inputs and outputs */
if ((Ntk_NetworkReadNumCombInputs(implNetwork) !=
Ntk_NetworkReadNumCombInputs(specNetwork)) ||
(Ntk_NetworkReadNumCombOutputs(implNetwork) !=
Ntk_NetworkReadNumCombOutputs(specNetwork))) {
(void) fprintf(vis_stderr, "** res error: Networks do not have equal number of inputs ");
(void) fprintf(vis_stderr, "or outputs\n");
goto cleanup;
} /* End of if */
/* Check if there has been some name matching file provided for outputs. */
if (fileMatchOut != NIL(char)) {
outputMatch = ReadMatchingPairs(fileMatchOut, implNetwork, specNetwork);
if (outputMatch == NIL(st_table)) {
(void) fprintf(vis_stderr, "** res error: Error reading Output match file ");
(void) fprintf(vis_stderr, "%s\n", fileMatchOut);
goto cleanup;
} /* End of if */
} /* End of if */
/* Check if there has been some name matching file provided for inputs. */
if (fileMatchIn != NIL(char)) {
inputMatch = ReadMatchingPairs(fileMatchIn, implNetwork, specNetwork);
if (inputMatch == NIL(st_table)) {
(void) fprintf(vis_stderr, "** res error: Error reading Input match file ");
(void) fprintf(vis_stderr, "%s\n", fileMatchIn);
/* Clean up */
goto cleanup;
} /* End of if */
} /* End of if */
/* Transfer names of outputs starting with MSB from the file to an
* array_t
*/
if (fileOutputOrder != NIL(char)) {
outputOrderArray = ReadOutputOrder(fileOutputOrder, specNetwork);
} else if (defaultOutputOrder) {
outputOrderArray = GenerateDefaultOutputOrder(specNetwork);
}
if (outputOrderArray == NIL(array_t)) {
/* Clean up */
fprintf(vis_stderr, "** res error: Output order(msb first) required for residue method.\n");
goto usage;
} else if (array_n(outputOrderArray) != Ntk_NetworkReadNumCombOutputs(specNetwork)) {
fprintf(vis_stderr, "** res error: Number of Outputs seem to be %d\n", Ntk_NetworkReadNumCombOutputs(specNetwork));
fprintf(vis_stderr, "** res error: The output order seems to contain %d outputs\n", array_n(outputOrderArray));
fprintf(vis_stderr, "** res error: Partial Orders or mismatch in the above two numbers is not allowed in the -o option\n");
goto usage;
}
/* Start the timer before calling the verifyer */
if (timeOutPeriod > 0) {
(void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
(void) alarm(timeOutPeriod);
/* The second time setjmp is called, it returns here !!*/
if (setjmp(timeOutEnv) > 0) {
(void) fprintf(vis_stdout, "Residue Verification timeout occurred after%d seconds.\n",
timeOutPeriod);
alarm(0);
/* Note that there is a huge memory leak here. */
goto cleanup;
} /* End of if */
}
/* number of outputs to directly verify should be less than the
* number of outputs for the circuit. If all flag set, number of
* directly verified circuit, set it to number of combinational
* outputs.
*/
if (allFlag == 0) {
outputsToVerifyDirectly = Ntk_NetworkReadNumCombOutputs(specNetwork);
}
if (outputsToVerifyDirectly > Ntk_NetworkReadNumCombOutputs(specNetwork)) {
fprintf(vis_stderr, "** res error: More outputs to directly verify than that exist in the circuit\n");
goto usage;
}
error_init();
/* main procedure for residue verification */
status = Res_NetworkResidueVerify(specNetwork,
implNetwork,
outputsToVerifyDirectly,
outputOrderArray,
outputMatch,
inputMatch);
/* Deactivate the alarm */
alarm(0);
/* If the computation succeded store the result in specNetwork */
if (status == 0) {
Res_ResidueInfo_t *residueInfo;
residueInfo = (Res_ResidueInfo_t *) Ntk_NetworkReadApplInfo(specNetwork,
RES_NETWORK_APPL_KEY);
/* Print out the error string in case success is false */
success = Res_ResidueInfoReadSuccess(residueInfo);
switch (success) {
case FALSE:
(void) fprintf(vis_stdout, "Residue Verification failed !\n");
break;
case TRUE:
(void) fprintf(vis_stdout, "Residue Verification successful\n");
break;
default:
(void) fprintf(vis_stderr, "** res error: Residue Verification unable to produce ");
(void) fprintf(vis_stderr, "result\n");
break;
}
} else {
(void) fprintf(vis_stderr, "%s", error_string());
}
/* Clean up */
error_cleanup();
goto cleanup;
/* update with all functions */
usage:
(void) fprintf(vis_stderr, "usage: res_verify [-b] ");
(void) fprintf(vis_stderr, "[-d n] [-h] -i impl file\n ");
(void) fprintf(vis_stderr, "[-m file] [-n file] -o file [-s spec file] ");
(void) fprintf(vis_stderr, "[-t secs]\n");
(void) fprintf(vis_stderr, " -b The file format to be read is ");
(void) fprintf(vis_stderr, "blif-mv (default is blif)\n");
(void) fprintf(vis_stderr, " -d n Number of outputs to verify ");
(void) fprintf(vis_stderr, "directly\n");
(void) fprintf(vis_stderr, " -h Print the usage of the command\n");
(void) fprintf(vis_stderr, " -i impl Implementation file (required)\n");
(void) fprintf(vis_stderr, " -m file File specifying the matching pair ");
(void) fprintf(vis_stderr, "of names for the outputs\n");
(void) fprintf(vis_stderr, " -n file File specifying the matching pair");
(void) fprintf(vis_stderr, " of names for the inputs\n");
(void) fprintf(vis_stderr, " -o Output order starting with MSB (required or -O required)\n");
(void) fprintf(vis_stderr, " -O Default output order (required or -o required)\n");
(void) fprintf(vis_stderr, " -s file Specification File\n");
(void) fprintf(vis_stderr, " -t secs Seconds allowed for computation\n");
/* Clean up */
cleanup:
if ((specFileName == NIL(char)) && (specHmgr != NIL(Hrc_Manager_t))) {
int zerorefcountbdds;
bdd_manager *ddManager;
Hrc_ManagerFree(specHmgr);
if (specNetwork != NIL(Ntk_Network_t)) {
ddManager = (bdd_manager *)Ntk_NetworkReadMddManager(specNetwork);
if (ddManager != NIL(bdd_manager)) {
zerorefcountbdds = bdd_check_zero_ref((bdd_manager *)Ntk_NetworkReadMddManager(specNetwork));
if (zerorefcountbdds) {
fprintf(vis_stdout, "Number of Nodes with non zero ref count are %d\n", zerorefcountbdds);
fprintf(vis_stdout, "Size of DD manager = %d\n", bdd_num_vars(ddManager));
}
}
}
Ntk_NetworkFree(specNetwork);
}
if (implHmgr != NIL(Hrc_Manager_t)) {
Hrc_ManagerFree(implHmgr);
/* dont free manager if not set here */
if ((specNetwork != NIL(Ntk_Network_t)) &&
((bdd_manager *)Ntk_NetworkReadMddManager(specNetwork) != NIL(bdd_manager))) {
Ntk_NetworkSetMddManager(implNetwork, NIL(bdd_manager));
}
Ntk_NetworkFree(implNetwork);
}
if (outputMatch != NIL(st_table)) {
st_foreach_item(outputMatch, stGen, &key, &value) {
/* free only the key, cos the value appears as a key also */
FREE(key);
}
st_free_table(outputMatch);
} /* End of if */
if (inputMatch != NIL(st_table)) {
st_foreach_item(inputMatch, stGen, &key, &value) {
/* free only the key, cos the value appears as a key also */
FREE(key);
}
st_free_table(inputMatch);
}
if (outputOrderArray != NIL(array_t)) {
char * name;
arrayForEachItem(char *, outputOrderArray, i, name) {
FREE(name);
}
array_free(outputOrderArray);
}
return status;
} /* End of CommandResVerify */
Here is the call graph for this function:
Here is the caller graph for this function:
| static array_t * GenerateDefaultOutputOrder | ( | Ntk_Network_t * | specNetwork | ) | [static] |
Function********************************************************************
Synopsis [Generates a default output order .]
Description [This order is as provided in the file]
SideEffects []
SeeAlso [CommandResVerify]
Definition at line 1080 of file resCmd.c.
{
array_t *outputOrderArray;
lsGen listGen;
Ntk_Node_t *nodePtr;
char *name, *ptr1;
int i;
i = 0;
outputOrderArray = array_alloc(char *,
Ntk_NetworkReadNumCombOutputs(specNetwork));
Ntk_NetworkForEachCombOutput(specNetwork, listGen, nodePtr) {
name = Ntk_NodeReadName(nodePtr);
ptr1 = util_strsav(name);
array_insert(char *, outputOrderArray, i, ptr1);
i++;
}
return outputOrderArray;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static st_table * ReadMatchingPairs | ( | char * | fileName, |
| Ntk_Network_t * | ntk1, | ||
| Ntk_Network_t * | ntk2 | ||
| ) | [static] |
Function********************************************************************
Synopsis [Builds a table with the pairs of names given in a file.]
Description [Given a file, it opens the and reads lines of the form name1 name2 and stores the pairs (name1, name2) and (name2, name1) in a table that returns as result.]
SideEffects []
SeeAlso [CommandResVerify]
Definition at line 849 of file resCmd.c.
{
st_table *result = NIL(st_table);
int check;
char name1[80], name2[80]; /* Note the size of buffer is used in fscanf */
char *ptr1, *ptr2;
FILE *fp;
#if HAVE_MKSTEMP && HAVE_CLOSE
int fd;
#else
char buffer[512];
#endif
char *realFileName, *blifMvFileName, *visDirectoryName;
char command[512];
int cmdStatus;
fp = Cmd_FileOpen(fileName, "r", &realFileName, 1 /* silent */);
if (fp == NIL(FILE)) {
FREE(realFileName);
(void) fprintf(vis_stderr, "** res error: Cannot open %s to read.\n", fileName);
return result;
} /* End of if */
if (fp != stdin){
(void)fclose(fp);
}
#if HAVE_MKSTEMP && HAVE_CLOSE
blifMvFileName = util_strsav("/tmp/vis.XXXXXX");
fd = mkstemp(blifMvFileName);
if (fd == -1){
#else
blifMvFileName = util_strsav(tmpnam(buffer));
if (blifMvFileName == NIL(char)){
#endif
FREE(realFileName);
(void)fprintf(vis_stderr,"** res error: Could not create temporary file. ");
(void)fprintf(vis_stderr,"** res error: Clean up /tmp an try again.\n");
return NIL(st_table);
}
#if HAVE_MKSTEMP && HAVE_CLOSE
close(fd);
#endif
/* Invoking an awk script */
visDirectoryName = Vm_VisObtainLibrary();
(void)sprintf(command,"sed 's/^\\./@/g' %s | sed 's/\\./$/g' | sed 's/^@/\\./g' | sed 's/{/</g' | sed 's/}/>/g'| sed 's/(/<</g' | sed 's/)/>>/g' > %s", realFileName, blifMvFileName);
/* the following is missing two new sed processings
(void)sprintf(command,"sed 's/^\\./@/g' %s | sed 's/\\./$/g' | sed 's/^@/\\./g' | sed 's/{/</g' | sed 's/}/>/g'| %s -f %s/ioBlifToMv.nawk > %s", realFileName, NAWK, visDirectoryName, blifMvFileName);
*/
cmdStatus = system(command);
FREE(visDirectoryName);
FREE(realFileName);
if (cmdStatus != 0) {
return NIL(st_table);
}
fp = Cmd_FileOpen(blifMvFileName, "r", NIL(char *), 1);
assert(fp != NIL(FILE));
result = st_init_table(st_ptrcmp, st_ptrhash);
while (!feof(fp)) {
check = fscanf(fp, "%80s %80s", name1, name2);
if (check != 2 && check != EOF) {
st_free_table(result);
result = NIL(st_table);
return result;
} /* End of if */
if (Ntk_NetworkFindNodeByName(ntk1, name1) == NIL(Ntk_Node_t) &&
Ntk_NetworkFindNodeByName(ntk2, name1) == NIL(Ntk_Node_t)) {
(void) fprintf(vis_stderr, "** res error: While reading matching file. ");
(void) fprintf(vis_stderr, "** res error: Node %s not found in any of the networks.\n",
name1);
st_free_table(result);
result = NIL(st_table);
return result;
}
if (Ntk_NetworkFindNodeByName(ntk1, name2) == NIL(Ntk_Node_t) &&
Ntk_NetworkFindNodeByName(ntk2, name2) == NIL(Ntk_Node_t)) {
(void) fprintf(vis_stderr, "** res error: While reading matching file. ");
(void) fprintf(vis_stderr, "** res error: Node %s not found in any of the networks.\n",
name2);
st_free_table(result);
result = NIL(st_table);
return result;
}
ptr1 = util_strsav(name1);
ptr2 = util_strsav(name2);
st_insert(result, ptr1, ptr2);
st_insert(result, ptr2, ptr1);
} /* End of while */
fclose(fp);
#if HAVE_UNLINK
unlink(blifMvFileName);
#endif
FREE(blifMvFileName);
return result;
} /* End of ReadMatchingPairs */
Here is the call graph for this function:
Here is the caller graph for this function:
| static array_t * ReadOutputOrder | ( | char * | fileName, |
| Ntk_Network_t * | ntk1 | ||
| ) | [static] |
Function********************************************************************
Synopsis [Builds an array with the names given in a file.]
Description [Given a file, it opens the and reads lines of the form name1 and stores the name1 in an array that returns as result.]
SideEffects []
SeeAlso [CommandResVerify]
Definition at line 969 of file resCmd.c.
{
FILE *fp;
#if HAVE_MKSTEMP && HAVE_CLOSE
int fd;
#else
char buffer[512];
#endif
array_t *result = NIL(array_t);
int check;
char name1[80]; /* Note the size of buffer is used in fscanf */
char *ptr1;
char *realFileName, *blifMvFileName, *visDirectoryName;
char command[512];
int cmdStatus;
fp = Cmd_FileOpen(fileName, "r", &realFileName, 1 /* silent */);
if (fp == NIL(FILE)) {
FREE(realFileName);
(void) fprintf(vis_stderr, "** res error: Cannot open %s to read.\n", fileName);
return result;
} /* End of if */
if (fp != stdin){
(void)fclose(fp);
}
#if HAVE_MKSTEMP && HAVE_CLOSE
blifMvFileName = util_strsav("/tmp/vis.XXXXXX");
fd = mkstemp(blifMvFileName);
if (fd == -1){
#else
blifMvFileName = util_strsav(tmpnam(buffer));
if (blifMvFileName == NIL(char)){
#endif
FREE(realFileName);
(void)fprintf(vis_stderr,"** res error: Could not create temporary file. ");
(void)fprintf(vis_stderr,"** res error: Clean up /tmp an try again.\n");
return NIL(array_t);
}
#if HAVE_MKSTEMP && HAVE_CLOSE
close(fd);
#endif
/* Invoking an awk script */
visDirectoryName = Vm_VisObtainLibrary();
(void)sprintf(command,"sed 's/^\\./@/g' %s | sed 's/\\./$/g' | sed 's/^@/\\./g' | sed 's/{/</g' | sed 's/}/>/g'| sed 's/(/<</g' | sed 's/)/>>/g' > %s", realFileName, blifMvFileName);
/* the following is missing two new sed processings
(void)sprintf(command,"sed 's/^\\./@/g' %s | sed 's/\\./$/g' | sed 's/^@/\\./g' | sed 's/{/</g' | sed 's/}/>/g'| %s -f %s/ioBlifToMv.nawk > %s", realFileName, NAWK, visDirectoryName, blifMvFileName);
*/
cmdStatus = system(command);
FREE(visDirectoryName);
FREE(realFileName);
if (cmdStatus != 0) {
return NIL(array_t);
}
fp = Cmd_FileOpen(blifMvFileName, "r", NIL(char *), 1);
assert(fp != NIL(FILE));
result = array_alloc(char *, 0);
while (!feof(fp)) {
check = fscanf(fp, "%80s", name1);
if (check != EOF) {
if (check != 1) {
array_free(result);
result = NIL(array_t);
return result;
} /* End of if */
if (Ntk_NetworkFindNodeByName(ntk1, name1) == NIL(Ntk_Node_t)) {
(void) fprintf(vis_stderr, "** res error: While reading output order file. ");
(void) fprintf(vis_stderr, "** res error: Node %s not found in the network.\n",
name1);
array_free(result);
result = NIL(array_t);
return result;
}
ptr1 = util_strsav(name1);
array_insert_last(char *, result, ptr1);
}
} /* End of while */
#ifdef DEBUG
arrayForEachItem(char *,result, i, ptr1) {
fprintf(vis_stdout, "%s\n", ptr1);
}
#endif
fclose(fp);
#if HAVE_UNLINK
unlink(blifMvFileName);
#endif
FREE(blifMvFileName);
return result;
} /* End of ReadMatchingPairs */
Here is the call graph for this function:
Here is the caller graph for this function:
| void Res_End | ( | void | ) |
Function********************************************************************
Synopsis [Ends the residue verification package.]
SideEffects []
SeeAlso [Tst_Init]
Definition at line 102 of file resCmd.c.
{
/*
* For example, free any global memory (if any) which the test package is
* responsible for.
*/
}
Here is the caller graph for this function:
| void Res_Init | ( | void | ) |
AutomaticEnd Function********************************************************************
Synopsis [Initializes the Residue Verification package.]
SideEffects []
SeeAlso [Tst_End]
Definition at line 86 of file resCmd.c.
{
Cmd_CommandAdd("res_verify", CommandResVerify, /* doesn't changes_network */ 0);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void TimeOutHandle | ( | void | ) | [static] |
Function********************************************************************
Synopsis [Handle the timeout signal.]
Description [This function is called when the time out occurs. In principle it could do something smarter, but so far it just transfers control to the point in the code where setjmp was called.]
SideEffects [This function gains control at any point in the middle of the computation, therefore the memory allocated so far leaks.]
Definition at line 830 of file resCmd.c.
{
longjmp(timeOutEnv, 1);
} /* End of TimeOutHandle */
Here is the caller graph for this function:
Variable Documentation
jmp_buf timeOutEnv [static] |
char rcsid [] UNUSED = "$Id: resCmd.c,v 1.58 2010/04/10 00:38:26 fabio Exp $" [static] |
CFile***********************************************************************
FileName [resCmd.c]
PackageName [res]
Synopsis [Implements the different commands related to the residue verification.]
Description [This file provides the wrapper functions for the commands involving the residue verification. The command res_verify receives at least one file describing an implementation and optionally a second one describing a specification of a circuit and a set of different options and calls the procedure to perform residue verification in the two systems. For more detailed information about the command res_verify, see also CommandResVerify]
Author [Kavita Ravi <ravi@duke.colorado.edu> and Abelardo Pardo <abel@duke.colorado.edu>]
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.]
