Guaranteeing properties of reconfigurable hardware circuits with proof-carrying hardware / by Tobias Wiersema ; [Supervisor: Prof. Dr. Marco Platzner, Reviewers: Prof. Dr. Marco Platzner, Prof. Dr. Heike Wehrheim, Prof. Dr. David Andrews]. Paderborn, 2021
Inhalt
- Abstract
- Zusammenfassung
- Publications
- Acknowledgments
- Contents
- List of Figures
- List of Listings
- List of Tables
- Acronyms
- Glossary
- 1 Introduction
- 2 Background
- 2.1 Reconfigurable Hardware
- 2.2 Hardware verification
- 2.3 Proof-carrying Hardware
- 2.4 Tools and Platforms
- 3 Realizing Bitstream-level PCH
- 4 Virtual Field-Programmable Gate Arrays
- 4.1 Virtualizing FPGAs
- 4.2 Related work
- 4.3 Extending ZUMA
- 4.4 ZUMA-based PCH Evaluation Platform
- 4.5 Timing Analysis and Optimization
- 4.6 Conclusion
- 5 Proving properties with PCH
- 5.1 Related Work
- 5.2 Property classification
- 5.3 Sequential Property Checking
- 5.4 Monitor-based Property Checking
- 5.5 Scalability
- 5.6 Conclusion
- 6 Non-functional Property Checking
- 6.1 Worst-Case Completion Time
- 6.2 Information Flow Security
- 6.3 Approximation Quality
- 6.4 General Self-Composition Miters
- 6.5 Conclusion
- 7 PCH Demonstrators
- 8 Conclusion
- 9 Outlook
- A Tables
- A.1 Virtual Field-Programmable Gate Arrays
- A.2 Proving properties with PCH
- A.3 Non-functional Property Checking
- A.4 PCH Demonstrators
- Bibliography
- Colophon