Scaling RTL property checking using feasible path analysis and decomposition

Lingyi Liu, Shobha Vasudevan

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Property checking at the Register Transfer Level (RTL) is a critical problem for verifying complex digital design. In this paper, we present a scalable solution for property checking at RTL. We check the properties of the form G(A=>X=tB), which means that once A is valid, B should be valid t cycles later. We introduce a decomposition strategy to scale high level bounded property checking. This decomposition strategy partitions the monolithic SMT based BMC problem into multiple smaller, independent subproblems. Every path in the RTL program is analyzed for feasibility/relevance using (a) a hybrid of concrete and symbolic execution and (b) property based pruning using the antecedent condition A. The partitions of the RTL source code that correspond to the feasible paths are then checked with respect to the property of interest using an SMT solver. We manage to prune a large percentage of the RTL design paths using feasibility check, such that the decomposed subproblems are small and easily verifiable.

Original languageEnglish (US)
Title of host publicationGLSVLSI 2013 - Proceedings of the ACM International Conference of the Great Lakes Symposium on VLSI
Pages173-178
Number of pages6
DOIs
StatePublished - May 30 2013
Event23rd ACM International Conference of the Great Lakes Symposium on VLSI, GLSVLSI 2013 - Paris, France
Duration: May 2 2013May 3 2013

Publication series

NameProceedings of the ACM Great Lakes Symposium on VLSI, GLSVLSI

Other

Other23rd ACM International Conference of the Great Lakes Symposium on VLSI, GLSVLSI 2013
CountryFrance
CityParis
Period5/2/135/3/13

    Fingerprint

Keywords

  • property checking
  • rtl
  • symbolic execution

ASJC Scopus subject areas

  • Engineering(all)

Cite this

Liu, L., & Vasudevan, S. (2013). Scaling RTL property checking using feasible path analysis and decomposition. In GLSVLSI 2013 - Proceedings of the ACM International Conference of the Great Lakes Symposium on VLSI (pp. 173-178). (Proceedings of the ACM Great Lakes Symposium on VLSI, GLSVLSI). https://doi.org/10.1145/2483028.2483086