{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:47:52Z","timestamp":1725551272122},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540665595"},{"type":"electronic","value":"9783540481539"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48153-2_18","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T21:13:28Z","timestamp":1269897208000},"page":"238-250","source":"Crossref","is-referenced-by-count":3,"title":["Formal Verification of Designs with Complex Control by Symbolic Simulation"],"prefix":"10.1007","author":[{"given":"Gerd","family":"Ritter","sequence":"first","affiliation":[]},{"given":"Hans","family":"Eveking","sequence":"additional","affiliation":[]},{"given":"Holger","family":"Hinrichsen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,6,3]]},"reference":[{"key":"18_CR1","series-title":"Lect Notes Comput Sci","volume-title":"Proc. FMCAD\u201996","author":"C. W. Barrett","year":"1996","unstructured":"C. W. Barrett, D.L. Dill, and J. R. Levitt: Validity checking for combinations of theories with equality. In Proc. FMCAD\u201996,Springer LNCS 1166, 1996."},{"key":"18_CR2","doi-asserted-by":"crossref","unstructured":"C. W. Barrett, D. L. Dill, and J. R. Levitt: A decision procedure for bit-vector arithmetic. In Proc. DAC\u201998, 1998.","DOI":"10.21236\/ADA400400"},{"key":"18_CR3","doi-asserted-by":"crossref","unstructured":"D. L. Beatty and R. E. Bryant: Formally verifying a microprocessor using a simulation methodology. In Proc. DAC\u201994, 1994.","DOI":"10.1145\/196244.196575"},{"key":"18_CR4","unstructured":"B. Brock, W. A. Hunt, and M. Kaufmann: The FM9001 microprocessor proof. Technical Report 86, Computational Logic Inc., 1994."},{"key":"18_CR5","series-title":"Lect Notes Comput Sci","volume-title":"Proc. FMCAD\u201996","author":"B. Brock","year":"1996","unstructured":"B. Brock, M. Kaufmann, and J. S. Moore: ACL2 theorems about commercial microprocessors. In Proc. FMCAD\u201996, Springer LNCS 1166, 1996."},{"key":"18_CR6","doi-asserted-by":"crossref","unstructured":"R. E. Bryant: Graph-based algorithms for Boolean function manipulation. In IEEE Trans. on Computers, Vol. C-35, No. 8, pages 677\u2013691, 1986.","DOI":"10.1109\/TC.1986.1676819"},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"R. E. Bryant and Y.-A. Chen: Verification of arithmetic functions with binary moment diagrams. Technical Report CMU-CS-94-160, Carnegie Mellon University, 1994.","DOI":"10.21236\/ADA281028"},{"key":"18_CR8","doi-asserted-by":"crossref","unstructured":"R. E. Bryant and Y.-A. Chen: Verification of arithmetic circuits with binary moment diagrams. In Proc. DAC\u201995, 1995.","DOI":"10.1145\/217474.217583"},{"key":"18_CR9","doi-asserted-by":"crossref","unstructured":"J. R Burch: Techniques for verifying superscalar microprocessors. In Proc. DAC7#x2019;96, 1996.","DOI":"10.1145\/240518.240623"},{"key":"18_CR10","doi-asserted-by":"crossref","unstructured":"J. R. Burch, E. Clarke, K. McMillan, and D. Dill: Sequential circuit verification using symbolic model checking. In Proc. DAC\u201990, 1990.","DOI":"10.1145\/123186.123223"},{"key":"18_CR11","series-title":"Lect Notes Comput Sci","volume-title":"In Proc. CAV\u201994","author":"J. R. Burch","year":"1994","unstructured":"J. R. Burch and D. L. Dill: Automatic verification of pipelined microprocessor control. In Proc. CAV\u201994. Springer LNCS 818, 1994."},{"key":"18_CR12","series-title":"Lect Notes Comput Sci","volume-title":"In Proc. Automatic Verification Methods for Finite State Systems","author":"O. Coudert","year":"1989","unstructured":"O. Coudert, C. Berthet, and J.-C. Madre: Verification of synchronous sequential machines based on symbolic execution. In Proc. Automatic Verification Methods for Finite State Systems, Springer LNCS 407, 1989."},{"key":"18_CR13","series-title":"Lect Notes Comput Sci","volume-title":"Proc. FMCAD\u201998","author":"D. A. Greve","year":"1998","unstructured":"D. A. Greve: Symbolic simulation of the JEM1 microprocessor. In Proc. FMCAD\u201998, Springer LNCS 1522, 1998."},{"key":"18_CR14","volume-title":"Computer architecture: a quantitative approach","author":"J. L. Hennessy","year":"1996","unstructured":"J. L. Hennessy, D. A. Patterson: Computer architecture: a quantitative approach. Morgan Kaufman, CA, second edition, 1996."},{"key":"18_CR15","unstructured":"H. Hinrichsen, H. Eveking, and G. Ritter: Formal synthesis for pipeline design. In Proc. DMTCS+CATS\u201999, Auckland, 1999."},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"S. H\u00f6reth: Implementation of a multiple-domain decision diagram package. In Proc. CHARME\u201997, pp. 185\u2013202, 1997.","DOI":"10.1007\/978-0-387-35190-2_12"},{"key":"18_CR17","unstructured":"S. H\u00f6reth:Hybrid Graph Manipulation Package Demo. URL: http:\/\/www.rs. etechnik.tu-darmstadt.de\/~sth\/demo.html ,Darmstadt 1998."},{"key":"18_CR18","series-title":"Lect Notes Comput Sci","volume-title":"Proc. CAV\u201998","author":"R. Hosabettu","year":"1998","unstructured":"R. Hosabettu, M. Srivas, and G. Gopalakrishnan: Decomposing the proof of correctness of pipelined microprocessors. In Proc. CAV\u201998, Springer LNCS 1427, 1998."},{"key":"18_CR19","doi-asserted-by":"crossref","unstructured":"R. B. Jones, D. L. Dill, and J. R. Burch: Efficient validity checking for processor verification. In Proc. ICCAD\u201995, November 1995.","DOI":"10.1109\/ICCAD.1995.479877"},{"key":"18_CR20","series-title":"Lect Notes Comput Sci","volume-title":"Proc. FMCAD\u201998","author":"R. B. Jones","year":"1998","unstructured":"R. B. Jones, J. U. Skakkeb\u00e6k, and D. L. Dill: Reducing manual abstraction in formal verification of out-of-order execution. In Proc. FMCAD\u201998, Springer LNCS 1522, 1998."},{"key":"18_CR21","series-title":"Lect Notes Comput Sci","volume-title":"Proc. FMCAD\u201998","author":"J. S. Moore","year":"1998","unstructured":"J. S. Moore: Symbolic simulation: an ACL2 approach. In Proc. FMCAD\u201998, Springer LNCS 1522, 1998."},{"key":"18_CR22","series-title":"Lect Notes Comput Sci","volume-title":"Proc. CAV\u201998","author":"J. U. Skakkeb\u00e6k","year":"1998","unstructured":"J. U. Skakkeb\u00e6k, R. B. Jones, and D. L. Dill: Formal verification of out-of-order execution using incremental flushing. In Proc. CAV\u201998, Springer LNCS 1427, 1998."},{"key":"18_CR23","doi-asserted-by":"crossref","unstructured":"M. Srivas and S. P. Miller: Applying formal verification to a commercial microprocessor. In Computer Hardware Description Language, August 1995.","DOI":"10.1109\/ASPDAC.1995.486361"},{"key":"18_CR24","series-title":"Lect Notes Comput Sci","volume-title":"FMCAD\u201998","author":"M. N. Velev","year":"1998","unstructured":"M. N. Velev and R. E. Bryant: Bit-level abstraction in the verification of pipelined microprocessors by correspondence checking. In FMCAD\u201998, Springer LNCS 1522, 1998."},{"key":"18_CR25","doi-asserted-by":"crossref","unstructured":"P. J. Windley and J. R. Burch: Mechanically checking a lemma used in an automatic verification tool. In Proc. FMCAD\u201996, November 1996.","DOI":"10.1007\/BFb0031821"}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48153-2_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T18:55:37Z","timestamp":1558983337000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48153-2_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540665595","9783540481539"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-48153-2_18","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}