A hierarchical approach to formal modeling and verification of asynchronous circuits

dc.contributor.advisorHunt, Warren A., 1958-
dc.contributor.committeeMemberGouda, Mohamed
dc.contributor.committeeMemberLifschitz, Vladimir
dc.contributor.committeeMemberRoncken, Marly
dc.contributor.committeeMemberSutherland, Ivan
dc.creatorChau, Cuong Kim
dc.creator.orcid0000-0002-9723-9557
dc.date.accessioned2019-07-10T15:37:12Z
dc.date.available2019-07-10T15:37:12Z
dc.date.created2019-05
dc.date.issued2019-06-17
dc.date.submittedMay 2019
dc.date.updated2019-07-10T15:37:13Z
dc.description.abstractThe self-timed (or asynchronous) approach to circuit design has demonstrated benefits in a number of different areas for its low energy consumption, high operating speed, composability, and modularity. Nonetheless, the asynchronous paradigm exposes challenges that are not found in the synchronous (or clock-driven) paradigm. For the verification task, a challenge emerges from the large number of potential operational interleavings exhibited in the asynchronous paradigm. Simply exploring all interleavings is, in general, intractable because the number of interleavings can grow exponentially. This dissertation focuses on developing scalable methods that are capable of reasoning effectively about the interleaving problem exhibited in self-timed systems. We specify and verify finite-state-machine representations of self-timed circuit designs using the DE system, a formal hardware description language defined using the ACL2 theorem-proving system. We apply a link-joint paradigm to model self-timed circuits as networks of channels that communicate with each other locally via handshake protocols. This link-joint model has been shown to be a universal model for various self-timed circuit families. In addition, this model has a clean formalization in the ACL2 logic and provides a protocol level that abstracts away timing constraints at the circuit level. Unlike many efforts for validating timing and communication properties of self-timed systems, we are interested in verifying functional properties. Specifically, we verify the functional correctness of self-timed systems in terms of relationships between their input and output sequences. To mitigate the consideration of all interleavings simultaneously, we address the verification problem hierarchically and avoid exploring the internal structures of verified submodules as well as their operational interleavings. The input-output relationship of a verified submodule is determined based on the communication signals at the submodule's input and output ports, while abstracting away all execution paths internal to that submodule.
dc.description.departmentComputer Sciences
dc.format.mimetypeapplication/pdf
dc.identifier.urihttps://hdl.handle.net/2152/75087
dc.identifier.urihttp://dx.doi.org/10.26153/tsw/2194
dc.language.isoen
dc.subjectAsynchronous circuit
dc.subjectFormal verification
dc.subjectHierarchical verification
dc.subjectNon-deterministic behavior
dc.subjectFunctional correctness
dc.subjectLink-joint model
dc.subjectMechanical theorem proving
dc.subjectACL2
dc.subjectHardware description language
dc.titleA hierarchical approach to formal modeling and verification of asynchronous circuits
dc.typeThesis
dc.type.materialtext
thesis.degree.departmentComputer Sciences
thesis.degree.disciplineComputer Science
thesis.degree.grantorThe University of Texas at Austin
thesis.degree.levelDoctoral
thesis.degree.nameDoctor of Philosophy
Files
Original bundle
Now showing 1 - 1 of 1
Loading...
Thumbnail Image
Name:
CHAU-DISSERTATION-2019.pdf
Size:
547.89 KB
Format:
Adobe Portable Document Format
License bundle
Now showing 1 - 2 of 2
No Thumbnail Available
Name:
PROQUEST_LICENSE.txt
Size:
4.45 KB
Format:
Plain Text
Description:
No Thumbnail Available
Name:
LICENSE.txt
Size:
1.84 KB
Format:
Plain Text
Description: