Generating concise assertions with complete coverage

Chen Hsuan Lin, Lingyi Liu, Shobha Vasudevan

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

Abstract

Assertions are valuable and commonly applied to formal verification and simulation-based verification in IC design flow. Unfortunately, assertion generation is a time-consuming process that depends heavily on human efforts. Some dynamic methods based on simulation and static methods based on structure analysis are proposed to automate assertion generation process. However, dynamic methods cannot guarantee the quality of assertions due to incomplete simulation while static methods might have scalability limits. With the significant advances in Boolean satisfiability (SAT) solving, SAT solving becomes a promising technique to overcome these methods' weaknesses. In this paper, we successfully formulate assertion generation to a SAT problem and use unit assumption to generate concise assertions. Furthermore, we consider input constraints and word level features to generate meaningful and high-readability assertions. Experimental results on SpaceWire, Ethernet, and Floating Point designs show that the generated assertions can always achieve 100% input space coverage.

Original languageEnglish (US)
Title of host publicationGLSVLSI 2013 - Proceedings of the ACM International Conference of the Great Lakes Symposium on VLSI
Pages185-190
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

Ethernet
Scalability
Integrated circuit design
Formal verification

Keywords

  • assertion generation
  • complete coverage
  • input constraints
  • word level features

ASJC Scopus subject areas

  • Engineering(all)

Cite this

Lin, C. H., Liu, L., & Vasudevan, S. (2013). Generating concise assertions with complete coverage. In GLSVLSI 2013 - Proceedings of the ACM International Conference of the Great Lakes Symposium on VLSI (pp. 185-190). (Proceedings of the ACM Great Lakes Symposium on VLSI, GLSVLSI). https://doi.org/10.1145/2483028.2483088

Generating concise assertions with complete coverage. / Lin, Chen Hsuan; Liu, Lingyi; Vasudevan, Shobha.

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

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

Lin, CH, Liu, L & Vasudevan, S 2013, Generating concise assertions with complete coverage. 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. 185-190, 23rd ACM International Conference of the Great Lakes Symposium on VLSI, GLSVLSI 2013, Paris, France, 5/2/13. https://doi.org/10.1145/2483028.2483088
Lin CH, Liu L, Vasudevan S. Generating concise assertions with complete coverage. In GLSVLSI 2013 - Proceedings of the ACM International Conference of the Great Lakes Symposium on VLSI. 2013. p. 185-190. (Proceedings of the ACM Great Lakes Symposium on VLSI, GLSVLSI). https://doi.org/10.1145/2483028.2483088
Lin, Chen Hsuan ; Liu, Lingyi ; Vasudevan, Shobha. / Generating concise assertions with complete coverage. GLSVLSI 2013 - Proceedings of the ACM International Conference of the Great Lakes Symposium on VLSI. 2013. pp. 185-190 (Proceedings of the ACM Great Lakes Symposium on VLSI, GLSVLSI).
@inproceedings{445b232da1a34e468023b9d5d1d20c3a,
title = "Generating concise assertions with complete coverage",
abstract = "Assertions are valuable and commonly applied to formal verification and simulation-based verification in IC design flow. Unfortunately, assertion generation is a time-consuming process that depends heavily on human efforts. Some dynamic methods based on simulation and static methods based on structure analysis are proposed to automate assertion generation process. However, dynamic methods cannot guarantee the quality of assertions due to incomplete simulation while static methods might have scalability limits. With the significant advances in Boolean satisfiability (SAT) solving, SAT solving becomes a promising technique to overcome these methods' weaknesses. In this paper, we successfully formulate assertion generation to a SAT problem and use unit assumption to generate concise assertions. Furthermore, we consider input constraints and word level features to generate meaningful and high-readability assertions. Experimental results on SpaceWire, Ethernet, and Floating Point designs show that the generated assertions can always achieve 100{\%} input space coverage.",
keywords = "assertion generation, complete coverage, input constraints, word level features",
author = "Lin, {Chen Hsuan} and Lingyi Liu and Shobha Vasudevan",
year = "2013",
month = "5",
day = "30",
doi = "10.1145/2483028.2483088",
language = "English (US)",
isbn = "9781450319027",
series = "Proceedings of the ACM Great Lakes Symposium on VLSI, GLSVLSI",
pages = "185--190",
booktitle = "GLSVLSI 2013 - Proceedings of the ACM International Conference of the Great Lakes Symposium on VLSI",

}

TY - GEN

T1 - Generating concise assertions with complete coverage

AU - Lin, Chen Hsuan

AU - Liu, Lingyi

AU - Vasudevan, Shobha

PY - 2013/5/30

Y1 - 2013/5/30

N2 - Assertions are valuable and commonly applied to formal verification and simulation-based verification in IC design flow. Unfortunately, assertion generation is a time-consuming process that depends heavily on human efforts. Some dynamic methods based on simulation and static methods based on structure analysis are proposed to automate assertion generation process. However, dynamic methods cannot guarantee the quality of assertions due to incomplete simulation while static methods might have scalability limits. With the significant advances in Boolean satisfiability (SAT) solving, SAT solving becomes a promising technique to overcome these methods' weaknesses. In this paper, we successfully formulate assertion generation to a SAT problem and use unit assumption to generate concise assertions. Furthermore, we consider input constraints and word level features to generate meaningful and high-readability assertions. Experimental results on SpaceWire, Ethernet, and Floating Point designs show that the generated assertions can always achieve 100% input space coverage.

AB - Assertions are valuable and commonly applied to formal verification and simulation-based verification in IC design flow. Unfortunately, assertion generation is a time-consuming process that depends heavily on human efforts. Some dynamic methods based on simulation and static methods based on structure analysis are proposed to automate assertion generation process. However, dynamic methods cannot guarantee the quality of assertions due to incomplete simulation while static methods might have scalability limits. With the significant advances in Boolean satisfiability (SAT) solving, SAT solving becomes a promising technique to overcome these methods' weaknesses. In this paper, we successfully formulate assertion generation to a SAT problem and use unit assumption to generate concise assertions. Furthermore, we consider input constraints and word level features to generate meaningful and high-readability assertions. Experimental results on SpaceWire, Ethernet, and Floating Point designs show that the generated assertions can always achieve 100% input space coverage.

KW - assertion generation

KW - complete coverage

KW - input constraints

KW - word level features

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

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

U2 - 10.1145/2483028.2483088

DO - 10.1145/2483028.2483088

M3 - Conference contribution

SN - 9781450319027

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

SP - 185

EP - 190

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

ER -