Formal Methods for Intellectual Property Composition Across Synchronization Domains

Simple item page
dc.contributor.authorSuhaib, Syed Mohammeden
dc.contributor.committeechairShukla, Sandeep K.en
dc.contributor.committeememberHsiao, Michael S.en
dc.contributor.committeememberHa, Dong Samen
dc.contributor.committeememberKachroo, Pushkinen
dc.contributor.committeememberShockley, James E.en
dc.contributor.departmentElectrical and Computer Engineeringen
dc.date.accessioned2014-03-14T20:16:10Zen
dc.date.adate2007-09-25en
dc.date.available2014-03-14T20:16:10Zen
dc.date.issued2007-08-29en
dc.date.rdate2007-09-25en
dc.date.sdate2007-09-12en
dc.description.abstractA significant part of the System-on-a-Chip (SoC) design problem is in the correct composition of intellectual property (IP) blocks. Ever increasing clock frequencies make it impossible for signals to reach from one end of the chip to the other end within a clock cycle; this invalidates the so-called synchrony assumption, where the timing of computation and communication are assumed to be negligible, and happen within a clock cycle. Missing the timing deadline causes this violation, and may have ramifications on the overall system reliability. Although latency insensitive protocols (LIPs) have been proposed as a solution to the problem of signal propagation over long interconnects, they have their own limitations. A more generic solution comes in the form of globally asynchronous locally synchronous (GALS) designs. However, composing synchronous IP blocks either over long multicycle delay interconnects or over asynchronous communication links for a GALS design is a challenging task, especially for ensuring the functional correctness of the overall design. In this thesis, we analyze various solutions for solving the synchronization problems related with IP composition. We present alternative LIPs, and provide a validation framework for ensuring their correctness. Our notion of correctness is that of latency equivalence between a latency insensitive design and its synchronous counterpart. We propose a trace-based framework for analyzing synchronous behaviors of different IPs, and provide a correct-by-construction protocol for their transformation to a GALS design. We also present a design framework for facilitating GALS designs. In the framework, Kahn process network specifications are refined into correct-by-construction GALS designs. We present formal definitions for the refinements towards different GALS architectures. For facilitating GALS in distributed embedded software, we analyze certain subclasses of synchronous designs using a Pomset-based semantic model that allows for desynchronization toward GALS.en
dc.description.degreePh. D.en
dc.identifier.otheretd-09122007-153123en
dc.identifier.sourceurlhttp://scholar.lib.vt.edu/theses/available/etd-09122007-153123/en
dc.identifier.urihttp://hdl.handle.net/10919/28952en
dc.publisherVirginia Techen
dc.relation.haspartssuhaib_etd.pdfen
dc.rightsIn Copyrighten
dc.rights.urihttp://rightsstatements.org/vocab/InC/1.0/en
dc.subjectGlobally Asynchronous Locally Synchronous Designsen
dc.subjectIntellectual Property Compositionen
dc.subjectLatency Insensitive Designsen
dc.subjectCorrect-by-Construction Protocolsen
dc.titleFormal Methods for Intellectual Property Composition Across Synchronization Domainsen
dc.typeDissertationen
thesis.degree.disciplineElectrical and Computer Engineeringen
thesis.degree.grantorVirginia Polytechnic Institute and State Universityen
thesis.degree.leveldoctoralen
thesis.degree.namePh. D.en

Files

Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
ssuhaib_etd.pdf
Size:
1.61 MB
Format:
Adobe Portable Document Format
Download

Collections

Doctoral Dissertations