#include "eqvInt.h"
Include dependency graph for eqvVerify.c:
Go to the source code of this file.
Functions | |
| boolean | Eqv_NetworkVerifyCombinationalEquivalence (Ntk_Network_t *network1, Ntk_Network_t *network2, st_table *leavesMap, st_table *rootsMap, OFT AssignCommonOrder, Part_PartitionMethod method1, Part_PartitionMethod method2) |
| boolean | Eqv_NetworkVerifySequentialEquivalence (Ntk_Network_t *network1, Ntk_Network_t *network2, st_table *rootsTable, st_table *leavesTable, Part_PartitionMethod partMethod, boolean useBackwardReach, boolean reordering) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: eqvVerify.c,v 1.10 2009/04/11 01:40:06 fabio Exp $" |
Function Documentation
| boolean Eqv_NetworkVerifyCombinationalEquivalence | ( | Ntk_Network_t * | network1, |
| Ntk_Network_t * | network2, | ||
| st_table * | leavesMap, | ||
| st_table * | rootsMap, | ||
| OFT | AssignCommonOrder, | ||
| Part_PartitionMethod | method1, | ||
| Part_PartitionMethod | method2 | ||
| ) |
AutomaticStart AutomaticEnd Function********************************************************************
Synopsis [This function does combinational verification between network1 and network2.]
Description [roootsMap and leavesMap contain corresponding nodes in network1 and network2. It is assumed that the set of leaf nodes forms a complete support of the set of root nodes in both the networks. This function verifies the combinational equivalence of corresponding roots in terms of the leaves. method1 and method2 specify the partition methods to be used for partitioning network1 and network2 respectively. AssignCommonOrder is a pointer to a function which takes two networks, whose mdd managers are identical, and a hash table containing corresponding leaf nodes whose mdd Id should be the same. AssignCommonOrder() orders the two networks ensuring that identical mddIds are assigned to the corresponding leaf nodes in the hash table. This function has to be supplied by the user.
This function returns TRUE if all the root pairs are combinationally equivalent otherwise it returns FALSE. It is assumed that network1 already has a mdd manager. If a partition is registered with network1, and it has vertices corresponding to the specified roots and leaves it is used otherwise a new partition is created. A new partition is always created for network2.]
SideEffects []
Definition at line 83 of file eqvVerify.c.
{
mdd_manager *mddMgr;
lsList leavesList1, leavesList2;
lsList rootsList1, rootsList2;
st_table *leaves1, *leaves2;
array_t *roots1, *roots2;
st_generator *gen;
lsGen listGen;
graph_t *rootsToLeaves1, *rootsToLeaves2;
Ntk_Node_t *node1, *node2;
char *name1, *name2, *name;
Mvf_Function_t *func1, *func2;
int num, i, j;
array_t *mvfRoots1, *mvfRoots2;
boolean equivalent = TRUE;
lsList dummy = (lsList) 0;
int mddId1, mddId2;
vertex_t *vertex;
lsGeneric data;
boolean partValid = FALSE;
mdd_manager *mgr;
int mddId;
array_t *mddIdArray;
mdd_t *aMinterm, *diff;
char *mintermName;
mdd_t *comp1, *comp2;
int numComponents;
/* First check whether a partition is registered with network1 */
if(Ntk_NetworkReadApplInfo(network1, PART_NETWORK_APPL_KEY) != NIL(void)) {
/*
* Check whether the registered partition can be used to compute the roots
* in terms of the leaves. If it can be used, then i won't create a new
* one.
*/
partValid = TestPartitionIsValid(network1, rootsMap, leavesMap);
/*
* If a partition already exists, an mddManager also exists.
* So, don't allocate a new one.
*/
mddMgr = Ntk_NetworkReadMddManager(network1);
}
else {
mddMgr = Ntk_NetworkInitializeMddManager(network1);
}
assert(mddMgr != NIL(mdd_manager));
Ntk_NetworkSetMddManager(network2, mddMgr);
(*AssignCommonOrder)(network1, network2, leavesMap);
/* Create lists of leaves and roots for creating partitions. */
leavesList1 = lsCreate();
leavesList2 = lsCreate();
st_foreach_item(leavesMap, gen, &node1, &node2) {
mddId1 = Ntk_NodeReadMddId(node1);
mddId2 = Ntk_NodeReadMddId(node2);
assert(mddId1 == mddId2);
lsNewEnd(leavesList1, (lsGeneric) node1, LS_NH);
lsNewEnd(leavesList2, (lsGeneric) node2, LS_NH);
}
rootsList1 = lsCreate();
rootsList2 = lsCreate();
st_foreach_item(rootsMap, gen, &node1, &node2) {
lsNewEnd(rootsList1, (lsGeneric) node1, LS_NH);
lsNewEnd(rootsList2, (lsGeneric) node2, LS_NH);
}
if(partValid) {
rootsToLeaves1 = Part_NetworkReadPartition(network1);
}
else {
rootsToLeaves1 = Part_NetworkCreatePartition(network1, NIL(Hrc_Node_t),
"dummy", rootsList1,
leavesList1, NIL(mdd_t),
method1, dummy,
FALSE, FALSE, TRUE);
}
/*
* Generate arrays of root and leaf vertices in the first partition
* to pass as arguments to Part_PartitionCollapse().
*/
roots1 = array_alloc(vertex_t *, 0);
lsForEachItem(rootsList1, listGen, data) {
name = Ntk_NodeReadName((Ntk_Node_t *) data);
vertex = Part_PartitionFindVertexByName(rootsToLeaves1, name);
assert(vertex != NIL(vertex_t));
array_insert_last(vertex_t *, roots1, vertex);
}
leaves1 = st_init_table(st_ptrcmp, st_ptrhash);
lsForEachItem(leavesList1, listGen, data) {
name = Ntk_NodeReadName((Ntk_Node_t *) data);
vertex = Part_PartitionFindVertexByName(rootsToLeaves1, name);
/* assert(vertex != NIL(vertex_t)); */
if(vertex != NIL(vertex_t)) {
/*
* If a leaf is not actually in the support of the roots then
* it will not be present in the partition.
*/
mddId = Part_VertexReadMddId(vertex);
st_insert(leaves1, (char *) vertex, (char *) (long) mddId);
}
}
lsDestroy(rootsList1, (void (*) (lsGeneric)) 0);
lsDestroy(leavesList1, (void (*) (lsGeneric)) 0);
rootsToLeaves2 = Part_NetworkCreatePartition(network2, NIL(Hrc_Node_t),
"dummy", rootsList2,
leavesList2, NIL(mdd_t),
method2, dummy, FALSE,
FALSE, TRUE);
/*
* Generate arrays of root and leaf vertices in the second partition
* to pass as arguments to Part_PartitionCollapse().
*/
roots2 = array_alloc(vertex_t *, 0);
lsForEachItem(rootsList2, listGen, data) {
name = Ntk_NodeReadName((Ntk_Node_t *) data);
vertex = Part_PartitionFindVertexByName(rootsToLeaves2, name);
assert(vertex != NIL(vertex_t));
array_insert_last(vertex_t *, roots2, vertex);
}
leaves2 = st_init_table(st_ptrcmp, st_ptrhash);
lsForEachItem(leavesList2, listGen, data) {
name = Ntk_NodeReadName((Ntk_Node_t *) data);
vertex = Part_PartitionFindVertexByName(rootsToLeaves2, name);
/* assert(vertex != NIL(vertex_t)); */
if(vertex != NIL(vertex_t)) {
/*
* If a leaf is not actually in the support of the roots then
* it will not be present in the partition.
*/
mddId = Part_VertexReadMddId(vertex);
st_insert(leaves2, (char *) vertex, (char *) (long) mddId);
}
}
lsDestroy(rootsList2, (void (*) (lsGeneric)) 0);
lsDestroy(leavesList2, (void (*) (lsGeneric)) 0);
assert(Part_PartitionReadMddManager(rootsToLeaves1) ==
Part_PartitionReadMddManager(rootsToLeaves2));
mvfRoots1 = Part_PartitionCollapse(rootsToLeaves1, roots1, leaves1, NIL(mdd_t));
mvfRoots2 = Part_PartitionCollapse(rootsToLeaves2, roots2, leaves2, NIL(mdd_t));
assert(array_n(mvfRoots1) == array_n(mvfRoots2));
num = array_n(mvfRoots1);
mddIdArray = array_alloc(int, 0);
st_foreach_item_int(leaves1, gen, &vertex, &mddId) {
array_insert_last(int, mddIdArray, mddId);
}
/*
* For each pair of corresponding outputs in the two arrays mvfRoots1 and
* mvfRoots2, I will compute the mdd representing all the input combinations
* for which they are different. For each pair, I will print one input
* combination for which they are different.
*/
for(i = 0; i<num; ++i) {
func1 = array_fetch(Mvf_Function_t *, mvfRoots1, i);
func2 = array_fetch(Mvf_Function_t *, mvfRoots2, i);
if(!Mvf_FunctionTestIsEqualToFunction(func1, func2)) {
mgr = Mvf_FunctionReadMddManager(func1);
assert(mgr == Mvf_FunctionReadMddManager(func2));
numComponents = Mvf_FunctionReadNumComponents(func1);
for(j=0; j<numComponents; ++j) {
comp1 = Mvf_FunctionReadComponent(func1, j);
comp2 = Mvf_FunctionReadComponent(func2, j);
diff = mdd_xor(comp1, comp2);
if(!mdd_is_tautology(diff, 0)) {
aMinterm = Mc_ComputeAMinterm(diff, mddIdArray, mddMgr);
mintermName = Mc_MintermToString(aMinterm, mddIdArray, network1);
vertex = array_fetch(vertex_t *, roots1, i);
name1 = Part_VertexReadName(vertex);
vertex = array_fetch(vertex_t *, roots2, i);
name2 = Part_VertexReadName(vertex);
(void) fprintf(vis_stdout, "%s from network1 and %s from network2 differ on input values\n%s",
name1, name2, mintermName);
FREE(mintermName);
mdd_free(aMinterm);
mdd_free(diff);
break;
}
mdd_free(diff);
}
equivalent = FALSE;
}
}
array_free(mddIdArray);
if(!partValid) {
Part_PartitionFree(rootsToLeaves1);
}
Part_PartitionFree(rootsToLeaves2);
array_free(roots1);
array_free(roots2);
st_free_table(leaves1);
st_free_table(leaves2);
arrayForEachItem(Mvf_Function_t *, mvfRoots1, i, func1) {
Mvf_FunctionFree(func1);
}
array_free(mvfRoots1);
arrayForEachItem(Mvf_Function_t *, mvfRoots2, i, func2) {
Mvf_FunctionFree(func2);
}
array_free(mvfRoots2);
Ntk_NetworkSetMddManager(network2, NIL(mdd_manager));
/*
* This is needed because Ntk_NetworkFree() will be called on both network1
* and network2.
*/
return equivalent;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| boolean Eqv_NetworkVerifySequentialEquivalence | ( | Ntk_Network_t * | network1, |
| Ntk_Network_t * | network2, | ||
| st_table * | rootsTable, | ||
| st_table * | leavesTable, | ||
| Part_PartitionMethod | partMethod, | ||
| boolean | useBackwardReach, | ||
| boolean | reordering | ||
| ) |
Function********************************************************************
Synopsis [This function does sequential verification between network1 and network2.]
Description [It accepts as input the two networks, and two hash tables of node names - rootsTable and leavesTable. leavesTable gives the names of corresponding primary inputs in the two networks. If leavesTable is NULL, the inputs are simply matched by names. rootsTable gives the names of corresponding nodes in the two networks whose sequential equivalence has to be verified. If rootsTable is NULL, it is assumed that all the primary outputs need to be verified and that they are to be associated by names. The function returns TRUE if the all the corresponding nodes are sequentially equivalent otherwise it returns FALSE. The verification is done by appending network1 to network2, thereby forming the product machine. A set of states in which the corresponding outputs to be verified are different for some input is calculated and it is checked whether any of these states is reachable from an initial state of the product machine.]
SideEffects [network2 is modified in this function.]
Definition at line 330 of file eqvVerify.c.
{
array_t *roots;
st_table *leaves;
lsList rootsList;
lsList rootsPartList = (lsList) 0;
st_table *outputMap = NIL(st_table);
Ntk_Node_t *node1, *node2, *node;
char *name1, *name2, *temp;
st_generator *gen;
lsGen listGen;
graph_t *partition;
vertex_t *vertex;
mdd_manager *mddMgr;
array_t *mvfArray;
Mvf_Function_t *mvf1, *mvf2;
mdd_t *badStates, *initialStates;
mdd_t *mddTemp, *mdd1, *mdd2, *tautology;
mdd_t *mddComp1, *mddComp2;
int n, i, j, numComponents;
int id;
array_t *inputIdArray;
lsList dummy = (lsList) 0;
lsGeneric data;
Ntk_Node_t *input;
Fsm_Fsm_t *modelFsm;
array_t *onionRings;
array_t *aPath;
boolean inequivalent;
boolean rootsFlag = (rootsTable == NIL(st_table)) ? FALSE : TRUE;
array_t *careStatesArray = array_alloc(mdd_t *, 0);
/* If rootsFlag is FALSE, all primary outputs are to be verified */
if(rootsFlag == FALSE) {
outputMap = MapPrimaryOutputsByName(network1, network2);
}
/*
* If leavesFlag is FALSE, the primary inputs in the two networks are
* assumed to have same names. In the network returned by
* Ntk_NetworkAppendNetwork(), the two corresponding nodes will be merged.
* If leavesFlag is TRUE, the name correspondence between the primary inputs
* in the two networks is specified in leavesTable.
*/
if(leavesTable == NIL(st_table)) {
st_table *emptyTable = st_init_table(strcmp, st_strhash);
Ntk_NetworkAppendNetwork(network2, network1, emptyTable);
st_free_table(emptyTable);
}
else {
Ntk_NetworkAppendNetwork(network2, network1, leavesTable);
}
/*
* network1 has been appended to the erstwhile network2, and the new network
* is now called network2.
*/
mddMgr = Ntk_NetworkInitializeMddManager(network2);
Ord_NetworkOrderVariables(network2, Ord_RootsByDefault_c,
Ord_NodesByDefault_c, FALSE, Ord_InputAndLatch_c,
Ord_Unassigned_c, dummy, FALSE);
if (reordering)
Ntk_NetworkSetDynamicVarOrderingMethod(network2, BDD_REORDER_SIFT,
BDD_REORDER_VERBOSITY);
/*
* Ntk_NetworkAppendNetwork() adds $NTK2 to the names of all the
* appended nodes. I want to find the appended nodes in new network2
* corresponding to the roots in network1. I will add all these nodes to
* rootsList. I will also add all the roots of the erstwhile network2, which
* exist in the network2 also. rootsList will finally contain all the nodes
* in network2 whose mdds have to be created by Part_Partition Collapse().
*/
rootsList = lsCreate();
if(rootsFlag == FALSE) {
st_foreach_item(outputMap, gen, &node1, &node2) {
name1 = Ntk_NodeReadName(node1);
temp = util_strcat3(name1, "$NTK2", "");
name1 = temp;
node1 = Ntk_NetworkFindNodeByName(network2, name1);
assert(node1 != NIL(Ntk_Node_t));
FREE(name1);
lsNewEnd(rootsList, (lsGeneric) node1, LS_NH);
lsNewEnd(rootsList, (lsGeneric) node2, LS_NH);
}
}
else {
st_foreach_item(rootsTable, gen, &name1, &name2) {
/* I am finding the node in the new network2 */
temp = util_strcat3(name1, "$NTK2", "");
name1 = temp;
node1 = Ntk_NetworkFindNodeByName(network2, name1);
FREE(name1);
lsNewEnd(rootsList, (lsGeneric) node1, LS_NH);
node2 = Ntk_NetworkFindNodeByName(network2, name2);
lsNewEnd(rootsList, (lsGeneric) node2, LS_NH);
}
}
if(outputMap) {
st_free_table(outputMap);
}
/* rootsPartList is the list of nodes which will passed to
* Part_NetworkCreatePartition(). I want all the next state functions i.e.
* latch data inputs as well as everything in rootsList to be in
* rootsPartList. If rootsFlag is FALSE, rootsPartList is simply passed as
* (lsList) 0.
*/
if(rootsFlag) {
rootsPartList = lsCreate();
Ntk_NetworkForEachCombOutput(network2, listGen, node) {
if(Ntk_NodeTestIsLatchDataInput(node) ||
Ntk_NodeTestIsLatchInitialInput(node)){
lsNewEnd(rootsPartList, (lsGeneric) node, LS_NH);
}
}
lsForEachItem(rootsList, listGen, node) {
if(!Ntk_NodeTestIsLatchDataInput(node) &&
!Ntk_NodeTestIsLatchInitialInput(node)) {
lsNewEnd(rootsPartList, (lsGeneric) node, LS_NH);
}
}
}
partition = Part_NetworkCreatePartition(network2, NIL(Hrc_Node_t), "dummy",
rootsPartList,
(lsList) 0, NIL(mdd_t), partMethod,
dummy, FALSE, FALSE, TRUE);
Ntk_NetworkAddApplInfo(network2, PART_NETWORK_APPL_KEY,
(Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
(void *) partition);
if(rootsPartList) {
lsDestroy(rootsPartList, (void (*) (lsGeneric)) 0);
}
/* Create roots and leaves for Part_PartitionCollapse().
*/
roots = array_alloc(vertex_t *, 0);
lsForEachItem(rootsList, listGen, data) {
name1 = Ntk_NodeReadName((Ntk_Node_t *) data);
vertex = Part_PartitionFindVertexByName(partition, name1);
assert(vertex != NIL(vertex_t));
array_insert_last(vertex_t *, roots, vertex);
}
lsDestroy(rootsList, (void (*) (lsGeneric)) 0);
leaves = st_init_table(st_ptrcmp, st_ptrhash);
Ntk_NetworkForEachCombInput(network2, listGen, node1) {
name1 = Ntk_NodeReadName(node1);
vertex = Part_PartitionFindVertexByName(partition, name1);
if(vertex != NIL(vertex_t)) {
/* A combinational input might not be present in the support of any
node in rootsPartList. If so, it will not be present in the partition
also. */
st_insert(leaves, (char *) vertex, (char *) (long) 0);
}
}
mvfArray = Part_PartitionCollapse(partition, roots, leaves, NIL(mdd_t));
array_free(roots);
st_free_table(leaves);
n = array_n(mvfArray);
assert(n%2 == 0);
n = n/2;
assert(mddMgr != NULL);
/* In mvfArray, the mvfs of corresponding nodes occur one after the other,
* because of the way rootsList was created. badStates will ultimately
* contain all the states for which any pair of corresponding nodes differ
* for some input.
*/
badStates = mdd_zero(mddMgr);
for(i=0; i<n; i++) {
mvf1 = array_fetch(Mvf_Function_t *, mvfArray, 2*i);
mvf2 = array_fetch(Mvf_Function_t *, mvfArray, 2*i +1);
numComponents = Mvf_FunctionReadNumComponents(mvf1);
mdd2 = mdd_zero(mddMgr);
/*
* Hopefully, mddMgr of the partition is the same as the mddMgr of the
* MVFs.
*/
for(j=0; j<numComponents; j++) {
mddComp1 = Mvf_FunctionObtainComponent(mvf1, j);
mddComp2 = Mvf_FunctionObtainComponent(mvf2, j);
mdd1 = mdd_and(mddComp1, mddComp2, 1, 1);
mdd_free(mddComp1);
mdd_free(mddComp2);
mddTemp = mdd_or(mdd2, mdd1, 1, 1);
mdd_free(mdd1);
mdd_free(mdd2);
mdd2 = mddTemp;
}
/*
* At this point, mdd2 represents the set of input and present state
* combinations in which mvf1 and mvf2 produce the same value. I want the
* set for which mvf1 and mvf2 are different.
*/
mddTemp = mdd_or(badStates, mdd2, 1, 0);
mdd_free(mdd2);
mdd_free(badStates);
badStates = mddTemp;
}
arrayForEachItem(Mvf_Function_t *, mvfArray, i, mvf1) {
Mvf_FunctionFree(mvf1);
}
array_free(mvfArray);
/* existentially quantify out the input variables */
inputIdArray = array_alloc(int, 0);
Ntk_NetworkForEachPrimaryInput(network2, listGen, input) {
id = Ntk_NodeReadMddId(input);
assert(id >= 0);
array_insert_last(int, inputIdArray, id);
}
mddTemp = mdd_smooth(mddMgr, badStates, inputIdArray);
mdd_free(badStates);
badStates = mddTemp;
array_free(inputIdArray);
modelFsm = Fsm_FsmCreateFromNetworkWithPartition(network2, NIL(graph_t));
assert(modelFsm != NIL(Fsm_Fsm_t));
Ntk_NetworkAddApplInfo(network2, FSM_NETWORK_APPL_KEY,
(Ntk_ApplInfoFreeFn) Fsm_FsmFreeCallback,
(void *) modelFsm);
onionRings = array_alloc(mdd_t *, 0);
initialStates = Fsm_FsmComputeInitialStates(modelFsm);
tautology = mdd_one(mddMgr);
/* Model checking function */
if (useBackwardReach == TRUE) {
array_insert(mdd_t *, careStatesArray, 0, tautology);
inequivalent = Mc_FsmComputeStatesReachingToSet(modelFsm, badStates,
careStatesArray, initialStates,
onionRings, McVerbosityNone_c, McDcLevelNone_c);
array_free(careStatesArray);
mdd_free(badStates);
mdd_free(tautology);
if (inequivalent) {
mdd_t *outerOnionRing = array_fetch_last(mdd_t *, onionRings);
mdd_t *badInitialStates = mdd_and(initialStates, outerOnionRing, 1, 1);
array_t *psVarMddIdArray = Fsm_FsmReadPresentStateVars(modelFsm);
mdd_t *aBadInitialState = Mc_ComputeAMinterm(initialStates, psVarMddIdArray, mddMgr);
mdd_free(badInitialStates);
aPath = Mc_BuildPathToCore(aBadInitialState, onionRings, modelFsm,
McGreaterOrEqualZero_c);
(void) Mc_PrintPath(aPath, modelFsm, TRUE); /* TRUE -> print inputs on path */
mdd_free(aBadInitialState);
mdd_free(initialStates);
mdd_array_free(aPath);
mdd_array_free(onionRings);
return FALSE;
}
else {
mdd_free(initialStates);
return TRUE;
}
}
else { /* do forward search */
array_insert(mdd_t *, careStatesArray, 0, tautology);
inequivalent = Mc_FsmComputeStatesReachableFromSet(modelFsm, initialStates,
careStatesArray, badStates, onionRings,
McVerbosityNone_c, McDcLevelNone_c);
array_free(careStatesArray);
mdd_free(tautology);
mdd_free(initialStates);
if (inequivalent) {
mdd_t *outerOnionRing = array_fetch_last(mdd_t *, onionRings);
mdd_t *reachableBadStates = mdd_and(badStates, outerOnionRing, 1, 1);
array_t *psVarMddIdArray = Fsm_FsmReadPresentStateVars(modelFsm);
mdd_t *aBadReachableState = Mc_ComputeAMinterm(reachableBadStates, psVarMddIdArray, mddMgr);
mdd_free(reachableBadStates);
psVarMddIdArray = Fsm_FsmReadPresentStateVars(modelFsm);
aPath = Mc_BuildPathFromCore(aBadReachableState, onionRings, modelFsm,
McGreaterOrEqualZero_c);
(void) Mc_PrintPath(aPath, modelFsm, TRUE); /* TRUE -> print inputs on path */
mdd_free(aBadReachableState);
mdd_free(badStates);
mdd_array_free(aPath);
mdd_array_free(onionRings);
return FALSE;
}
else {
mdd_free(badStates);
return TRUE;
}
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
Variable Documentation
char rcsid [] UNUSED = "$Id: eqvVerify.c,v 1.10 2009/04/11 01:40:06 fabio Exp $" [static] |
CFile***********************************************************************
FileName [eqvVerify.c]
PackageName [eqv]
Synopsis [This file contains the two routines which do combinational and sequential verification.]
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.]
Definition at line 39 of file eqvVerify.c.
