A methodology for the formal verification of composed hardware systems
E. Thomas Schubert · 1992
With increasing frequency, computers are being used in applications where failure can lead to loss of life or serious loss of property. To gain greater confidence in a system design, formal verification has been proposed as a complement to testing. Through mathematical proof, formal verification can demonstrate that a design satisfies a specification. This dissertation presents a framework to formally specify and verify the correctness of the communication between the hardware devices that make up a computer system. This approach is formalized within the HOL theorem proving system. Previous approaches to formal verification have decomposed systems into several hardware and software layers that may be independently verified. However, the hardware layer specifications have consisted of single CPU devices, and have not been representative of modern hardware implementations. To be more reflective of modern architectures, we present a correctness proof for a memory management unit. The methodology presented in this dissertation, allows a hardware system to be decomposed into a set of independently verified devices and provides a logic to specify and reason about the composed, aggregate system behavior. To formally specify and reason about composed systems, a process algebra is developed that integrates an extended interpreter model. This approach utilizes the interpreter model for device decomposition, while also being able to reason about larger systems that require interdevice communication. By combining these approaches, convenient notations are available to specify and verify both device independent properties (e.g., instruction sets) and device interdependent properties (e.g., communication protocols). Using the process algebra formalization, four types of device interactions (remote procedure call, message passing, process creation, and rendezvous) are represented and their interaction verified to behave as specified. A system with concurrently executing devices is presented and verified to correctly pass information and coordinate activities. The system consists of a CPU, a memory subsystem with a memory management unit, a direct memory access device, and a bus controller. This work can be applied to the verification of devices with concurrent components (e.g., pipelines, multiple functional unit processing units, or superscaler architectures). This work can also be applied to the verification of embedded system software.