Dominique Borrione Knihy

Hardbound. The objective of this book is to bring together the knowledge of developers and users of design automation tools, and compare the methods and algorithms by which correct circuit designs may be obtained from initial descriptions and specifications written in an appropriate hardware description language (HDL). In order to achieve the goal of designing correct circuits, two main directions of research are currently being formal verification of a (possibly manual) design, and automatic synthesis. Both approaches require that a high level specification of the circuit be given in a formal language, and an underlying model of hardware behaviour is necessary to allow for symbolic translations that preserve or verify some notion of correctness. Hardware models, formal proof of correctness, and synthesis are therefore the three key elements making up this volume.

The topic areas presented within this volume focus on design environments and the applications of hardware description and modelling - including simulation, verification by correctness proofs, synthesis and test. The strong relationship between the topics of CHDL'91 and the work around the use and re-standardization of the VHDL language is also explored. The quality of this proceedings, and its significance to the academic and professional worlds is assured by the excellent technical programme here compiled.

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