Computer Laboratory

Technical reports

A mechanised definition of Silage in HOL

Andrew D. Gordon

February 1993, 28 pages

Abstract

If formal methods of hardware verification are to have any impact on the practices of working engineers, connections must be made between the languages used in practice to design circuits, and those used for research into hardware verification. Silage is a simple dataflow language marketed for specifying digital signal processing circuits. Higher Order Logic (HOL) is extensively used for research into hardware verification. This paper presents a formal definition of a substantial subset of Silage, by mapping Silage declarations into HOL predicates. The definition has been mechanised in the HOL theorem prover to support the transformational design of Silage circuits as theorem proving in HOL.

Full text

DVI (0.0 MB)

BibTeX record

@TechReport{UCAM-CL-TR-287,
  author =	 {Gordon, Andrew D.},
  title = 	 {{A mechanised definition of Silage in HOL}},
  year = 	 1993,
  month = 	 feb,
  url = 	 {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-287.dvi.gz},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-287}
}