{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:30:28Z","timestamp":1725456628272},"publisher-location":"Berlin\/Heidelberg","reference-count":24,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354056778X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0021728","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T09:47:42Z","timestamp":1132739262000},"page":"242-257","source":"Crossref","is-referenced-by-count":1,"title":["Embedding hardware verification within a commercial design framework"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Kropf","sequence":"first","affiliation":[]},{"given":"Ramayya","family":"Kumar","sequence":"additional","affiliation":[]},{"given":"Klaus","family":"Schneider","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"19_CR1","unstructured":"M.C. McFarland, A.C. Parker, and R. Camposano. Tutorial on high-level synthesis. In 25th Design Automation Conference, pages 330\u2013336, 1988."},{"key":"19_CR2","doi-asserted-by":"crossref","unstructured":"O. Coudert, C. Berthet, and J.C. Madre. Verification of synchronous sequential machines based on symbolic execution. In Workshop on Automatic Verification Methods for Finite State Systems, pages 365\u2013373, June 1989.","DOI":"10.1007\/3-540-52148-8_30"},{"key":"19_CR3","doi-asserted-by":"crossref","unstructured":"J.R. Burch, E.M. Clarke, and D. E. Long. Representing circuits more efficiently in symbolic model checking. In 28th Design Automation Conference, pages 403\u2013407, 1991.","DOI":"10.1145\/127601.127702"},{"key":"19_CR4","doi-asserted-by":"crossref","unstructured":"Th. Kropf and H.-J. Wunderlich. A common approach to test generation and hardware-verification based on temporal logic. In Proceedings of the International Test Conference, pages 57\u201366, October 1991.","DOI":"10.1109\/TEST.1991.519494"},{"key":"19_CR5","volume-title":"PhD thesis","author":"W. A. Hunt","year":"1985","unstructured":"W. A. Hunt. FM8501: A Verified Microprocessor. PhD thesis, University of Texas, Austin, 1985."},{"key":"19_CR6","doi-asserted-by":"crossref","unstructured":"M.J.C. Gordon. A proof generating system for higher-order logic. In G. Birtwistle and P.A. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis. Kluwer, 1988.","DOI":"10.1007\/978-1-4613-2007-4_3"},{"issue":"2","key":"19_CR7","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1007\/BF01383880","volume":"2","author":"R. Kumar","year":"1993","unstructured":"R. Kumar, K. Schneider, and Th. Kropf. Structuring and automating hardware proofs in a higher-order theorem-proving environment. Journal of Formal System Design, 2(2):165\u2013230, 1993.","journal-title":"Journal of Formal System Design"},{"key":"19_CR8","unstructured":"M.J.C. Gordon. Why higher-order logic is a good formalism for specifying and verifying hardware. In G. Milne and P.A. Subrahmanyam, editors, Formal aspects of VLSI Design. North-Holland, 1986."},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"J. Joyce. Formal verification and implementation of a microprocessor. In G. Birtwistle and P.A. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis. Kluwer, 1988.","DOI":"10.1007\/978-1-4613-2007-4_4"},{"key":"19_CR10","unstructured":"J. Joyce. More reasons why higher-order logic is a good formalism for specifying and verifying hardware. In International Workshop on Formal Methods in VLSI Design, Miami, 1991."},{"key":"19_CR11","unstructured":"J.D. Morison, N.E. Peeling, and T.L. Thorp. ELLA: A hardware description language. In International Conference on Circuits and Computers, pages 604\u2013607, 1988."},{"key":"19_CR12","unstructured":"R. Boulton, A. Gordon, M. Gordon, J. Herbert, and J. van Tassel. Experiences with Embedding hardware description languages in HOL. In V. Stavridou, T.F. Melham, and R. Boute, editors, Conference on Theorem Provers in Circuit Design, IFIP Transactions A-10, pages 129\u2013156. North-Holland, 1992."},{"key":"19_CR13","unstructured":"CADENCE Design Systems Inc. CADENCE User Manuals, July 1989."},{"key":"19_CR14","unstructured":"E. Mayger and M. P. Fourman. Integration of formal methods with system design. In International Conference on Very Large Scale Integration, pages 59\u201369, 1991. Edinburgh."},{"key":"19_CR15","unstructured":"F.K. Hanna and N. Daeche. Specification and verification using higher-order logic. In C.J. Koomen and T. Moto-Oka, editors, Conference on Computer Hardware Description Languages and their Applications, pages 418\u2013433. North-Holland, 1985."},{"key":"19_CR16","doi-asserted-by":"crossref","unstructured":"P. Camurati and P. Prinetto. Formal verification of hardware correctness: Introduction and survey of current research. IEEE-Computer, pages 8\u201319, 1988.","DOI":"10.1109\/2.65"},{"key":"19_CR17","doi-asserted-by":"crossref","unstructured":"H. Eveking. Verifikation digitaler Systeme. Teubner Verlag, 1991.","DOI":"10.1007\/978-3-322-94684-3"},{"key":"19_CR18","unstructured":"J.H. Gallier. Logic for Computer Science\u2014Foundations of Automated Theorem Proving. Number 5 in Computer Science and Technology Series. Harper & Row, 1986."},{"key":"19_CR19","first-page":"766","volume-title":"number 607 in Lecture Notes in Computer Science","author":"K. Schneider","year":"1992","unstructured":"K. Schneider, R. Kumar, and Th. Kropf. The FAUST prover. In D. Kapur, editor, 11th Conference on Automated Deduction, number 607 in Lecture Notes in Computer Science, pages 766\u2013770. Springer Verlag, Albany, New York,1992."},{"key":"19_CR20","unstructured":"K. Schneider, R. Kumar, and Th. Kropf. Accelerating tableaux proofs using compact representations. Journal of Formal System Design, 1993."},{"key":"19_CR21","doi-asserted-by":"crossref","unstructured":"K. Schneider, R. Kumar, and Th. Kropf. Modelling generic hardware structures by abstract datatypes. In M. Gordon L. Claesen, editor, International Workshop on Higher Order Logic Theorem Proving and its Applications, pages 419\u2013429. Elsevier Science Publishers, 1992.","DOI":"10.1016\/B978-0-444-89880-7.50017-6"},{"key":"19_CR22","unstructured":"K. Schneider, R. Kumar, and Th. Kropf. Hardware verification with first-order BDD's. In Conference on Computer Hardware Description Languages, 1993."},{"key":"19_CR23","doi-asserted-by":"crossref","unstructured":"K. G\u00f6del. \u00dcber formal unentscheidbare S\u00e4tze der Principia Mathematica und verwandter Systeme. Monatshefte f\u00fcr Mathematik und Physik, 1, 1931.","DOI":"10.1007\/BF01700692"},{"key":"19_CR24","unstructured":"R. Reetz and Th. Kropf. Ein formales Flu\u00dfgraphenmodell zur Integration von Hardwarebeschreibungssprachen in die Hardware-Verifikation (in german). In Th. Kropf, R. Kumar, and D. Schmid, editors, Proc. GI\/ITG Workshop on Formal Methods for Correct System Design, Technical Report 10\/93. University of Karlsruhe, 1993."}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/www.springerlink.com\/index\/pdf\/10.1007\/BFb0021728","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T04:50:33Z","timestamp":1586580633000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0021728"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354056778X"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/bfb0021728","relation":{},"subject":[]}}