Technical reports

A structured approach to the verification of low level microcode

Paul Curzon

265 pages

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

DOI: 10.48456/tr-215

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 microcode is supplied. Some demand that it be written in a high level microprogramming language. Conventional software verification techniques are then applied. 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 modelled 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 it is transformed by the system to a high level program which may 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.

Full text

PDF (12.0 MB)

BibTeX record

@TechReport{UCAM-CL-TR-215,
  author =	 {Curzon, Paul},
  title = 	 {{A structured approach to the verification of low level
         	   microcode}},
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-215.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-215},
  number = 	 {UCAM-CL-TR-215}
}