Skip to main content
SpringerLink
Log in

Hardware Specification, Verification and Synthesis: Mathematical Aspects

Mathematical Sciences Institute Workshop. Cornell University Ithaca, New York, USA. July 5-7, 1989. Proceedings

  • Conference proceedings
  • © 1990

Overview

Editors:
  1. Miriam Leeser
    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Geoffrey Brown
    View editor publications

    You can also search for this editor in PubMed   Google Scholar

Part of the book series: Lecture Notes in Computer Science (LNCS, volume 408)

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

Access this book

Log in via an institution
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 (19 papers)

  1. Front Matter

    Download chapter PDF

  2. Design for verifiability

    • George J. Milne
    Pages 1-13

  3. Verification of synchronous circuits by symbolic logic simulation

    • Randal E. Bryant
    Pages 14-24

  4. Constraints, abstraction, and verification

    • Daniel Weise
    Pages 25-39

  5. Formalising the design of an SECD chip

    • Brian Graham, Graham Birtwistle
    Pages 40-66

  6. Reasoning about state machines in higher-order logic

    • Paul Loewenstein
    Pages 67-89

  7. A mechanically derived systolic implementation of pyramid initialization

    • Christian Lengauer, Bikash Sabata, Farshid Arman
    Pages 90-105

  8. Behavior-preserving transformations for high-level synthesis

    • R. Camposano
    Pages 106-128

  9. From programs to transistors: Verifying hardware synthesis tools

    • Geoffrey M. Brown, Miriam E. Leeser
    Pages 129-151

  10. Combining engineering vigor with mathematical rigor

    • Shiu-Kai Chin
    Pages 152-176

  11. Totally verified systems: Linking verified software to verified hardware

    • Jeffrey J. Joyce
    Pages 177-201

  12. What's in a timing discipline? Considerations in the specification and synthesis of systems with interacting asynchronous and synchronous components

    • P. A. Subrahmanyam
    Pages 202-223

  13. Complete trace structures

    • David L. Dill
    Pages 224-243

  14. The design of a delay-insensitive microprocessor: An example of circuit synthesis by program transformation

    • Alain J. Martin
    Pages 244-259

  15. Manipulating logical organization with system factorizations

    • Steven D. Johnson
    Pages 260-281

  16. The verification of a bit-slice ALU

    • Warren A. Hunt Jr., Bishop C. Brock
    Pages 282-306

  17. Verification of a pipelined microprocessor using clio

    • Mark Bickford, Mandayam Srivas
    Pages 307-332

  18. Verification of combinational logic in Nuprl

    • David A. Basin, Peter Del Vecchio
    Pages 333-357

  19. Veritas+: A specification language based on type theory

    • F K Hanna, N Daeche, M Longley
    Pages 358-379

  20. Categories for the working hardware designer

    • Mary Sheeran
    Pages 380-402
Back to top

Keywords

About this book

Current research into formal methods for hardware design is presented in the papers in this volume. Because of the complexity of VLSI circuits, assuring design validity before circuits are manufactured is imperative. The goal of research in this area is to develop methods of improving the design process and the quality of the resulting designs. The major trend apparent at the workshop is that researchers are rapidly moving away from post hoc proof techniques with their great expense. A number of papers were presented that dealt with problems of synthesizing correct circuits and of designing with the goal of verification. Researchers are also beginning to deal with the theoretical issues of reasoning about concurrent systems and asynchronous systems, and to introduce new logical tools such as constructive type theory and category theory. Most of the research reported was performed in the United States.

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation