Skip to main content
SpringerLink
Log in

An Accelerator for Resolution Proof Checking based on FPGA and Hybrid Memory Cube Technology

  • Published:
Journal of Signal Processing Systems Aims and scope Submit manuscript

Abstract

Modern Boolean satisfiability solvers can emit proofs of unsatisfiability. There is substantial interest in being able to verify such proofs and also in using them for further computations. In this paper, we present an FPGA accelerator for checking resolution proofs, a popular proof format. Our accelerator exploits parallelism at the low level by implementing the basic resolution step in hardware, and at the high level by instantiating a number of parallel modules for proof checking. Since proof checking involves highly irregular memory accesses, we employ Hybrid Memory Cube technology for accelerator memory. The results show that while the accelerator is scalable and achieves speedups for all benchmark proofs, performance improvements are currently limited by the overhead of transitioning the proof into the accelerator memory.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Figure 1
Figure 2
Figure 3
Figure 4
Figure 5
Figure 6
Figure 7
Figure 8
Figure 9
Figure 10
Figure 11
Figure 12

Similar content being viewed by others

Notes

  1. http://fmv.jku.at/tracecheck/

  2. www.micron.com/products/advanced-solutions/advanced-computing-solutions

  3. www.satcompetition.org

References

  1. Babb, J., Frank, M., Agarwal, A. (1996). Solving graph problems with dynamic computation structures. In Proceedings of SPIE: High-Speed Computing, Digital Signal Processing, and Filtering Using Reconfigurable Logic, vol. 2914, pp. 225–236.

  2. Biere, A. (2008). Picosat essentials. Journal on Satisfiability Boolean Modeling and Computation (JSAT), 4, 75–97.

    MATH  Google Scholar 

  3. Boyd, M., & Larrabee, T. (2000). A scalable, loadable custom programmable logic device for solving boolean satisfiability problems. In Proceedings of the 8th IEEE International Symposium on Field-Programmable Custom Computing Machines (FCCM).

  4. Chatterjee, S., Mishchenko, A., Brayton, R., Kuehlmann, A. (2007). On resolution proofs for combinational equivalence. In 2007 44Th ACM/IEEE design automation conference, pp. 600–605.

  5. Cook, S.A. (1971). The complexity of theorem-proving procedures. In Proceedings of the Third Annual ACM Symposium on Theory of Computing, STOC ’71 (pp. 151–158). New York: ACM.

  6. Dai, D., Huang, T., Chi, Y., Xu, N., Wang, Y., Yang, H. (2017). Foregraph: Exploring large-scale graph processing on multi-fpga architecture. In Proceedings of the International Symposium on Field-Programmable Gate Arrays (FPGA). ACM.

  7. Davis, M., Logemann, G., Loveland, D. (1962). A machine program for theorem proving. Communications of the ACM, 5(7), 394–397.

    Article  MathSciNet  Google Scholar 

  8. Davis, M., & Putnam, H. (1960). A computing procedure for quantification theory. Journal of the ACM, 7 (3), 201–216.

    Article  MathSciNet  Google Scholar 

  9. deLorimier, M., Kapre, N., ad Mehta, N., Rizzo, D., Eslick, I., Rubin, R., Uribe, T., Knight, T. Jr., DeHon, A. (2006). Graphstep: a system architecture for sparse-graph algorithms. In Proceedings of the 14th IEEE International Symposium on Field-Programmable Custom Computing Machines (FCCM).

  10. Drzevitzky, S., Kastens, U., Platzner, M. (2010). Proof-carrying hardware: Concept and prototype tool flow for online verification. International Journal of Reconfigurable Computing, 2010, 11.

    Article  Google Scholar 

  11. Hamadi, Y., & Merceron, D. (1997). Reconfigurable architectures: a new vision for optimization problems. In Proceedings of the 3rd International Conference on Principles and Practice of Constraint Programming (CP), Lecture Notes in Computer Science (LNCS), vol. 1330, pp. 209–221. Springer.

  12. Heule, M., & Biere, A. (2015). Proofs for satisfiability problems, vol. 55, pp. 1–22 College Publications.

  13. (2014). Hybrid Memory Cube Consortium: Hybrid memory cube specification 2.0.

  14. Isenberg, T., Platzner, M., Wehrheim, H., Wiersema, T. (2017). Proof-carrying hardware via inductive invariants. ACM Transactions on Design Automation of Electronic Systems, 22(4), 61:1–61:23.

    Article  Google Scholar 

  15. Leong, P., Sham, C., Wong, W., Wong, H., Yuen, W., Leong, M. (2001). A bitstream reconfigurable fpga implementation of the wsat algorithm. IEEE Transactions on VLSI Systems, 9(1), 197–201.

    Article  Google Scholar 

  16. McMillan, K. L. (2003). Interpolation and SAT-based Model Checking, pp. 1–13. Berlin: Springer.

    MATH  Google Scholar 

  17. Nai, L., Hadidi, R., Sim, J., Kim, H., Kumar, P., Kim, H. (2017). Graphpim: Enabling instruction-level pim offloading in graph computing frameworks. In 2017 IEEE International symposium on high performance computer architecture (HPCA), pp. 457–468.

  18. Pawlowski, J.T. (2011). Hybrid memory cube (hmc). In 2011 IEEE Hot chips 23 symposium (HCS), pp. 1–24.

  19. Petraglio, E., Wertenbroek, R., Capitao, F., Guex, N., Iseli, C., Thoma, Y. (2017). Genomic data clustering on fpgas for compression. In S. Wong, A.C. Beck, K. Bertels, L. Carro (Eds.) Applied reconfigurable computing (pp. 229–240). Cham: Springer International Publishing.

    Google Scholar 

  20. Platzner, M. (2000). Reconfigurable accelerators for combinatorial problems. IEEE Computer, 33(4), 58–60.

    Article  Google Scholar 

  21. Schmidt, J., Fröning, H., Brüning, U. (2016). Exploring time and energy for complex accesses to a hybrid memory cube. In Proceedings of the Second International Symposium on Memory Systems, MEMSYS ’16, pp. 142-150. New York: ACM.

  22. Shiozawa, T., Oguri, K., Nagami, K., Ito, H., Konishi, R., Imlig, N. (1998). A hardware implementation of constraint satisfaction problem based on new reconfigurante lsi architecture. In Proceedings of the 8th International Workshop on Field-Programmable Logic and Applications (FPL), Lecture Notes in Computer Science (LNCS), vol. 1482, pp. 426–430. Springer.

    Google Scholar 

  23. Skliarova, I., & de Brito Ferrari, A. (2004). Reconfigurable hardware sat solvers: a survey of systems. IEEE Transactions on Computers, 53(11), 1449–1461.

    Article  Google Scholar 

  24. Skliarova, I. (2002). Ferrari: a sat solver using software and reconfigurable hardware. In Proceedings of the Design, Automation and Test in Europe Conference (DATE).

  25. Suyama, T., Yokoo, M., Sawada, H., Nagoya, A. (2001). Solving satisfiability problems using reconfigurable computing. IEEE Transactions on VLSI Systems, 9(1), 109–116.

    Article  Google Scholar 

  26. Vazirani, V. (2001). Approximation algorithms. Berlin: Springer.

    MATH  Google Scholar 

  27. Zhang, J., Khoram, S., Li, J. (2017). Boosting the performance of fpga-based graph processor using hybrid memory cube: a case for breadth first search. In Proceedings of the 2017 ACM/SIGDA International Symposium on Field-Programmable Gate Arrays, FPGA ’17, pp. 207-216. New York: ACM.

  28. Zhong, P., Martonosi, M., Ashar, P., Malik, S. (1999). Using configurable computing to accelerate boolean satisfiability. IEEE Transactions CAD of Integrated Circuits and Systems, 18(6), 861–868.

    Article  Google Scholar 

Download references

Acknowledgements

This work was partially supported by the German Research Foundation (DFG) within the Collaborative Research Centre “On-The-Fly Computing” (SFB 901).

Author information

Authors and Affiliations

  1. Paderborn University, Warburger Str. 100, 33098, Paderborn, Germany

    Tim Hansmeier & Marco Platzner

  2. University of Arkansas, Fayetteville, AR, 72701, USA

    Md Jubaer Hossain Pantho & David Andrews

Authors
  1. Tim Hansmeier
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Marco Platzner
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Md Jubaer Hossain Pantho
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. David Andrews
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Tim Hansmeier.

Additional information

Publisher’s Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Hansmeier, T., Platzner, M., Pantho, M.J.H. et al. An Accelerator for Resolution Proof Checking based on FPGA and Hybrid Memory Cube Technology. J Sign Process Syst 91, 1259–1272 (2019). https://doi.org/10.1007/s11265-018-1435-y

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s11265-018-1435-y

Keywords

Search

Navigation