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.
CITATION STYLE
Mann, M., & Barrett, C. (2020). Partial order reduction for deep bug finding in synchronous hardware. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 12078 LNCS, pp. 367–386). Springer. https://doi.org/10.1007/978-3-030-45190-5_20
Mendeley helps you to discover research relevant for your work.