An inlining approach to formal hardware semantics

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