A Semantic Condition for Data Independence and Applications in Hardware Verification

Data independence is a useful technique in reasoning about systems. Commonly, if one knows that the qualitative behaviour of a system does not depend on the specific values of data inputs, the proof of facts about its behaviour can be simplified. Such knowledge typically comes from examination of the syntax of the program for the system. Industrial hardware verification flows lead to a requirement for automated proof of data independence without intrusion into the program, where the specification on which the proof is based makes no reference to details of the program language. This paper presents and proves a sufficient condition for data independence, expressed in terms of the behaviour of inputs and outputs of a system, that can be checked in practice by a model checker; and it demonstrates how this condition is used in two design applications.