Technical reports

Relating two models of hardware

Glynn Winskel

July 1987, 16 pages

DOI: 10.48456/tr-110

Abstract

The idea of this note is to show how Winskel’s static-configuration model of circuits is related formally to Gordon’s relational model. Once so related, the simpler proofs in the relational model can, for instance, be used to justify results in terms of the static-configurations model. More importantly, we can exhibit general conditions on circuits which ensure that assertions which hold of a circuit according to the simpler model are correct with respect to the more accurate model. The formal translation makes use of a simple adjunction between (partial order) categories associated with the two models, in a way reminiscient of abstract interpretation. Preliminary results suggest similar lines of approach may work for other kinds of abstraction such as temporal abstraction used in e.g. Melham’s work to reason about hardware, and, more generally, make possible a formal algebraic treatment of the relationship between different models of hardware.

Full text

PDF (0.8 MB)

BibTeX record

@TechReport{UCAM-CL-TR-110,
  author =	 {Winskel, Glynn},
  title = 	 {{Relating two models of hardware}},
  year = 	 1987,
  month = 	 jul,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-110.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-110},
  number = 	 {UCAM-CL-TR-110}
}