Technical Report MSC-2006-22

Title: Automatic Refinement and Vacuity Detection for Symbolic Trajectory Evaluation
Authors: Rachel Tzoref
Supervisors: 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 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. 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. 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.
CopyrightThe above paper is copyright by the Technion, Author(s), or others. Please contact the author(s) for more information

Remark: Any link to this technical report should be to this page (, rather than to the URL of the PDF files directly. The latter URLs may change without notice.

To the list of the MSC technical reports of 2006
To the main CS technical reports page

Computer science department, Technion