Department of Computer Science and Technology

Technical reports

Femto-VHDL:
the semantics of a subset of VHDL and its embedding in the HOL proof assistant

John Peter Van Tassel

November 1993, 122 pages

This technical report is based on a dissertation submitted July 1993 by the author for the degree of Doctor of Philosophy to the University of Cambridge, Gonville & Caius College.

DOI: 10.48456/tr-317

Abstract

The design of digital devices now resembles traditional computer programming. Components are specified in a specialised form of programming language known as a Hardware Description Language. Programs written in such languages are then executed to simulate the behaviour of the hardware they describe. These simulations cannot be exhaustive in most situations, so result in high, yet incomplete, confidence that the proper behaviour has been achieved.

The formal analysis of programming languages provides ways of mathematically proving properties of programs. These properties apply to behaviours resulting from all possible inputs rather then just a subset of them. The prerequisite for such an analysis is a formal understanding of the semantics of the language.

The Very High Speed Hardware Description Language (VHDL) is currently used to specify and simulate a wide range of digital devices. The language has no formal mathematical semantics as part of its definition, hence programs written in it have not been amenable to formal analysis.

The work presented here defines a structural operational semantics for a subset of VHDL. The semantics is then embedded in a mechanical proof assistant. This mechanisation allows one not only to reason about individual programs but also to express equivalences between programs. Examples which highlight the methodology used in this reasoning are provided as a series of case studies.

Full text

PDF (7.3 MB)

BibTeX record

@TechReport{UCAM-CL-TR-317,
  author =	 {Van Tassel, John Peter},
  title = 	 {{Femto-VHDL: the semantics of a subset of VHDL and its
         	   embedding in the HOL proof assistant}},
  year = 	 1993,
  month = 	 nov,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-317.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-317},
  number = 	 {UCAM-CL-TR-317}
}