[{"main_file_link":[{"open_access":"1","url":"https://nbn-resolving.de/urn:nbn:de:hbz:466:2-39800"}],"oa":"1","date_updated":"2022-01-06T06:57:26Z","author":[{"full_name":"Wiersema, Tobias","id":"3118","last_name":"Wiersema","first_name":"Tobias"}],"supervisor":[{"first_name":"Marco","full_name":"Platzner, Marco","id":"398","last_name":"Platzner"}],"place":"Paderborn","page":"293","citation":{"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.","ama":"Wiersema T. <i>Guaranteeing Properties of Reconfigurable Hardware Circuits with Proof-Carrying Hardware</i>. Paderborn University; 2021.","mla":"Wiersema, Tobias. <i>Guaranteeing Properties of Reconfigurable Hardware Circuits with Proof-Carrying Hardware</i>. Paderborn University, 2021.","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.","apa":"Wiersema, T. (2021). <i>Guaranteeing Properties of Reconfigurable Hardware Circuits with Proof-Carrying Hardware</i>. Paderborn University."},"publication_status":"published","_id":"26746","project":[{"name":"SFB 901","_id":"1"},{"_id":"3","name":"SFB 901 - Project Area B"},{"name":"SFB 901 - Subproject B4","_id":"12"}],"department":[{"_id":"78"}],"user_id":"3118","status":"public","type":"dissertation","title":"Guaranteeing Properties of Reconfigurable Hardware Circuits with Proof-Carrying Hardware","publisher":"Paderborn University","date_created":"2021-10-25T06:35:41Z","year":"2021","keyword":["Proof-Carrying Hardware","Formal Verification","Sequential Circuits","Non-Functional Properties","Functional Properties"],"ddc":["006"],"language":[{"iso":"eng"}],"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"},{"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.","lang":"ger"}]},{"publication":"IEEE Transactions On Very Large Scale Integration Systems","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."}],"language":[{"iso":"eng"}],"keyword":["Approximate circuit synthesis","approximate computing","error metrics","formal verification","proof-carrying hardware"],"issue":"9","quality_controlled":"1","year":"2020","date_created":"2020-07-06T11:21:30Z","publisher":"IEEE","title":"Proof-carrying Approximate Circuits","type":"journal_article","status":"public","user_id":"49051","department":[{"_id":"78"}],"project":[{"name":"SFB 901 - Subproject B4","_id":"12"},{"name":"SFB 901 - Project Area B","_id":"3"},{"_id":"1","name":"SFB 901"}],"_id":"17358","funded_apc":"1","article_type":"original","publication_status":"published","publication_identifier":{"issn":["1063-8210"],"eissn":["1557-9999"]},"citation":{"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.","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>","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.","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>.","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>"},"page":"2084 - 2088","intvolume":"        28","author":[{"full_name":"Witschen, Linus Matthias","id":"49051","last_name":"Witschen","first_name":"Linus Matthias"},{"first_name":"Tobias","last_name":"Wiersema","full_name":"Wiersema, Tobias","id":"3118"},{"first_name":"Marco","id":"398","full_name":"Platzner, Marco","last_name":"Platzner"}],"volume":28,"date_updated":"2022-01-06T06:53:09Z","doi":"10.1109/TVLSI.2020.3008061"},{"type":"bachelorsthesis","status":"public","department":[{"_id":"78"}],"user_id":"477","_id":"1097","project":[{"name":"SFB 901 - Subproject B4","_id":"12"},{"name":"SFB 901","_id":"1"},{"_id":"3","name":"SFB 901 - Project Area B"}],"language":[{"iso":"eng"}],"keyword":["Approximate Computing","Proof-Carrying Hardware","Formal Verification"],"citation":{"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.","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.","ama":"Jentzsch FP. <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":[{"first_name":"Tobias","last_name":"Wiersema","full_name":"Wiersema, Tobias","id":"3118"}],"date_created":"2018-01-15T16:48:05Z","date_updated":"2022-01-06T06:50:54Z","publisher":"Universität Paderborn","title":"Enforcing IP Core Connection Properties with Verifiable Security Monitors"},{"title":"Past- and Future-Oriented Time-Bound Temporal Properties with OCL","conference":{"name":" Proceedings of the Second International Conference on Software Engineering and Formal Methods"},"doi":"10.1109/SEFM.2004.1347516","date_updated":"2023-01-24T09:03:41Z","publisher":"IEEE","date_created":"2023-01-24T09:03:36Z","author":[{"last_name":"Flake","full_name":"Flake, Stephan","first_name":"Stephan"},{"first_name":"Wolfgang","id":"16243","full_name":"Müller, Wolfgang","last_name":"Müller"}],"place":"Beijing, China","year":"2004","citation":{"chicago":"Flake, Stephan, and Wolfgang Müller. “Past- and Future-Oriented Time-Bound Temporal Properties with OCL.” In <i>Proceedings of SEFM´04</i>. Beijing, China: IEEE, 2004. <a href=\"https://doi.org/10.1109/SEFM.2004.1347516\">https://doi.org/10.1109/SEFM.2004.1347516</a>.","ieee":"S. Flake and W. Müller, “Past- and Future-Oriented Time-Bound Temporal Properties with OCL,” presented at the  Proceedings of the Second International Conference on Software Engineering and Formal Methods, 2004, doi: <a href=\"https://doi.org/10.1109/SEFM.2004.1347516\">10.1109/SEFM.2004.1347516</a>.","ama":"Flake S, Müller W. Past- and Future-Oriented Time-Bound Temporal Properties with OCL. In: <i>Proceedings of SEFM´04</i>. IEEE; 2004. doi:<a href=\"https://doi.org/10.1109/SEFM.2004.1347516\">10.1109/SEFM.2004.1347516</a>","bibtex":"@inproceedings{Flake_Müller_2004, place={Beijing, China}, title={Past- and Future-Oriented Time-Bound Temporal Properties with OCL}, DOI={<a href=\"https://doi.org/10.1109/SEFM.2004.1347516\">10.1109/SEFM.2004.1347516</a>}, booktitle={Proceedings of SEFM´04}, publisher={IEEE}, author={Flake, Stephan and Müller, Wolfgang}, year={2004} }","short":"S. Flake, W. Müller, in: Proceedings of SEFM´04, IEEE, Beijing, China, 2004.","mla":"Flake, Stephan, and Wolfgang Müller. “Past- and Future-Oriented Time-Bound Temporal Properties with OCL.” <i>Proceedings of SEFM´04</i>, IEEE, 2004, doi:<a href=\"https://doi.org/10.1109/SEFM.2004.1347516\">10.1109/SEFM.2004.1347516</a>.","apa":"Flake, S., &#38; Müller, W. (2004). Past- and Future-Oriented Time-Bound Temporal Properties with OCL. <i>Proceedings of SEFM´04</i>.  Proceedings of the Second International Conference on Software Engineering and Formal Methods. <a href=\"https://doi.org/10.1109/SEFM.2004.1347516\">https://doi.org/10.1109/SEFM.2004.1347516</a>"},"publication_identifier":{"isbn":["0-7695-2222-X"]},"keyword":["Unified modeling language","Logic","Clocks","Boolean functions","Application software","Time factors","Real time systems","Formal verification","Buffer storage","Software packages"],"language":[{"iso":"eng"}],"_id":"39069","user_id":"5786","department":[{"_id":"672"}],"abstract":[{"lang":"eng","text":"We present the syntax and semantics of a past- and future-oriented temporal extension of the Object Constraint Language (OCL). Our extension supports designers to express time-bounded properties over a state-oriented UML model of a system under development. The semantics is formally defined over the system states of a mathematical object model. Additionally, we present a mapping to Clocked Linear Temporal Logic (Clocked LTL) formulae, which is the basis for further application in verification with model checking. We demonstrate the applicability of the approach by the example of a buffer specification in the context of a production system."}],"status":"public","type":"conference","publication":"Proceedings of SEFM´04"},{"abstract":[{"lang":"eng","text":"We present a rigorous but transparent semantics definition of the SpecC language that covers the execution of SpecC behaviors and their interaction with the kernel process. The semantics include wait, wait for, par, and try statements as they are introduced in SpecC. We present our definition in form of distributed abstract state machine (ASM) rules strictly following the lines of the SpecC Language Reference Manual. We mainly see our formal semantics in three application areas. First, it is a concise, unambiguous description for documentation and standardization. Second, it applies as a high-level, pseudo code-oriented specification for the implementation of a SpecC simulator. Finally, it is a first step for SpecC synthesis in order to identify similar concepts with other languages like VHDL and SystemC for the definition of common patterns and language subsets."}],"status":"public","publication":"Proceedings of the ISSS02","type":"conference","keyword":["Standardization","Kernel","Permission","Formal verification","Logic functions","Documentation","Reasoning about programs","Specification languages","Formal specifications","Software systems"],"language":[{"iso":"eng"}],"_id":"39382","department":[{"_id":"672"}],"user_id":"5786","year":"2002","place":"Nagoya, Japan","citation":{"ieee":"W. Müller, R. Dömer, and A. Gerstlauer, “The Formal Execution Semantics of SpecC,” 2002, doi: <a href=\"https://doi.org/10.1145/581199.581234 \">10.1145/581199.581234 </a>.","chicago":"Müller, Wolfgang, Rainer Dömer, and Andreas Gerstlauer. “The Formal Execution Semantics of SpecC.” In <i>Proceedings of the ISSS02</i>. Nagoya, Japan, 2002. <a href=\"https://doi.org/10.1145/581199.581234 \">https://doi.org/10.1145/581199.581234 </a>.","ama":"Müller W, Dömer R, Gerstlauer A. The Formal Execution Semantics of SpecC. In: <i>Proceedings of the ISSS02</i>. ; 2002. doi:<a href=\"https://doi.org/10.1145/581199.581234 \">10.1145/581199.581234 </a>","apa":"Müller, W., Dömer, R., &#38; Gerstlauer, A. (2002). The Formal Execution Semantics of SpecC. <i>Proceedings of the ISSS02</i>. <a href=\"https://doi.org/10.1145/581199.581234 \">https://doi.org/10.1145/581199.581234 </a>","short":"W. Müller, R. Dömer, A. Gerstlauer, in: Proceedings of the ISSS02, Nagoya, Japan, 2002.","bibtex":"@inproceedings{Müller_Dömer_Gerstlauer_2002, place={Nagoya, Japan}, title={The Formal Execution Semantics of SpecC}, DOI={<a href=\"https://doi.org/10.1145/581199.581234 \">10.1145/581199.581234 </a>}, booktitle={Proceedings of the ISSS02}, author={Müller, Wolfgang and Dömer, Rainer and Gerstlauer, Andreas}, year={2002} }","mla":"Müller, Wolfgang, et al. “The Formal Execution Semantics of SpecC.” <i>Proceedings of the ISSS02</i>, 2002, doi:<a href=\"https://doi.org/10.1145/581199.581234 \">10.1145/581199.581234 </a>."},"publication_identifier":{"isbn":["1-58113-576-9"]},"title":"The Formal Execution Semantics of SpecC","doi":"10.1145/581199.581234 ","date_updated":"2023-01-24T10:10:28Z","date_created":"2023-01-24T10:10:24Z","author":[{"id":"16243","full_name":"Müller, Wolfgang","last_name":"Müller","first_name":"Wolfgang"},{"first_name":"Rainer","full_name":"Dömer, Rainer","last_name":"Dömer"},{"first_name":"Andreas","full_name":"Gerstlauer, Andreas","last_name":"Gerstlauer"}]},{"user_id":"5786","department":[{"_id":"672"}],"_id":"39403","language":[{"iso":"eng"}],"keyword":["Unified modeling language","Logic","Formal verification","Real time systems","Programming profession","Vehicle dynamics","Software standards","Flexible manufacturing systems","Electronics industry","Protocols"],"type":"conference","publication":"Proceedings of HICSS-35","status":"public","abstract":[{"text":"The Unified Modeling Language (UML) has received wide acceptance as a standard language in the field of software specification by means of different diagram types. In a recent version of UML, the textual Object Constraint Language (OCL) was introduced to support specification of constraints for UML models. But OCL currently does not provide sufficient means to specify constraints over the dynamic behavior of a model. This article presents an OCL extension that is consistent with current OCL and enables modelers to specify state-related time-bounded constraints. We consider the case study of a flexible manufacturing system and identify typical real-time constraints. The constraints are presented in our temporal OCL extension as well as in temporal logic formulae. For general application, we define a semantics of our OCL extension by means of a time-bounded temporal logic based on Computational Tree Logic (CTL).","lang":"eng"}],"author":[{"first_name":"Stephan","last_name":"Flake","full_name":"Flake, Stephan"},{"first_name":"Wolfgang","last_name":"Müller","id":"16243","full_name":"Müller, Wolfgang"}],"date_created":"2023-01-24T10:22:12Z","date_updated":"2023-01-24T10:22:16Z","doi":"10.1109/HICSS.2002.994469","conference":{"location":"Big Island, HI, USA ","name":"Proceedings of the 35th Annual Hawaii International Conference on System Sciences"},"title":"Specification of Real-Time Properties for UML Models","publication_identifier":{"isbn":["0-7695-1435-9"]},"citation":{"short":"S. Flake, W. Müller, in: Proceedings of HICSS-35, Big Island, HI, USA , 2002.","bibtex":"@inproceedings{Flake_Müller_2002, place={Big Island, HI, USA }, title={Specification of Real-Time Properties for UML Models}, DOI={<a href=\"https://doi.org/10.1109/HICSS.2002.994469\">10.1109/HICSS.2002.994469</a>}, booktitle={Proceedings of HICSS-35}, author={Flake, Stephan and Müller, Wolfgang}, year={2002} }","mla":"Flake, Stephan, and Wolfgang Müller. “Specification of Real-Time Properties for UML Models.” <i>Proceedings of HICSS-35</i>, 2002, doi:<a href=\"https://doi.org/10.1109/HICSS.2002.994469\">10.1109/HICSS.2002.994469</a>.","apa":"Flake, S., &#38; Müller, W. (2002). Specification of Real-Time Properties for UML Models. <i>Proceedings of HICSS-35</i>. Proceedings of the 35th Annual Hawaii International Conference on System Sciences, Big Island, HI, USA . <a href=\"https://doi.org/10.1109/HICSS.2002.994469\">https://doi.org/10.1109/HICSS.2002.994469</a>","ama":"Flake S, Müller W. Specification of Real-Time Properties for UML Models. In: <i>Proceedings of HICSS-35</i>. ; 2002. doi:<a href=\"https://doi.org/10.1109/HICSS.2002.994469\">10.1109/HICSS.2002.994469</a>","chicago":"Flake, Stephan, and Wolfgang Müller. “Specification of Real-Time Properties for UML Models.” In <i>Proceedings of HICSS-35</i>. Big Island, HI, USA , 2002. <a href=\"https://doi.org/10.1109/HICSS.2002.994469\">https://doi.org/10.1109/HICSS.2002.994469</a>.","ieee":"S. Flake and W. Müller, “Specification of Real-Time Properties for UML Models,” presented at the Proceedings of the 35th Annual Hawaii International Conference on System Sciences, Big Island, HI, USA , 2002, doi: <a href=\"https://doi.org/10.1109/HICSS.2002.994469\">10.1109/HICSS.2002.994469</a>."},"place":"Big Island, HI, USA ","year":"2002"},{"citation":{"apa":"Müller, W., Ruf, J., Hoffmann, D. W., Gerlach, J., Kropf, T., &#38; Rosenstiehl, W. (2001). The Simulation Semantics of SystemC. <i>Proceedings of the Design, Automation, and Test in Europe (DATE’01)</i>.  Proceedings Design, Automation and Test in Europe. Conference and Exhibition 2001. <a href=\"https://doi.org/10.1109/DATE.2001.915002\">https://doi.org/10.1109/DATE.2001.915002</a>","bibtex":"@inproceedings{Müller_Ruf_Hoffmann_Gerlach_Kropf_Rosenstiehl_2001, place={Munich, Germany }, title={The Simulation Semantics of SystemC}, DOI={<a href=\"https://doi.org/10.1109/DATE.2001.915002\">10.1109/DATE.2001.915002</a>}, booktitle={Proceedings of the Design, Automation, and Test in Europe (DATE’01)}, publisher={IEEE}, author={Müller, Wolfgang and Ruf, Jürgen and Hoffmann, D. W. and Gerlach, Joachim and Kropf, Thomas and Rosenstiehl, W.}, year={2001} }","mla":"Müller, Wolfgang, et al. “The Simulation Semantics of SystemC.” <i>Proceedings of the Design, Automation, and Test in Europe (DATE’01)</i>, IEEE, 2001, doi:<a href=\"https://doi.org/10.1109/DATE.2001.915002\">10.1109/DATE.2001.915002</a>.","short":"W. Müller, J. Ruf, D.W. Hoffmann, J. Gerlach, T. Kropf, W. Rosenstiehl, in: Proceedings of the Design, Automation, and Test in Europe (DATE’01), IEEE, Munich, Germany , 2001.","ama":"Müller W, Ruf J, Hoffmann DW, Gerlach J, Kropf T, Rosenstiehl W. The Simulation Semantics of SystemC. In: <i>Proceedings of the Design, Automation, and Test in Europe (DATE’01)</i>. IEEE; 2001. doi:<a href=\"https://doi.org/10.1109/DATE.2001.915002\">10.1109/DATE.2001.915002</a>","ieee":"W. Müller, J. Ruf, D. W. Hoffmann, J. Gerlach, T. Kropf, and W. Rosenstiehl, “The Simulation Semantics of SystemC,” presented at the  Proceedings Design, Automation and Test in Europe. Conference and Exhibition 2001, 2001, doi: <a href=\"https://doi.org/10.1109/DATE.2001.915002\">10.1109/DATE.2001.915002</a>.","chicago":"Müller, Wolfgang, Jürgen Ruf, D. W. Hoffmann, Joachim Gerlach, Thomas Kropf, and W. Rosenstiehl. “The Simulation Semantics of SystemC.” In <i>Proceedings of the Design, Automation, and Test in Europe (DATE’01)</i>. Munich, Germany : IEEE, 2001. <a href=\"https://doi.org/10.1109/DATE.2001.915002\">https://doi.org/10.1109/DATE.2001.915002</a>."},"year":"2001","place":"Munich, Germany ","publication_identifier":{"isbn":["0-7695-0993-2"]},"doi":"10.1109/DATE.2001.915002","conference":{"name":" Proceedings Design, Automation and Test in Europe. Conference and Exhibition 2001"},"title":"The Simulation Semantics of SystemC","date_created":"2023-01-24T10:39:33Z","author":[{"first_name":"Wolfgang","full_name":"Müller, Wolfgang","id":"16243","last_name":"Müller"},{"full_name":"Ruf, Jürgen","last_name":"Ruf","first_name":"Jürgen"},{"full_name":"Hoffmann, D. W.","last_name":"Hoffmann","first_name":"D. W."},{"last_name":"Gerlach","full_name":"Gerlach, Joachim","first_name":"Joachim"},{"full_name":"Kropf, Thomas","last_name":"Kropf","first_name":"Thomas"},{"full_name":"Rosenstiehl, W.","last_name":"Rosenstiehl","first_name":"W."}],"publisher":"IEEE","date_updated":"2023-01-24T10:39:38Z","status":"public","abstract":[{"text":"We present a rigorous but transparent semantics definition of SystemC that covers method, thread, and clocked thread behavior as well as their interaction with the simulation kernel process. The semantics includes watching statements, signal assignment, and wait statements as they are introduced in SystemC V1.O. We present our definition in form of distributed Abstract State Machines (ASMs) rules reflecting the view given in the SystemC User's Manual and the reference implementation. We mainly see our formal semantics as a concise, unambiguous, high-level specification for SystemC-based implementations and for standardization. Additionally, it can be used as a sound basis to investigate SystemC interoperability with Verilog and VHDL.","lang":"eng"}],"type":"conference","publication":"Proceedings of the Design, Automation, and Test in Europe (DATE’01)","language":[{"iso":"eng"}],"keyword":["Yarn","Formal verification","Kernel","Hardware design languages","Electronic design automation and methodology","Algebra","Computational modeling","Logic functions","Computer languages","Clocks"],"user_id":"5786","department":[{"_id":"672"}],"_id":"39421"},{"year":"1995","place":"Dordrecht","citation":{"bibtex":"@inbook{Börger_Glässer_Müller_1995, place={Dordrecht}, title={A Formal Definition of an Abstract VHDL’93 Simulator by EA-Machines}, DOI={<a href=\"https://doi.org/10.1007/978-1-4615-2237-9_5\">10.1007/978-1-4615-2237-9_5</a>}, booktitle={Semantics of VHDL}, publisher={Kluwer Academic Publishers}, author={Börger, Egon and Glässer, Uwe and Müller, Wolfgang}, editor={Delgado Kloos, C. and Breuer, Peter T.}, year={1995}, pages={107–139} }","short":"E. Börger, U. Glässer, W. Müller, in: C. Delgado Kloos, P.T. Breuer (Eds.), Semantics of VHDL, Kluwer Academic Publishers, Dordrecht, 1995, pp. 107–139.","mla":"Börger, Egon, et al. “A Formal Definition of an Abstract VHDL’93 Simulator by EA-Machines.” <i>Semantics of VHDL</i>, edited by C. Delgado Kloos and Peter T. Breuer, Kluwer Academic Publishers, 1995, pp. 107–39, doi:<a href=\"https://doi.org/10.1007/978-1-4615-2237-9_5\">10.1007/978-1-4615-2237-9_5</a>.","apa":"Börger, E., Glässer, U., &#38; Müller, W. (1995). A Formal Definition of an Abstract VHDL’93 Simulator by EA-Machines. In C. Delgado Kloos &#38; P. T. Breuer (Eds.), <i>Semantics of VHDL</i> (pp. 107–139). Kluwer Academic Publishers. <a href=\"https://doi.org/10.1007/978-1-4615-2237-9_5\">https://doi.org/10.1007/978-1-4615-2237-9_5</a>","ama":"Börger E, Glässer U, Müller W. A Formal Definition of an Abstract VHDL’93 Simulator by EA-Machines. In: Delgado Kloos C, Breuer PT, eds. <i>Semantics of VHDL</i>. Kluwer Academic Publishers; 1995:107-139. doi:<a href=\"https://doi.org/10.1007/978-1-4615-2237-9_5\">10.1007/978-1-4615-2237-9_5</a>","chicago":"Börger, Egon, Uwe Glässer, and Wolfgang Müller. “A Formal Definition of an Abstract VHDL’93 Simulator by EA-Machines.” In <i>Semantics of VHDL</i>, edited by C. Delgado Kloos and Peter T. Breuer, 107–39. Dordrecht: Kluwer Academic Publishers, 1995. <a href=\"https://doi.org/10.1007/978-1-4615-2237-9_5\">https://doi.org/10.1007/978-1-4615-2237-9_5</a>.","ieee":"E. Börger, U. Glässer, and W. Müller, “A Formal Definition of an Abstract VHDL’93 Simulator by EA-Machines,” in <i>Semantics of VHDL</i>, C. Delgado Kloos and P. T. Breuer, Eds. Dordrecht: Kluwer Academic Publishers, 1995, pp. 107–139."},"page":"107 - 139","publication_identifier":{"isbn":["978-1-4615-2237-9"]},"title":"A Formal Definition of an Abstract VHDL'93 Simulator by EA-Machines","doi":"10.1007/978-1-4615-2237-9_5","date_updated":"2022-12-15T11:43:14Z","publisher":"Kluwer Academic Publishers","author":[{"first_name":"Egon","last_name":"Börger","full_name":"Börger, Egon"},{"first_name":"Uwe","last_name":"Glässer","full_name":"Glässer, Uwe"},{"id":"16243","full_name":"Müller, Wolfgang","last_name":"Müller","first_name":"Wolfgang"}],"date_created":"2022-12-15T11:42:48Z","editor":[{"first_name":"C.","last_name":"Delgado Kloos","full_name":"Delgado Kloos, C."},{"last_name":"Breuer","full_name":"Breuer, Peter T.","first_name":"Peter T."}],"abstract":[{"text":"We present a rigorous but transparent semantic definition for VHDL corresponding to the IEEE VHDL’ 93 standard [68, 9, 84]. Our definition covers the full behavior of signal and variable assignments as well as the behavior of the various wait statements including delta, time, and postponed cycles. We consider explicitly declared signals, ports, local variables, and shared variables. Our specification defines an abstract VHDL ’ 93 interpreter in the form of transition rules for an evolving algebra machine (EA-Machine) [60]. It faithfully reflects and supports the view of simulation given in the IEEE VHDL ’ 93 standard language reference manual. The definition can be understood without any prior formal training. We illustrate our definition by running the example VHDL program set out in the Introduction to this volume.","lang":"eng"}],"status":"public","type":"book_chapter","publication":"Semantics of VHDL","keyword":["Transition Rule     Formal Verification     Variable Assignment     Kernel Process     Simulation Cycle"],"language":[{"iso":"eng"}],"_id":"34448","user_id":"5786","department":[{"_id":"672"}]}]