Combining Symmetry
Reduction with Generalized Symbolic Trajectory Evaluation
Yongjian
Li, Naiju Zeng, William N. N. Hung, Xiaoyu Song
Symbolic trajectory evaluation
(STE) is an efficient formal hardware verification method that has grown from
the combination of multi-valued simulation and symbolic simulation. One of the
main disadvantages of STE is that it can only deal with properties ranging over
a finite number of time-steps. Generalised Symbolic Trajectory Evaluation
(GSTE) is an extension of STE that can deal with properties ranging over
unbounded time. This extension is a double-edged sword. On one side, it
enhances the expressiveness of STE by GSTE assertion graphs. GSTE assertion
graphs can specify any omega-regular properties. On the other side, the
complexity of GSTE algorithms is also increased because fix-points computations
are involved while STE does not need these computations.
Symmetry reduction technique is very useful to reduce the complexity of
verification when symmetries abound in the circuits under verification. For
instance, data-dominated circuits such as memory modules intrinsically have
plenty of structure symmetries. Symmetry reduction has been combined with STE.
However, no work has tried to combine GSTE with symmetry reduction. In this
work, we try to bridge this gap in the literature. We try to design and
implement a sound methodology of symmetry reduction in a context of GSTE. In
this work, we focus on taking advantage of symmetry information to reduce the
assertion graphs under verification into smaller ones. The symmetry information
can either be obtained by type-checking or in-line checking the isomorphism of
graph of netlists. How to obtain the structure symmetry is not cared by us in
this paper.
Our implementation and case studies are as follows:
Some
notes
- All the
proof scripts have been checked by Forte.
March 29, 2011