Correct Hardware Design and Verification Methods: 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L’Aquila, Italy, October 21-24, 2003. ProceedingsAuthor: Daniel Geist, Enrico Tronci Published by Springer Berlin Heidelberg ISBN: 978-3-540-20363-6 DOI: 10.1007/b93958Table of Contents:What Is beyond the RTL Horizon for Microprocessor and System Design? The Charme of Abstract Entities The PSL/Sugar Specification Language A Language for all Seasons Finding Regularity: Describing and Analysing Circuits That Are Not Quite Regular Predicate Abstraction with Minimum Predicates Efficient Symbolic Model Checking of Software Using Partial Disjunctive Partitioning Instantiating Uninterpreted Functional Units and Memory System: Functional Verification of the VAMP A Hazards-Based Correctness Statement for Pipelined Circuits Analyzing the Intel Itanium Memory Ordering Rules Using Logic Programming and SAT On Complementing Nondeterministic Büchi Automata Coverage Metrics for Formal Verification “More Deterministic” vs. “Smaller” Büchi Automata for Efficient LTL Model Checking An Optimized Symbolic Bounded Model Checking Engine Constrained Symbolic Simulation with Mathematica and ACL2 Semi-formal Verification of Memory Systems by Symbolic Simulation CTL May Be Ambiguous When Model Checking Moore Machines Reasoning about GSTE Assertion Graphs Towards Diagrammability and Efficiency in Event Sequence Languages Executing the Formal Semantics of the Accellera Property Specification Language by Mechanised Theorem Proving On Combining Symmetry Reduction and Symbolic Representation for Efficient Model Checking, Electronic reproduction, Text (HTML/PDF), image (GIF/PDF) and search engine, Mode of access: Intranet, Caption title ; description based on screen of 2005-03-02, Includes bibliographical references