Buch, Englisch, 158 Seiten, Format (B × H): 160 mm x 241 mm, Gewicht: 448 g
ISBN: 978-0-7923-8375-8
Verlag: Springer US
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.
Zielgruppe
Research
Autoren/Hrsg.
Fachgebiete
- Mathematik | Informatik Mathematik Mathematik Interdisziplinär Systemtheorie
- Technische Wissenschaften Elektronik | Nachrichtentechnik Elektronik Mikroprozessoren
- Technische Wissenschaften Technik Allgemein Computeranwendungen in der Technik
- Mathematik | Informatik EDV | Informatik Professionelle Anwendung Computer-Aided Design (CAD)
- Geisteswissenschaften Design Produktdesign, Industriedesign
- Interdisziplinäres Wissenschaften Wissenschaften: Forschung und Information Kybernetik, Systemtheorie, Komplexe Systeme
- Technische Wissenschaften Elektronik | Nachrichtentechnik Elektronik Bauelemente, Schaltkreise
- Mathematik | Informatik EDV | Informatik Programmierung | Softwareentwicklung Programmier- und Skriptsprachen
- Technische Wissenschaften Elektronik | Nachrichtentechnik Elektronik Schaltungsentwurf
- Mathematik | Informatik EDV | Informatik Angewandte Informatik Computeranwendungen in Wissenschaft & Technologie
- Mathematik | Informatik EDV | Informatik Technische Informatik Hardware: Grundlagen und Allgemeines
- Technische Wissenschaften Technik Allgemein Konstruktionslehre und -technik
Weitere Infos & Material
1. Introduction.- 1.1 Goals of the Work.- 1.2 Scope of the Work.- 1.3 Notation.- 1.4 Overview of Book.- 2. Related Work.- 2.1 Higher Order Logic.- 2.2 Denotational Semantics.- 2.3 Functional Semantics.- 2.4 Axiomatic Semantics.- 2.5 Petri Nets.- 2.6 Evolving Algebras.- 2.7 Boyer-Moore Logic.- 2.8 Summary.- 3. The Static Model.- 3.1 The VHDL World.- 3.2 Signals.- 3.3 Variables.- 3.4 The Port Hierarchy.- 3.5 Data Types.- 3.6 Expressions.- 3.7 Subprograms.- 3.8 Sequential Statements.- 3.9 Concurrent Statements.- 3.10 Summary.- 4. A Well-Formed VHDL Model.- 4.1 Signals.- 4.2 Variables.- 4.3 The Port Hierarchy.- 4.4 Data Types.- 4.5 Expressions.- 4.6 Sequential Statements.- 4.7 Concurrent Statements.- 4.8 Summary.- 5. The Reduction Algebra.- 5.1 Signal Assignment Statements.- 5.2 Concurrent Statements.- 5.3 The Reduced Form.- 6. Completeness of the Reduced Form.- 6.1 A Brief Overview of PVS.- 6.2 The Specification of the Reduction Algebra in PVS.- 6.3 Signal Assignment Reduction.- 6.4 Completeness.- 6.5 Irreducibility.- 6.6 Conclusion.- 7. Interval Temporal Logic.- 8. The Dynamic Model.- 8.1 Methodology.- 8.2 Evaluation of VHDL Statements.- 8.3 Transaction Lists.- 8.4 The State Space.- 8.5 Waveforms.- 8.6 Observability.- 8.7 Attributes.- 8.8 Conclusions.- 9. Applications of the Dynamic Model.- 9.1 Similarity Revisited.- 9.2 Process Folding.- 9.3 Signal Collapsing.- 9.4 Elimination of Marking.- 9.5 Summary.- 10. A Framework for Proving Equivalences using PVS.- 10.1 The Dynamic Model.- 10.2 Validation of the Semantics.- 10.3 Developing Proofs of Optimizations.- 10.4 Applications to Practical Use.- 11. Conclusions.- 11.1 Contributions of this research.- 11.2 Future Work.- Appendices A—.- A.1 The relation during(b,a) holds.- A.2 The relation finishes(b,a) holds.- A.3 Therelation overlaps(a,b) holds.- References.
