Department of Computer Science and Technology

Technical reports

Proving a computer correct with the LCF_LSM hardware verification system

Mike Gordon

September 1983, 49 pages

Abstract

A machine generated correctness proof of a simple computer is described.

At the machine code level the computer has a memory and two registers: a 13 bit program counter and a 16-bit accumulator. There are 8 machine instructions: halt, unconditional jump, jump when the accumulator contains 0, add contents of a memory location to accumulator, subtract contents of a location from accumulator, load accumulator from memory, store contents of accumulator in memory, and skip. The machine can be interrupted by pushing a button on its front panel.

The implementation which we prove correct has 6 data registers, and ALU, a memory, and a microcode controller. The controller consists of a ROM holding 26 30-bit microinstructions, a microprogram counter, and some combinatorial microinstruction decode logic.

Formal specifications of the target and host machines are given, and we describe the main steps in proving that the host correctly fetches, decodes and executes machine instructions.

The utility of LCF_LSM for general manipulaton is illustrated in two appendices. In appendix 1 we show how to code a microassembler. In appendix 2 we use the LCF_LSM inference rules to design a hard-wired controller equivalent to the original microcoded one.

N.B. This report should be read in conjunction with LCF_LSM: A system for specifying and verifying hardware. University of Cambridge, Computer Laboratory technical report number 41.

Full text

PDF (2.1 MB)

BibTeX record

@TechReport{UCAM-CL-TR-42,
  author =	 {Gordon, Mike},
  title = 	 {{Proving a computer correct with the LCF\_LSM hardware
         	   verification system}},
  year = 	 1983,
  month = 	 sep,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-42.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-42}
}