Exploring Structural Symmetry Automatically in Symbolic Trajectory Evaluation

Yongjian Li, William N. N. Hung, Xiaoyu Song, Naiju Zeng

---

Symbolic trajectory evaluation (STE) is an efficient formal hardware verification method that has grown from the combination of multi-valued simulaiton and symbolic simulation. It has shown great promise in verifying medium to large scale industrial hardware designs with a higher degree of automation. Moreover, symmetry reduction technique is very useful to reduce the complexity of verification when symmetries abound in the circuits under verification.

In this paper, we solve two challenge problems in combining symmetry reduction with STE. The first is a theoretical result to indentify symmetry sormally, to introduce the symmetry reduction theorem, and to prove its soundness. The second is to provide an effective implementation of symmetry reduction method.

Our implementation and symmetry tables generated during proof procedure are as follows:

• The main code of the theorem prover
• The netlist of CAM
• The proof of CAM
• The symmetry table of CAM
• The netlist of FIFO
• The proof of FIFO
• The symmetry table of FIFO

Some notes

• All the proof scripts have been checked by Forte.

Formalization on Semantics of Symbolic Trajectory Evaluation in Isabelle (including Formalization on Netlists)

• Isabelle theory in Isabelle 2005.(thy files or html files)
• Long version of technique report.

---

October 29, 2010