2010, En, EN , Thesis edition: Provably correct on-chip communication: a formal approach to automatic synthesis of SoC protocol converters Avnit, Karin, Computer Science & Engineering, Faculty of Engineering, UNSW

User activity

Send to:
 
Bookmark: http://trove.nla.gov.au/version/48127474
Physical Description
  • Thesis
  • PhD Doctorate
Published
  • Awarded By:University of New South Wales. Computer Science &​ Engineering , 2010
Language
  • En
  • EN

Edition details

Title
  • Provably correct on-chip communication: a formal approach to automatic synthesis of SoC protocol converters
Author
  • Avnit, Karin, Computer Science &​ Engineering, Faculty of Engineering, UNSW
Other Contributors
  • Sowmya, Arcot, Computer Science &​ Engineering, Faculty of Engineering, UNSW
  • Parameswaran, Sri, Computer Science &​ Engineering, Faculty of Engineering, UNSW
Published
  • Awarded By:University of New South Wales. Computer Science &​ Engineering , 2010
Physical Description
  • Thesis
  • PhD Doctorate
Subjects
Summary
  • The field of chip design is characterized by contradictory pressures to reduce time-to-market and maintain a high level of reliability. As a result, module reuse has become common practice in chip design. To save time on both design and verification, Systems-on-Chips (SoCs) are composed using pre-designed and pre-verified modules. The integrated modules are often designed by different groups and for different purposes, and are later integrated into a single chip. In the absence of a single interface standard for such modules, "plug-n-play" style integration is not likely, as the subject modules are often designed to comply with different interface protocols. For such modules to communicate correctly there is a need for some glue logic, also called a protocol converter that mediates between them. Though much research has been dedicated to the protocol converter synthesis problem of SoC communication, converter synthesis is still performed manually, consuming development and verification time and risking human error. Current approaches to automatic synthesis of protocol converters mostly lack formal foundations and either employ abstractions far removed from the Hardware Description Language (HDL) implementation level or grossly simplify the structure of the protocols considered. This thesis develops and presents techniques for automatic synthesis of provably correct on-chip protocol converters. Basing the solution on a formal approach, a novel state-machine based formalism is presented for modelling bus-based protocols and formalizing the notions of protocol compatibility and correct protocol conversion. Algorithms for automatic compatibility checking and provably-correct converter synthesis are derived from the formalism, including a systematic exploration of the design space of the protocol converter, the first in the field, which enables generation of various alternative deterministic converters. The work presented is unique in its combination of a completely formal approach and the use of a low abstraction level that enables precise modelling of protocol characteristics and automatic translation of the constructed converter to HDL.
Terms of Use
Language
  • En
  • EN
Related Resource
  • SHELF:T/​2010/​1 (Ask at Level 2 Information Desk, UNSW Library)
Identifier
  • oai:unsworks.unsw.edu.au:unsworks:8001

Get this edition

  • Set up My libraries

    How do I set up "My libraries"?

    In order to set up a list of libraries that you have access to, you must first login or sign up. Then set up a personal list of libraries from your profile page by clicking on your user name at the top right of any screen.

  • All (1)
  • NSW (1)
None of your libraries hold this item.
None of your libraries hold this item.

This single location in New South Wales:

Library Access Call number(s) Formats held Language
University of New South Wales. UNSW Library. Open to the public Thesis En; EN
Show 0 more libraries...
None of your libraries hold this item.
None of your libraries hold this item.
None of your libraries hold this item.
None of your libraries hold this item.
None of your libraries hold this item.
None of your libraries hold this item.

User activity


e.g. test cricket, Perth (WA), "Parkes, Henry"

Separate different tags with a comma. To include a comma in your tag, surround the tag with double quotes.

Be the first to add a tag for this edition

Be the first to add this to a list

Comments and reviews

What are comments? Add a comment

No user comments or reviews for this version

Add a comment