Skip to main content
SpringerLink
Log in

Software in a Hardware View

New Models for HW-dependent Software in SoC Verification

  • Chapter
  • First Online:
Formal System Verification

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.

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

Access this chapter

Log in via an institution
eBook
USD 16.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 129.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 129.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. T. Aitch, Aquarius: a pipelined RISC CPU (2003)

    Google Scholar 

  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–198

    Google Scholar 

  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–830

    Google Scholar 

  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. 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–157

    Google Scholar 

  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–207

    Google Scholar 

  7. C. Cadar, K. Sen, Symbolic execution for software testing: three decades later. Commun. ACM 56(2), 82–90 (2013)

    Article  Google Scholar 

  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)

    Article  MATH  Google Scholar 

  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 –135

    Google Scholar 

  10. N.Eén, N.Sörensson. An extensible SAT solver. in SAT (2003), pp. 502–518

    Google Scholar 

  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)

    Article  Google Scholar 

  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. 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:3

    Google Scholar 

  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)

    Article  Google Scholar 

  15. Onespin Solutions GmbH. Germany. OneSpin 360MV. http://www.onespin-solutions.com

  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–166

    Google Scholar 

  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)

    Article  Google Scholar 

  18. B. Schlich, Model checking of software for microcontrollers. ACM Trans. Embed. Comput. Syst. 9(4), 36:1–36:27 (2010)

    Google Scholar 

  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–145

    Google Scholar 

  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–128

    Google Scholar 

  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 

Download references

Author information

Authors and Affiliations

  1. Department of Electrical and Computer Engineering, University of Kaiserslautern, Kaiserslautern, Germany

    Carlos Villarraga, Dominik Stoffel & Wolfgang Kunz

Authors
  1. Carlos Villarraga
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Dominik Stoffel
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Wolfgang Kunz
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Carlos Villarraga .

Editor information

Editors and Affiliations

  1. DFKI, University of Bremen, Bremen, Germany

    Rolf Drechsler

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG

About this chapter

Cite this chapter

Villarraga, C., Stoffel, D., Kunz, W. (2018). Software in a Hardware View. In: Drechsler, R. (eds) Formal System Verification. Springer, Cham. https://doi.org/10.1007/978-3-319-57685-5_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-57685-5_4

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-57683-1

  • Online ISBN: 978-3-319-57685-5

  • eBook Packages: EngineeringEngineering (R0)

Publish with us

Policies and ethics

Search

Navigation