Abstract
The pressure to create a working System on Chip design as early as possible leads designers to consider using a platform based design method. In this approach, designing an application is a matter of selecting from a set of standard components with compatible specifications. Subsequently, a formal verification platform can be constructed. The formal verification platform provides an environment to analysed the combined properties of the design. In this paper, we present a methodology to do formal System on Chip analysis by developing generic formal components that can be integrated in a formal verification platform. First, we develop reusable formal properties of standard components. Second, we define a generic formal platform in which components of System on Chip design can be integrated. The platform contains basic components such as a standard bus protocol and a processor. Third, we combine the properties of standard components and obtain a set of refined properties of the system. We use these properties to develop the required specifications of the remaining components.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Aagaard, M.D., Jones, R.B., Seger, C.-J.H.: Combining Theorem Proving and Trajectory Evaluation in an Industrial Environment. In: The 35th Design Automation Conference, San Francisco, California, June 1998, pp. 538–541 (1998)
ARM, ARM-7 Datasheet, DDI 0020C (December 1994)
ARM, AMBA specification ver 2.0, IHI-0011A (May 1999)
Birnbaum, M., Sachs, H.: How VSIA Answers the SOC Dilemma. In: IEEE Computer magazine, June 1999, pp. 42–50 (1999)
Camilleri, A.J.: A Hybrid Approach to Verifying Liveness in a Symmetric Multi- Processor. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol. 1275, pp. 49–67. Springer, Heidelberg (1997)
Chang, H., Cooke, L., Hunt, M., Martin, G., McNelly, A., Todd, L.: Surviving the SOC Revolution. In: A Guide to Platform-Based Design. Kluwer, Dordrecht (1999)
Dennis, L.A., Collins, G., Norrish, M., Boulton, R., Slind, K., Robinson, G., Gordon, M., Melham, T.: The PROSPER Toolkit. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 78–92. Springer, Heidelberg (2000)
Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, Cambridge (1993)
The HOL System Description, HOL98 Taupo–6, University of Cambridge (February 2000)
Hunt, W.A.: FM8501: A Verified Microprocessor. LNCS, vol. 795. Springer, Heidelberg (1994)
Ip, C.N., Dill, D.L.: Better Verification Through Symmetry. In: Agnew, D., Claesen, L., Compasano, R. (eds.) Computer Hardware Description Languages and their Applications, pp. 87–100. Elsevier Science Publishers, Amsterdam
Jones, R.B., O’Leary, J.W., Seger, C.-J.H., Aagaard, M.D., Melham, T.F.: Practical Formal Verification in Microprocessor Design. IEEE Design & Test of Computers magazine, 16–25 (July/August 2001)
Litterick, M.: ARM Integration Platform Power Management, Scotland. The Institute of System Level Integration (November 2001)
Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning, An Approach. Kluwer, Dordrecht (2000)
Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning, ACL2 Case Studies. Kluwer, Dordrecht (2000)
Keating, M., Bricaud, P.: Reuse Methodology Manual For System–On– a–Chip Designs. Kluwer Academic Publisher, Norwell (1999)
McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publisher, Norwell (1993)
Moore, J.S.: Symbolic Simulation: An ACL2 Approach. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol. 1522, pp. 334–350. Springer, Heidelberg (1998)
Pixley, C.: Formal Verification of Commercial Integrated Circuits. IEEE Design & Test of Computers magazine, 4–5 (July/August 2001)
RAPIER, The Institute of System Level Integration, Scotland (2001)
Rincon, A.M., Cherichetti, C., Monzel, J.A., Stauffer, D.R., Trick, M.T.: Core Design and System-on-a-Chip Integration. IEEE Design & Test of Computers magazine, 26–35 (October–December 1997)
Schneider, K.: Yet another look at LTL model checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 321–325. Springer, Heidelberg (1999)
Shimizu, K., Dill, D.L., Chou, C.-T.: A Specification Methodology by a Collection of Compact Properties as Applied to the Intel Itanium Processor Bus Protocol. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol. 2144, pp. 340–354. Springer, Heidelberg (2001)
Srivas, M., Rueβ, H., Cyrluk, D.: Hardware Verification using PVS. In: Kropf, T. (ed.) Formal Hardware Verification. LNCS, vol. 1287, pp. 156–205. Springer, Heidelberg (1997)
Staples, M.: Linking ACL2 and Hol, Computer Laboratory, University of Cambridge, Technical Report No. 476 (November 1999)
Susanto, K.W.: An integrated Formal Approach for System on Chip. In: IP based Design, Grenoble, France, October 2002, pp. 119–123 (2002)
Winston, P.H., Horn, B.K.P.: LISP. Addison-Wesley Pub.Co., Reading (1989)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Susanto, K.W., Melham, T. (2003). An AMBA-ARM7 Formal Verification Platform. In: Dong, J.S., Woodcock, J. (eds) Formal Methods and Software Engineering. ICFEM 2003. Lecture Notes in Computer Science, vol 2885. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39893-6_5
Download citation
DOI: https://doi.org/10.1007/978-3-540-39893-6_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20461-9
Online ISBN: 978-3-540-39893-6
eBook Packages: Springer Book Archive