Technical reports

The HOL verification of ELLA designs

Richard Boulton, Mike Gordon, John Herbert, John Van Tassel

August 1990, 22 pages

DOI: 10.48456/tr-199

Abstract

HOL is a public domain system for generating proofs in higher order predicate calculus. It has been in experimental and commercial use in several countries for a number of years.

ELLA is a hardware design language developed at the Royal Signals and Radar Establishment (RSRE) and marketed by Computer General Electronic Design. It supports simulation models at a variety of different abstraction levels.

A preliminary methodology for reasoning about ELLA designs using HOL is described. Our approach is to semantically embed a subset of the ELLA language in higher order logic, and then to make this embedding convenient to use with parsers and pretty-printers. There are a number of semantic issues that may affect the ease of verification. We discuss some of these briefly. We also give a simple example to illustrate the methodology.

Full text

PS (0.1 MB)

BibTeX record

@TechReport{UCAM-CL-TR-199,
  author =	 {Boulton, Richard and Gordon, Mike and Herbert, John and Van
          	  Tassel, John},
  title = 	 {{The HOL verification of ELLA designs}},
  year = 	 1990,
  month = 	 aug,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-199.ps.gz},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-199},
  number = 	 {UCAM-CL-TR-199}
}