“Partial Order Reduction for Deep Bug Finding in Synchronous Hardware” by Makai Mann and Clark Barrett. In Proceedings of the 26^th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '20), (Armin Biere and David Parker, eds.), Apr. 2020, pp. 367-386.
Symbolic model checking has become an important part of the verification flow in industrial hardware design. However, its use is still limited due to scaling issues. One way to address this is to exploit the large amounts of symmetry present in many real world designs. In this paper, we adapt partial order reduction for bounded model checking of synchronous hardware and introduce a novel technique that makes partial order reduction practical in this new domain. These approaches are largely automatic, requiring only minimal manual effort. We evaluate our technique on open-source and commercial packet mover circuits - designs containing FIFOs and arbiters.
BibTeX entry:
@inproceedings{MB20,
author = {Makai Mann and Clark Barrett},
editor = {Armin Biere and David Parker},
title = {Partial Order Reduction for Deep Bug Finding in Synchronous
Hardware},
booktitle = {Proceedings of the {\it 26^{th}} International Conference
on Tools and Algorithms for the Construction and Analysis of
Systems (TACAS '20)},
series = {Lecture Notes in Computer Science},
volume = {12078},
pages = {367--386},
publisher = {Springer},
month = apr,
year = {2020},
isbn = {978-3-030-45190-5},
url = {http://theory.stanford.edu/~barrett/pubs/MB20.pdf}
}
(This webpage was created with bibtex2web.)