From HDL descriptions to guaranteed correct circuit designs

En savoir plus sur le livre

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.