Advertisement

Parameterized Hardware Verification Through a Term-Level Generalized Symbolic Trajectory Evaluation

  • Yongjian LiEmail author
  • Bow-yaw Wang
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11852)

Abstract

This paper proposes a term-level generalized symbolic trajectory evaluation (GSTE) to tackle parameterized hardware verification. We develop a theorem-proving technique for parameterized GSTE verification. In our technique, a constraint is associated with a node in GSTE graphs to specify reachable states. Generalized inductive relations between nodes of GSTE graphs are formulated; instantaneous implications are formalized on edges of GSTE graphs. Based on these formalization, parameterized GSTE are verified. We moreover formalize our techniques in Isabelle. We demonstrate the effectiveness of our techniques in case studies. Interestingly, subtleties between different implementations of FIFOs are discovered by our parameterized verification although these circuits have been extensively studied previously.

Notes

Acknowledgements

Yongjian Li is supported by grant 61672503 from National Natural Science Foundation and grant 2017YFB0801900 from the National Key Research and Development Program in China.

References

  1. 1.
    Seger, C.J.H., Bryant, R.E.: Formal verification by symbolic evaluation of partially-ordered trajectories. Formal Meth. Syst. Des. 6(2), 147–189 (1995)CrossRefGoogle Scholar
  2. 2.
    Gordon, M.: Directions in formal and semi-formal verification (2011). http://www.cl.cam.ac.uk/~mjcg/Research00/
  3. 3.
    Yang, J., Seger, C.J.H.: Introduction to generalized symbolic trajectory evaluation. IEEE Trans. VLSI Syst. 11(3), 345–353 (2003)CrossRefGoogle Scholar
  4. 4.
    Yang, J., Goel, A.: GSTE through a case study. In: Pileggi, L.T., Kuehlmann, A. (eds.) ICCAD, pp. 534–541. ACM (2002)Google Scholar
  5. 5.
    Seger, C.J.H., et al.: An industrially effective environment for formal hardware verification. IEEE Trans. Comput. -Aided Des. Integrated Circ. Syst. 24(9), 1381–1405 (2005)Google Scholar
  6. 6.
    Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL — A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002).  https://doi.org/10.1007/3-540-45949-9
  7. 7.
    Technical Publications and Training, Intel Corporation: Forte/fl user guide, 2003 edn (2003)Google Scholar
  8. 8.
    Parameterized generalized symbolic trajetory eveluation. https://github.com/raphelIos/parametricGste
  9. 9.
    Brayton, R.K., et al.: VIS: A system for verification and synthesis. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 428–432. Springer, Heidelberg (1996).  https://doi.org/10.1007/3-540-61474-5_95CrossRefGoogle Scholar
  10. 10.
    Adams, S., Bjork, M., Melham, T., Seger, C.J.: Automatic abstraction in symbolic trajectory evaluation. In: FMCAD 2007: Proceedings of the Formal Methods in Computer Aided Design, pp. 127–135. IEEE Computer Society, Washington, DC, USA (2007)Google Scholar
  11. 11.
    Pandey, M., Raimi, R., Bryant, R.E., Abadir, M.S.: Formal verification of content addressable memories using symbolic trajectory evaluation. In: DAC 1997: Proceedings of the 34th annual Design Automation Conference. pp. 167–172. ACM, New York, NY, USA (1997)Google Scholar
  12. 12.
    Jones, R.B.: Applications of symbolic simulation to the formal verification of microprocessors. Ph.D. thesis, Stanford, CA, USA (1999). AAI9958122Google Scholar
  13. 13.
    Adams, S., Björk, M., Melham, T., Seger, C.J.: Automatic abstraction in symbolic trajectory evaluation. In: Baumgartner, J., Sheeran, M. (eds.) Formal Methods in Computer Aided Design: FMCAD 2007: November 11–14 2007, Austin, Texas, USA. pp. 127–135. IEEE Computer Society (2007). http://www.cs.ox.ac.uk/tom.melham/pub/Adams-2007-AAS.pdf
  14. 14.
    Chen, Y., Xie, F., Yang, J.: Optimizing automatic abstraction refinement for generalized symbolic trajectory evaluation. In: Proceedings of the 45th Annual Design Automation Conference, pp. 143–148. DAC 2008, ACM, New York, NY, USA (2008). http://doi.acm.org/10.1145/1391469.1391508
  15. 15.
    Li, Y., Zeng, N., Hung, W.N.N., Song, X.: Combining symmetry reduction with generalized symbolic trajectory evaluation. Comput. J. 57(1), 115–128 (2014)CrossRefGoogle Scholar
  16. 16.
    Chakraborty, S., et al.: Word-Level Symbolic Trajectory Evaluation. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 128–143. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-21668-3_8CrossRefGoogle Scholar
  17. 17.
    Li, Y., et al.: An automatic proving approach to parameterized verification. ACM Trans. Comput. Logic 19(4), 27:1–27:25 (2018)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.State Key Laboratory of Computer Science, Institute of SoftwareChinese Academy of SciencesBeijingChina
  2. 2.Institute of Information Science Academia SinicaTaipeiTaiwan

Personalised recommendations