טכניון מכון טכנולוגי לישראל
הטכניון מכון טכנולוגי לישראל - בית הספר ללימודי מוסמכים  
M.Sc Thesis
M.Sc StudentBrel Rachel
SubjectAutomatic Refinement and Vacuity Detection for Symbolic
Trajectory Evaluation
DepartmentDepartment of Computer Science
Supervisor Professor Orna Grumberg


Abstract

Model checking is an efficient procedure to check whether or not a given model fulfills a desired specification. Symbolic Trajectory Evaluation (STE) is a powerful technique for model checking of hardware circuits. It is applied to a circuit, described as a graph over nodes (gates and latches). The specification consists of assertions in a restricted temporal language. STE is based on 3-valued symbolic simulation, using 0, 1 and X ("unknown"). The X value is used to abstract away parts of the circuit. The abstraction is derived from the user's specification. STE computes a symbolic representation for each node at specific times. The size of this representation depends on the size of the specification, rather than on the circuit size. A refinement amounts to changing the assertion in order to present node values more accurately. Currently the process of abstraction and refinement in STE is performed manually. Our work presents an automatic refinement technique for STE. The technique is based on a clever selection of constraints that are added to the specification so that on the one hand the semantics of the original specification is preserved, and on the other hand, the part of the state space in which the "unknown" result is received is significantly decreased or totally eliminated. Selecting a "right" set of constraints has a crucial role in the success of the abstraction and refinement process: selecting too many constraints will add many variables to the computation of the symbolic representation, and may result in memory and time explosion. On the other hand, selecting too few constraints or selecting constraints that do not affect the result of the verification will lead to many iterations with an "unknown" result. Our experimental results show success in automatically identifying a set of constraints that are crucial for reaching a definite result. In addition, our work raises the problem of vacuity of passed and failed specifications. This problem was never discussed in the framework of STE. We describe when an STE specification may vacuously pass or fail, and propose a method for vacuity detection in STE.