- Library Home /
- Search Collections /
- Open Collections /
- Browse Collections /
- UBC Theses and Dissertations /
- Verifying a self-timed division chip
Open Collections
UBC Theses and Dissertations
UBC Theses and Dissertations
Verifying a self-timed division chip Ono-Tesfaye, Tarik
Abstract
The formal verification of asynchronous circuits is challenging, because they often have non-deterministic timing relations between circuit components. This thesis presents a formal proof strategy for verifying the correctness of a dual-rail, asynchronous divider chip. For that purpose, this thesis will extend timing verification techniques that were originally developed for combinational logic to apply to dual-rail, self-timed designs. The proof strategy is refinement based and employs four progressively more detailed models of the divider. Key safety properties are first established for the abstract models using model checking. These properties are then shown to hold for the more detailed models by verifying refinement between adjacent levels in the model hierarchy.
Item Metadata
Title |
Verifying a self-timed division chip
|
Creator | |
Publisher |
University of British Columbia
|
Date Issued |
1997
|
Description |
The formal verification of asynchronous circuits is challenging, because they often
have non-deterministic timing relations between circuit components. This thesis
presents a formal proof strategy for verifying the correctness of a dual-rail, asynchronous
divider chip. For that purpose, this thesis will extend timing verification
techniques that were originally developed for combinational logic to apply to dual-rail,
self-timed designs. The proof strategy is refinement based and employs four
progressively more detailed models of the divider. Key safety properties are first
established for the abstract models using model checking. These properties are then
shown to hold for the more detailed models by verifying refinement between adjacent
levels in the model hierarchy.
|
Extent |
3626084 bytes
|
Genre | |
Type | |
File Format |
application/pdf
|
Language |
eng
|
Date Available |
2009-03-26
|
Provider |
Vancouver : University of British Columbia Library
|
Rights |
For non-commercial purposes only, such as research, private study and education. Additional conditions apply, see Terms of Use https://open.library.ubc.ca/terms_of_use.
|
DOI |
10.14288/1.0050991
|
URI | |
Degree | |
Program | |
Affiliation | |
Degree Grantor |
University of British Columbia
|
Graduation Date |
1997-11
|
Campus | |
Scholarly Level |
Graduate
|
Aggregated Source Repository |
DSpace
|
Item Media
Item Citations and Data
Rights
For non-commercial purposes only, such as research, private study and education. Additional conditions apply, see Terms of Use https://open.library.ubc.ca/terms_of_use.