384
M. Mann and C. Barrett
7 Conclusion
We have presented a set of conservative conditions over transition systems and
automated techniques for proving these conditions. If the conditions can be
proved, then constraints can be added to the system that break path symmetries. We evaluated our approach on parameterized open-source and commercial
packet-mover circuits and demonstrated significant improvements in bounded
model checking performance.
Some potential future work includes improvements to the ProveRIS procepacket movers, developing more targeted condition proofs by associating actions
with particular data inputs, and building an interactive tool which helps the
user identify and manage reduced instruction sets and partial order reductions.
8 Data Availability Statement
The experimental results and the necessary software for reproducing results in
a standard Ubuntu 18.04 installation are available in the Figshare repository:
https://doi.org/10.6084/m9.figshare.11874687.
References
1. Bailey, B.: When bugs escape (July 2018), https://semiengineering.com/
when-bugs-escape/, [Online]
2. Bengtsson, J., Jonsson, B., Lilius, J., Yi, W.: Partial order reductions for timed
systems. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR’98 Concurrency Theory.
pp. 485–500. Springer Berlin Heidelberg, Berlin, Heidelberg (1998)
3. Bhattacharya, R., German, S., Gopalakrishnan, G.: Symbolic partial order reduction for rule based transition systems. In: Borrione, D., Paul, W. (eds.) Correct
Hardware Design and Verification Methods. pp. 332–335. Springer Berlin Heidelberg, Berlin, Heidelberg (2005)
4. Biere, A.: CaDiCaL, Lingeling, Plingeling, Treengeling, YalSAT Entering the SAT
Competition 2017. In: Balyo, T., Heule, M., J¨ arvisalo, M. (eds.) Proc. of SAT
Competition 2017 – Solver and Benchmark Descriptions. vol. B-2017-1, pp. 14–15.
University of Helsinki (2017)
5. Biere, A., Artho, C., Schuppan, V.: Liveness checking as safety checking. Electr.
Notes Theor. Comput. Sci. 66(2), 160–177 (2002)
6. Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without bdds.
In: Cleaveland, W.R. (ed.) Tools and Algorithms for the Construction and Analysis
of Systems. pp. 193–207. Springer Berlin Heidelberg, Berlin, Heidelberg (1999)
7. Biere, A., Heljanko, K., Wieringa, S.: AIGER 1.9 and beyond. Tech. rep., FMV
Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria (2011)
8. Bjesse, P.: A practical approach to word level model checking of industrial netlists.
pp. 446–458 (07 2008)
9. Bjesse, P.: Word-level sequential memory abstraction for model checking. In: FMCAD. pp. 1–9. IEEE (2008)
dure, investigating applications of partial order reduction to sequentially-composed
M. Mann and C. Barrett
7 Conclusion
We have presented a set of conservative conditions over transition systems and
automated techniques for proving these conditions. If the conditions can be
proved, then constraints can be added to the system that break path symmetries. We evaluated our approach on parameterized open-source and commercial
packet-mover circuits and demonstrated significant improvements in bounded
model checking performance.
Some potential future work includes improvements to the ProveRIS procepacket movers, developing more targeted condition proofs by associating actions
with particular data inputs, and building an interactive tool which helps the
user identify and manage reduced instruction sets and partial order reductions.
8 Data Availability Statement
The experimental results and the necessary software for reproducing results in
a standard Ubuntu 18.04 installation are available in the Figshare repository:
https://doi.org/10.6084/m9.figshare.11874687.
References
1. Bailey, B.: When bugs escape (July 2018), https://semiengineering.com/
when-bugs-escape/, [Online]
2. Bengtsson, J., Jonsson, B., Lilius, J., Yi, W.: Partial order reductions for timed
systems. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR’98 Concurrency Theory.
pp. 485–500. Springer Berlin Heidelberg, Berlin, Heidelberg (1998)
3. Bhattacharya, R., German, S., Gopalakrishnan, G.: Symbolic partial order reduction for rule based transition systems. In: Borrione, D., Paul, W. (eds.) Correct
Hardware Design and Verification Methods. pp. 332–335. Springer Berlin Heidelberg, Berlin, Heidelberg (2005)
4. Biere, A.: CaDiCaL, Lingeling, Plingeling, Treengeling, YalSAT Entering the SAT
Competition 2017. In: Balyo, T., Heule, M., J¨ arvisalo, M. (eds.) Proc. of SAT
Competition 2017 – Solver and Benchmark Descriptions. vol. B-2017-1, pp. 14–15.
University of Helsinki (2017)
5. Biere, A., Artho, C., Schuppan, V.: Liveness checking as safety checking. Electr.
Notes Theor. Comput. Sci. 66(2), 160–177 (2002)
6. Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without bdds.
In: Cleaveland, W.R. (ed.) Tools and Algorithms for the Construction and Analysis
of Systems. pp. 193–207. Springer Berlin Heidelberg, Berlin, Heidelberg (1999)
7. Biere, A., Heljanko, K., Wieringa, S.: AIGER 1.9 and beyond. Tech. rep., FMV
Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria (2011)
8. Bjesse, P.: A practical approach to word level model checking of industrial netlists.
pp. 446–458 (07 2008)
9. Bjesse, P.: Word-level sequential memory abstraction for model checking. In: FMCAD. pp. 1–9. IEEE (2008)
dure, investigating applications of partial order reduction to sequentially-composed