From Hardware Description Languages Descriptions to Guaranteed Correct Circuit Designs: Conference Proceedings

The objective of this book is to bring together the knowledge of developers and users of design automation tools, and compare the methods and algorithms by which correct circuit designs may be obtained from initial descriptions and specifications written in an appropriate hardware description language (HDL). In order to achieve the goal of designing correct circuits, two main directions of research are currently being pursued: formal verification of a (possibly manual) design, and automatic synthesis. Both approaches require that a high level specification of the circuit be given in a formal language, and an underlying model of hardware behaviour is necessary to allow for symbolic translations that preserve or verify some notion of correctness. Hardware models, formal proof of correctness, and synthesis are therefore the three key elements making up this volume.

Table of Contents:
Proof Oriented Hardware Models. The Role of Behaviour in VLSI Design Languages (B.S. Davie, G.J. Milne). A Functional Model for Descriptions and Specifications of Digital Devices (J.-L. Paillet). Hardware Verification Using Higher-Order Logic (A. Camilleri, M. Gordon, T. Melham). Describing and Designing Circuits by means of a Synchronous Declarative Language (N. Halbwachs, A. Lonchampt, D. Pilaud). SML - A High Level Language for the Design and Verification of Finite State Machines (M.C. Browne, E.M. Clarke). Proof of Correctness. Proving Correctness of Digital Designs in the Multidimensional Design Space (J. Smit et al.). The Mechanical Verification of a Microprocessor Design (W.A. Hunt, Jr.). CAMILOD - A Program System for Designing Digital Hardware with Proven Correctness (W. Grass, R. Rauscher). From Algebraic Specifications to Correct VLSI Circuits (G.C. Gopalakrishnan, M.K. Srivas, D.R. Smith). Synthesis. Self-Timed FIFO: An Exercise in Compiling Programs into VLSI Circuits (A.J. Martin). The Karlsruhe DSL Synthesis System (W. Rosenstiel, R. Camposano). Proof and Synthesis: Cooperative Approaches. Verification, Synthesis and Correctness-Preserving Transformations - Cooperative Approaches to Correct Hardware Design (H. Eveking). Proofs and Synthesis are Cooperative Approaches for Correct Circuit Designs (T. Uehara). Invited Paper: FORCE: A Formal Checker of Executability (F. Anceau).