Efficient Equivalence Checking in a Modular Design Environment
Hasteer, Gagan
This item is only available for download by members of the University of Illinois community. Students, faculty, and staff at the U of I may log in with your NetID and password to view the item. If you are trying to access an Illinois-restricted dissertation or thesis, you can request a copy through your library's Inter-Library Loan office or purchase a copy directly from ProQuest.
Permalink
https://hdl.handle.net/2142/81909
Description
Title
Efficient Equivalence Checking in a Modular Design Environment
Author(s)
Hasteer, Gagan
Issue Date
1998
Doctoral Committee Chair(s)
Banerjee, Prithviraj
Department of Study
Computer Science
Discipline
Computer Science
Degree Granting Institution
University of Illinois at Urbana-Champaign
Degree Name
Ph.D.
Degree Level
Dissertation
Keyword(s)
Computer Science
Language
eng
Abstract
We address the issue of transforming multi-phase designs, a popular industry practice to equivalent one-phase designs to enable the application of the current equivalence checking techniques. We propose an algorithm to compute the steady states of a machine by relaxing the assumption of a designated set of initial states (DIS). This assumption is used in research but is often restrictive in an industrial design environment. We use the paradigm of sequential hardware equivalence (SHE), which does not make the DIS assumption, for checking the equivalence of two machines. We show that two machines are SHE if the outputs of their product machine are 0 in the steady states. We propose machine partitioning and minimum area retiming to alleviate the problem of large state spaces common in industrial designs. Our techniques result in exponential reductions in the state space and enable equivalence checking of machines which cannot be handled otherwise. Lastly, we address the issue of interface verification arising out of a modular design environment. We show that the constraints required to express the input don't care space for equivalence checking of a module need to be verified formally for the completeness of equivalence checking. We characterize these constraints as combinationally provable and sequentially provable. Subsequently, we develop an assertion checking framework with efficient techniques to handle both types of constraints.
Use this login method if you
don't
have an
@illinois.edu
email address.
(Oops, I do have one)
IDEALS migrated to a new platform on June 23, 2022. If you created
your account prior to this date, you will have to reset your password
using the forgot-password link below.
