Skip to main content
SpringerLink
Log in

SimSoC: A Fast, Proven Faithful, Full System Virtual Prototyping Framework

  • Chapter
  • First Online:
Model-Implementation Fidelity in Cyber Physical System Design

  • 495 Accesses

Abstract

This chapter presents the SimSoC virtual prototyping framework, a full system simulation framework, based on SystemC and Transaction Level Modeling. SimSoC takes as input a binary executable file, which can be a full operating system, and simulates the behavior of the target hardware on the host system. It is using internally dynamic binary translation from target code to host code to simulate the application software. A potential issue with simulators is that they might not accurately simulate the real hardware. We aimed at filling this gap by proving that the ARM instruction set simulator coded in C is a high fidelity implementation of the ARM architecture, using the Coq theorem prover, and starting from a formal architectural model in Coq. The first part of the chapter presents the general architecture and features of SimSoC. The second part describes the proof of the ARM simulator.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 109.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

Notes

  1. 1.

    Note that this problem is the same as for the work done by Cambridge University.

References

  1. J. Alglave, A. Fox, S. Ishtiaq, M.O. Myreen, S. Sarkar, P. Sewell, F.Z. Nardelli, The semantics of power and ARM multiprocessor machine code. In DAMP’09 (ACM, New York, NY, USA, 2008), pp. 13–24

    Google Scholar 

  2. V. Bala, E. Duesterwald, S. Banerjia, Dynamo: a transparent dynamic optimization system. SIGPLAN Not. 35 (5), 1–12 (2000)

    Article  Google Scholar 

  3. F. Bellard, Qemu, a fast and portable dynamic translator. In ATEC ’05: Proceedings of the Annual Conference on USENIX Annual Technical Conference (USENIX Association, Berkeley, CA, USA, 2005), pp. 41–41

    Google Scholar 

  4. Y. Bertot, P. Castéran, Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science (Springer, New York, 2004)

    Google Scholar 

  5. F. Bobot, J.C. Filliâtre, C. Marché, A. Paskevich, Why3: Shepherd your herd of provers. Boogie 2011, 53–64 (2011)

    Google Scholar 

  6. D. Burger, T.M. Austin, The simplescalar tool set, version 2.0. SIGARCH Comput. Archit. News 25 (3), 13–25 (1997)

    Google Scholar 

  7. B. Campbell, An executable semantics for Compcert C. In Certified Programs and Proofs (Springer, New York, 2012), pp. 60–75

    Google Scholar 

  8. G. Canet, P. Cuoq, B. Monate, A value analysis for C programs. In SCAM’09 (IEEE, Los Alamitos, 2009), pp. 123–124

    Google Scholar 

  9. B. Cmelik, D. Keppel, Shade: A fast instruction-set simulator for execution profiling. In SIGMETRICS ’94: Proceedings of the 1994 ACM SIGMETRICS Conference on Measurement and Modeling of Computer Systems (ACM, New York, NY, USA, 1994), pp. 128–137

    Google Scholar 

  10. Coq Development Team, The Coq Reference Manual, Version 8.2. INRIA Rocquencourt, France, 2008. http://coq.inria.fr/

  11. J.-C. Filliâtre, C. Marché, The Why/Krakatoa/Caduceus platform for deductive program verification. In Proceedings of the 19th International Conference on Computer Aided Verification, Lecture Notes in Computer Science 4590, 2007. http://why.lri.fr/

  12. A.C.J. Fox, M.O. Myreen, A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture. In ITP, pp. 243–258, 2010

    Google Scholar 

  13. Y. Futamura, Partial evaluation of computation process—an approach to a compiler-compiler. Higher Order Symb. Comput. 12 (4), 381–391 (1999)

    Article  MATH  Google Scholar 

  14. F. Ghenassia (ed.), Transaction-Level Modeling with SystemC. TLM Concepts and Applications for Embedded Systems (Springer, New York, 2005). ISBN 0-387-26232-6

    Google Scholar 

  15. G. Hamerly, E. Perelman, B. Calder, How to use simpoint to pick simulation points. SIGMETRICS Perform. Eval. Rev. 31 (4), 25–30 (2004)

    Article  Google Scholar 

  16. C. Helmstetter, V. Joloboff, SimSoC: A SystemC TLM integrated ISS for full system simulation. In IEEE Asia Pacific Conference on Circuits and Systems - APCCAS’08, November 2008. http://formes.asia/cms/software/simsoc

  17. H. Hongwei, S. Jiajia, C. Helmstetter, V. Joloboff, Generation of executable representation for processor simulation with dynamic translation. In Proceedings of the International Conference on Computer Science and Software Engineering (IEEE, Wuhan, China, 2008)

    Google Scholar 

  18. IEEE, Open SystemC Language Reference Manual, 2011. http://standards.ieee.org/getieee/1666/download/1666-2011.pdf

    Google Scholar 

  19. V. Joloboff, X. Zhou, C. Helmstetter, X. Gao, Fast Instruction Set Simulation Using LLVM-based Dynamic Translation. In International MultiConference of Engineers and Computer Scientists 2011, vol. 2188, IAENG (Springer, Hong Kong, China, 2011), pp. 212–216

    Google Scholar 

  20. D. Jones, N. Topham, High speed cpu simulation using ltu dynamic binary translation. In Proceedings of the 4th International Conference on High Performance Embedded Architectures and Compilers, HiPEAC ’09 (Springer, Berlin, Heidelberg, 2009), pp. 50–64

    Google Scholar 

  21. G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, S. Winwood, sel4: Formal verification of an os kernel. In Proceedings of the ACM SIGOPS 22Nd Symposium on Operating Systems Principles, SOSP ’09 (ACM, New York, NY, USA, 2009), pp. 207–220

    Google Scholar 

  22. C. Lattner, V. Adve, LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. In Proceedings of the 2004 International Symposium on Code Generation and Optimization (CGO’04), Palo Alto, California, Mar 2004

    Google Scholar 

  23. X. Leroy, Formal verification of a realistic compiler. Commun. ACM 52 (7), 107–115 (2009)

    Article  Google Scholar 

  24. X. Leroy, The CompCert C verified compiler. Documentation and user’s manual. INRIA Paris-Rocquencourt, March 2012. http://creativecommons.org/licenses/by-nc-sa/3.0/

  25. W. Liu, M.C. Huang, Expert: expedited simulation exploiting program behavior repetition. In Proceedings of the 18th Annual International Conference on Supercomputing, ICS ’04 (ACM, New York, NY, USA, 2004), pp. 126–135

    Google Scholar 

  26. J.-F. Monin, X. Shi, Handcrafted inversions made operational on operational semantics. In ITP 2013 vol. 7998 of LNCS, ed. by S. Blazy, C. Paulin, D. Pichardie (Springer, Rennes, France, 2013), pp. 338–353

    Google Scholar 

  27. A. Nohl, G. Braun, O. Schliebusch, R. Leupers, H. Meyr, A. Hoffmann, A universal technique for fast and flexible instruction-set architecture simulation. In DAC ’02: Proceedings of the 39th Conference on Design Automation, DAC ’02 (ACM, New York, NY, USA, 2002), pp. 22–27

    Google Scholar 

  28. Open SystemC Initiative, OSCI SystemC TLM 2.0 User Manual, 2008. http://www.systemc.org/

  29. C. Pusch, Proving the soundness of a Java bytecode verifier specification in Isabelle/HOL. In TACAS’99 (Springer, New York, 1999), pp. 89–103

    Google Scholar 

  30. W. Qin, J. D’Errico, X. Zhu, A multiprocessing approach to accelerate retargetable and portable dynamic-compiled instruction-set simulation. In CODES+ISSS’06 (ACM, New York, NY, USA, 2006), pp. 193–198

    Google Scholar 

  31. M. Reshadi, P. Mishra, N. Dutt, Instruction set compiled simulation: a technique for fast and flexible instruction set simulation. In Design Automation Conference, 2003. Proceedings, pp. 758–763, 2003

    Google Scholar 

  32. K. Scott, N. Kumar, S. Velusamy, B. Childers, J.W. Davidson, M.L. Soffa, Retargetable and reconfigurable software dynamic translation. In Proceedings of the International Symposium on Code Generation and Optimization (CGO’03), 2003

    Google Scholar 

  33. D. Seal, ARM Architecture Reference Manual (Addison-Wesley Longman Publishing, Boston, 2000)

    Google Scholar 

  34. H. Shi, Y. Wang, H. Guan, A. Liang, An intermediate language level optimization framework for dynamic binary translation. SIGPLAN Not. 42 (5), 3–9 (2007)

    Article  Google Scholar 

  35. E. Witchel, M. Rosenblum, Embra: fast and flexible machine simulation. In SIGMETRICS ’96: Proceedings of the 1996 ACM SIGMETRICS International Conference on Measurement and Modeling of Computer Systems (ACM, New York, NY, USA, 1996), pp. 68–79

    Google Scholar 

  36. R.E. Wunderlich, T.F. Wenisch, B. Falsafi, J.C. Hoe, Smarts: accelerating microarchitecture simulation via rigorous statistical sampling. In Proceedings. 30th Annual International Symposium on Computer Architecture, 2003, pp. 84–95, 2003

    Google Scholar 

  37. Z. Zhang, V. Joloboff, X. Zhou, C. Helmstetter, Fast dynamic translation using llvm on multi-core hosts. In 5th Workshop on Architectural and Microarchitectural Support for Binary Translation (AMAS-BT) (Intel Corporation, Portland, Oregon, USA, June 2012)

    Google Scholar 

Download references

Acknowledgements

This work has been partly funded by the international collaboration support of France ANR and NSFC China in the SIVES project.

Author information

Authors and Affiliations

  1. East China Normal University, Shanghai, China

    Vania Joloboff

  2. INRIA, Grenoble, France

    Vania Joloboff

  3. Verimag, Université Grenoble Alpes, Grenoble, France

    Jean-Francois Monin

  4. Tsinghua University, Shanghai, China

    Xiaomu Shi

Authors
  1. Vania Joloboff
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jean-Francois Monin
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Xiaomu Shi
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Vania Joloboff .

Editor information

Editors and Affiliations

  1. Campus MINATEC, CEA, Grenoble, France

    Anca Molnos

  2. Campus MINATEC, CEA, Grenoble, France

    Christian Fabre

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this chapter

Cite this chapter

Joloboff, V., Monin, JF., Shi, X. (2017). SimSoC: A Fast, Proven Faithful, Full System Virtual Prototyping Framework. In: Molnos, A., Fabre, C. (eds) Model-Implementation Fidelity in Cyber Physical System Design. Springer, Cham. https://doi.org/10.1007/978-3-319-47307-9_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-47307-9_5

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-47306-2

  • Online ISBN: 978-3-319-47307-9

  • eBook Packages: EngineeringEngineering (R0)

Publish with us

Policies and ethics

Search

Navigation