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

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