From HDL descriptions to guaranteed correct circuit designs : proceedings of the IFIP WG 10.2 Working Conference on from HDL Descriptions to Guaranteed Correct Circuit Designs, Grenoble, France, 9-11 September, 1986
D. Borrione, Ifip Wg · North-Holland eBooks · 1987
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).