The application of program verification techniques to hardware verification

Abstract

We have explained the notion of symbolic execution and shown how this concept is used in one method of program verification. We have also explored the application of program verification techniques to the problem of hardware verification. In particular we have looked at how one could prove that a microprogram and supporting hardware have the behavior specified in an architecture description. Also we looked at how one might prove that a network of logic primitives behaves as a higher level description requires. In both cases we found that the techniques of program verification do apply in a straightforward manner, particularly the notion of symbolic execution and Milner's method of proving simulation [6]. But as new semantic concepts are used in the descriptive languages, additional theories are required to simplify the symbolic expressions and to prove the theorems that arise.