Skip to main content
SpringerLink
Log in
Book cover

Designing Correct Circuits

Workshop jointly organised by the Universities of Oxford and Glasgow, 26–28 September 1990, Oxford

  • Conference proceedings
  • © 1991

Overview

Editors:
  1. Geraint Jones

    1. Oxford University Computing Laboratory, Oxford, England

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Mary Sheeran

    1. Department of Computing Science, University of Glasgow, Glasgow, Scotland

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

Part of the book series: Workshops in Computing (WORKSHOPS COMP.)

This is a preview of subscription content, log in via an institution to check access.

Access this book

Log in via an institution
eBook USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

Licence this eBook for your library

Institutional subscriptions

Table of contents (18 papers)

  1. Front Matter

    Pages i-viii
    Download chapter 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
    Download chapter PDF
Back to top

Keywords

About this book

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.

Editors and Affiliations

  • Oxford University Computing Laboratory, Oxford, England

    Geraint Jones

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

    Mary Sheeran

Bibliographic Information

  • Book Title: Designing Correct Circuits

  • Book Subtitle: Workshop jointly organised by the Universities of Oxford and Glasgow, 26–28 September 1990, Oxford

  • Editors: Geraint Jones, Mary Sheeran

  • Series Title: Workshops in Computing

  • DOI: https://doi.org/10.1007/978-1-4471-3544-9

  • Publisher: Springer London

  • eBook Packages: Springer Book Archive

  • Copyright Information: Springer-Verlag London 1991

  • Softcover ISBN: 978-3-540-19659-4Published: 30 April 1991

  • eBook ISBN: 978-1-4471-3544-9Published: 14 December 2013

  • Series ISSN: 1431-1682

  • Edition Number: 1

  • Number of Pages: VIII, 355

  • Number of Illustrations: 6 b/w illustrations

  • Additional Information: Jointly published with the British Computer Society

  • Topics: Artificial Intelligence, Processor Architectures, Mathematical Logic and Formal Languages

Publish with us

Policies and ethics

Back to top

Search

Navigation