The HOL Verification of ELLA Designs1

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

University of Cambridge Computer Laboratory

New Museums Site

Pembroke Street

Cambridge CB2 3QG

United Kingdom

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.

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 1991.
2ELLA is a registered trademark of the Secretary of State for Defence, UK.