+612 9045 4394
Correct Hardware Design and Verification Methods : 12th Ifip Wg 10.5 Advanced Research Working Conference, Charme 2003, l'Aquila, Italy, October 21-24, 2003, Proceedings - Daniel Geist

Correct Hardware Design and Verification Methods

12th Ifip Wg 10.5 Advanced Research Working Conference, Charme 2003, l'Aquila, Italy, October 21-24, 2003, Proceedings

By: Daniel Geist (Editor), Enrico Tronci (Editor)


Published: 10th October 2003
Ships: 15 business days
15 business days
or 4 easy payments of $40.21 with Learn more

This volume contains the proceedings of CHARME 2003, the12th Advanced - search Working Conference on Correct Hardware Design and Veri?cation - thods. CHARME 2003 continues the series of working conferences devoted to the development and use of leading-edge formal techniques and tools for the design and veri?cation of hardware and hardware-like systems. Previous events in the 'CHARME' series were held in Edinburgh (2001), Bad Herrenalb (1999), Montreal (1997), Frankfurt (1995), Arles (1993) and - rin (1991). This series of meetings were organized in cooperation with IFIP WG 10.5and10.2.Priormeetings, stretchingbacktotheearliestdaysofformalha- wareveri?cationwereheldundervariousnamesinMiami(1990), Leuven(1989), Glasgow (1988), Grenoble (1986), Edinburgh (1985) and Darmstadt (1984). We now have a well-established convention whereby the European CHARME con- rence alternates with its biennial counterpart, the International Conference on Formal Methods in Computer-Aided Design(FMCAD), whichisheldinev- numbered years in the USA. CHARME 2003 took place during 21-24 October 2003 at the Computer Science Department of the University of L'Aquila, Italy. It was cosponsored by the IFIP TC10/WG10 Working Group on Design and Engineering of Electronic Systems. The CHARME 2003 scienti?c program was comprised of: - A morning Tutorial by Daniel Geist aimed at industrial and academic - terchange. - Two Invited Lectures by Wolfgang Roesner and Fabio Somenzi. - Regular Sessions, featuring 24 papers selected out of 65 submissions, r- ging from foundational contributions to tool presentations. - Short Presentations, featuring 8 short contributions accompanied by a short presentation. The conference, of course, also included informal tool demonstrations, not announced in the o?cial program.

What Is beyond the RTL Horizon for Microprocessor and System Design?p. 1
The Charme of Abstract Entitiesp. 2
The PSL/Sugar Specification Language: A Language for all Seasonsp. 3
Finding Regularity: Describing and Analysing Circuits That Are Not Quite Regularp. 4
Predicate Abstraction with Minimum Predicatesp. 19
Efficient Symbolic Model Checking of Software Using Partial Disjunctive Partitioningp. 35
Instantiating Uninterpreted Functional Units and Memory System: Functional Verification of the VAMPp. 51
A Hazards-Based Correctness Statement for Pipelined Circuitsp. 66
Analyzing the Intel Itanium Memory Ordering Rules Using Logic Programming and SATp. 81
On Complementing Nondeterministic Buchi Automatap. 96
Coverage Metrics for Formal Verificationp. 111
"More Deterministic" vs. "Smaller" Buchi Automata for Efficient LTL Model Checkingp. 126
An Optimized Symbolic Bounded Model Checking Enginep. 141
Constrained Symbolic Simulation with Mathematica and ACL2p. 150
Semi-formal Verification of Memory Systems by Symbolic Simulationp. 158
CTL May be Ambiguous When Model Checking Moore Machinesp. 164
Reasoning about GSTE Assertion Graphsp. 170
Towards Diagrammability and Efficiency in Event Sequence Languagesp. 185
Executing the Formal Semantics of the Accellera Property Specification Language by Mechanised Theorem Provingp. 200
On Combining Symmetry Reduction and Symbolic Representation for Efficient Model Checkingp. 216
On the Correctness of an Intrusion-Tolerant Group Communication Protocolp. 231
Exact and Efficient Verification of Parameterized Cache Coherence Protocolsp. 247
Design and Implementation of an Abstract Interpreter for VHDLp. 263
A Programming Language Based Analysis of Operand Forwardingp. 270
Integrating RAM and Disk Based Verification within the Mur[phi] Verifierp. 277
Design and Verification of CoreConnectTM IP Using Esterelp. 283
Inductive Assertions and Operational Semanticsp. 289
A Compositional Theory of Refinement for Branching Timep. 304
Linear and Nonlinear Arithmetic in ACL2p. 319
Efficient Distributed SAT and SAT-Based Distributed Bounded Model Checkingp. 334
Convergence Testing in Term-Level Bounded Model Checkingp. 348
The ROBDD Size of Simple CNF Formulasp. 363
Efficient Hybrid Reachability Analysis for Asynchronous Concurrent Systemsp. 378
Finite Horizon Analysis of Markov Chains with the Mur[phi] Verifierp. 394
Improved Symbolic Verification Using Partitioning Techniquesp. 410
Author Indexp. 425
Table of Contents provided by Blackwell. All Rights Reserved.

ISBN: 9783540203636
ISBN-10: 354020363X
Series: Lecture Notes in Computer Science
Audience: General
Format: Paperback
Language: English
Number Of Pages: 432
Published: 10th October 2003
Country of Publication: DE
Dimensions (cm): 23.39 x 15.6  x 2.29
Weight (kg): 0.62