- Library Home /
- Search Collections /
- Open Collections /
- Browse Collections /
- UBC Theses and Dissertations /
- ST to FL translation for hardware design verification
Open Collections
UBC Theses and Dissertations
UBC Theses and Dissertations
ST to FL translation for hardware design verification Lee, Wing Sang
Abstract
Due to the rapid advances of VLSI technology in the past two decades, complicated hardware designs are now practical and common. Such designs are difficult to verify. Traditionally, design validation had relied on simulation, but exhaustive simulation is impractical, and as designs get larger, simulation becomes more and more inadequate. In my research, I have developed rigorous, formal methods to verify hardware described in ST — a simple, intuitive hardware description language. This goal is achieved by translating hardware modeled in ST to an equivalent representation in FL — a general purpose functional language. With its built-in support for Ordered Binary Decision Diagrams (OBDDs), Boolean expressions can be easily and efficiently manipulated by FL programs. My research is mostly concentrated on safety property verification. Such properties assert that bad things don’t happen to the hardware designs. By using the weakest invari ant calculation algorithm designed, which is based primarily on Boolean manipulations, we are able to verify safety properties of ST programs efficiently. Moreover, a refinement rule is also defined. This refinement rule produces a safety property of an implementation description; it guarantees that all safety properties of its design specification also hold for the implementation. Consequently, we are able to verify a specification, and to verify that all subsequent refinements of the specification are suitable related.
Item Metadata
| Title |
ST to FL translation for hardware design verification
|
| Creator | |
| Publisher |
University of British Columbia
|
| Date Issued |
1994
|
| Description |
Due to the rapid advances of VLSI technology in the past two decades, complicated
hardware designs are now practical and common. Such designs are difficult to verify.
Traditionally, design validation had relied on simulation, but exhaustive simulation is
impractical, and as designs get larger, simulation becomes more and more inadequate.
In my research, I have developed rigorous, formal methods to verify hardware described
in ST — a simple, intuitive hardware description language. This goal is achieved by
translating hardware modeled in ST to an equivalent representation in FL — a general
purpose functional language. With its built-in support for Ordered Binary Decision
Diagrams (OBDDs), Boolean expressions can be easily and efficiently manipulated by
FL programs.
My research is mostly concentrated on safety property verification. Such properties
assert that bad things don’t happen to the hardware designs. By using the weakest invari
ant calculation algorithm designed, which is based primarily on Boolean manipulations,
we are able to verify safety properties of ST programs efficiently. Moreover, a refinement
rule is also defined. This refinement rule produces a safety property of an implementation
description; it guarantees that all safety properties of its design specification also hold
for the implementation. Consequently, we are able to verify a specification, and to verify
that all subsequent refinements of the specification are suitable related.
|
| Extent |
1442871 bytes
|
| Genre | |
| Type | |
| File Format |
application/pdf
|
| Language |
eng
|
| Date Available |
2009-02-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.0051293
|
| URI | |
| Degree | |
| Program | |
| Affiliation | |
| Degree Grantor |
University of British Columbia
|
| Graduation Date |
1994-05
|
| Campus | |
| Scholarly Level |
Graduate
|
| Aggregated Source Repository |
DSpace
|
Item Media
Loading media...
Item Citations and Data
Permanent URL (DOI):
Copied to clipboard.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.