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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
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)
Gordon, M.: Directions in formal and semi-formal verification (2011). http://www.cl.cam.ac.uk/~mjcg/Research00/
Yang, J., Seger, C.J.H.: Introduction to generalized symbolic trajectory evaluation. IEEE Trans. VLSI Syst. 11(3), 345–353 (2003)
Yang, J., Goel, A.: GSTE through a case study. In: Pileggi, L.T., Kuehlmann, A. (eds.) ICCAD, pp. 534–541. ACM (2002)
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)
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
Technical Publications and Training, Intel Corporation: Forte/fl user guide, 2003 edn (2003)
Parameterized generalized symbolic trajetory eveluation. https://github.com/raphelIos/parametricGste
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_95
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)
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)
Jones, R.B.: Applications of symbolic simulation to the formal verification of microprocessors. Ph.D. thesis, Stanford, CA, USA (1999). AAI9958122
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
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
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)
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_8
Li, Y., et al.: An automatic proving approach to parameterized verification. ACM Trans. Comput. Logic 19(4), 27:1–27:25 (2018)
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.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Li, Y., Wang, By. (2019). Parameterized Hardware Verification Through a Term-Level Generalized Symbolic Trajectory Evaluation. In: Ait-Ameur, Y., Qin, S. (eds) Formal Methods and Software Engineering. ICFEM 2019. Lecture Notes in Computer Science(), vol 11852. Springer, Cham. https://doi.org/10.1007/978-3-030-32409-4_25
Download citation
DOI: https://doi.org/10.1007/978-3-030-32409-4_25
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-32408-7
Online ISBN: 978-3-030-32409-4
eBook Packages: Computer ScienceComputer Science (R0)