Professor, Computer Science dept., Technion, Haifa, Israel
Automatic Refinement and Vacuity Detection for Symbolic Trajectory Evaluation
Symbolic Trajectory Evaluation (STE) is a powerful technique
for model checking. 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. This
paper 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.
In addition, this paper 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.
This is a joint work with Rachel Tzoref