Generating concise assertions with complete coverage

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.