Correct Hardware Design and Verification Methods

Inhaltsverzeichnis

• Invited Talks.
• Is Formal Verification Bound to Remain a Junior Partner of Simulation?.
• Verification Challenges in Configurable Processor Design with ASIP Meister.
• Tutorial.
• Towards the Pervasive Verification of Automotive Systems.
• Functional Approaches to Design Description.
• Wired: Wire-Aware Circuit Design.
• Formalization of the DE2 Language.
• Game Solving Approaches.
• Finding and Fixing Faults.
• Verifying Quantitative Properties Using Bound Functions.
• Abstraction.
• How Thorough Is Thorough Enough?.
• Interleaved Invariant Checking with Dynamic Abstraction.
• Automatic Formal Verification of Liveness for Pipelined Processors with Multicycle Functional Units.
• Algorithms and Techniques for Speeding (DD-Based) Verification 1.
• Efficient Symbolic Simulation via Dynamic Scheduling, Don’t Caring, and Case Splitting.
• Achieving Speedups in Distributed Symbolic Reachability Analysis Through Asynchronous Computation.
• Saturation-Based Symbolic Reachability Analysis Using Conjunctive and Disjunctive Partitioning.
• Real Time and LTL Model Checking.
• Real-Time Model Checking Is Really Simple.
• Temporal Modalities for Concisely Capturing Timing Diagrams.
• Regular Vacuity.
• Algorithms and Techniques for Speeding Verification 2.
• Automatic Generation of Hints for Symbolic Traversal.
• Maximal Input Reduction of Sequential Netlists via Synergistic Reparameterization and Localization Strategies.
• A New SAT-Based Algorithm for Symbolic Trajectory Evaluation.
• Evaluation of SAT-Based Tools.
• An Analysis of SAT-Based Model Checking Techniques in an Industrial Environment.
• Model Reduction.
• Exploiting Constraints in Transformation-Based Verification.
• Identification and Counter Abstraction for Full Virtual Symmetry.
• Verification of Memory Hierarchy Mechanisms.
• On the Verificationof Memory Management Mechanisms.
• Counterexample Guided Invariant Discovery for Parameterized Cache Coherence Verification.
• Short Papers.
• Symbolic Partial Order Reduction for Rule Based Transition Systems.
• Verifying Timing Behavior by Abstract Interpretation of Executable Code.
• Behavior-RTL Equivalence Checking Based on Data Transfer Analysis with Virtual Controllers and Datapaths.
• Deadlock Prevention in the Æthereal Protocol.
• Acceleration of SAT-Based Iterative Property Checking.
• Error Detection Using BMC in a Parallel Environment.
• Formal Verification of Synchronizers.
• A Parameterized Benchmark Suite of Hard Pipelined-Machine-Verification Problems.
• Improvements to the Implementation of Interpolant-Based Model Checking.
• High-Level Modelling, Analysis, and Verification on FPGA-Based Hardware Design.
• Proving Parameterized Systems: The Use of Pseudo-Pipelines in Polyhedral Logic.
• Resolving Quartz Overloading.
• FPGA Based Accelerator for 3-SAT Conflict Analysis in SAT Solvers.
• Predictive Reachability Using a Sample-Based Approach.
• Minimizing Counterexample of ACTL Property.
• Data Refinement for Synchronous System Specification and Construction.
• Introducing Abstractions via Rewriting.
• A Case Study: Formal Verification of Processor Critical Properties.