Department of Computer Science and Technology

Technical reports

Formal verification of basic memory devices

John Herbert

February 1988, 46 pages

DOI: 10.48456/tr-124

Abstract

Formal methods have been used recently to verify high-level functional specifications of digital systems. Such formal proofs have used simple models of circuit components. In this article we describe complementary work which uses a more detailed model of components and demonstrates how hardware can be specified and verified at this level.

In this model all circuits can be described as structures of gates, each gate having an independent propagation delay. The behaviour of digital signals in real time is captured closely. The function and timing of asynchronous and synchronous memory elements implemented using gates is derived. Formal proofs of correctness show that, subject to certain constraints on gate delays and signal timing parameters, these devices act as memory elements and exhibit certain timing properties.

All the proofs have been mechanically generated using Gordon’s HOL system.

Full text

PDF (1.6 MB)

BibTeX record

@TechReport{UCAM-CL-TR-124,
  author =	 {Herbert, John},
  title = 	 {{Formal verification of basic memory devices}},
  year = 	 1988,
  month = 	 feb,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-124.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-124},
  number = 	 {UCAM-CL-TR-124}
}