“Unlocking the Power of Formal Hardware Verification with CoSA and Symbolic QED: Invited Paper” by Florian Lonsing, Karthik Ganesan, Makai Mann, Srinivasa Shashank Nuthakki, Eshan Singh, Mario Srouji, Yahan Yang, Subhasish Mitra, and Clark Barrett. In Proceedings of the International Conference on Computer-Aided Design (ICCAD '19), (David Pan, ed.), Nov. 2019. Westminster, Colorado.
As designs grow in size and complexity, design verification becomes one of the most difficult and costly tasks facing design teams. Formal verification techniques offer great promise because of their ability to exhaustively explore design behaviors. However, formal techniques also have a reputation for being labor-intensive and limited to small blocks. Is there any hope for successful application of formal techniques at design scale? We answer this question affirmatively by digging deeper to understand what the real technological issues and opportunities are. First, we look at satisfiability solvers, the engines underlying formal techniques such as model checking. Given the recent innovations in satisfiability solving, we argue that there are many reasons to be optimistic that formal techniques will scale to designs of practical interest. We use our CoSA model checker as a demonstration platform to illustrate how advances in solvers can improve scalability. However, even if solvers become blazingly fast, applying them well is still labor-intensive. This is because formal tools are only as useful as the properties they are given to prove, which traditionally have required great effort to develop. Symbolic quick error detection (SQED) addresses this issue by using a single, universal property that checks designs automatically. We demonstrate how SQED can automatically find logic bugs in a variety of designs and report on bugs found and efficiency gains realized in academic and industry designs. We also present a generator for an improved SQED module that further reduces the amount of manual effort that has to be spent by the designer.
BibTeX entry:
@inproceedings{LGM+19,
author = {Florian Lonsing and Karthik Ganesan and Makai Mann and
Srinivasa Shashank Nuthakki and Eshan Singh and Mario Srouji and
Yahan Yang and Subhasish Mitra and Clark Barrett},
editor = {David Pan},
title = {Unlocking the Power of Formal Hardware Verification with
{CoSA} and Symbolic {QED}: Invited Paper},
booktitle = {Proceedings of the International Conference on
Computer-Aided Design (ICCAD '19)},
publisher = {IEEE},
month = nov,
year = {2019},
doi = {10.1109/ICCAD45719.2019.8942096},
note = {Westminster, Colorado},
url = {http://theory.stanford.edu/~barrett/pubs/LGM+19.pdf}
}
(This webpage was created with bibtex2web.)