TY - GEN
T1 - Generating concise assertions with complete coverage
AU - Lin, Chen Hsuan
AU - Liu, Lingyi
AU - Vasudevan, Shobha
PY - 2013
Y1 - 2013
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
AN - SCOPUS:84878171425
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
T2 - 23rd ACM International Conference of the Great Lakes Symposium on VLSI, GLSVLSI 2013
Y2 - 2 May 2013 through 3 May 2013
ER -