Correct hardware design and verification methods : 11th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2001, Livingston, Scotland, UK, September 4-7, 2001 : proceedings

Correct Hardware Design and Verification Methods: 11th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2001 Livingston, Scotland, UK, September 4–7, 2001 Proceedings
Author: Tiziana Margaria, Tom Melham
Published by Springer Berlin Heidelberg
ISBN: 978-3-540-42541-0
DOI: 10.1007/3-540-44798-9

Table of Contents:

• View from the Fringe of the Fringe
• Hardware Synthesis Using SAFL and Application to Processor Design
• Applications of Hierarchical Verification in Model Checking
• Pruning Techniques for the SAT-Based Bounded Model Checking Problem
• Heuristics for Hierarchical Partitioning with Application to Model Checking
• Efficient Reachability Analysis and Refinement Checking of Timed Automata Using BDDs
• Deriving Real-Time Programs from Duration Calculus Specifications
• Reproducing Synchronization Bugs with Model Checking
• Formally-Based Design Evaluation
• Multiclock Esterel
• Register Transformations with Multiple Clock Domains
• Temporal Properties of Self-Timed Rings
• Coverability Analysis Using Symbolic Model Checking
• Specifying Hardware Timing with ET-Lotos
• Formal Pipeline Design
• Verification of Basic Block Schedules Using RTL Transformations
• Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking
• Proof Engineering in the Large: Formal Verification of Pentium®4 Floating-Point Divider
• Towards Provably-Correct Hardware Compilation Tools Based on Pass Separation Techniques
• A Higher-Level Language for Hardware Synthesis

Includes bibliographical references and index