Symbolic methods in simulation-based verification
| dc.contributor.advisor | Aziz, Adnan | en |
| dc.creator | Yuan, Jun | en |
| dc.date.accessioned | 2008-08-28T21:45:12Z | en |
| dc.date.available | 2008-08-28T21:45:12Z | en |
| dc.date.issued | 2002 | en |
| dc.description | text | en |
| dc.description.abstract | This dissertation conducts research in automating the design of digital hard- ware. Specifically we apply symbolic methods in simulation-based functional ver- ification. Simulation, due to its simplicity and close coupling with the electronic design process, has been the prevalent approach to checking the correctness of de- signs. However, it suffers from several drawbacks. First, simulation verifies only the portion of design behavior that is exercised by input vectors; in addition, input vector generation itself is a time-consuming and error-prone process. Both prob- lems are aggravated by the exponential growth in integrated circuit design com- plexity. On the other side, formal verification is “vector-less” in that it certifies cor- rectness either through mathematically rigorous proofs, or by exhaustive enumera- tion of design behaviors. Needless to mention, this approach requires either enor- mous computation resources or a great deal of manual intervention to verify large designs. The problem, however, is greatly alleviated by the advent of symbolic methods, particularly the introduction of Binary Decision Diagrams to represent sets of state and transition dynamics. Symbolic formal verification has since been adopted in practice, but still limited to simple protocols and small designs. It is natural to explore ways to leverage symbolic methods in simulation verification. To this end, we introduce several such applications. We first describe what we referred to as “saturated simulation” and “retrograde analysis” in checking invariant properties that are common to electronics designs. State and transition coverage are used as the guidance for a partial symbolic simulation. Consequently, a higher level of verification confidence is achieved. We then present a symbolic input vector generation method, in which state- dependent constraints and input biases are used to confine the generated vectors to “legal” and “interesting” cases. The constraints and biases are both of a dynamic nature, that is, they can depend upon the state of the design. This enables generation of complicated sequences of vectors. We also discuss methods of optimizing the vector generation process through efficient extraction of a special kind of constraints, in which the inputs are fully specified by the state of the design. In the end, we present an alternative vector gen- eration method based on constraint synthesis. Beyond its obvious role in simulation, the method also provides a constraint based interface model for other verification approaches, such as model checking and emulation. | |
| dc.description.department | Electrical and Computer Engineering | en |
| dc.format.medium | electronic | en |
| dc.identifier | b57476342 | en |
| dc.identifier.oclc | 57192614 | en |
| dc.identifier.proqst | 3108545 | en |
| dc.identifier.uri | http://hdl.handle.net/2152/1077 | en |
| dc.language.iso | eng | en |
| dc.rights | Copyright is held by the author. Presentation of this material on the Libraries' web site by University Libraries, The University of Texas at Austin was made possible under a limited license grant from the author who has retained all copyrights in the works. | en |
| dc.subject.lcsh | Integrated circuits--Verification | en |
| dc.subject.lcsh | Integrated circuits--Design and construction | en |
| dc.title | Symbolic methods in simulation-based verification | en |
| dc.type.genre | Thesis | en |