#include "eqvInt.h"
Include dependency graph for eqvMisc.c:
Go to the source code of this file.
Functions | |
| static boolean | NodesMatchUp (Ntk_Node_t *node1, Ntk_Node_t *node2) |
| st_table * | MapPrimaryInputsByName (Ntk_Network_t *network1, Ntk_Network_t *network2) |
| st_table * | MapCombInputsByName (Ntk_Network_t *network1, Ntk_Network_t *network2) |
| st_table * | MapPrimaryOutputsByName (Ntk_Network_t *network1, Ntk_Network_t *network2) |
| st_table * | MapCombOutputsByName (Ntk_Network_t *network1, Ntk_Network_t *network2) |
| OFT | FindOrderingMethod (void) |
| boolean | TestRootsAndLeavesAreValid (Ntk_Network_t *network1, Ntk_Network_t *network2, st_table *inputMap, st_table *outputMap) |
| st_table * | MapNamesToNodes (Ntk_Network_t *network1, Ntk_Network_t *network2, st_table *names) |
| int | ReadRootLeafMap (FILE *inputFile, st_table *rootsTable, st_table *leavesTable) |
| void | DefaultCommonOrder (Ntk_Network_t *network1, Ntk_Network_t *network2, st_table *inputMap) |
| boolean | TestLeavesAreValid (Ntk_Network_t *network1, Ntk_Network_t *network2, st_table *leavesTable) |
| boolean | TestRootsAreValid (Ntk_Network_t *network1, Ntk_Network_t *network2, st_table *rootsTable) |
| boolean | TestPartitionIsValid (Ntk_Network_t *network, st_table *roots, st_table *leaves) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: eqvMisc.c,v 1.10 2009/04/11 01:40:06 fabio Exp $" |
Function Documentation
| void DefaultCommonOrder | ( | Ntk_Network_t * | network1, |
| Ntk_Network_t * | network2, | ||
| st_table * | inputMap | ||
| ) |
Function********************************************************************
Synopsis [This function generates the default ordering of leaf nodes.]
Description [The function checks if network1 has a partition registered with it. If there is no partition, The function orders the variables of network1, using the option Ord_All_c i.e. orders all the nodes. If a partition exists, the existing ordering is left undisturbed. It then copies the mddIds of those nodes of network1 which are present in inputMap into the corresponding nodes of network2.]
SideEffects []
SeeAlso []
Definition at line 860 of file eqvMisc.c.
{
st_generator *gen;
Ntk_Node_t *node1, *node2;
int id;
lsList dummy = (lsList) 0;
if(Ntk_NetworkReadApplInfo(network1, PART_NETWORK_APPL_KEY) == NIL(void)) {
Ord_NetworkOrderVariables(network1, Ord_RootsByDefault_c,
Ord_NodesByDefault_c, FALSE, Ord_All_c,
Ord_Unassigned_c, dummy, 0);
}
st_foreach_item(inputMap, gen, &node1, &node2) {
id = Ntk_NodeReadMddId(node1);
Ntk_NodeSetMddId(node2, id);
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| OFT FindOrderingMethod | ( | void | ) |
| st_table* MapCombInputsByName | ( | Ntk_Network_t * | network1, |
| Ntk_Network_t * | network2 | ||
| ) |
Function********************************************************************
Synopsis [The function returns a hash table of corresponding combinational input nodes in network1 and network2.]
Description [The hash table returned by the function contains corresponding combinational input nodes in network1 and network2. The correspondence is based on the names of the nodes. The following conditions constitute an error: 1) the number of combinational inputs in the two networks is different. 2) there is no combinational input in network2 by the same name as one occurring in network1. 3) the two combinational inputs in network1 and network2 having same names have different variable types. If an error occurs, NULL is returned.]
SideEffects []
SeeAlso []
Definition at line 236 of file eqvMisc.c.
{
lsGen gen1, gen2;
Ntk_Node_t *node1, *node2;
Var_Variable_t *var1, *var2;
char *name1, *name2;
boolean flag = FALSE;
boolean equivalent = TRUE;
boolean causeOfError = TRUE;
st_table *inputMap;
int numValues;
int i;
if(Ntk_NetworkReadNumCombInputs(network1) !=
Ntk_NetworkReadNumCombInputs(network2)) {
error_append("Different number of combinational inputs in the two networks\n");
return NIL(st_table);
}
inputMap = st_init_table(st_ptrcmp, st_ptrhash);
Ntk_NetworkForEachCombInput(network1, gen1, node1) {
name1 = Ntk_NodeReadName(node1);
Ntk_NetworkForEachCombInput(network2, gen2, node2) {
name2 = Ntk_NodeReadName(node2);
if (strcmp(name1, name2) == 0) {
boolean a, b;
var1 = Ntk_NodeReadVariable(node1);
var2 = Ntk_NodeReadVariable(node2);
a = Var_VariableTestIsEnumerative(var1);
b = Var_VariableTestIsEnumerative(var2);
if((a && !b) || (!a && b)) {
error_append("Input ");
error_append(name1);
error_append(" and ");
error_append(name2);
error_append(" have different variable types\n");
causeOfError = FALSE;
}
else {
numValues = Var_VariableReadNumValues(var1);
if(a && b) {
if(numValues == Var_VariableReadNumValues(var2)) {
st_insert(inputMap, (char *) node1, (char *) node2);
flag = TRUE;
}
else {
error_append("Input ");
error_append(name1);
error_append(" and ");
error_append(name2);
error_append(" have different range of values\n");
causeOfError = FALSE;
}
}
else {/* both are symbolic */
boolean flag2 = TRUE;
for(i=0; i<numValues; i++) {
if(strcmp(Var_VariableReadSymbolicValueFromIndex(var1, i),
Var_VariableReadSymbolicValueFromIndex(var2, i)))
{
flag2 = FALSE;
error_append("Input ");
error_append(name1);
error_append(" and ");
error_append(name2);
error_append(" have different symbolic values\n");
causeOfError = FALSE;
}
}
if(flag2) {
st_insert(inputMap, (char *) node1, (char *) node2);
flag = TRUE;
}
}
}
}
}
if(!flag) {
equivalent = FALSE; /* name1 did not find a match in network2 */
if(causeOfError) {
error_append("Input ");
error_append(name1);
error_append(" does not have a match\n");
}
else {
causeOfError = TRUE;
}
}
else {
flag = FALSE;
}
}
if(!equivalent) {
st_free_table(inputMap);
return NIL(st_table);
}
else {
return inputMap;
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| st_table* MapCombOutputsByName | ( | Ntk_Network_t * | network1, |
| Ntk_Network_t * | network2 | ||
| ) |
Function********************************************************************
Synopsis [This function returns a hash table of corresponding combinational output nodes in network1 and network2.]
Description [The hash table returned by the function contains corresponding combinational output nodes in network1 and network2. The correspondence is based on the names of the nodes. The following conditions constitute an error: 1) the number of combinational outputs in the two networks is different. 2) there is no combinational output in network2 by the same name as one occurring in network1. 3) the two combinational outputs in network1 and network2 having same names have different variable types. If an error occurs, NULL is returned.]
SideEffects []
SeeAlso []
Definition at line 494 of file eqvMisc.c.
{
lsGen gen1, gen2;
Ntk_Node_t *node1, *node2;
Var_Variable_t *var1, *var2;
char *name1, *name2;
boolean flag = FALSE;
boolean equivalent = TRUE;
boolean causeOfError = TRUE;
st_table *outputMap;
int numValues;
int i;
if(Ntk_NetworkReadNumCombOutputs(network1) !=
Ntk_NetworkReadNumCombOutputs(network2)) {
error_append("Different number of combinational outputs in the two networks\n");
return NIL(st_table);
}
outputMap = st_init_table(st_ptrcmp, st_ptrhash);
Ntk_NetworkForEachCombOutput(network1, gen1, node1) {
name1 = Ntk_NodeReadName(node1);
Ntk_NetworkForEachCombOutput(network2, gen2, node2) {
name2 = Ntk_NodeReadName(node2);
if (NodesMatchUp(node1, node2)) {
boolean a, b;
var1 = Ntk_NodeReadVariable(node1);
var2 = Ntk_NodeReadVariable(node2);
a = Var_VariableTestIsEnumerative(var1);
b = Var_VariableTestIsEnumerative(var2);
if((a && !b) || (!a && b)) {
error_append("Output ");
error_append(name1);
error_append(" and ");
error_append(name2);
error_append(" have different variable types\n");
causeOfError = FALSE;
}
else {
numValues = Var_VariableReadNumValues(var1);
if(a && b) {
if(numValues == Var_VariableReadNumValues(var2)) {
st_insert(outputMap, (char *) node1, (char *) node2);
flag = TRUE;
}
else {
error_append("Output ");
error_append(name1);
error_append(" and ");
error_append(name2);
error_append(" have different range of values\n");
causeOfError = FALSE;
}
}
else {/* both are symbolic */
boolean flag2 = TRUE;
for(i=0; i<numValues; i++) {
if(strcmp(Var_VariableReadSymbolicValueFromIndex(var1, i),
Var_VariableReadSymbolicValueFromIndex(var2, i)))
{
flag2 = FALSE;
error_append("Output ");
error_append(name1);
error_append(" and ");
error_append(name2);
error_append(" have different symbolic values\n");
causeOfError = FALSE;
}
}
if(flag2) {
st_insert(outputMap, (char *) node1, (char *) node2);
flag = TRUE;
break;
}
}
}
}
}
if(!flag) {
equivalent = FALSE; /* name1 did not find a match in network2 */
if(causeOfError) {
error_append("Output ");
error_append(name1);
error_append(" does not have a match\n");
}
else {
causeOfError = TRUE;
}
}
else {
flag = FALSE;
}
}
if(!equivalent) {
st_free_table(outputMap);
return NIL(st_table);
}
else {
return outputMap;
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| st_table* MapNamesToNodes | ( | Ntk_Network_t * | network1, |
| Ntk_Network_t * | network2, | ||
| st_table * | names | ||
| ) |
Function********************************************************************
Synopsis [This function takes a hash table of names and generates a hash table of nodes.]
Description [The input to the function is a hash table of names of nodes. It returns a hash table of nodes corresponding to the names. In the hash table names, key is a name in network1 and value is a name in network2. Similarly, in the table which is returned, key is a node in network1 and value a node in network2. If no node by a certain name is found in a network, NULL is returned.]
SideEffects []
SeeAlso []
Definition at line 694 of file eqvMisc.c.
{
st_table *nodes = st_init_table(st_ptrcmp, st_ptrhash);
char *name1, *name2;
Ntk_Node_t *node1, *node2;
boolean error = FALSE;
st_generator *gen;
st_foreach_item(names, gen, &name1, &name2) {
if((node1 = Ntk_NetworkFindNodeByName(network1, name1)) ==
NIL(Ntk_Node_t)) {
error = TRUE;
error_append(name1);
error_append(" not present in network1.\n");
}
if((node2 = Ntk_NetworkFindNodeByName(network2, name2)) ==
NIL(Ntk_Node_t)) {
error = TRUE;
error_append(name2);
error_append(" not present in network2.\n");
}
st_insert(nodes, (char *) node1, (char *) node2);
}
if(error) {
st_free_table(nodes);
return NIL(st_table);
}
else {
return nodes;
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| st_table* MapPrimaryInputsByName | ( | Ntk_Network_t * | network1, |
| Ntk_Network_t * | network2 | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [This function returns a hash table of corresponding primary input nodes in network1 and network2.]
Description [The hash table returned by the function contains corresponding primary input nodes in network1 and network2. The correspondence is based on the names of the nodes. The following conditions constitute an error: 1) the number of primary inputs in the two networks is different. 2) there is no primary input in network2 by the same name as one occurring in network1. 3) the two primary inputs in network1 and network2 having the same names have different variable types. If an error occurs, NULL is returned.]
SideEffects []
SeeAlso []
Definition at line 107 of file eqvMisc.c.
{
lsGen gen1, gen2;
Ntk_Node_t *node1, *node2;
Var_Variable_t *var1, *var2;
char *name1, *name2;
boolean flag = FALSE;
boolean equivalent = TRUE;
boolean causeOfError = TRUE;
st_table *inputMap;
int numValues;
int i;
if(Ntk_NetworkReadNumPrimaryInputs(network1) !=
Ntk_NetworkReadNumPrimaryInputs(network2)) {
error_append("Different number of primary inputs in the two networks\n");
return NIL(st_table);
}
inputMap = st_init_table(st_ptrcmp, st_ptrhash);
Ntk_NetworkForEachPrimaryInput(network1, gen1, node1) {
name1 = Ntk_NodeReadName(node1);
Ntk_NetworkForEachPrimaryInput(network2, gen2, node2) {
name2 = Ntk_NodeReadName(node2);
if (strcmp(name1, name2) == 0) {
boolean a, b;
var1 = Ntk_NodeReadVariable(node1);
var2 = Ntk_NodeReadVariable(node2);
a = Var_VariableTestIsEnumerative(var1);
b = Var_VariableTestIsEnumerative(var2);
if((a && !b) || (!a && b)) {
error_append("Input ");
error_append(name1);
error_append(" and ");
error_append(name2);
error_append(" have different variable types\n");
causeOfError = FALSE;
}
else {
numValues = Var_VariableReadNumValues(var1);
if(a && b) {
if(numValues == Var_VariableReadNumValues(var2)) {
st_insert(inputMap, (char *) node1, (char *) node2);
flag = TRUE;
}
else {
error_append("Input ");
error_append(name1);
error_append(" and ");
error_append(name2);
error_append(" have different range of values\n");
causeOfError = FALSE;
}
}
else {/* both are symbolic */
boolean flag2 = TRUE;
for(i=0; i<numValues; i++) {
if(strcmp(Var_VariableReadSymbolicValueFromIndex(var1, i),
Var_VariableReadSymbolicValueFromIndex(var2, i)))
{
flag2 = FALSE;
error_append("Input ");
error_append(name1);
error_append(" and ");
error_append(name2);
error_append(" have different symbolic values\n");
causeOfError = FALSE;
}
}
if(flag2) {
st_insert(inputMap, (char *) node1, (char *) node2);
flag = TRUE;
}
}
}
}
}
if(!flag) {
equivalent = FALSE; /* name1 did not find a match in network2 */
if(causeOfError) {
error_append("Input ");
error_append(name1);
error_append(" does not have a match\n");
}
else {
causeOfError = TRUE;
}
}
else {
flag = FALSE;
}
}
if(!equivalent) {
st_free_table(inputMap);
return NIL(st_table);
}
else {
return inputMap;
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| st_table* MapPrimaryOutputsByName | ( | Ntk_Network_t * | network1, |
| Ntk_Network_t * | network2 | ||
| ) |
Function********************************************************************
Synopsis [This function returns a hash table of corresponding primary output nodes in network1 and network2.]
Description [The hash table returned by the function contains corresponding primary output nodes in network1 and network2. The correspondence is based on the names of the nodes. The following conditions constitute an error: 1) the number of primary outputs in the two networks is different. 2) there is no primary output in network2 by the same name as one occurring in network1. 3) the two primary outputs in network1 and network2 having the same names have different variable types. If an error occurs, NULL is returned.]
SideEffects []
SeeAlso []
Definition at line 364 of file eqvMisc.c.
{
lsGen gen1, gen2;
Ntk_Node_t *node1, *node2;
Var_Variable_t *var1, *var2;
char *name1, *name2;
boolean flag = FALSE;
boolean equivalent = TRUE;
boolean causeOfError = TRUE;
st_table *outputMap;
int numValues;
int i;
if(Ntk_NetworkReadNumPrimaryOutputs(network1) !=
Ntk_NetworkReadNumPrimaryOutputs(network2)) {
error_append("Different number of primary outputs in the two networks\n");
return NIL(st_table);
}
outputMap = st_init_table(st_ptrcmp, st_ptrhash);
Ntk_NetworkForEachPrimaryOutput(network1, gen1, node1) {
name1 = Ntk_NodeReadName(node1);
Ntk_NetworkForEachPrimaryOutput(network2, gen2, node2) {
name2 = Ntk_NodeReadName(node2);
if (strcmp(name1, name2) == 0) {
boolean a, b;
var1 = Ntk_NodeReadVariable(node1);
var2 = Ntk_NodeReadVariable(node2);
a = Var_VariableTestIsEnumerative(var1);
b = Var_VariableTestIsEnumerative(var2);
if((a && !b) || (!a && b)) {
error_append("Output ");
error_append(name1);
error_append(" and ");
error_append(name2);
error_append(" have different variable types\n");
causeOfError = FALSE;
}
else {
numValues = Var_VariableReadNumValues(var1);
if(a && b) {
if(numValues == Var_VariableReadNumValues(var2)) {
st_insert(outputMap, (char *) node1, (char *) node2);
flag = TRUE;
}
else {
error_append("Output ");
error_append(name1);
error_append(" and ");
error_append(name2);
error_append(" have different range of values\n");
causeOfError = FALSE;
}
}
else {/* both are symbolic */
boolean flag2 = TRUE;
for(i=0; i<numValues; i++) {
if(strcmp(Var_VariableReadSymbolicValueFromIndex(var1, i),
Var_VariableReadSymbolicValueFromIndex(var2, i)))
{
flag2 = FALSE;
error_append("Output ");
error_append(name1);
error_append(" and ");
error_append(name2);
error_append(" have different symbolic values\n");
causeOfError = FALSE;
}
}
if(flag2) {
st_insert(outputMap, (char *) node1, (char *) node2);
flag = TRUE;
}
}
}
}
}
if(!flag) {
equivalent = FALSE; /* name1 did not find a match in network2 */
if(causeOfError) {
error_append("Output ");
error_append(name1);
error_append(" does not have a match\n");
}
else {
causeOfError = TRUE;
}
}
else {
flag = FALSE;
}
}
if(!equivalent) {
st_free_table(outputMap);
return NIL(st_table);
}
else {
return outputMap;
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static boolean NodesMatchUp | ( | Ntk_Node_t * | node1, |
| Ntk_Node_t * | node2 | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Check whether two nodes may be matched by name.]
Description [Check whether two nodes from different networks may be matched by name in equivalence verification. If the two nodes have the same names, then they match. Moreover, if the two nodes are latch inputs and the corresponding latches match by name, they also match. This last clause makes comb_verify a lot more useful because small changes in Verilog source or in its translation to blif-mv usually leave the latch names unchanged, but alter the names of the next state variables.]
SideEffects [none]
SeeAlso [MapCombOutputsByName]
Definition at line 1065 of file eqvMisc.c.
{
char *name1, *name2;
name1 = Ntk_NodeReadName(node1);
name2 = Ntk_NodeReadName(node2);
if (strcmp(name1, name2) == 0)
return TRUE;
/* Try to match through the state variables. */
if ((Ntk_NodeTestIsLatchDataInput(node1) &&
Ntk_NodeTestIsLatchDataInput(node2)) ||
(Ntk_NodeTestIsLatchInitialInput(node1) &&
Ntk_NodeTestIsLatchInitialInput(node2))) {
Ntk_Node_t *latch1, *latch2;
char *nameLatch1, *nameLatch2;
array_t *fanout1, *fanout2;
fanout1 = Ntk_NodeReadFanouts(node1);
if (array_n(fanout1) != 1) return FALSE;
fanout2 = Ntk_NodeReadFanouts(node2);
if (array_n(fanout2) != 1) return FALSE;
latch1 = array_fetch(Ntk_Node_t *, fanout1, 0);
assert(Ntk_NodeTestIsLatch(latch1));
latch2 = array_fetch(Ntk_Node_t *, fanout2, 0);
assert(Ntk_NodeTestIsLatch(latch2));
nameLatch1 = Ntk_NodeReadName(latch1);
nameLatch2 = Ntk_NodeReadName(latch2);
return (strcmp(nameLatch1, nameLatch2) == 0);
}
return FALSE;
} /* NodesMatchUp */
Here is the call graph for this function:
Here is the caller graph for this function:
| int ReadRootLeafMap | ( | FILE * | inputFile, |
| st_table * | rootsTable, | ||
| st_table * | leavesTable | ||
| ) |
Function********************************************************************
Synopsis [This function reads an input file containing names of roots and leaves, and stores the corresponding names in the two hash tables- rootsTable and leavesTable.]
Description [The function returns 0 if there are no roots or leaves in the file. It is an error not to have either roots or leaves in the file. It returns 1 if there are roots but no leaves, 2 if there are leaves but no roots, and 3 if there are both roots and leaves.]
SideEffects []
SeeAlso []
Definition at line 750 of file eqvMisc.c.
{
char *name;
char *rootName1, *rootName2;
char *leafName1, *leafName2;
char c;
boolean rootsFlag= 0;
boolean leavesFlag = 0;
st_generator *gen;
while(((c = fgetc(inputFile)) == ' ') || (c == '\t') || (c== '\n' ));
ungetc(c, inputFile);
name = ALLOC(char, 20);
if(fscanf(inputFile, "%s", name) == EOF) {
FREE(name);
return 0;
/* both roots and leaves absent */
}
if(!strcmp(name, ".roots")) {
rootsFlag = 1;
while(((c = fgetc(inputFile)) == ' ') || (c == '\t') || (c== '\n' ));
ungetc(c, inputFile);
while((fscanf(inputFile, "%s", name) != EOF) && strcmp(name, ".leaves")) {
rootName1 = ALLOC(char, strlen(name) + 1);
strcpy(rootName1, name);
while(((c = fgetc(inputFile)) == ' ') || (c == '\t') || (c== '\n' ));
ungetc(c, inputFile);
if((fscanf(inputFile, "%s", name) == EOF) || (!strcmp(name, ".leaves"))) {
FREE(name);
FREE(rootName1);
st_foreach_item(rootsTable, gen, &rootName1, &rootName2) {
FREE(rootName1);
FREE(rootName2);
return 0;
}
}
rootName2 = ALLOC(char, strlen(name) + 1);
strcpy(rootName2, name);
st_insert(rootsTable, rootName1, rootName2);
while(((c = fgetc(inputFile)) == ' ') || (c == '\t') || (c== '\n' ));
ungetc(c, inputFile);
name[0] = '\0'; /* this is to insure that whenever the while loop
is terminated, only one of the conditions is false */
}
}
if(!strcmp(name, ".leaves")) {
leavesFlag = 1;
while(((c = fgetc(inputFile)) == ' ') || (c == '\t') || (c== '\n' ));
ungetc(c, inputFile);
while(fscanf(inputFile, "%s", name) != EOF) {
leafName1 = ALLOC(char, strlen(name) + 1);
strcpy(leafName1, name);
while(((c = fgetc(inputFile)) == ' ') || (c == '\t') || (c== '\n' ));
ungetc(c, inputFile);
if(fscanf(inputFile, "%s", name) == EOF) {
FREE(name);
FREE(leafName1);
st_foreach_item(leavesTable, gen, &leafName1, &leafName2) {
FREE(leafName1);
FREE(leafName2);
return 0;
}
}
leafName2 = ALLOC(char, strlen(name) + 1);
strcpy(leafName2, name);
st_insert(leavesTable, leafName1, leafName2);
while(((c = fgetc(inputFile)) == ' ') || (c == '\t') || (c== '\n' ));
ungetc(c, inputFile);
}
}
FREE(name);
if(rootsFlag == 1) {
if(leavesFlag == 1) {
return 3; /* both leaves and roots present */
}
else {
return 2; /* roots present but leaves absent */
}
}
else {
if(leavesFlag == 1) {
return 1; /* roots absent but leaves present */
}
else {
return 0;
}
}
}
Here is the caller graph for this function:
| boolean TestLeavesAreValid | ( | Ntk_Network_t * | network1, |
| Ntk_Network_t * | network2, | ||
| st_table * | leavesTable | ||
| ) |
Function********************************************************************
Synopsis [This function checks whether the leaves present in leavesTable constitute the full set of primary inputs of network1 and network2.]
Description [leavesTable contains names of corresponding leaves in network1 and network2. The function returns TRUE if the leaves present in leavesTable constitute the full set of primary inputs of network1 and network2. The following conditions result in a return value of FALSE: a) there is no node by a name present in leavesTable. b) the node with a particular name is not a primary input c) the number of leaves is different from the number of primary inputs in either network.]
SideEffects []
SeeAlso []
Definition at line 904 of file eqvMisc.c.
{
st_generator *gen;
Ntk_Node_t *node1, *node2;
char *name1, *name2;
boolean valid = TRUE;
int count = 0;
st_foreach_item(leavesTable, gen, &name1, &name2) {
node1 = Ntk_NetworkFindNodeByName(network1, name1);
node2 = Ntk_NetworkFindNodeByName(network2, name2);
if(node1 == NIL(Ntk_Node_t)) {
error_append(name1);
error_append(" not found in network1.\n");
valid = FALSE;
}
else {
if(!Ntk_NodeTestIsPrimaryInput(node1)) {
error_append(name1);
error_append(" is not a primary input node\n");
valid = FALSE;
}
}
if(node2 == NIL(Ntk_Node_t)) {
error_append(name2);
error_append(" not found in network2.\n");
valid = FALSE;
}
else {
if(!Ntk_NodeTestIsPrimaryInput(node2)) {
error_append(name2);
error_append(" is not a primary input node\n");
valid = FALSE;
}
}
count ++;
}
if(valid) {
if(!((Ntk_NetworkReadNumPrimaryInputs(network1) == count) && (Ntk_NetworkReadNumPrimaryInputs(network2) == count))) {
error_append("All primary inputs not specified in the input file\n");
valid = FALSE;
}
}
return valid;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| boolean TestPartitionIsValid | ( | Ntk_Network_t * | network, |
| st_table * | roots, | ||
| st_table * | leaves | ||
| ) |
Function********************************************************************
Synopsis [The function checks whether the partition registered with network has vertices corresponding to nodes stored as keys in roots and leaves.]
Description [The function returns TRUE if all the nodes stored as keys in roots and leaves have corresponding vertices in the partition of network. It returns FALSE otherwise. It is assumed that network has a partition associated with it.]
SideEffects []
SeeAlso []
Definition at line 1016 of file eqvMisc.c.
{
graph_t *partition = Part_NetworkReadPartition(network);
st_generator *gen;
char *name;
Ntk_Node_t *node1, *node2;
boolean flag = TRUE;
st_foreach_item(roots, gen, &node1, &node2) {
name = Ntk_NodeReadName(node1);
if(Part_PartitionFindVertexByName(partition, name) == NIL(vertex_t)) {
flag = FALSE;
}
}
st_foreach_item(leaves, gen, &node1, &node2) {
name = Ntk_NodeReadName(node1);
if(Part_PartitionFindVertexByName(partition, name) == NIL(vertex_t)) {
flag = FALSE;
}
}
return flag;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| boolean TestRootsAndLeavesAreValid | ( | Ntk_Network_t * | network1, |
| Ntk_Network_t * | network2, | ||
| st_table * | inputMap, | ||
| st_table * | outputMap | ||
| ) |
Function********************************************************************
Synopsis [The function checks whether inputMap and outputMap form valid roots and leaves for network1 and network2.]
Description [inputMap is a hash table of the corresponding leaves in network1 and network2. outputMap is a hash table of the corresponding roots in network1 and network2. The function checks whether the leaves of each network form a complete support of its roots. If this turns out to be false for any network, FALSE is returned otherwise TRUE is returned.]
SideEffects []
SeeAlso []
Definition at line 633 of file eqvMisc.c.
{
st_generator *gen;
array_t *roots1, *roots2;
st_table *leaves1, *leaves2;
Ntk_Node_t *node1, *node2;
boolean test = TRUE;
roots1 = array_alloc(Ntk_Node_t *, 0);
roots2 = array_alloc(Ntk_Node_t *, 0);
st_foreach_item(outputMap, gen, &node1, &node2) {
array_insert_last(Ntk_Node_t *, roots1, node1);
array_insert_last(Ntk_Node_t *, roots2, node2);
}
leaves1 = st_init_table(st_ptrcmp, st_ptrhash);
leaves2 = st_init_table(st_ptrcmp, st_ptrhash);
st_foreach_item(inputMap, gen, &node1, &node2) {
st_insert(leaves1, node1, NULL);
st_insert(leaves2, node2, NULL);
}
if(!Ntk_NetworkTestLeavesCoverSupportOfRoots(network1, roots1,
leaves1)) {
error_append("Leaves do not form a complete support for roots in network1.\n");
test = FALSE;
}
if(!Ntk_NetworkTestLeavesCoverSupportOfRoots(network2, roots2,
leaves2)) {
error_append("Leaves do not form a complete support for roots in network2.\n");
test = FALSE;
}
array_free(roots1);
array_free(roots2);
st_free_table(leaves1);
st_free_table(leaves2);
return test;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| boolean TestRootsAreValid | ( | Ntk_Network_t * | network1, |
| Ntk_Network_t * | network2, | ||
| st_table * | rootsTable | ||
| ) |
Function********************************************************************
Synopsis [The function checks whether the names present in rootsTable have nodes corresponding to them present in network1 and network2.]
Description [rootsTable contains names of corresponding roots in network1 and network2. The function returns TRUE if the roots present in rootsTable have nodes corresponding to them in the network1 and network2. Otherwise, FALSE is returned.]
SideEffects []
SeeAlso []
Definition at line 972 of file eqvMisc.c.
{
st_generator *gen;
char *name1, *name2;
boolean valid = TRUE;
st_foreach_item(rootsTable, gen, &name1, &name2) {
if(Ntk_NetworkFindNodeByName(network1, name1) == NIL(Ntk_Node_t)) {
valid = FALSE;
error_append(name1);
error_append(" not present in network1.\n");
}
if(Ntk_NetworkFindNodeByName(network2, name2) == NIL(Ntk_Node_t)) {
valid = FALSE;
error_append(name2);
error_append(" not present in network2.\n");
}
}
return valid;
}
Here is the call graph for this function:
Here is the caller graph for this function:
Variable Documentation
char rcsid [] UNUSED = "$Id: eqvMisc.c,v 1.10 2009/04/11 01:40:06 fabio Exp $" [static] |
CFile***********************************************************************
FileName [eqvMisc.c]
PackageName [eqv]
Synopsis [This file provides some miscellaneous functions for the eqv package.]
Description []
SeeAlso []
Author [Shaz Qadeer]
Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of California. All rights reserved.
Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software.
IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
