---
_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'
...
---
_id: '17358'
abstract:
- lang: eng
  text: 'Approximate circuits trade-off computational accuracy against improvements
    in hardware area, delay, or energy consumption. IP core vendors who wish to create
    such circuits need to convince consumers of the resulting approximation quality.
    As a solution we propose proof-carrying approximate circuits: The vendor creates
    an approximate IP core together with a certificate that proves the approximation
    quality. The proof certificate is bundled with the approximate IP core and sent
    off to the consumer. The consumer can formally verify the approximation quality
    of the IP core at a fraction of the typical computational cost for formal verification.
    In this paper, we first make the case for proof-carrying approximate circuits
    and then demonstrate the feasibility of the approach by a set of synthesis experiments
    using an exemplary approximation framework.'
article_type: original
author:
- first_name: Linus Matthias
  full_name: Witschen, Linus Matthias
  id: '49051'
  last_name: Witschen
- first_name: Tobias
  full_name: Wiersema, Tobias
  id: '3118'
  last_name: Wiersema
- first_name: Marco
  full_name: Platzner, Marco
  id: '398'
  last_name: Platzner
citation:
  ama: Witschen LM, Wiersema T, Platzner M. Proof-carrying Approximate Circuits. <i>IEEE
    Transactions On Very Large Scale Integration Systems</i>. 2020;28(9):2084-2088.
    doi:<a href="https://doi.org/10.1109/TVLSI.2020.3008061">10.1109/TVLSI.2020.3008061</a>
  apa: Witschen, L. M., Wiersema, T., &#38; Platzner, M. (2020). Proof-carrying Approximate
    Circuits. <i>IEEE Transactions On Very Large Scale Integration Systems</i>, <i>28</i>(9),
    2084–2088. <a href="https://doi.org/10.1109/TVLSI.2020.3008061">https://doi.org/10.1109/TVLSI.2020.3008061</a>
  bibtex: '@article{Witschen_Wiersema_Platzner_2020, title={Proof-carrying Approximate
    Circuits}, volume={28}, DOI={<a href="https://doi.org/10.1109/TVLSI.2020.3008061">10.1109/TVLSI.2020.3008061</a>},
    number={9}, journal={IEEE Transactions On Very Large Scale Integration Systems},
    publisher={IEEE}, author={Witschen, Linus Matthias and Wiersema, Tobias and Platzner,
    Marco}, year={2020}, pages={2084–2088} }'
  chicago: 'Witschen, Linus Matthias, Tobias Wiersema, and Marco Platzner. “Proof-Carrying
    Approximate Circuits.” <i>IEEE Transactions On Very Large Scale Integration Systems</i>
    28, no. 9 (2020): 2084–88. <a href="https://doi.org/10.1109/TVLSI.2020.3008061">https://doi.org/10.1109/TVLSI.2020.3008061</a>.'
  ieee: L. M. Witschen, T. Wiersema, and M. Platzner, “Proof-carrying Approximate
    Circuits,” <i>IEEE Transactions On Very Large Scale Integration Systems</i>, vol.
    28, no. 9, pp. 2084–2088, 2020.
  mla: Witschen, Linus Matthias, et al. “Proof-Carrying Approximate Circuits.” <i>IEEE
    Transactions On Very Large Scale Integration Systems</i>, vol. 28, no. 9, IEEE,
    2020, pp. 2084–88, doi:<a href="https://doi.org/10.1109/TVLSI.2020.3008061">10.1109/TVLSI.2020.3008061</a>.
  short: L.M. Witschen, T. Wiersema, M. Platzner, IEEE Transactions On Very Large
    Scale Integration Systems 28 (2020) 2084–2088.
date_created: 2020-07-06T11:21:30Z
date_updated: 2022-01-06T06:53:09Z
department:
- _id: '78'
doi: 10.1109/TVLSI.2020.3008061
funded_apc: '1'
intvolume: '        28'
issue: '9'
keyword:
- Approximate circuit synthesis
- approximate computing
- error metrics
- formal verification
- proof-carrying hardware
language:
- iso: eng
page: 2084 - 2088
project:
- _id: '12'
  name: SFB 901 - Subproject B4
- _id: '3'
  name: SFB 901 - Project Area B
- _id: '1'
  name: SFB 901
publication: IEEE Transactions On Very Large Scale Integration Systems
publication_identifier:
  eissn:
  - 1557-9999
  issn:
  - 1063-8210
publication_status: published
publisher: IEEE
quality_controlled: '1'
status: public
title: Proof-carrying Approximate Circuits
type: journal_article
user_id: '49051'
volume: 28
year: '2020'
...
---
_id: '1097'
author:
- first_name: Felix Paul
  full_name: Jentzsch, Felix Paul
  last_name: Jentzsch
citation:
  ama: Jentzsch FP. <i>Enforcing IP Core Connection Properties with Verifiable Security
    Monitors</i>. Universität Paderborn; 2018.
  apa: Jentzsch, F. P. (2018). <i>Enforcing IP Core Connection Properties with Verifiable
    Security Monitors</i>. Universität Paderborn.
  bibtex: '@book{Jentzsch_2018, title={Enforcing IP Core Connection Properties with
    Verifiable Security Monitors}, publisher={Universität Paderborn}, author={Jentzsch,
    Felix Paul}, year={2018} }'
  chicago: Jentzsch, Felix Paul. <i>Enforcing IP Core Connection Properties with Verifiable
    Security Monitors</i>. Universität Paderborn, 2018.
  ieee: F. P. Jentzsch, <i>Enforcing IP Core Connection Properties with Verifiable
    Security Monitors</i>. Universität Paderborn, 2018.
  mla: Jentzsch, Felix Paul. <i>Enforcing IP Core Connection Properties with Verifiable
    Security Monitors</i>. Universität Paderborn, 2018.
  short: F.P. Jentzsch, Enforcing IP Core Connection Properties with Verifiable Security
    Monitors, Universität Paderborn, 2018.
date_created: 2018-01-15T16:48:05Z
date_updated: 2022-01-06T06:50:54Z
department:
- _id: '78'
keyword:
- Approximate Computing
- Proof-Carrying Hardware
- Formal Verification
language:
- iso: eng
project:
- _id: '12'
  name: SFB 901 - Subproject B4
- _id: '1'
  name: SFB 901
- _id: '3'
  name: SFB 901 - Project Area B
publisher: Universität Paderborn
status: public
supervisor:
- first_name: Tobias
  full_name: Wiersema, Tobias
  id: '3118'
  last_name: Wiersema
title: Enforcing IP Core Connection Properties with Verifiable Security Monitors
type: bachelorsthesis
user_id: '477'
year: '2018'
...