Computer Laboratory

Technical reports

A HOL semantics for a subset of ELLA

Richard J. Boulton

April 1992, 104 pages

Abstract

Formal verification is an important tool in the design of computer systems, especially when the systems are safety or security critical. However, the formal techniques currently available are not well integrated into the set of tools more traditionally used by designers. This work is aimed at improving the integration by providing a formal semantics for a subset of the hardware description language ELLA, and by supporting this semantics in the HOL theorem proving system, which has been used extensively for hardware verification.

A semantics for a subset of ELLA is described, and an outline of a proof of the equivalence of parallel and recursive implementations of an n-bit adder is given as an illustration of the semantics. The proof has been performed in an extension of the HOL system. Some proof tools written to support the verification are also described.

Full text

DVI (0.1 MB)

BibTeX record

@TechReport{UCAM-CL-TR-254,
  author =	 {Boulton, Richard J.},
  title = 	 {{A HOL semantics for a subset of ELLA}},
  year = 	 1992,
  month = 	 apr,
  url = 	 {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-254.dvi.gz},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-254}
}