Skip to main content
SpringerLink
Log in
Book cover

VLSI Specification, Verification and Synthesis

  • Book
  • © 1988

Overview

Editors:
  1. Graham Birtwistle

    1. University of Calgary, Canada

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. P. A. Subrahmanyam

    1. AT&T Bell Laboratories, USA

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 109.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 (13 chapters)

  1. Front Matter

    Pages i-xi
    Download chapter PDF

  2. Implementing Safety-Critical Systems: The VIPER Microprocessor

    • W. J. Cullyer
    Pages 1-25

  3. A Proof of Correctness of the Viper Microprocessor: The First Level

    • Avra Cohn
    Pages 27-71

  4. HOL: A Proof Generating System for Higher-Order Logic

    • Michael J. C. Gordon
    Pages 73-128

  5. Formal Verification and Implementation of a Microprocessor

    • Jeffrey J. Joyce
    Pages 129-157

  6. Towards a framework for dealing with system timing in Very High Level Silicon Compilers

    • P. A. Subrahmanyam
    Pages 159-215

  7. BIDS: A Method for Specifying and Verifying Bidirectional Hardware Devices

    • David R. Musser, Paliath Narendran, William J. Premerlani
    Pages 217-233

  8. Hardware Verification in the Interactive VHDL Workstation

    • Paliath Narendran, Jonathan Stillman
    Pages 235-255

  9. Contextual Constraints for Design and Verification

    • Bruce S. Davie, George J. Milne
    Pages 257-265

  10. Abstraction Mechanisms for Hardware Verification

    • Thomas F. Melham
    Pages 267-291

  11. Formal Validation of an Integrated Circuit Design Style

    • I. S. Dhingra
    Pages 293-321

  12. A Compositional Model of MOS Circuits

    • Glynn Winskel
    Pages 323-347

  13. A Tactical Framework for Hardware Design

    • Steven D. Johnson, Bhaskar Bose, C. David Boyer
    Pages 349-383

  14. Verification of Asynchronous Circuits: Behaviors, Constraints and Specifications

    • C. Berthet, E. Cerny
    Pages 385-404
Back to top

Keywords

About this book

VLSI Specification, Verification and Synthesis Proceedings of a workshop held in Calgary from 12-16 January 1987. The collection of papers in this book represents some of the discussions and presentations at a workshop on hardware verification held in Calgary, January 12-16 1987. The thrust of the workshop was to give the floor to a few leading researchers involved in the use of formal approaches to VLSI design, and provide them ample time to develop not only their latest ideas but also the evolution of these ideas. In contrast to simulation, where the objective is to assist in detecting errors in system behavior in the case of some selected inputs, the intent of hardware verification is to formally prove that a chip design meets a specification of its intended behavior (for all acceptable inputs). There are several important applications where formal verification of designs may be argued to be cost-effective. Examples include hardware components used in "safety critical" applications such as flight control, industrial plants, and medical life-support systems (such as pacemakers). The problems are of such magnitude in certain defense applications that the UK Ministry of Defense feels it cannot rely on commercial chips and has embarked on a program of producing formally verified chips to its own specification. Hospital, civil aviation, and transport boards in the UK will also use these chips. A second application domain for verification is afforded by industry where specific chips may be used in high volume or be remotely placed.

Editors and Affiliations

  • University of Calgary, Canada

    Graham Birtwistle

  • AT&T Bell Laboratories, USA

    P. A. Subrahmanyam

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation