---
_id: '26746'
abstract:
- lang: eng
  text: "Previous research in proof-carrying hardware has established the feasibility
    and utility of the approach, and provided a concrete solution for employing it
    for the certification of functional equivalence checking against a specification,
    but fell short in connecting it to state-of-the-art formal verification insights,
    methods and tools. Due to the immense complexity of modern circuits, and verification
    challenges such as the state explosion problem for sequential circuits, this restriction
    of readily-available verification solutions severely limited the applicability
    of the approach in wider contexts.\r\n\r\nThis thesis closes the gap between the
    PCH approach and current advances in formal hardware verification, provides methods
    and tools to express and certify a wide range of circuit properties, both functional
    and non-functional, and presents for the first time prototypes in which circuits
    that are implemented on actual reconfigurable hardware are verified with PCH methods.
    Using these results, designers can now apply PCH to establish trust in more complex
    circuits, by using more diverse properties which they can express using modern,
    efficient property specification techniques."
- lang: ger
  text: "Die bisherige Forschung zu Proof-Carrying Hardware (PCH) hat dessen Machbarkeit
    und Nützlichkeit gezeigt und einen Ansatz zur Zertifizierung der funktionalen
    Äquivalenz zu einer Spezifikation geliefert, jedoch ohne PCH mit aktuellen Erkenntnissen,
    Methoden oder Werkzeugen formaler Hardwareverifikation zu verknüpfen. Aufgrund
    der Komplexität moderner Schaltungen und Verifikationsherausforderungen wie der
    Zustandsexplosion bei sequentiellen Schaltungen, limitiert diese Einschränkung
    sofort verfügbarer Verifikationslösungen die Anwendbarkeit des Ansatzes in einem
    größeren Kontext signifikant.\r\n\r\nDiese Dissertation schließt die Lücke zwischen
    PCH und modernen Entwicklungen in der Schaltungsverifikation und stellt Methoden
    und Werkzeuge zur Verfügung, welche die Zertifizierung einer großen Bandbreite
    von Schaltungseigenschaften ermöglicht; sowohl funktionale, als auch nicht-funktionale.
    Überdies werden erstmals Prototypen vorgestellt in welchen Schaltungen mittels
    PCH verifiziert werden, die auf tatsächlicher rekonfigurierbarer Hardware realisiert
    sind. Dank dieser Ergebnisse können Entwickler PCH zur Herstellung von Vertrauen
    in weit komplexere Schaltungen verwenden, unter Zuhilfenahme einer größeren Vielfalt
    von Eigenschaften, welche durch moderne, effiziente Spezifikationstechniken ausgedrückt
    werden können."
author:
- first_name: Tobias
  full_name: Wiersema, Tobias
  id: '3118'
  last_name: Wiersema
citation:
  ama: Wiersema T. <i>Guaranteeing Properties of Reconfigurable Hardware Circuits
    with Proof-Carrying Hardware</i>. Paderborn University; 2021.
  apa: Wiersema, T. (2021). <i>Guaranteeing Properties of Reconfigurable Hardware
    Circuits with Proof-Carrying Hardware</i>. Paderborn University.
  bibtex: '@book{Wiersema_2021, place={Paderborn}, title={Guaranteeing Properties
    of Reconfigurable Hardware Circuits with Proof-Carrying Hardware}, publisher={Paderborn
    University}, author={Wiersema, Tobias}, year={2021} }'
  chicago: 'Wiersema, Tobias. <i>Guaranteeing Properties of Reconfigurable Hardware
    Circuits with Proof-Carrying Hardware</i>. Paderborn: Paderborn University, 2021.'
  ieee: 'T. Wiersema, <i>Guaranteeing Properties of Reconfigurable Hardware Circuits
    with Proof-Carrying Hardware</i>. Paderborn: Paderborn University, 2021.'
  mla: Wiersema, Tobias. <i>Guaranteeing Properties of Reconfigurable Hardware Circuits
    with Proof-Carrying Hardware</i>. Paderborn University, 2021.
  short: T. Wiersema, Guaranteeing Properties of Reconfigurable Hardware Circuits
    with Proof-Carrying Hardware, Paderborn University, Paderborn, 2021.
date_created: 2021-10-25T06:35:41Z
date_updated: 2022-01-06T06:57:26Z
ddc:
- '006'
department:
- _id: '78'
keyword:
- Proof-Carrying Hardware
- Formal Verification
- Sequential Circuits
- Non-Functional Properties
- Functional Properties
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://nbn-resolving.de/urn:nbn:de:hbz:466:2-39800
oa: '1'
page: '293'
place: Paderborn
project:
- _id: '1'
  name: SFB 901
- _id: '3'
  name: SFB 901 - Project Area B
- _id: '12'
  name: SFB 901 - Subproject B4
publication_status: published
publisher: Paderborn University
status: public
supervisor:
- first_name: Marco
  full_name: Platzner, Marco
  id: '398'
  last_name: Platzner
title: Guaranteeing Properties of Reconfigurable Hardware Circuits with Proof-Carrying
  Hardware
type: dissertation
user_id: '3118'
year: '2021'
...