“CoSA: Integrated Verification for Agile Hardware Design” by Cristian Mattarei, Makai Mann, Clark Barrett, Ross G. Daly, Dillon Huff, and Pat Hanrahan. In Proceedings of the 18^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '18), (Nikolaj Bjørner and Arie Gurfinkel, eds.), Oct. 2018, pp. 7-11. Austin, Texas.
Symbolic model-checking is a well-established technique used in hardware design to assess, and formally verify, functional correctness. However, most modern model-checkers encode the problem into propositional satisfiability (SAT) and do not leverage any additional information beyond the input design, which is typically provided in a hardware description language such as Verilog. In this paper, we present CoSA (CoreIR Symbolic Analyzer), a model-checking tool for CoreIR designs. CoreIR is a new intermediate representation for hardware. CoSA encodes model-checking queries into first-order formulas that can be solved by Satisfiability Modulo Theories (SMT) solvers. In particular, it natively supports encodings using the theories of bitvectors and arrays. CoSA is closely integrated with CoreIR and can thus leverage CoreIR-generated metadata in addition to user-provided lemmas to assist with formal verification. CoSA supports multiple input formats and provides a broad set of analyses including equivalence checking and safety and liveness verification. CoSA is open-source and written in Python, making it easily extendable.
BibTeX entry:
@inproceedings{MMB+18,
author = {Cristian Mattarei and Makai Mann and Clark Barrett and Ross
G. Daly and Dillon Huff and Pat Hanrahan},
editor = {Nikolaj Bj{\o}rner and Arie Gurfinkel},
title = {{CoSA}: Integrated Verification for Agile Hardware Design},
booktitle = {Proceedings of the {\it 18^{th}} International Conference
on Formal Methods In Computer-Aided Design (FMCAD '18)},
pages = {7--11},
publisher = {FMCAD Inc.},
month = oct,
year = {2018},
isbn = {978-0-9835678-8-2},
doi = {10.23919/FMCAD.2018.8603014},
note = {Austin, Texas},
url = {http://theory.stanford.edu/~barrett/pubs/MMB+18.pdf}
}
(This webpage was created with bibtex2web.)