Formalizing abstraction mechanisms for hardware verification in higher order logic

From bibtex.

Abstract

Recent advances in microelectronics have given designers of digital hardware the potential to build devices of remarkable size and complexity. Along with this however, it becomes increasingly difficult to ensure that such systems are free from design errors, where complete simulation of even moderately sized circuits is impossible. One solution to these problems is that of hardware verification, where the functional behaviour of the hardware is described mathematically and formal proof is used to show that the design meets rigorous specifications of the intended operation. This dissertation therefore seeks to develop this, showing how reasoning about the correctness of hardware using formal proof can be achieved using fundamental abstraction mechanisms to relate specifications of hardware at different levels. Therefore a systematic method is described for defining any instance of a wide class of concrete data types in higher order logic. This process has been automated in the HOL theorem prover, and provides a firm logical basis for representing data in formal specifications. Further, these abstractions have been developed into a new technique for modelling the behaviour of entire classes of hardware designs. This is based on a formal representation in logic for the structure of circuit designs using the recursive types defined by the above method. Two detailed examples are presented showing how this work can be applied in practice. Finally, some techniques for temporal abstraction are explained, and the means for asserting the correctness of a model containing time-dependent behaviour is described. This work is then illustrated using a case study; the formal verification on HOL of a simple ring communication network. [Abstract by Nicholas Cutler (librarian), as none was submitted with the report.]