Partial Order Reduction for Deep Bug Finding
in Synchronous Hardware
Makai Mann and Clark Barrett
Stanford University, Stanford, CA 94305 USA
Abstract. 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.
1 Introduction
Modern society relies increasingly on electronic systems, powered by hardware
components that continue to grow in complexity and variety. Ensuring the functional correctness of these components is essential, as bugs and errors can have
consequences ranging from undermining a company’s reputation to jeopardizing human safety [1,22,25,32,33]. Most electronic designs must therefore include
a significant verification effort, and this effort often consumes more time and
resources than all other aspects of the design process [17,34].
Formal methods such as symbolic model checking have become a crucial part
of the verification effort because of their strong guarantees and automation [24].
However, due to the state space explosion problem [14], model checking typically
only works well for small- to medium-sized circuits with primarily control logic,
limiting its potential for addressing industry verification challenges.
One approach for combating the state space explosion problem is partial order reduction [14]. While symbolic partial order reduction has been successfully
applied for the verification of asynchronous systems [37], its use in synchronous
systems has been limited. In this paper, we introduce a novel approach for adapting symbolic partial order reduction to model checking of synchronous hardware
This work was supported by the National Science Foundation Graduate Research
Fellowship Program under Grant No. DGE-1656518. Any opinions, findings, and
conclusions or recommendations expressed in this material are those of the author(s)
and do not necessarily reflect the views of the National Science Foundation. This
work was also supported by the Defense Advanced Research Projects Agency, grant
FA8650-18-2-7854. We thank the funding agencies and our corporate collaborators
for their support.
c
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 367–386, 2020.
https://doi.org/10.1007/978-3-030-45190-5 20
TACAS
Evaluation
Artifact
2020
Accepted
in Synchronous Hardware
Makai Mann and Clark Barrett
Stanford University, Stanford, CA 94305 USA
Abstract. 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.
1 Introduction
Modern society relies increasingly on electronic systems, powered by hardware
components that continue to grow in complexity and variety. Ensuring the functional correctness of these components is essential, as bugs and errors can have
consequences ranging from undermining a company’s reputation to jeopardizing human safety [1,22,25,32,33]. Most electronic designs must therefore include
a significant verification effort, and this effort often consumes more time and
resources than all other aspects of the design process [17,34].
Formal methods such as symbolic model checking have become a crucial part
of the verification effort because of their strong guarantees and automation [24].
However, due to the state space explosion problem [14], model checking typically
only works well for small- to medium-sized circuits with primarily control logic,
limiting its potential for addressing industry verification challenges.
One approach for combating the state space explosion problem is partial order reduction [14]. While symbolic partial order reduction has been successfully
applied for the verification of asynchronous systems [37], its use in synchronous
systems has been limited. In this paper, we introduce a novel approach for adapting symbolic partial order reduction to model checking of synchronous hardware
This work was supported by the National Science Foundation Graduate Research
Fellowship Program under Grant No. DGE-1656518. Any opinions, findings, and
conclusions or recommendations expressed in this material are those of the author(s)
and do not necessarily reflect the views of the National Science Foundation. This
work was also supported by the Defense Advanced Research Projects Agency, grant
FA8650-18-2-7854. We thank the funding agencies and our corporate collaborators
for their support.
c
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 367–386, 2020.
https://doi.org/10.1007/978-3-030-45190-5 20
TACAS
Evaluation
Artifact
2020
Accepted