Technical reports

Formalising an integrated circuit design style in higher order logic

Inderpreet-Singh Dhingra

November 1988, 195 pages

This technical report is based on a dissertation submitted March 1988 by the author for the degree of Doctor of Philosophy to the University of Cambridge, King’s College.

DOI: 10.48456/tr-151

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 from experience. These rules of thumb are guidelines for deciding which 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 fomulated. These statements are based on a small number of definitions which define the behaviour of transistors and capacitors and the necessary axiomisation 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 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 gigital 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.

Full text

PDF (9.0 MB)

BibTeX record

@TechReport{UCAM-CL-TR-151,
  author =	 {Dhingra, Inderpreet-Singh},
  title = 	 {{Formalising an integrated circuit design style in higher
         	   order logic}},
  year = 	 1988,
  month = 	 nov,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-151.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-151},
  number = 	 {UCAM-CL-TR-151}
}