As hardware systems are becoming bigger and more complex, it is becoming
increasingly harder to design and reason about these systems in a monolithic
fashion. While hardware is often designed in a modular manner, its verification
is rarely performed modularly. Moreover, any modular refinement to an existing
system requires a full system verification to guarantee correctness, even if
only a few components of the system has been refined.
In this thesis, we present a new framework for modular verification of hardware
designs written in the Bluespec language. That is, we formalize the idea of
components in a hardware design, with well-defined input and output channels;
and we show how to specify and verify components individually. For verifying a
full system, we show how the proofs can be composed when composing the
corresponding components, treating the components as black-boxes and not
looking beyond the specification of the components.
As a demonstration of this methodology, we verify a fairly realistic
implementation of a multicore shared-memory system with two types of
components: memory system and processor, with machine-checked proofs in the Coq
proof assistant. Both components include nontrivial optimizations, with the
memory system employing an arbitrary hierarchy of cache nodes that communicate
with each other concurrently, and with the processor doing speculative
execution of many concurrent read operations. Nonetheless, we prove that the
combined system implements sequential consistency. To our knowledge, our
memory-system proof is the first machine verification of a cache-coherence
protocol parameterized over an arbitrary cache hierarchy, and our full-system
proof is the first machine verification of sequential consistency for a
multicore hardware design that includes caches and speculative processors.
We also embed the Bluespec language in the Coq proof assistant and formalize
its modular semantics, enabling a verification engineer to obtain
machine-checked proofs for Bluespec designs using our framework.
Thesis Supervisors: Profs. Arvind and Chlipala