The HOL Verification of ELLA Designs1
Richard Boulton, Mike Gordon, John Herbert, John Van Tassel
University of Cambridge Computer Laboratory
New Museums Site
Cambridge CB2 3QG
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.
ELLA2 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.
1Presented at the International Workshop on Formal Methods in VLSI Design, Miami, January
2ELLA is a registered trademark of the Secretary of State for Defence, UK.