A Structured Approach to the Verification of Low Level Microcode

Paul Curzon. Technical Report Number 215, University of Cambridge Computer Laboratory, February 1991. PhD Thesis.

Abstract

Errors in microprograms are especially serious since all higher level programs on the machine depend on the microcode. Formal verification presents one avenue which may be used to discover such errors. Previous systems which have been used for formally verifying microcode may be categorised by the form in which the microprogram is supplied. Some demand that it be written in a high level microprogramming language. Conventional software verification techniques are then employed. Other methods allow the microcode to be supplied in the form of a memory image. It is treated as data to an interpreter modelling the behaviour of the microarchitecture. The proof is then performed by symbolic execution. A third solution is for the code to be supplied in an assembly language and verified at that level. The assembler instructions are converted to commands in a modelling language. The resulting program is verified using traditional software verification techniques.

In this dissertation, I present a new universal microprogram verification system. It achieves many of the advantages of the other kinds of systems by adopting a hybrid approach. The microcode is supplied as a memory image, but is transformed by the system to a high level program which may then be verified using standard software verification techniques. The structure of the high level program is obtained from user supplied documentation. I show that this allows microcode to be split into small, independently validatable portions even when it was not written in that way. I also demonstrate that the techniques allow the complexity of detail due to the underlying microarchitecture to be controlled at an early stage in the validation process. I suggest that the system described would combine well with other validation tools and provide help throughout the firmware development cycle. Two case studies are given. The first describes the verification of Gordon's computer. This example, being fairly simple, provides a good illustration of the techniques used by the system. The second case study is concerned with the High Level Hardware Orion computer which is a commercially produced machine with a fairly complex microarchitecture. This example shows that the techniques scale well to production microarchitectures.

Obtaining the paper

A hard copy of this paper can be ordered via ...

Email: tech_reports@cl.cam.ac.uk

Phone: +44 1223 334648

Bibtex Entry


@TechReport{Curzon91THESIS,

  author = 	"Paul Curzon",

  title = 	"A Structured Approach to the Verification

		 of Low Level Microcode",

  institution = "University of Cambridge, Computer Laboratory",

  year = 	"1991",

  number = 	"215",

  month = 	feb,

  note =	"PhD Thesis"

}