Refining Specifications to Programmable Logic

Hilton, Adrian and Hall, Jon G. (2002). Refining Specifications to Programmable Logic. Technical Report 2002/06; Department of Computing, The Open University.



Combined hardware/software systems are increasingly being used for safety-critical systems, with hardware taking processing load off the software. To attain the necessary safety integrity levels, new safety standards require that the correctness arguments for safety-critical hardware and software are developed together with the same rigour as for software alone.In this paper we describe work in progress on the continuing development of such a notation and proof system. Based on process description using Synchronous Receptive Proof Theory, we propose refinement rules for developing a specification into an SRPT implementation. As illustration, we demonstrate the full formal refinement of a 2k bit carry look-ahead adder into a Pebble implementation, and test the implementation.

Viewing alternatives

Download history


Public Attention

Altmetrics from Altmetric

Number of Citations

Citations from Dimensions

Item Actions