[{"type":"dissertation","status":"public","user_id":"3118","department":[{"_id":"78"}],"project":[{"name":"SFB 901","_id":"1"},{"_id":"3","name":"SFB 901 - Project Area B"},{"_id":"12","name":"SFB 901 - Subproject B4"}],"_id":"26746","publication_status":"published","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.","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."},"page":"293","place":"Paderborn","supervisor":[{"full_name":"Platzner, Marco","id":"398","last_name":"Platzner","first_name":"Marco"}],"author":[{"first_name":"Tobias","full_name":"Wiersema, Tobias","id":"3118","last_name":"Wiersema"}],"oa":"1","date_updated":"2022-01-06T06:57:26Z","main_file_link":[{"open_access":"1","url":"https://nbn-resolving.de/urn:nbn:de:hbz:466:2-39800"}],"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"}],"language":[{"iso":"eng"}],"ddc":["006"],"keyword":["Proof-Carrying Hardware","Formal Verification","Sequential Circuits","Non-Functional Properties","Functional Properties"],"year":"2021","date_created":"2021-10-25T06:35:41Z","publisher":"Paderborn University","title":"Guaranteeing Properties of Reconfigurable Hardware Circuits with Proof-Carrying Hardware"},{"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>.","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} }","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."},"publication_identifier":{"eissn":["1557-9999"],"issn":["1063-8210"]},"publication_status":"published","doi":"10.1109/TVLSI.2020.3008061","volume":28,"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"},{"last_name":"Platzner","id":"398","full_name":"Platzner, Marco","first_name":"Marco"}],"date_updated":"2022-01-06T06:53:09Z","status":"public","type":"journal_article","funded_apc":"1","article_type":"original","department":[{"_id":"78"}],"user_id":"49051","_id":"17358","project":[{"_id":"12","name":"SFB 901 - Subproject B4"},{"_id":"3","name":"SFB 901 - Project Area B"},{"_id":"1","name":"SFB 901"}],"year":"2020","issue":"9","quality_controlled":"1","title":"Proof-carrying Approximate Circuits","date_created":"2020-07-06T11:21:30Z","publisher":"IEEE","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","language":[{"iso":"eng"}],"keyword":["Approximate circuit synthesis","approximate computing","error metrics","formal verification","proof-carrying hardware"]},{"year":"2018","citation":{"apa":"Jentzsch, F. P. (2018). <i>Enforcing IP Core Connection Properties with Verifiable Security Monitors</i>. Universität Paderborn.","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.","bibtex":"@book{Jentzsch_2018, title={Enforcing IP Core Connection Properties with Verifiable Security Monitors}, publisher={Universität Paderborn}, author={Jentzsch, Felix Paul}, year={2018} }","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."},"date_updated":"2022-01-06T06:50:54Z","publisher":"Universität Paderborn","date_created":"2018-01-15T16:48:05Z","author":[{"first_name":"Felix Paul","full_name":"Jentzsch, Felix Paul","last_name":"Jentzsch"}],"supervisor":[{"first_name":"Tobias","id":"3118","full_name":"Wiersema, Tobias","last_name":"Wiersema"}],"title":"Enforcing IP Core Connection Properties with Verifiable Security Monitors","type":"bachelorsthesis","status":"public","_id":"1097","project":[{"name":"SFB 901 - Subproject B4","_id":"12"},{"_id":"1","name":"SFB 901"},{"name":"SFB 901 - Project Area B","_id":"3"}],"department":[{"_id":"78"}],"user_id":"477","keyword":["Approximate Computing","Proof-Carrying Hardware","Formal Verification"],"language":[{"iso":"eng"}]},{"status":"public","abstract":[{"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.","lang":"eng"}],"type":"conference","publication":"Proceedings of SEFM´04","language":[{"iso":"eng"}],"keyword":["Unified modeling language","Logic","Clocks","Boolean functions","Application software","Time factors","Real time systems","Formal verification","Buffer storage","Software packages"],"user_id":"5786","department":[{"_id":"672"}],"_id":"39069","citation":{"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>","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>.","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>","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>.","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} }"},"place":"Beijing, China","year":"2004","publication_identifier":{"isbn":["0-7695-2222-X"]},"doi":"10.1109/SEFM.2004.1347516","conference":{"name":" Proceedings of the Second International Conference on Software Engineering and Formal Methods"},"title":"Past- and Future-Oriented Time-Bound Temporal Properties with OCL","author":[{"full_name":"Flake, Stephan","last_name":"Flake","first_name":"Stephan"},{"first_name":"Wolfgang","id":"16243","full_name":"Müller, Wolfgang","last_name":"Müller"}],"date_created":"2023-01-24T09:03:36Z","date_updated":"2023-01-24T09:03:41Z","publisher":"IEEE"},{"user_id":"5786","department":[{"_id":"672"}],"_id":"39382","language":[{"iso":"eng"}],"keyword":["Standardization","Kernel","Permission","Formal verification","Logic functions","Documentation","Reasoning about programs","Specification languages","Formal specifications","Software systems"],"type":"conference","publication":"Proceedings of the ISSS02","status":"public","abstract":[{"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.","lang":"eng"}],"author":[{"first_name":"Wolfgang","last_name":"Müller","id":"16243","full_name":"Müller, Wolfgang"},{"first_name":"Rainer","full_name":"Dömer, Rainer","last_name":"Dömer"},{"first_name":"Andreas","last_name":"Gerstlauer","full_name":"Gerstlauer, Andreas"}],"date_created":"2023-01-24T10:10:24Z","date_updated":"2023-01-24T10:10:28Z","doi":"10.1145/581199.581234 ","title":"The Formal Execution Semantics of SpecC","publication_identifier":{"isbn":["1-58113-576-9"]},"citation":{"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>","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>.","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>.","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>","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} }","short":"W. Müller, R. Dömer, A. Gerstlauer, in: Proceedings of the ISSS02, Nagoya, Japan, 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>."},"place":"Nagoya, Japan","year":"2002"},{"date_updated":"2023-01-24T10:22:16Z","date_created":"2023-01-24T10:22:12Z","author":[{"last_name":"Flake","full_name":"Flake, Stephan","first_name":"Stephan"},{"first_name":"Wolfgang","last_name":"Müller","id":"16243","full_name":"Müller, Wolfgang"}],"title":"Specification of Real-Time Properties for UML Models","doi":"10.1109/HICSS.2002.994469","conference":{"name":"Proceedings of the 35th Annual Hawaii International Conference on System Sciences","location":"Big Island, HI, USA "},"publication_identifier":{"isbn":["0-7695-1435-9"]},"year":"2002","place":"Big Island, HI, USA ","citation":{"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>.","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} }","short":"S. Flake, W. Müller, in: Proceedings of HICSS-35, Big Island, HI, USA , 2002.","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>","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>.","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>.","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>"},"_id":"39403","user_id":"5786","department":[{"_id":"672"}],"keyword":["Unified modeling language","Logic","Formal verification","Real time systems","Programming profession","Vehicle dynamics","Software standards","Flexible manufacturing systems","Electronics industry","Protocols"],"language":[{"iso":"eng"}],"type":"conference","publication":"Proceedings of HICSS-35","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"}],"status":"public"},{"year":"2001","place":"Munich, Germany ","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.","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>.","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>.","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>"},"publication_identifier":{"isbn":["0-7695-0993-2"]},"title":"The Simulation Semantics of SystemC","conference":{"name":" Proceedings Design, Automation and Test in Europe. Conference and Exhibition 2001"},"doi":"10.1109/DATE.2001.915002","date_updated":"2023-01-24T10:39:38Z","publisher":"IEEE","date_created":"2023-01-24T10:39:33Z","author":[{"first_name":"Wolfgang","last_name":"Müller","id":"16243","full_name":"Müller, Wolfgang"},{"first_name":"Jürgen","full_name":"Ruf, Jürgen","last_name":"Ruf"},{"full_name":"Hoffmann, D. W.","last_name":"Hoffmann","first_name":"D. W."},{"first_name":"Joachim","full_name":"Gerlach, Joachim","last_name":"Gerlach"},{"first_name":"Thomas","last_name":"Kropf","full_name":"Kropf, Thomas"},{"full_name":"Rosenstiehl, W.","last_name":"Rosenstiehl","first_name":"W."}],"abstract":[{"lang":"eng","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."}],"status":"public","publication":"Proceedings of the Design, Automation, and Test in Europe (DATE’01)","type":"conference","keyword":["Yarn","Formal verification","Kernel","Hardware design languages","Electronic design automation and methodology","Algebra","Computational modeling","Logic functions","Computer languages","Clocks"],"language":[{"iso":"eng"}],"_id":"39421","department":[{"_id":"672"}],"user_id":"5786"},{"department":[{"_id":"672"}],"user_id":"5786","_id":"34448","language":[{"iso":"eng"}],"keyword":["Transition Rule     Formal Verification     Variable Assignment     Kernel Process     Simulation Cycle"],"publication":"Semantics of VHDL","type":"book_chapter","status":"public","editor":[{"last_name":"Delgado Kloos","full_name":"Delgado Kloos, C.","first_name":"C."},{"first_name":"Peter T.","full_name":"Breuer, Peter T.","last_name":"Breuer"}],"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"}],"author":[{"first_name":"Egon","last_name":"Börger","full_name":"Börger, Egon"},{"full_name":"Glässer, Uwe","last_name":"Glässer","first_name":"Uwe"},{"first_name":"Wolfgang","id":"16243","full_name":"Müller, Wolfgang","last_name":"Müller"}],"date_created":"2022-12-15T11:42:48Z","date_updated":"2022-12-15T11:43:14Z","publisher":"Kluwer Academic Publishers","doi":"10.1007/978-1-4615-2237-9_5","title":"A Formal Definition of an Abstract VHDL'93 Simulator by EA-Machines","publication_identifier":{"isbn":["978-1-4615-2237-9"]},"page":"107 - 139","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} }","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>.","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.","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>","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.","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>."},"place":"Dordrecht","year":"1995"}]