Correct Hardware Design and Verification Methods 正确的硬件设计与验证法

书籍目录

Invited Talks　What Is beyond the RTL Horizon for Microprocessor and　System Design?　The Charme of Abstract EntitiesTutorial　The PSL/Sugar Specification Language　A Language for all SeasonsSoftware Verification　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 PartitioningProcessor Verification　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 SATAutomata Based Methods　On Complementing Nondeterministic Bfichi Automata　Coverage Metrics for Formal Verification　Efficient LTL Model CheckingShort Papers 1　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 MachinesSpecification Methods　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 ProvingProtocol Verification　On Combining Symmetry Reduction and Symbolic Representation for　Efficient Model Checking……Short Paers 2Theorem ProvingBounded Model CheckingModel Checking and ApplicationAuthor Index

作者简介

This book constitutes the refereed proceedings of the 12th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, CHARME 2003, held in L'Aquila, Italy in October 2003.    The 24 revised full papers and 8 short papers presented were carefully reviewed and selected from 65 submissions. The papers are organized in topical sections on software verification, automata based methods, processor verification, specification methods, theorem proving, bounded model checking, and model checking and applications.

 Correct Hardware Design and Verification Methods 正确的硬件设计与验证法下载