Correct Hardware Design and Verification Methods: 13th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2005, Saarbrücken, Germany, October 3-6, 2005. Proceedings

This book constitutes the refereed proceedings of the 13th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, CHARME 2005, held in Saarbr?cken, Germany, in October 2005. The 21 revised full papers and 18 short papers presented together with 2 invited talks and one tutorial were carefully reviewed and selected from 79 submissions. The papers are organized in topical sections on functional approaches to design description, game solving approaches, abstraction, algorithms and techniques for speeding (DD-based) verification, real time and LTL model checking, evaluation of SAT-based tools, model reduction, and verification of memory hierarchy mechanisms. Front Matter....Pages - Is Formal Verification Bound to Remain a Junior Partner of Simulation?....Pages 1-1 Verification Challenges in Configurable Processor Design with ASIP Meister....Pages 2-2 Towards the Pervasive Verification of Automotive Systems....Pages 3-4 Wired: Wire-Aware Circuit Design....Pages 5-19 Formalization of the DE2 Language....Pages 20-34 Finding and Fixing Faults....Pages 35-49 Verifying Quantitative Properties Using Bound Functions....Pages 50-64 How Thorough Is Thorough Enough?....Pages 65-80 Interleaved Invariant Checking with Dynamic Abstraction....Pages 81-96 Automatic Formal Verification of Liveness for Pipelined Processors with Multicycle Functional Units....Pages 97-113 Efficient Symbolic Simulation via Dynamic Scheduling, Don’t Caring, and Case Splitting....Pages 114-128 Achieving Speedups in Distributed Symbolic Reachability Analysis Through Asynchronous Computation....Pages 129-145 Saturation-Based Symbolic Reachability Analysis Using Conjunctive and Disjunctive Partitioning....Pages 146-161 Real-Time Model Checking Is Really Simple....Pages 162-175 Temporal Modalities for Concisely Capturing Timing Diagrams....Pages 176-190 Regular Vacuity....Pages 191-206 Automatic Generation of Hints for Symbolic Traversal....Pages 207-221 Maximal Input Reduction of Sequential Netlists via Synergistic Reparameterization and Localization Strategies....Pages 222-237 A New SAT-Based Algorithm for Symbolic Trajectory Evaluation....Pages 238-253 An Analysis of SAT-Based Model Checking Techniques in an Industrial Environment....Pages 254-268 Exploiting Constraints in Transformation-Based Verification....Pages 269-284 Identification and Counter Abstraction for Full Virtual Symmetry....Pages 285-300 On the Verification of Memory Management Mechanisms....Pages 301-316 Counterexample Guided Invariant Discovery for Parameterized Cache Coherence Verification....Pages 317-331 Symbolic Partial Order Reduction for Rule Based Transition Systems....Pages 332-335 Verifying Timing Behavior by Abstract Interpretation of Executable Code....Pages 336-339 Behavior-RTL Equivalence Checking Based on Data Transfer Analysis with Virtual Controllers and Datapaths....Pages 340-344 Deadlock Prevention in the Æthereal Protocol....Pages 345-348 Acceleration of SAT-Based Iterative Property Checking....Pages 349-353 Error Detection Using BMC in a Parallel Environment....Pages 354-358 Formal Verification of Synchronizers....Pages 359-362 A Parameterized Benchmark Suite of Hard Pipelined-Machine-Verification Problems....Pages 363-366 Improvements to the Implementation of Interpolant-Based Model Checking....Pages 367-370 High-Level Modelling, Analysis, and Verification on FPGA-Based Hardware Design....Pages 371-375 Proving Parameterized Systems: The Use of Pseudo-Pipelines in Polyhedral Logic....Pages 376-379 Resolving Quartz Overloading....Pages 380-383 FPGA Based Accelerator for 3-SAT Conflict Analysis in SAT Solvers....Pages 384-387 Predictive Reachability Using a Sample-Based Approach....Pages 388-392 Minimizing Counterexample of ACTL Property....Pages 393-397 Data Refinement for Synchronous System Specification and Construction....Pages 398-401 Introducing Abstractions via Rewriting....Pages 402-405 A Case Study: Formal Verification of Processor Critical Properties....Pages 406-409 Back Matter....Pages -

this Book Constitutes The Refereed Proceedings Of The 13th Ifip Wg 10.5 Advanced Research Working Conference On Correct Hardware Design And Verification Methods, Charme 2005, Held In Saarbrücken, Germany, In October 2005.

the 21 Revised Full Papers And 18 Short Papers Presented Together With 2 Invited Talks And One Tutorial Were Carefully Reviewed And Selected From 79 Submissions. The Papers Are Organized In Topical Sections On Functional Approaches To Design Description, Game Solving Approaches, Abstraction, Algorithms And Techniques For Speeding (dd-based) Verification, Real Time And Ltl Model Checking, Evaluation Of Sat-based Tools, Model Reduction, And Verification Of Memory Hierarchy Mechanisms.

This Book Constitutes The Refereed Proceedings Of The 13th Ifip Wg 10.5 Advanced Research Working Conference On Correct Hardware Design And Verification Methods, Charme 2005, Held In Saarbrücken, Germany, In October 2005. The 21 Revised Full Papers And 18 Short Papers Presented Together With 2 Invited Talks And One Tutorial Were Carefully Reviewed And Selected From 79 Submissions. The Papers Are Organized In Topical Sections On Functional Approaches To Design Description, Game Solving Approaches, Abstraction, Algorithms And Techniques For Speeding (dd-based) Verification, Real Time And Ltl Model Checking, Evaluation Of Sat-based Tools, Model Reduction, And Verification Of Memory Hierarchy Mechanisms. Constitutes the refereed proceedings of the 13th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, CHARME 2005, held in Saarbrucken, Germany, in October 2005.