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
Content
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