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:

• The main code of GSTE Symmetry
• The structure of Register Shifting Based FIFO
• The proof of Register Shifting Based FIFO
• The structure of Ring Buffer Based FIFO
• The proof of Ring Buffer Based FIFO
• The structure of Shift Memory
• The proof of Shift Memory

Some notes

• All the proof scripts have been checked by Forte.

---

March 29, 2011