Correct Hardware Design and Verification Methods

Invited Contributions.- View from the Fringe of the Fringe.- Hardware Synthesis Using SAFL and Application to Processor Design.- FMCAD 2000.- Applications of Hierarchical Verification in Model Checking.- Model Checking 1.- Pruning Techniques for the SAT-Based Bounded Model Checking Problem.- Heuristics for Hierarchical Partitioning with Application to Model Checking.- Short Papers 1.- Efficient Reachability Analysis and Refinement Checking of Timed Automata Using BDDs.- Deriving Real-Time Programs from Duration Calculus Specifications.- Reproducing Synchronization Bugs with Model Checking.- Formally-Based Design Evaluation.- Clocking Issues.- Multiclock Esterel.- Register Transformations with Multiple Clock Domains.- Temporal Properties of Self-Timed Rings.- Short Papers 2.- Coverability Analysis Using Symbolic Model Checking.- Specifying Hardware Timing with ET-Lotos.- Formal Pipeline Design.- Verification of Basic Block Schedules Using RTL Transformations.- Joint Session with TPHOLs.- Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking.- Proof Engineering in the Large: Formal Verification of Pentium®4 Floating-Point Divider.- Hardware Compilation.- Towards Provably-Correct Hardware Compilation Tools Based on Pass Separation Techniques.- A Higher-Level Language for Hardware Synthesis.- Tools.- Hierarchical Verification Using an MDG-HOL Hybrid Tool.- Exploiting Transition Locality in Automatic Verification.- Efficient Debugging in a Formal Verification Environment.- Model Checking 2.- Using Combinatorial Optimization Methods for Quantification Scheduling.- Net Reductions for LTL Model-Checking.- Component Verification.- Formal Verification of the VAMP Floating Point Unit.- A Specification Methodology by a Collection ofCompact Properties as Applied to the Intel® Itanium(TM) Processor Bus Protocol.- The Design and Verification of a Sorter Core.- Case Studies.- Refinement-Based Formal Verification of Asynchronous Wrappers for Independently Clocked Domains in Systems on Chip.- Using Abstract Specifications to Verify PowerPC(TM) Custom Memories by Symbolic Trajectory Evaluation.- Algorithm Verification.- Formal Verification of Conflict Detection Algorithms.- Induction-Oriented Formal Verification in Symmetric Interconnection Networks.- A Framework for Microprocessor Correctness Statements.- Duration Calculus.- From Operational Semantics to Denotational Semantics for Verilog.- Efficient Verification of a Class of Linear Hybrid Automata Using Linear Programming.