Formalization and Verification of Computer System Interconnect Busses

University Of Utah, Salt Lake City UT

Investigators

Abstract

ABSTRACT To overcome the limitations of current design verification methods for computer interconnect busses, this project explores application-specific heuristics that can significantly reduce the amount of fresh intellectual effort needed in verification. These heuristics are supported by a suitable integration of deductive and algorithmic methods. Separate application of deductive and algorithmic methods to verification results in either inordinate human effort or inadequate coverage due to ad hoc abstractions. This project addresses coverage by formally verifying the adequacy of abstractions using a deductive theorem prover. It reduces proof effort by carrying out much of the reasoning using automated finite-state model-checking. These ideas are explored in the context of bus-bridge connected I/O systems and distributed shared memory systems, with verified properties including transaction orderings and formal memory models, and with case studies drawn from commercial I/O bus standards and commercial shared memory systems.