MMU Simulation in Hardware Simulator Based-on State Transition Models

Authors: Zhang Xiuping, Yang Guowu, Zheng Desheng

Abstract:

Embedded hardware simulator is a valuable computeraided tool for embedded application development. This paper focuses on the ARM926EJ-S MMU, builds state transition models and formally verifies critical properties for the models. The state transition models include loading instruction model, reading data model, and writing data model. The properties of the models are described by CTL specification language, and they are verified in VIS. The results obtained in VIS demonstrate that the critical properties of MMU are satisfied in the state transition models. The correct models can be used to implement the MMU component in our simulator. In the end of this paper, the experimental results show that the MMU can successfully accomplish memory access requests from CPU.

Keywords: MMU, State transition, Model, Simulation.

Digital Object Identifier (DOI): doi.org/10.5281/zenodo.1076322

References:

[1] ARM. ARM926EJ-S Technical Reference Manual. ARM Limited, www.arm.com, r0p5 edition, 2008.
[2] C. Helmstetter, V. Joloboff, and H. Xiao. Simsoc: A full system simulation software for embedded systems. In Open-source Software for Scientific Computation (OSSC), 2009 IEEE International Workshop on, pages 49-55. IEEE.
[3] T. Andersson and P. Magnusson. Powerpc mmu simulation. Bachelor-s project, Karlstad University, Sweden, http://www.cs.kau.se/cs/, 2001.
[4] B. Egger, S. Kim, C. Jang, J. Lee, S.L. Min, and H. Shin. Scratchpad memory management techniques for code in embedded systems without an mmu. Computers, IEEE Transactions on, 59(8):1047-1062, 2010.
[5] J.R. Haigh, M.W. Wilkerson, J.B. Miller, T.S. Beatty, S.J. Strazdus, and L.T. Clark. A low-power 2.5-ghz 90-nm level 1 cache and memory management unit. Solid-State Circuits, IEEE Journal of, 40(5):1190- 1199, 2005.
[6] S.K. Agun and J.M. Chang. Design of a reusable memory management system. In ASIC/SOC Conference, 2001. Proceedings. 14th Annual IEEE International, pages 369-373. IEEE, 2001.
[7] X. Zhang, G. Yang, and D. Zheng. Component-based model for simulating the mmu coprocessor. In Information Engineering and Computer Science (ICIECS), 2010 2nd International Conference on, pages 1-4. IEEE.
[8] DC McLernon. Properties for state-transition matrix of lptv twodimensional filter. Electronics Letters, 38(25):1748-1750, 2002.
[9] Y.C. Lee and A.Y. Zomaya. A novel state transition method for metaheuristic-based scheduling in heterogeneous computing systems. IEEE Transactions on Parallel and Distributed Systems, pages 1215- 1223, 2008.
[10] A. Chander, D. Dean, and J.C. Mitchell. A state-transition model of trust management and access control. In Proceedings of the 14th IEEE Computer Security Foundations Workshop, pages 27-43. Citeseer, 2001.
[11] E. Clarke. Model checking. In Foundations of Software Technology and Theoretical Computer Science, pages 54-56. Springer, 1997.
[12] B. Nicolescu, N. Gorse, Y. Savaria, E.M. Aboulhamid, and R. Velazco. On the use of model checking for the verification of a dynamic signature monitoring approach. Nuclear Science, IEEE Transactions on, 52(5):1555-1561, 2005.
[13] T. Han, J.P. Katoen, and B. Damman. Counterexample generation in probabilistic model checking. IEEE transactions on software engineering, pages 241-257, 2009.
[14] R. Brayton, G. Hachtel, A. Sangiovanni-Vincentelli, F. Somenzi, A. Aziz, S. Cheng, S. Edwards, S. Khatri, Y. Kukimoto, A. Pardo, et al. Vis: A system for verification and synthesis. In Computer Aided Verification, pages 428-432. Springer, 1996.
[15] H. Peng, S. Tahar, and F. Khendek. Comparison of spin and vis for protocol verification. International Journal on Software Tools for Technology Transfer (STTT), 4(2):234-245, 2003.
[16] J. Yoo, E. Jee, and S.S. Cha. Formal modeling and verification of safetycritical software. IEEE Software, pages 42-49, 2009.
[17] Q. Zhao and B.H. Krogh. Formal verification of statecharts using finite-state model checkers. In American Control Conference, 2001. Proceedings of the 2001, volume 1, pages 313-318. IEEE, 2001.
[18] M. Bourahla. Distributed ctl model checking. In Software, IEE Proceedings-, volume 152, pages 297-308. IET, 2005.