MMU Simulation in Hardware Simulator Based-on State Transition Models
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.
[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.
[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.
@article{"International Journal of Information, Control and Computer Sciences:60012", author = "Zhang Xiuping and Yang Guowu and Zheng Desheng", title = "MMU Simulation in Hardware Simulator Based-on State Transition Models", 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.", volume = "5", number = "8", pages = "917-5", }
