Designing Correct Circuits

1. Front Matter

   Pages i-viii

   PDF

2. Constrained Proofs: A Logic for Dealing with Behavioural Constraints in Formal Hardware Verification

   • Michael Mendler

   Pages 1-28

3. Hardware synthesis in constructive type theory

   • Dany Suk

   Pages 29-49

4. An Algebraic Framework for Data Abstraction in Hardware Description

   • Zheng Zhu, Steven D. Johnson

   Pages 50-67

5. Generic Specification of Digital Hardware

   • Jeffrey J. Joyce

   Pages 68-91

6. Sampling and Proof: A Half-Case Study

   • John Hughes

   Pages 92-98

7. High Level Test Generation via Process Composition

   • Venkatesh Akella, Ganesh Gopalakrishnan

   Pages 99-119

8. Towards Truly Delay-Insensitive Circuit Realizations of Process Algebras

   • Geoffrey M. Brown

   Pages 120-131

9. The Design of a Delay-Insensitive Stack

   • Mark B. Josephs, Jan Tijmen Udding

   Pages 132-152

10. Specifying the Micro-program Parallelism for Microprocessors of the Von Neumann style

    • Hélène Collavizza, Dominique Borrione

    Pages 153-170

11. The Implementation and Proof of a Boolean Simplification System

    • Mark Aagaard, Miriam Leeser

    Pages 171-195

12. A Model for Synchronous Switching Circuits and its Theory of Correctness

    • Zhou Chaochen, C. A. R. Hoare

    Pages 196-211

13. Efficient Circuits as Implementations of Non-Strict Functions

    • Carlos Delgado Kloos, Walter Dosch

    Pages 212-230

14. Verification of Synchronous Concurrent Algorithms Using OBJ3: A Case Study of the Pixel-Planes Architecture

    • S. M. Eker, V. Stavridou, J. V. Tucker

    Pages 231-252

15. Use of the OTTER theorem prover for the formal verification of hardware

    • Paolo Camurati, Tiziana Margaria, Paolo Prinetto

    Pages 253-270

16. Proof-based transformation of formal hardware models

    • Holger Busch

    Pages 271-296

17. Ruby algebra

    • Lars Rossen

    Pages 297-312

18. Using the Declarative Language LUSTRE for Circuit Verification

    • Ghislaine Thuau, Daniel Pilaud

    Pages 313-331

19. Optimising designs by transposition

    • Wayne Luk

    Pages 332-354

20. Back Matter

    Pages 355-355

    PDF

These proceedings contain the papers presented at a workshop on Designing Correct Circuits, jointly organised by the Universities of Oxford and Glasgow, and held in Oxford on 26-28 September 1990. There is a growing interest in the application to hardware design of the techniques of software engineering. As the complexity of hardware systems grows, and as the cost both in money and time of making design errors becomes more apparent, so there is an eagerness to build on the success of mathematical techniques in program develop­ ment. The harsher constraints on hardware designers mean both that there is a greater need for good abstractions and rigorous assurances of the trustworthyness of designs, and also that there is greater reason to expect that these benefits can be realised. The papers presented at this workshop consider the application of mathematics to hardware design at several different levels of abstraction. At the lowest level of this spectrum, Zhou and Hoare show how to describe and reason about synchronous switching circuits using UNilY, a formalism that was developed for reasoning about parallel programs. Aagaard and Leeser use standard mathematical tech­ niques to prove correct their implementation of an algorithm for Boolean simplification. The circuits generated by their formal synthesis system are thus correct by construction. Thuau and Pilaud show how the declarative language LUSTRE, which was designed for program­ ming real-time systems, can be used to specify synchronous circuits.

• Digital systems
• Formal methods
• Hardware
• Mathematica
• Specification driven design
• algebra
• algorithms
• complexity
• formal method
• formal verification
• mathematics
• parallelism
• process algebra
• processor
• verification

• Oxford University Computing Laboratory, Oxford, England

  Geraint Jones

• Department of Computing Science, University of Glasgow, Glasgow, Scotland

  Mary Sheeran

Policies and ethics