Generating concise assertions with complete coverage

Chen Hsuan Lin, Lingyi Liu, Shobha Vasudevan

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


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
Number of pages6
StatePublished - 2013
Externally publishedYes
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


Other23rd ACM International Conference of the Great Lakes Symposium on VLSI, GLSVLSI 2013


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

ASJC Scopus subject areas

  • Engineering(all)


Dive into the research topics of 'Generating concise assertions with complete coverage'. Together they form a unique fingerprint.

Cite this