An inlining approach to formal hardware semantics
Thesis: S.M., Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science, 2016.
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Language: | eng |
| Published: |
Massachusetts Institute of Technology
2016
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/1721.1/105576 |
| _version_ | 1811092095447859200 |
|---|---|
| author | Choi, Joonwon |
| author2 | Arvind. |
| author_facet | Arvind. Choi, Joonwon |
| author_sort | Choi, Joonwon |
| collection | MIT |
| description | Thesis: S.M., Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science, 2016. |
| first_indexed | 2024-09-23T15:12:35Z |
| format | Thesis |
| id | mit-1721.1/105576 |
| institution | Massachusetts Institute of Technology |
| language | eng |
| last_indexed | 2024-09-23T15:12:35Z |
| publishDate | 2016 |
| publisher | Massachusetts Institute of Technology |
| record_format | dspace |
| spelling | mit-1721.1/1055762019-04-11T06:42:04Z An inlining approach to formal hardware semantics Choi, Joonwon Arvind. Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science. Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science. Electrical Engineering and Computer Science. Thesis: S.M., Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science, 2016. This electronic version was submitted by the student author. The certified thesis is available in the Institute Archives and Special Collections. Cataloged from student-submitted PDF version of thesis. Includes bibliographical references (page 61). Hardware components are extremely complex due to concurrency. Modularity has been considered as an effective way to design and understand such complex hardware components. Among various hardware description languages (HDLs), Bluespec allows designers to develop hardware not only based on modularity, but also based on the notion of guarded atomic actions (GAAs). Following the concepts of modularity and GAA, we have been defining a framework called Kami to specify, verify, and synthesize Bluespec-style hardware components. However, modular semantics has an inherent weakness in that it is hard to infer internal changes. In this thesis, I present a new semantic approach based on inlining. Inlining semantics is defined for open hardware systems and resolves the weakness by construction. An implication from modular semantics to inlining semantics is also formally proven; thus the inlining semantics can be used to efficiently prove hardware properties. by Joonwon Choi. S.M. 2016-12-05T19:11:17Z 2016-12-05T19:11:17Z 2016 2016 Thesis http://hdl.handle.net/1721.1/105576 964450829 eng M.I.T. theses are protected by copyright. They may be viewed from this source for any purpose, but reproduction or distribution in any format is prohibited without written permission. See provided URL for inquiries about permission. http://dspace.mit.edu/handle/1721.1/7582 61 pages application/pdf Massachusetts Institute of Technology |
| spellingShingle | Electrical Engineering and Computer Science. Choi, Joonwon An inlining approach to formal hardware semantics |
| title | An inlining approach to formal hardware semantics |
| title_full | An inlining approach to formal hardware semantics |
| title_fullStr | An inlining approach to formal hardware semantics |
| title_full_unstemmed | An inlining approach to formal hardware semantics |
| title_short | An inlining approach to formal hardware semantics |
| title_sort | inlining approach to formal hardware semantics |
| topic | Electrical Engineering and Computer Science. |
| url | http://hdl.handle.net/1721.1/105576 |
| work_keys_str_mv | AT choijoonwon aninliningapproachtoformalhardwaresemantics AT choijoonwon inliningapproachtoformalhardwaresemantics |