Formal Semantics and Proof Techniques for Optimizing VHDL Models

ISBN-13: 9781461373315 / Angielski / Miękka / 2012 / 158 str.

Kothanda Umamageswaran; Sheetanshu L. Pandey; Philip A. Wilsey

Opis

Written expressly for hardware designers, this book presents a formal model of VHDL clearly specifying both the static and dynamic semantics of VHDL. It provides a mathematical framework for representing VHDL constructs and shows how those constructs can be formally manipulated to reason about VHDL.

Spis treści

1. Introduction. 2. Related Work. 3. The Static Model. 4. A Well-Formed VHDL Model. 5. The Reduction Algebra. 6. Completeness of the Reduced Form. 7. Interval Temporal Logic. 8. The Dynamic Model. 9. Applications of the Dynamic Model. 10. A Framework for Proving Equivalences Using PVS. 11. Conclusions. Appendices. References. Index.