Bit-Precise Formal Verification for SystemC Using Satisfiability Modulo Theories Solving

Conference paper
Part of the IFIP Advances in Information and Communication Technology book series (IFIPAICT, volume 523)

Abstract

Hardware/software codesigns are often modeled with the system level design language SystemC. Especially for safety critical applications, it is crucial to guarantee that such a design meets its requirement. In this paper, we present an approach to formally verify SystemC designs using the UCLID satisfiability modulo theories (SMT) solver. UCLID supports finite precision bitvector arithmetics. Thus, we can handle SystemC designs on a bit-precise level, which enables us to formally verify deeply integrated hardware/software systems that comprise detailed hardware models. At the same time, we exploit UCLID’s ability to handle symbolic variables and use k-inductive invariant checking for SystemC designs. With this inductive approach, we can counteract the state space explosion problem, which model checking approaches suffer from. We demonstrate the practical applicability of our approach with a SystemC design that comprises a bit- and cycle-accurate model of a UART and software that reads data from the UART.

References

  1. 1.
    Brady, B., Seshia, S., Lahiri, S., Bryant, R.: A user’s guide to UCLID (2008)Google Scholar
  2. 2.
    Chang, C.-W., Dömer, R.: Formal deadlock analysis of SpecC models using satisfiability modulo theories. In: Schirner, G., Götz, M., Rettberg, A., Zanella, M.C., Rammig, F.J. (eds.) IESS 2013. IAICT, vol. 403, pp. 116–127. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-38853-8_11CrossRefGoogle Scholar
  3. 3.
    Cimatti, A., Narasamdya, I., Roveri, M.: Software model checking SystemC. IEEE Trans. CAD Integr. Circuits Syst. 32(5), 774–787 (2013)CrossRefGoogle Scholar
  4. 4.
    Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-24730-2_15CrossRefMATHGoogle Scholar
  5. 5.
    Elshuber, M., Kandl, S., Puschner, P.P., Choppy, C., Sun, J.: Improving system-level verification of SystemC models with SPIN. In: FSFMA, pp. 74–79 (2013)Google Scholar
  6. 6.
    Garavel, H., Helmstetter, C., Ponsini, O., Serwe, W.: Verification of an industrial SystemC/TLM model using LOTOS and CADP. In: MEMOCODE, pp. 46–55. IEEE Computer Society (2009)Google Scholar
  7. 7.
    Große, D., Le, H.M., Drechsler, R.: Proving transaction and system-level properties of untimed SystemC TLM designs. In: MEMOCODE, pp. 113–122. IEEE Computer Society (2010)Google Scholar
  8. 8.
    Habibi, A., Moinudeen, H., Tahar, S.: Generating finite state machines from SystemC. In: Design, Automation and Test in Europe, pp. 76–81. IEEE (2006)Google Scholar
  9. 9.
    Helmstetter, C.: TLM.open: a SystemC/TLM frontend for the CADP verification toolbox. Leibniz Trans. Embed. Syst. 1(1) (2014)Google Scholar
  10. 10.
    Herber, P., Fellmuth, J., Glesner, S.: Model checking SystemC designs using timed automata. In: CODES+ISSS, pp. 131–136. ACM Press (2008)Google Scholar
  11. 11.
    IEEE Standards Association: IEEE Std. 1666–2011, Open SystemC Language Reference Manual. IEEE Press (2011)Google Scholar
  12. 12.
    Karlsson, D., Eles, P., Peng, Z.: Formal verification of SystemC designs using a petri-net based representation. In: DATE, pp. 1228–1233. IEEE Press (2006)Google Scholar
  13. 13.
    Lahiri, S.K., Seshia, S.A.: The UCLID decision procedure. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 475–478. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-27813-9_40CrossRefGoogle Scholar
  14. 14.
    Pockrandt, M., Herber, P., Klös, V., Glesner, S.: Model checking memory-related properties of hardware/software co-designs. In: Schirner, G., Götz, M., Rettberg, A., Zanella, M.C., Rammig, F.J. (eds.) IESS 2013. IAICT, vol. 403, pp. 92–103. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-38853-8_9CrossRefGoogle Scholar
  15. 15.
    Brummayer, R., Biere, A.: Boolector: an efficient SMT solver for bit-vectors and arrays. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 174–177. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-00768-2_16CrossRefMATHGoogle Scholar
  16. 16.
    Sheeran, M., Singh, S., Stålmarck, G.: Checking safety properties using induction and a SAT-solver. In: Hunt, W.A., Johnson, S.D. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 127–144. Springer, Heidelberg (2000).  https://doi.org/10.1007/3-540-40922-X_8CrossRefGoogle Scholar

Copyright information

© IFIP International Federation for Information Processing 2017

Authors and Affiliations

  1. 1.Technische Universität BerlinBerlinGermany

Personalised recommendations