Dissertation/Thesis Abstract

Formal Modeling and Verification of Delay-Insensitive Circuits
by Park, Hoon, Ph.D., Portland State University, 2015, 187; 3743768
Abstract (Summary)

Einstein's relativity theory tells us that the notion of simultaneity can only be approximated for events distributed over space. As a result, the use of asynchronous techniques is unavoidable in systems larger than a certain physical size. Traditional design techniques that use global clocks face this barrier of scale already within the space of a modern microprocessor chip. The most common response by the chip industry for overcoming this barrier is to use Globally Asynchronous Locally Synchronous (GALS) design techniques. The circuits investigated in this thesis can be viewed as examples of GALS design. To make such designs trustworthy it is necessary to model formally the relative signal delays and timing requirements that make these designs work correctly. With trustworthy asynchrony one can build reliable, large, and scalable systems, and exploit the lower power and higher speed features of asynchrony.

This research presents ARCtimer, a framework for modeling, generating, verifying, and enforcing timing constraints for individual self-timed handshake components that use bounded-bundled-data handshake protocols. The constraints guarantee that the component's gate-level circuit implementation obeys the component's handshake protocol specification. Because the handshake protocols are delay insensitive, self-timed systems built using ARCtimer-verified components can be made delay insensitive. Any delay sensitivity inside a component is detected and repaired by ARCtimer. In short: by carefully considering time locally, we can ignore time globally.

ARCtimer applies early in the design process as part of building a library of verified components for later system use. The library also stores static timing analysis (STA) code to validate and enforce the component's constraints in any self-timed system built using the library. The library descriptions of a handshake component's circuit, protocol, timing constraints, and STA code are robust to circuit modifications applied later in the design process by technology mapping or layout tools.

New contributions of ARCtimer include: 1. Upfront modeling on a component by component basis to reduce the validation effort required to (a) reimplement components in different technologies, (b) assemble components into systems, and (c) guarantee system-level timing closure. 2. Modeling of bounded-bundled-data timing constraints that permit the control signals to lead or lag behind data signals to optimize system timing.

Indexing (document details)
Advisor: Song, Xiaoyu
Commitee: Hall, Douglas V., Li, Fu, Li, Jingke, Roncken, Marly, Teuscher, Christof
School: Portland State University
Department: Electrical and Computer Engineering
School Location: United States -- Oregon
Source: DAI-B 77/05(E), Dissertation Abstracts International
Subjects: Computer Engineering, Engineering, Electrical engineering
Keywords: Asynchronous circuits, Delay-insensitive protocol, Formal modeling and verification, Self-timed circuits, Static timing analysis, Timing closure
Publication Number: 3743768
ISBN: 978-1-339-36514-5
Copyright © 2020 ProQuest LLC. All rights reserved. Terms and Conditions Privacy Policy Cookie Policy