Formalising an integrated circuit design style in higher order logic

From bibtex.

Abstract

If the activities of an integrated circuit designer are examined, we find that rather than keeping track of all the details, he uses simple rules of thumb which have been refined with experience. These rules of thumb are guidelines for deciding which building blocks to use and how they are to be connected. This thesis gives a formal foundation, in higher order logic, to the design rules of a dynamic CMOS integrated circuit design style. Correctness statements for the library of basic elements are formulated. These statements are based on a small number of definitions which define the behaviour of transistors and capacitors and the necessary axiomatisation of the four-valued algebra for signals. The correctness statements of large and complex circuits are then derived from the library of previously proved correctness statements, using logical inference rules instead of the rules of thumb. For example, one gate from the library can drive another only if its output constraints are satisfied by the input constraints of the gate that it drives. In formalising the design rules, these constraints are captured as predicates and are part of the correctness statements of these gates. So when two gates are to be connected, it is only necessary to check that the predicates match. These ideas are fairly general and widely applicable for formalising the rules of many systems. A number of worked examples are presented based on these formal techniques. Proofs are presented at various stages of development to show how the correctness statement for a device evolves and how the proof is constructed. In particular it is demonstrated how such formal techniques can help improve and sharpen the final specifications. As a major case study to test all these techniques, a new design for a digital phase-locked loop is presented. This has been designed down to the gate level using the above dynamic design style, and has been described and simulated using ELLA. Some of the subcomponents have been formally verified down to the detailed circuit level while others have merely been specified without formal proofs of correctness. An informal proof of correctness of this device is also presented based on the formal specifications of the various submodules.