Correct hardware design and verification methods

Mehr zum Buch

The book features a comprehensive exploration of formal verification and its relationship with simulation, addressing various challenges in configurable processor design and automotive systems. It includes discussions on functional design descriptions and wire-aware circuit design, along with formalization of the DE2 language. The text delves into game-solving approaches, fault detection, and verification of quantitative properties using bound functions. Key topics include abstraction techniques and the effectiveness of interleaved invariant checking with dynamic abstraction. The book also presents automatic formal verification methods for liveness in pipelined processors with multicycle functional units, along with algorithms to enhance verification speed, such as efficient symbolic simulation and distributed symbolic reachability analysis. Real-time model checking and the use of temporal modalities for timing diagrams are discussed, alongside algorithms for generating hints for symbolic traversal and input reduction in sequential netlists. Additional content covers verification of memory hierarchy and management mechanisms, alongside counterexample-guided invariant discovery for cache coherence verification. Short papers address symbolic partial order reduction, timing behavior verification, and deadlock prevention in protocols. The book concludes with insights into high-level modeling, parameterized systems, and formal ve