{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,3]],"date-time":"2025-04-03T06:03:46Z","timestamp":1743660226109},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540412199"},{"type":"electronic","value":"9783540409229"}],"license":[{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-40922-x_17","type":"book-chapter","created":{"date-parts":[[2007,11,29]],"date-time":"2007-11-29T04:41:36Z","timestamp":1196311296000},"page":"300-319","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":18,"title":["A Methodology for Large-Scale Hardware Verification"],"prefix":"10.1007","author":[{"given":"Mark D.","family":"Aagaard","sequence":"first","affiliation":[]},{"given":"Robert B.","family":"Jones","sequence":"additional","affiliation":[]},{"given":"Thomas F.","family":"Melham","sequence":"additional","affiliation":[]},{"given":"John W.","family":"O\u2019Leary","sequence":"additional","affiliation":[]},{"given":"Carl-Johan H.","family":"Seger","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,6,18]]},"reference":[{"key":"17_CR1","unstructured":"J. Bergeron, Writing Testbenches: Functional Verification of HDL Models, Kluwer Academic Publishers, 2000."},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"T. Kropf, Introduction to Formal Hardware Verification, Springer-Verlag, 1999.","DOI":"10.1007\/978-3-662-03809-3"},{"key":"17_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/3-540-49519-3_5","volume-title":"Formal Methods in Computer-Aided Design","author":"\u00c1. Th. Th. Eirkksson","year":"1998","unstructured":"\u00c1. Th. Eirkksson, \u201cThe formal design of 1M-gate ASICs,\u201d in Formal Methods in Computer-Aided Design, G. Gopalakrishnan and P. Windley, Eds. 1998, vol. 1522 of Lecture Notes in Computer Science, pp. 49\u201363, Springer Verlag."},{"key":"17_CR4","unstructured":"J. O'Leary, X. Zhao, R. Gerth, and C.-J. H. Seger, \u201cFormally verifying IEEE compliance of floating-point hardware,\u201d Intel Technical Journal, First quarter, 1999, Available at developer.\n                    http:\/\/intel.com\/technology\/itj\/"},{"key":"17_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1007\/3-540-48153-2_10","volume-title":"Correct Hardware Design and VerificationMethods","author":"Y. Xu","year":"1999","unstructured":"Y. Xu, E. Cerny, A. Silburt, A. Coady, Y. Liu, and P. Pownall, \u201cPractical appli-cation of formal verification techniques on a frame mux\/demux chip from Nortel Semiconductors,\u201d in Correct Hardware Design and VerificationMethods, Laurence Pierre and Thomas Kropf, Eds. 1999, vol. 1703 of Lecture Notes in Computer Science, pp. 110\u2013124, Springer-Verlag."},{"issue":"2","key":"17_CR6","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BF01383966","volume":"6","author":"C.-J. H. Seger","year":"1995","unstructured":"C.-J. H. Seger and R. E. Bryant, \u201cFormal verification by symbolic evaluation of partially-ordered trajectories,\u201d Formal Methods in System Design, vol. 6, no. 2, pp. 147\u2013189, March 1995.","journal-title":"Formal Methods in System Design"},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"L. Paulson, ML for the Working Programmer, Cambridge University Press, 1996.","DOI":"10.1017\/CBO9780511811326"},{"key":"17_CR8","unstructured":"E. M. Clarke, O. Grumberg, and D. Peled, Model Checking, MIT Press, 1999."},{"issue":"8","key":"17_CR9","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. E. Bryant","year":"1986","unstructured":"R. E. Bryant, \u201cGraph-based algorithms for boolean function manipulation,\u201d IEEE Transactions on Computers, vol. C-35, no. 8, pp. 677\u2013691, 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"M. D. Aagaard, R. B. Jones, and C.-J. H. Seger, \u201cFormal verification using parametric representations of boolean constraints,\u201d in ACM\/IEEE Design Automation Conference, 1999.","DOI":"10.1145\/309847.309968"},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"M. D. Aagaard, R. B. Jones, and C.-J. H. Seger, \u201cCombining theorem proving and trajectory evaluation in an industrial environment,\u201d in ACM\/IEEE Design Automation Conference, 1998, pp. 538\u2013541.","DOI":"10.1145\/277044.277189"},{"key":"17_CR12","unstructured":"M. J. C. Gordon and T. F. Melham, Eds., Introduction to HOL: A theorem proving environment for higher order logic, Cambridge University Press, 1993."},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"L. Augustson, \u201cA compiler for lazy-ml,\u201d in ACM Symposium on Functional Programming, 1984, pp. 218\u2013227.","DOI":"10.1145\/800055.802038"},{"key":"17_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/3-540-48256-3_22","volume-title":"Theorem Proving in Higher Order Logics","author":"M. D. Aagaard","year":"1999","unstructured":"M. D. Aagaard, R. B. Jones, and C.-J. H. Seger, \u201cLifted-fl: A pragmatic implementation of combined model checking and theorem proving,\u201d in Theorem Proving in Higher Order Logics, Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Th\u00e9ry, Eds. 1999, vol. 1690 of Lecture Notes in Computer Science, pp. 323\u2013340, Springer-Verlag."},{"key":"17_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/3-540-48256-3_14","volume-title":"Theorem Proving in Higher Order Logics","author":"D. Syme","year":"1999","unstructured":"D. Syme, \u201cThree tactic theorem proving,\u201d in Theorem Proving in Higher Order Logics, Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin,and L. Th\u00e9ry, Eds. 1999, vol. 1690 of Lecture Notes in Computer Science, pp. 203\u2013220, Springer-Verlag."},{"key":"17_CR16","unstructured":"J. Feldman and C. Retter, Computer Architecture: A Designer\u2019s Text Based on a Generic RISC, McGraw-Hill, 1994."}],"container-title":["Lecture Notes in Computer Science","Formal Methods in Computer-Aided Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-40922-X_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,29]],"date-time":"2020-01-29T07:48:11Z","timestamp":1580284091000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-40922-X_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540412199","9783540409229"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-40922-x_17","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]},"assertion":[{"value":"18 June 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}