Symbolic methods in simulation-based verification

dc.contributor.advisorAziz, Adnanen
dc.creatorYuan, Junen
dc.date.accessioned2008-08-28T21:45:12Zen
dc.date.available2008-08-28T21:45:12Zen
dc.date.issued2002en
dc.descriptiontexten
dc.description.abstractThis 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.departmentElectrical and Computer Engineeringen
dc.format.mediumelectronicen
dc.identifierb57476342en
dc.identifier.oclc57192614en
dc.identifier.proqst3108545en
dc.identifier.urihttp://hdl.handle.net/2152/1077en
dc.language.isoengen
dc.rightsCopyright 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.lcshIntegrated circuits--Verificationen
dc.subject.lcshIntegrated circuits--Design and constructionen
dc.titleSymbolic methods in simulation-based verificationen
dc.type.genreThesisen
thesis.degree.departmentElectrical and Computer Engineeringen
thesis.degree.disciplineElectrical and Computer Engineeringen
thesis.degree.grantorThe University of Texas at Austinen
thesis.degree.levelDoctoralen
thesis.degree.nameDoctor of Philosophyen

Access full-text files

Original bundle

Now showing 1 - 1 of 1
Loading...
Thumbnail Image
Name:
yuanj026.pdf
Size:
597.85 KB
Format:
Adobe Portable Document Format

License bundle

Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
1.65 KB
Format:
Plain Text
Description: