Title page for ETD etd-09122007-153123


Type of Document Dissertation
Author Suhaib, Syed Mohammed
Author's Email Address ssuhaib@vt.edu
URN etd-09122007-153123
Title Formal Methods for Intellectual Property Composition Across Synchronization Domains.
Degree PhD
Department Electrical and Computer Engineering
Advisory Committee
Advisor Name Title
Shukla, Sandeep K. Committee Chair
Ha, Dong Sam Committee Member
Hsiao, Michael S. Committee Member
Kachroo, Pushkin Committee Member
Shockley, James E. Committee Member
Keywords
  • Globally Asynchronous Locally Synchronous Designs
  • Intellectual Property Composition
  • Latency Insensitive Designs
  • Correct-by-Construction Protocols
Date of Defense 2007-08-29
Availability unrestricted
Abstract
A 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.

Files
  Filename       Size       Approximate Download Time (Hours:Minutes:Seconds) 
 
 28.8 Modem   56K Modem   ISDN (64 Kb)   ISDN (128 Kb)   Higher-speed Access 
  ssuhaib_etd.pdf 1.69 Mb 00:07:49 00:04:01 00:03:31 00:01:45 00:00:09

Browse All Available ETDs by ( Author | Department )

dla home
etds imagebase journals news ereserve special collections
virgnia tech home contact dla university libraries

If you have questions or technical problems, please Contact DLA.