Benchmark-circuits for hardware-verification -- Reasoning about pipelines with structural hazards -- A correctness model for pipelined microprocessors -- Non-restoring integer square root: A case study in design by principled optimization -- An automatic generalization method for the inductive proof of replicated and parallel architectures -- A compositional circuit model and verification by composition -- Exploiting structural similarities in a BDD-based verification method -- Studies of the single pulser in various reasoning systems -- Mechanized verification of speed-independence -- Automatic correctness proof of the implementation of synchronous sequential circuits using an algebraic approach -- Mechanized verification of refinement -- Effective theorem proving for hardware verification -- A formal framework for high level synthesis -- Tutorial on design verification with synchronized transitions -- A tutorial on using PVS for hardware verification -- A reduced instruction set proof environment -- Quantitative evaluation of formal based synthesis in ASIC design -- Formal verification of characteristic properties -- Extending formal reasoning with support for hardware diagrams.