{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T22:04:56Z","timestamp":1725573896980},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540204619"},{"type":"electronic","value":"9783540398936"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-39893-6_5","type":"book-chapter","created":{"date-parts":[[2011,1,7]],"date-time":"2011-01-07T15:35:57Z","timestamp":1294414557000},"page":"48-67","source":"Crossref","is-referenced-by-count":4,"title":["An AMBA-ARM7 Formal Verification Platform"],"prefix":"10.1007","author":[{"given":"Kong Woei","family":"Susanto","sequence":"first","affiliation":[]},{"given":"Tom","family":"Melham","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"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\u2013541 (1998)","DOI":"10.1145\/277044.277189"},{"key":"5_CR2","unstructured":"ARM, ARM-7 Datasheet, DDI 0020C (December 1994)"},{"key":"5_CR3","unstructured":"ARM, AMBA specification ver 2.0, IHI-0011A (May 1999)"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"Birnbaum, M., Sachs, H.: How VSIA Answers the SOC Dilemma. In: IEEE Computer magazine, June 1999, pp. 42\u201350 (1999)","DOI":"10.1109\/2.769442"},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/BFb0028385","volume-title":"Theorem Proving in Higher Order Logics","author":"A.J. Camilleri","year":"1997","unstructured":"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.\u00a01275, pp. 49\u201367. Springer, Heidelberg (1997)"},{"key":"5_CR6","volume-title":"A Guide to Platform-Based Design","author":"H. Chang","year":"1999","unstructured":"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)"},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/3-540-46419-0_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L.A. Dennis","year":"2000","unstructured":"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.\u00a01785, pp. 78\u201392. Springer, Heidelberg (2000)"},{"volume-title":"Introduction to HOL: A theorem proving environment for higher order logic","year":"1993","key":"5_CR8","unstructured":"Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, Cambridge (1993)"},{"key":"5_CR9","unstructured":"The HOL System Description, HOL98 Taupo\u20136, University of Cambridge (February 2000)"},{"key":"5_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-57960-5","volume-title":"FM8501: A Verified Microprocessor","author":"W.A. Hunt","year":"1994","unstructured":"Hunt, W.A.: FM8501: A Verified Microprocessor. LNCS, vol.\u00a0795. Springer, Heidelberg (1994)"},{"key":"5_CR11","unstructured":"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\u2013100. Elsevier Science Publishers, Amsterdam"},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"Jones, R.B., O\u2019Leary, 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\u201325 (July\/August 2001)","DOI":"10.1109\/54.936245"},{"key":"5_CR13","unstructured":"Litterick, M.: ARM Integration Platform Power Management, Scotland. The Institute of System Level Integration (November 2001)"},{"key":"5_CR14","volume-title":"Computer-Aided Reasoning, An Approach","author":"M. Kaufmann","year":"2000","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning, An Approach. Kluwer, Dordrecht (2000)"},{"key":"5_CR15","volume-title":"Computer-Aided Reasoning, ACL2 Case Studies","author":"M. Kaufmann","year":"2000","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning, ACL2 Case Studies. Kluwer, Dordrecht (2000)"},{"key":"5_CR16","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-5037-2","volume-title":"Reuse Methodology Manual For System\u2013On\u2013 a\u2013Chip Designs","author":"M. Keating","year":"1999","unstructured":"Keating, M., Bricaud, P.: Reuse Methodology Manual For System\u2013On\u2013 a\u2013Chip Designs. Kluwer Academic Publisher, Norwell (1999)"},{"key":"5_CR17","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publisher, Norwell (1993)"},{"key":"5_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/3-540-49519-3_22","volume-title":"Formal Methods in Computer-Aided Design","author":"J.S. Moore","year":"1998","unstructured":"Moore, J.S.: Symbolic Simulation: An ACL2 Approach. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol.\u00a01522, pp. 334\u2013350. Springer, Heidelberg (1998)"},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"Pixley, C.: Formal Verification of Commercial Integrated Circuits. IEEE Design & Test of Computers magazine, 4\u20135 (July\/August 2001)","DOI":"10.1109\/MDT.2001.936243"},{"key":"5_CR20","unstructured":"RAPIER, The Institute of System Level Integration, Scotland (2001)"},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"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\u201335 (October\u2013December 1997)","DOI":"10.1109\/54.632878"},{"key":"5_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/3-540-48153-2_25","volume-title":"Correct Hardware Design and Verification Methods","author":"K. Schneider","year":"1999","unstructured":"Schneider, K.: Yet another look at LTL model checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol.\u00a01703, pp. 321\u2013325. Springer, Heidelberg (1999)"},{"key":"5_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/3-540-44798-9_27","volume-title":"Correct Hardware Design and Verification Methods","author":"K. Shimizu","year":"2001","unstructured":"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.\u00a02144, pp. 340\u2013354. Springer, Heidelberg (2001)"},{"key":"5_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"156","DOI":"10.1007\/3-540-63475-4_4","volume-title":"Formal Hardware Verification","author":"M. Srivas","year":"1997","unstructured":"Srivas, M., Rue\u03b2, H., Cyrluk, D.: Hardware Verification using PVS. In: Kropf, T. (ed.) Formal Hardware Verification. LNCS, vol.\u00a01287, pp. 156\u2013205. Springer, Heidelberg (1997)"},{"key":"5_CR25","unstructured":"Staples, M.: Linking ACL2 and Hol, Computer Laboratory, University of Cambridge, Technical Report No. 476 (November 1999)"},{"key":"5_CR26","unstructured":"Susanto, K.W.: An integrated Formal Approach for System on Chip. In: IP based Design, Grenoble, France, October 2002, pp. 119\u2013123 (2002)"},{"key":"5_CR27","volume-title":"LISP","author":"P.H. Winston","year":"1989","unstructured":"Winston, P.H., Horn, B.K.P.: LISP. Addison-Wesley Pub.Co., Reading (1989)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-39893-6_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T17:43:35Z","timestamp":1559929415000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-39893-6_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540204619","9783540398936"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-39893-6_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}