NASA Contractor Report 189588 Mechanically Verified Hardware Implementing an 8-Bit Parallel IO Byzantine Agreement Processor

Consider a network of four processors that use the Oral Messages (Byzantine Generals) algorithm of Pease, Shostak and Lamport to achieve agreement in the presence of faults. Bevier and Young have published a functional description of a single processor that, when interconnected appropriately with three identical others, implements this network under the assumption that the four processors step in synchrony. By formalizing the original Pease, Shostak and Lamport work, Bevier and Young mechanically proved that such a network achieves fault tolerance. In this paper we develop, formalize and discuss a hardware design that has been mechanically proved to implement their processor. In particular, we formally define mapping functions from the abstract state space of the Bevier-Young processor to a concrete state space of a hardware module and state a theorem that expresses the claim that the hardware correctly implements the processor. We briefly discuss the Brock-Hunt Formal Hardware Description Language which permits designs both to be proved correct with the Boyer-Moore theorem prover and to be expressed in a commercially supported hardware description language for additional electrical analysis and layout. We briefly describe our implementation, which actually takes the form of a hardware design generator which produces a design as a function of the desired word size. We exhibit the theorem that establishes that the generator is correct. We exhibit the instance generated for sense data of width 8, in the syntax of NDL, a hardware description language supported by LSI Logic, Inc. We exhibit some results of processing the verified design with commercially available tools. We discuss two unrealistic aspects of our verified design. (a) The use of parallel instead of serial io requires an excessive number of pins. (b) The assumption that all four processors step in synchrony is implemented by having them share a common clock — introducing an unacceptable single-point failure mode