Optimizing automatic abstraction refinement for generalized symbolic trajectory evaluation

ABSTRACT

In this paper, we present a suite of optimizations targeting automatic abstraction refinement for Generalized Symbolic Trajectory Evaluation (GSTE). We optimize both model refinement and spec refinement supported by AutoGSTE: a counterexample-guided refinement loop for GSTE. Experiments on a family of benchmark circuits have shown that our optimizations lead to major efficiency improvements in verification involving abstraction refinement.

REFERENCES

• 1: Sara Adams , Magnus Bjork , Tom Melham , Carl-Johan Seger, Automatic Abstraction in Symbolic Trajectory Evaluation, Proceedings of the Formal Methods in Computer Aided Design, p.127-135, November 11-14, 2007 [doi>10.1109/FMCAD.2007.10]
• 2: R. Bryant and C.-J. Seger. Digital circuit verification using partially-ordered state models. In Twenty-Fourth International Symposium on Multiple-Valued Logic, 1994.
• 3: Yan Chen , Yujing He , Fei Xie , Jin Yang, Automatic Abstraction Refinement for Generalized Symbolic Trajectory Evaluation, Proceedings of the Formal Methods in Computer Aided Design, p.111-118, November 11-14, 2007 [doi>10.1109/FMCAD.2007.11]
• 4: Ching-Tsun Chou, The Mathematical Foundation fo Symbolic Trajectory Evaluation, Proceedings of the 11th International Conference on Computer Aided Verification, p.196-207, July 06-10, 1999
• 5: S. Hazelhurst and C.-J. Seger. A simple theorem prover based on symbolic trajectory evaluation and OBDDs. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 14(4), April 1995.
• 6: J.-W. Roorda and K. Claessen. SAT-based assistance to abstraction refinement for symbolic trajectory evaluation. In Proc. of CAV, 2006.
• 7: Carl-Johan H. Seger , Randal E. Bryant, Formal verification by symbolic evaluation of partially-ordered trajectories, Formal Methods in System Design, v.6 n.2, p.147-189, March 1995 [doi>10.1007/BF01383966]
• 8: C.-J. Seger, R. Jones, J. O'Leary, T. Melham, M. Aagaard, C. Barrett, and D. Syme. An industrially effective environment for formal hardware verification. IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems, 24(9), 2005.
• 9: R. Tzoref and O. Grumberg. Automatic refinement and vacuity detection for symbolic trajectory evaluation. In CAV, 2006.
• 10: Jin Yang , Carl-Johan H. Seger, Introduction to generalized symbolic trajectory evaluation, IEEE Transactions on Very Large Scale Integration (VLSI) Systems, v.11 n.3, p.345-353, June 2003 [doi>10.1109/TVLSI.2003.812320]

INDEX TERMS

Primary Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.3 Design Aids

General Terms:
Algorithms, Performance, Verification

Keywords:
automatic abstraction refinement, generalized symbolic trajectory evaluation, model checking