Advertisement

Software in a Hardware View

New Models for HW-dependent Software in SoC Verification
Chapter

Abstract

In current practices of SoC design a trend can be observed to integrate more and more low-level software components into the hardware at different levels of granularity. The implementation of important control functions is frequently shifted from the SoC’s hardware into its firmware. This calls for new methods for verification based on a joint analysis of hardware and software. While most techniques of software verification operate at a hardware-independent level, this chapter elaborates on the possible merits of a hardware-dependent software view. The chapter reviews a recently developed model for formal verification of low-level embedded system software called program netlist and details on its applications. In particular, applications for speed-independent and cycle-accurate hardware/software integration are reported. For each studied scenario, this chapter describes how the different challenges of modeling the hardware/software interface can be solved by exploiting the characteristics of the program netlist. For speed-independent hardware/software interaction the equivalence checking problem is studied and results of our proposed solution are presented. For the case of a cycle-accurate hardware/software integration, a model for hardware/software co-verification is developed and experimentally evaluated by applying it to property checking.

References

  1. 1.
    T. Aitch, Aquarius: a pipelined RISC CPU (2003)Google Scholar
  2. 2.
    T. Arons, E. Elster, L. Fix, S. Mador-Haim, M. Mishaeli, J. Shalev, E. Singerman, A. Tiemeyer, M.Y. Vardi, L.D. Zuck, Formal verification of backward compatibility of microcode, in Proceedings of the 17th International Conference on Computer Aided Verification, CAV’05 (Springer, Heidelberg, 2005), pp. 185–198Google Scholar
  3. 3.
    T. Arons, E. Elster, S. Ozer, J. Shalev, E. Singerman, Efficient symbolic simulation of low level software, in Design, Automation and Test in Europe, DATE ’08 (2008), pp. 825–830Google Scholar
  4. 4.
    B. Bao, C. Villarraga, B. Schmidt, D. Stoffel, W. Kunz, A new property language for the specification of hardware-dependent embedded system software, in Proceedings of Forum on Specification and Design Languages (FDL), Munich, Germany, Oct 2014. (accepted for publication)Google Scholar
  5. 5.
    C. Bartsch, C. Villarraga, B. Schmidt, D. Stoffel, W. Kunz, Efficient SAT/simulation-based model generation for low-level embedded software, in 17. GI/ITG/GMM Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV) (2014), pp. 147–157Google Scholar
  6. 6.
    A. Biere, A. Cimatti, E. Clarke, Y. Zhu, Symbolic model checking without BDDs, in Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS ’99 (Springer, London, 1999), pp. 193–207Google Scholar
  7. 7.
    C. Cadar, K. Sen, Symbolic execution for software testing: three decades later. Commun. ACM 56(2), 82–90 (2013)CrossRefGoogle Scholar
  8. 8.
    D. Currie, X. Feng, M. Fujita, A.J. Hu, M. Kwan, S. Rajan, Embedded software verification using symbolic execution and uninterpreted functions. Int. J. Parallel Program. 34(1), 61–91 (2006)CrossRefzbMATHGoogle Scholar
  9. 9.
    D.W. Ecker, V. Esen, T. Steininger, Memory models for the formal verification of assembler code using bounded model checking, in Proceedings of IEEE International Symposium on Object-Oriented Real-Time Distributed Computing (2004), pp. 129 –135Google Scholar
  10. 10.
    N.Eén, N.Sörensson. An extensible SAT solver. in SAT (2003), pp. 502–518Google Scholar
  11. 11.
    A. Hazra, R. Mukherjee, P. Dasgupta, A. Pal, K. Harer, A. Banerjee, S. Mukherjee, Power-tructor: An integrated tool flow for formal verification and coverage of architectural power intent. IEEE Trans. Comput. Aided Des. Integr. Circ. Syst. 32(11), 1801–1813 (2013)CrossRefGoogle Scholar
  12. 12.
    A. Horn, M. Tautschnig, C. Val, L. Liang, T. Melham, J. Grundy, D. Kroening, Formal co-validation of low-level hardware/software interfaces. Formal Methods Comput. Aided Des. (FMCAD) 2013, 121–128 (2013)Google Scholar
  13. 13.
    J. Koestersm, A. Goryachev, Verification of non-mainline functions in today’s processor chips. in Proceedings International Design Automation Conference (DAC), DAC’14 (ACM, New York, 2014), pp. 1:1–1:3Google Scholar
  14. 14.
    M.D. Nguyen, M. Thalmaier, M. Wedler, J. Bormann, D. Stoffel, W. Kunz, Unbounded protocol compliance verification using interval property checking with invariants. IEEE Trans. Comput. Aided Des 27(11), 2068–2082 (2008)CrossRefGoogle Scholar
  15. 15.
    Onespin Solutions GmbH. Germany. OneSpin 360MV. http://www.onespin-solutions.com
  16. 16.
    A. Pnueli, M. Siegel, E. Singerman, Translation validation, in Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS ’98 (Springer, London, 1998), pp. 151–166Google Scholar
  17. 17.
    C.S. Păsăreanu, W. Visser, A survey of new trends in symbolic execution for software testing and analysis. Int. J. Softw. Tools Technol. Transf. 11(4), 339–353 (2009)CrossRefGoogle Scholar
  18. 18.
    B. Schlich, Model checking of software for microcontrollers. ACM Trans. Embed. Comput. Syst. 9(4), 36:1–36:27 (2010)Google Scholar
  19. 19.
    B. Schmidt, C. Villarraga, T. Fehmel, J. Bormann, M. Wedler, M. Nguyen, D. Stoffel, W. Kunz, A new formal verification approach for hardware-dependent embedded system software, IPSJ Transactions on System LSI Design Methodology (Special Issue on ASPDAC-2013), vol. 6 (2013), pp. 135–145Google Scholar
  20. 20.
    C. Villarraga, B. Schmidt, C. Bartsch, J. Bormann, D. Stoffel, W. Kunz, An equivalence checker for hardware-dependent software, in 11 ACM-IEEE International Conference on Formal Methods and Models for Codesign (2013), pp. 119–128Google Scholar
  21. 21.
    M. Wedler, E. Cabrill, S. Graham, L. Patrick, Using formal verfication for HW/SW co-verification of an FPGA IP core. Xcell Journal (Xilinx, Inc.) 0, 56–61 (2012)Google Scholar

Copyright information

© Springer International Publishing AG 2018

Authors and Affiliations

  1. 1.Department of Electrical and Computer EngineeringUniversity of KaiserslauternKaiserslauternGermany

Personalised recommendations