Top

Published in:

2019 | OriginalPaper | Chapter

When Are Software Verification Results Valid for Approximate Hardware?

Authors : Tobias Isenberg, Marie-Christine Jakobs, Felix Pauck, Heike Wehrheim

Published in: Tests and Proofs

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Approximate computing (AC) is an emerging paradigm for energy-efficient computation. The basic idea of AC is to sacrifice high precision for low energy by allowing hardware to carry out only “approximately correct” calculations. This provides a major challenge for software quality assurance: Programs successfully verified to be correct might be erroneous on approximate hardware.

In this paper, we present a novel approach for determining under what conditions a software verification result is valid for approximate hardware. To this end, we compute the allowed tolerances for AC hardware from successful verification runs. More precisely, we derive a set of constraints which – when met by the AC hardware – guarantee that the verification result carries over to AC. Our approach is based on the framework of abstract interpretation. Furthermore, we show (1) how to practically extract tolerances from verification runs employing predicate abstraction, and (2) how to check such constraints on hardware designs. We have implemented all techniques, and exemplify them on example C programs and a number of recently proposed approximate adders.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

next chapter Testing Robots Using CSP

For the practical evaluation we, however, allow arbitrary C programs.

The operation of interest is made configurable in CPAchecker.

A generalization to a family of constraints is straightforward.

Some additions first had to be brought into three-address code form and in some programs we replaced some constant assignments by proper addition.

Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Addison-Wesley, Boston (1986)MATH

Albarghouthi, A., Dillig, I., Gurfinkel, A.: Maximal specification synthesis. In: Proceedings of the POPL, pp. 789–801. ACM (2016)CrossRef

Apt, K.R., de Boer, F.S., Olderog, E.R.: Verification of Sequential and Concurrent Programs. Springer, London (2009). https://doi.org/10.1007/978-1-84882-745-5CrossRefMATH

Ball, T., Podelski, A., Rajamani, S.K.: Boolean and cartesian abstraction for model checking C programs. STTT 5(1), 49–58 (2003)CrossRef

Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard: Version 2.5. Technical report, Department of Computer Science, The University of Iowa (2015). http://www.SMT-LIB.org

ABC, Berkeley: A system for sequential synthesis and verification (2005)

Besson, F., Jensen, T.P., Turpin, T.: Small witnesses for abstract interpretation-based proofs. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 268–283. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71316-6_19CrossRef

Beyer, D.: Software verification and verifiable witnesses. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 401–416. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_31CrossRef

Beyer, D., Keremoglu, M.E., Wendler, P.: Predicate abstraction with adjustable-block encoding. In: Proceedings of the FMCAD, pp. 189–198. IEEE (2010)

10.

Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184–190. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_16CrossRef

11.

Biere, A.: Picosat (2013). http://fmv.jku.at/picosat

12.

Carbin, M., Kim, D., Misailovic, S., Rinard, M.C.: Verified integrity properties for safe approximate program transformations. In: Proceedings of the PEPM, pp. 63–66. ACM (2013)

13.

Carbin, M., Misailovic, S., Rinard, M.C.: Verifying quantitative reliability for programs that execute on unreliable hardware. In: Proceedings of the OOPSLA, pp. 33–52. ACM (2013)

14.

Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: Proceedings of the PLDI, pp. 415–426. ACM (2006)

15.

Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the POPL. ACM (1977)

16.

Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997). https://doi.org/10.1007/3-540-63166-6_10CrossRef

17.

Han, J., Orshansky, M.: Approximate computing: an emerging paradigm for energy-efficient design. In: Proceedings of the ETS, pp. 1–6. IEEE Computer Society (2013)

18.

He, S., Lahiri, S.K., Rakamarić, Z.: Verifying relative safety, accuracy, and termination for program approximations. In: Rayadurgam, S., Tkachuk, O. (eds.) NFM 2016. LNCS, vol. 9690, pp. 237–254. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40648-0_19CrossRef

19.

He, S., Lahiri, S.K., Rakamaric, Z.: Verifying relative safety, accuracy, and termination for program approximations. JAR 60(1), 23–42 (2018)MathSciNetCrossRef

20.

Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Proceedings of the POPL, pp. 232–244. ACM (2004)

21.

Hoare, C.A.R.: Procedures and parameters: an axiomatic approach. In: Engeler, E. (ed.) Symposium on Semantics of Algorithmic Languages. LNM, vol. 188, pp. 102–116. Springer, Heidelberg (1971). https://doi.org/10.1007/BFb0059696CrossRef

22.

Isenberg, T., Jakobs, M.C., Pauck, F., Wehrheim, H.: Deriving Approximation Tolerance Constraints from Verification Runs. CoRR abs/1604.08784 (2016). http://arxiv.org/abs/1604.08784

23.

Isenberg, T., Jakobs, M., Pauck, F., Wehrheim, H.: Validity of software verification results on approximate hardware. ESL 10(1), 22–25 (2018)

24.

Jakobs, M.-C.: Speed up configurable certificate validation by certificate reduction and partitioning. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 159–174. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-22969-0_12CrossRef

25.

Jakobs, M.-C., Wehrheim, H.: Compact proof witnesses. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 389–403. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-57288-8_28CrossRef

26.

Kahng, A.B., Kang, S.: Accuracy-configurable adder for approximate arithmetic designs. In: Proceedings of the DAC, pp. 820–825. ACM (2012)

27.

Kugler, L.: Is “good enough” computing good enough? Commun. ACM 58(5), 12–14 (2015)CrossRef

28.

Manna, Z., Pnueli, A.: Temporal verification of reactive systems: progress (1996)

29.

Misailovic, S., Carbin, M., Achour, S., Qi, Z., Rinard, M.C.: Chisel: reliability- and accuracy-aware optimization of approximate computational kernels. In: Proceedings of the OOPSLA, pp. 309–328. ACM (2014)CrossRef

30.

Mittal, S.: A survey of techniques for approximate computing. ACM Comput. Surv. 48(4), 62:1–62:33 (2016)

31.

Pauck, F.: Generierung von Eigenschaftsprüfern in einem Hardware/Software-Co-Verifikationsverfahren. Bachelor thesis, Paderborn University (2014)

32.

Podelski, A., Rybalchenko, A.: Transition invariants. In: Proceedings of the LICS, pp. 32–41. IEEE Computer Society (2004)

33.

Sampson, A., Dietl, W., Fortuna, E., Gnanapragasam, D., Ceze, L., Grossman, D.: EnerJ: approximate data types for safe and general low-power computation. In: Proceedings of the PLDI, pp. 164–174. ACM (2011)CrossRef

34.

Sery, O., Fedyukovich, G., Sharygina, N.: Interpolation-based function summaries in bounded model checking. In: Eder, K., Lourenço, J., Shehory, O. (eds.) HVC 2011. LNCS, vol. 7261, pp. 160–175. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-34188-5_15CrossRef

35.

Shafique, M., Ahmad, W., Hafiz, R., Henkel, J.: A low latency generic accuracy configurable adder. In: Proceedings of the DAC, pp. 86:1–86:6. ACM (2015)

36.

Verma, A.K., Brisk, P., Ienne, P.: Variable latency speculative addition: a new paradigm for arithmetic circuit design. In: Proceedings of the DATE, pp. 1250–1255. ACM (2008)

37.

Wolf, C.: Yosys open synthesis suite. http://www.clifford.at/yosys/

38.

Ye, R., Wang, T., Yuan, F., Kumar, R., Xu, Q.: On reconfiguration-oriented approximate adder design and its application. In: Proceedings of the CAD, pp. 48–54. IEEE Press (2013)

39.

Zhu, N., Goh, W.L., Yeo, K.S.: An enhanced low-power high-speed adder for error-tolerant application. In: Proceedings of the International Symposium on Integrated Circuits, pp. 69–72. IEEE (2009)

Title: When Are Software Verification Results Valid for Approximate Hardware?
Authors: Tobias Isenberg
Marie-Christine Jakobs
Felix Pauck
Heike Wehrheim
Publisher: Springer International Publishing
Book: Tests and Proofs
Print ISBN: 978-3-030-31156-8

Electronic ISBN: 978-3-030-31157-5

Copyright Year: 2019
DOI: https://doi.org/10.1007/978-3-030-31157-5_1

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"