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

Surface mount technology
Decomposition
Concretes

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

Scaling RTL property checking using feasible path analysis and decomposition. / Liu, Lingyi; Vasudevan, Shobha.

GLSVLSI 2013 - Proceedings of the ACM International Conference of the Great Lakes Symposium on VLSI. 2013. p. 173-178 (Proceedings of the ACM Great Lakes Symposium on VLSI, GLSVLSI).

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

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. Proceedings of the ACM Great Lakes Symposium on VLSI, GLSVLSI, pp. 173-178, 23rd ACM International Conference of the Great Lakes Symposium on VLSI, GLSVLSI 2013, Paris, France, 5/2/13. https://doi.org/10.1145/2483028.2483086
Liu L, Vasudevan S. 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. 2013. p. 173-178. (Proceedings of the ACM Great Lakes Symposium on VLSI, GLSVLSI). https://doi.org/10.1145/2483028.2483086
Liu, Lingyi ; Vasudevan, Shobha. / Scaling RTL property checking using feasible path analysis and decomposition. GLSVLSI 2013 - Proceedings of the ACM International Conference of the Great Lakes Symposium on VLSI. 2013. pp. 173-178 (Proceedings of the ACM Great Lakes Symposium on VLSI, GLSVLSI).
@inproceedings{5bd06f9310874782ae57f4dbd1e5bc75,
title = "Scaling RTL property checking using feasible path analysis and decomposition",
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.",
keywords = "property checking, rtl, symbolic execution",
author = "Lingyi Liu and Shobha Vasudevan",
year = "2013",
month = "5",
day = "30",
doi = "10.1145/2483028.2483086",
language = "English (US)",
isbn = "9781450319027",
series = "Proceedings of the ACM Great Lakes Symposium on VLSI, GLSVLSI",
pages = "173--178",
booktitle = "GLSVLSI 2013 - Proceedings of the ACM International Conference of the Great Lakes Symposium on VLSI",

}

TY - GEN

T1 - Scaling RTL property checking using feasible path analysis and decomposition

AU - Liu, Lingyi

AU - Vasudevan, Shobha

PY - 2013/5/30

Y1 - 2013/5/30

N2 - 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.

AB - 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.

KW - property checking

KW - rtl

KW - symbolic execution

UR - http://www.scopus.com/inward/record.url?scp=84878175881&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84878175881&partnerID=8YFLogxK

U2 - 10.1145/2483028.2483086

DO - 10.1145/2483028.2483086

M3 - Conference contribution

SN - 9781450319027

T3 - Proceedings of the ACM Great Lakes Symposium on VLSI, GLSVLSI

SP - 173

EP - 178

BT - GLSVLSI 2013 - Proceedings of the ACM International Conference of the Great Lakes Symposium on VLSI

ER -