Proving a Computer Correct with the LCF_LSM Hardware Verification System

From bibtex.

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, an ALU, a memory, and a microcode controller. This controller consists of a ROM holding 26 30-bit microinstructions, a microprogram counter, and some combinational 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 manipulation 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.