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

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 -