A model of register transfer systems with applications to microcode and VLSI correctness
Gordon, MJC · Apollo (University of Cambridge) · 1982
In this paper we describe and illustrate a simple semantic model of register transfer systems — i.e. systems built by connecting together storage devices like registers and.memories via combinational circuits like gates and arithmetic units. The goal is to develop an elegant and efficient framework in which to conduct correctness proofs. After explaining the model we illustrate our methods by presenting two case studies. In the first of these we completely specify a small general purpose computer, and then prove correct a microcoded implementation. This involves showing that the signals generated by the microprogrammed controller cause register transfers in the host which correctly fetch, decode and execute machine instructions; and also that the control unit correctly interprets and sequences microinstructions according to the microcode semantics. In the second case study we go down a level and verify nMOS implementations of devices like those used to build the computer. Starting from four primitives — gates, joins, pullups and ground — we first implement and verify not and nor elements. Using these we then specify, implement and verify a stackcell and controller taken from.Mead and Conway's book "Introduction to VLSI Systems". In both case studies the proofs are highly structured. For example, in the nMOS study the stack controller is expressed as the composition of two subsystems and a clock, and its correctness follows from the correctness of the subsystems; the correctness of these, in turn, follows from the correctness of their immediate constituents (not and nor elements). It is not necessary to flatten down to the gate level and hence proofs do not explode in size.