Show simple item record

dc.contributor.authorYang, Bo 12:57:30 (GMT) 12:57:30 (GMT)
dc.description.abstractWe propose a novel encoding called guard-value encoding for the ternary domain {0, 1, X}. Among the advantages it has over the more conventional dual-rail encoding, the flexibility of representing X with either of <0, 0> or <0, 1> is especially important. We develop data abstraction and memory abstraction techniques based on the guard-value encoding. Our data abstraction reduces much more of the state space than conventional ternary abstraction's approach of over-approximating a set of Boolean values with a smaller set of ternary values. We also show how our data abstraction can enable bit-width reduction which helps further simplify verification problems. Our memory abstraction is applicable to any array of elements which makes it much more general than the existing memory abstraction techniques. We show how our memory abstraction can effectively reduce an array to just a few elements even when existing approaches are not applicable. We make extensive use of symbolic indexing to construct symbolic ternary values which are used in symbolic simulation. Lastly, we give a new perspective on refinement for ternary abstraction. Refinement is needed when too much information is lost due to use of the ternary domain such that the property is evaluated to the unknown X. We present a collection of new refinement approaches that distinguish themselves from existing ones by modifying the transition function instead of the initial ternary state and ternary stimulus. This way, our refinement either preserves the abstraction level or only degrades it slightly. We demonstrate our proposed techniques with a wide range of designs and properties. With data abstraction, we usually observe at least 10X improvement in verification time compared to Boolean verification algorithms such as Boolean Bounded Model Checking (BMC), as well as usually at least 2X and often 10X improvement over conventional ternary abstraction. Our memory abstraction significantly improves how the verification time scales with the design parameters and the depth (the number of cycles) of the verification. Our refinement approaches are also demonstrated to be much better than existing ones most of the time. For example, when verifying a property of a synthetic example based on a superscalar microprocessor's bypass paths, with our data abstraction, it takes 505 seconds while both of ternary abstraction and BMC time out at 1800 seconds. The bit-width reduction can further save 44 seconds and our memory abstraction can save 237 seconds. This verification problem requires refinement. If we substitute our refinement with an existing approach, the verification time with the data abstraction doubles.en
dc.publisherUniversity of Waterlooen
dc.subjectformal verificationen
dc.subjectformal hardware verificationen
dc.subjectsymbolic trajectory evaluationen
dc.subjectmemory abstractionen
dc.subjectternary abstractionen
dc.subjectsymbolic simulationen
dc.subjectsymbolic indexingen
dc.subjectternary encodingen
dc.subjectabstraction refinementen
dc.subjectdata abstractionen
dc.titleAbstraction and Refinement Techniques for Ternary Symbolic Simulation with Guard-value Encodingen
dc.typeDoctoral Thesisen
dc.pendingfalse and Computer Engineeringen and Computer Engineeringen of Waterlooen
uws-etd.degreeDoctor of Philosophyen
uws.contributor.advisorAagaard, Mark
uws.contributor.affiliation1Faculty of Engineeringen

Files in this item


This item appears in the following Collection(s)

Show simple item record


University of Waterloo Library
200 University Avenue West
Waterloo, Ontario, Canada N2L 3G1
519 888 4883

All items in UWSpace are protected by copyright, with all rights reserved.

DSpace software

Service outages