[{"department":[{"_id":"78"}],"user_id":"3118","_id":"26746","project":[{"_id":"1","name":"SFB 901"},{"name":"SFB 901 - Project Area B","_id":"3"},{"_id":"12","name":"SFB 901 - Subproject B4"}],"status":"public","type":"dissertation","main_file_link":[{"url":"https://nbn-resolving.de/urn:nbn:de:hbz:466:2-39800","open_access":"1"}],"author":[{"last_name":"Wiersema","id":"3118","full_name":"Wiersema, Tobias","first_name":"Tobias"}],"supervisor":[{"last_name":"Platzner","id":"398","full_name":"Platzner, Marco","first_name":"Marco"}],"oa":"1","date_updated":"2022-01-06T06:57:26Z","page":"293","citation":{"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} }","short":"T. Wiersema, Guaranteeing Properties of Reconfigurable Hardware Circuits with Proof-Carrying Hardware, Paderborn University, Paderborn, 2021.","mla":"Wiersema, Tobias. <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.","ama":"Wiersema T. <i>Guaranteeing Properties of Reconfigurable Hardware Circuits with Proof-Carrying Hardware</i>. Paderborn University; 2021.","ieee":"T. Wiersema, <i>Guaranteeing Properties of Reconfigurable Hardware Circuits with Proof-Carrying Hardware</i>. Paderborn: Paderborn University, 2021.","chicago":"Wiersema, Tobias. <i>Guaranteeing Properties of Reconfigurable Hardware Circuits with Proof-Carrying Hardware</i>. Paderborn: Paderborn University, 2021."},"place":"Paderborn","publication_status":"published","language":[{"iso":"eng"}],"keyword":["Proof-Carrying Hardware","Formal Verification","Sequential Circuits","Non-Functional Properties","Functional Properties"],"ddc":["006"],"abstract":[{"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":"eng"},{"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."}],"title":"Guaranteeing Properties of Reconfigurable Hardware Circuits with Proof-Carrying Hardware","date_created":"2021-10-25T06:35:41Z","publisher":"Paderborn University","year":"2021"},{"year":"2020","quality_controlled":"1","issue":"9","title":"Proof-carrying Approximate Circuits","publisher":"IEEE","date_created":"2020-07-06T11:21:30Z","abstract":[{"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.","lang":"eng"}],"publication":"IEEE Transactions On Very Large Scale Integration Systems","keyword":["Approximate circuit synthesis","approximate computing","error metrics","formal verification","proof-carrying hardware"],"language":[{"iso":"eng"}],"intvolume":"        28","page":"2084 - 2088","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>","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.","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>.","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>.","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} }","short":"L.M. Witschen, T. Wiersema, M. Platzner, IEEE Transactions On Very Large Scale Integration Systems 28 (2020) 2084–2088.","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>"},"publication_identifier":{"eissn":["1557-9999"],"issn":["1063-8210"]},"publication_status":"published","doi":"10.1109/TVLSI.2020.3008061","date_updated":"2022-01-06T06:53:09Z","volume":28,"author":[{"full_name":"Witschen, Linus Matthias","id":"49051","last_name":"Witschen","first_name":"Linus Matthias"},{"first_name":"Tobias","id":"3118","full_name":"Wiersema, Tobias","last_name":"Wiersema"},{"id":"398","full_name":"Platzner, Marco","last_name":"Platzner","first_name":"Marco"}],"status":"public","type":"journal_article","article_type":"original","funded_apc":"1","_id":"17358","project":[{"name":"SFB 901 - Subproject B4","_id":"12"},{"name":"SFB 901 - Project Area B","_id":"3"},{"name":"SFB 901","_id":"1"}],"department":[{"_id":"78"}],"user_id":"49051"},{"citation":{"ama":"Jentzsch FP. <i>Enforcing IP Core Connection Properties with Verifiable Security Monitors</i>. Universität Paderborn; 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.","apa":"Jentzsch, F. P. (2018). <i>Enforcing IP Core Connection Properties with Verifiable Security Monitors</i>. Universität Paderborn.","short":"F.P. Jentzsch, Enforcing IP Core Connection Properties with Verifiable Security Monitors, Universität Paderborn, 2018.","bibtex":"@book{Jentzsch_2018, title={Enforcing IP Core Connection Properties with Verifiable Security Monitors}, publisher={Universität Paderborn}, author={Jentzsch, Felix Paul}, year={2018} }","mla":"Jentzsch, Felix Paul. <i>Enforcing IP Core Connection Properties with Verifiable Security Monitors</i>. Universität Paderborn, 2018."},"year":"2018","author":[{"full_name":"Jentzsch, Felix Paul","last_name":"Jentzsch","first_name":"Felix Paul"}],"supervisor":[{"full_name":"Wiersema, Tobias","id":"3118","last_name":"Wiersema","first_name":"Tobias"}],"date_created":"2018-01-15T16:48:05Z","publisher":"Universität Paderborn","date_updated":"2022-01-06T06:50:54Z","title":"Enforcing IP Core Connection Properties with Verifiable Security Monitors","type":"bachelorsthesis","status":"public","department":[{"_id":"78"}],"user_id":"477","_id":"1097","project":[{"_id":"12","name":"SFB 901 - Subproject B4"},{"name":"SFB 901","_id":"1"},{"_id":"3","name":"SFB 901 - Project Area B"}],"language":[{"iso":"eng"}],"keyword":["Approximate Computing","Proof-Carrying Hardware","Formal Verification"]}]