Abstract

MLP is a functional theory of synchronous circuit computation, built to support formal reasoning about sequential hardware. MLP comprises precise model-theoretic semantics based on string-functions and a mechanization of the theory inside the Boyer-Moore theorem-prover. The motivation is that current validation methods are expensive, not very reliable, and less and less able to cope with increasingly complex circuits. In contrast, formal methods combined with the leverage of mathematical reasoning, offer hopes of better verification and, some day, transformational design to guarantee correctness. ;Formal design methods require a formal underlying semantics. Therefore we propose a new semantics for synchronous circuits based on Monotonic Length-Preserving functions on finite strings, inspired by history-functional work in concurrent software. Our string theory is defined relative to an arbitrary algebra for combinational components, allowing reasoning at a high abstraction level as easily as at the boolean level. To prove the existence of the needed mathematical objects, we build Scott-style domains of finite strings, and of monotonic length-preserving string-functions. We validate all constructions from the foundations. Moreover, we prove the equivalence of the extensional semantics with a simple operational semantics, and a characterization of circuits that obey the "every loop is clocked" rule. ;For hardware design to benefit from this work, mechanical tools are required. Therefore we mechanized a first-order fragment of MLP inside the Boyer-Moore theorem-prover, and wrote a Lisp preprocessor which performs some second-order reasoning by generating Boyer-Moore lemmas from circuit descriptions. Our goals were soundness and usability/generality. For soundness we do not add axioms to Boyer-Moore, but instead use one "shell" followed by definitions and lemmas. For generality, we use a layered methodology that separates circuit dependent and independent facts, and maximizes the latter. Within this system, we prove correctness properties for several synchronous designs, including a circuit reasoning benchmark: "The 7 Paillet circuits" with very few lemmas per circuit. We also formalize two forms of pipelining, and prove correctness of the Saxe-Leiserson retimed correlator, a pipelined ripple adder, and an abstract pipelined CPU