UBC Theses and Dissertations

UBC Theses Logo

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 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.