{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,23]],"date-time":"2025-01-23T00:40:32Z","timestamp":1737592832132,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"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_28","type":"book-chapter","created":{"date-parts":[[2007,11,29]],"date-time":"2007-11-29T09:41:36Z","timestamp":1196329296000},"page":"492-506","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Symbolic Checking of Signal-Transition Consistency for Verifying High-Level Designs"],"prefix":"10.1007","author":[{"given":"Kiyoharu","family":"Hamaguchi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hidekazu","family":"Urushihara","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Toshinobu","family":"Kashiwabara","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,6,18]]},"reference":[{"issue":"2","key":"28_CR1","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1109\/54.587740","volume":"14","author":"R. A. Bergamaschi","year":"1997","unstructured":"R. A. Bergamaschi and S. Raje. Observable Time Windows: Verifying The Results of High-Level Synthesis. IEEE Design and Test of Computers, 14(2):40\u201350, 1997.","journal-title":"IEEE Design and Test of Computers"},{"key":"28_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"470","DOI":"10.1007\/3-540-48683-6_40","volume-title":"Exploiting positive equality in a logic of equality with uninterpreted functions","author":"R. E. Bryant","year":"1999","unstructured":"R. E. Bryant, S. German, and M. N. Velve. Exploiting positive equality in a logic of equality with uninterpreted functions. In Conference on Computer-Aided Verification, LNCS 1633, pages 470\u2013482, July 1999."},{"key":"28_CR3","doi-asserted-by":"crossref","unstructured":"J. R. Burch, E. M. Clarke, D. E. Long, K. L. McMillan, and D. L. Dill. Symbolic Model Checking for Sequential Circuit Verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 13(4), April 1994.","DOI":"10.1109\/43.275352"},{"key":"28_CR4","doi-asserted-by":"crossref","unstructured":"J. R. Burch and D. L. Dill. Automatic Verification of Pipelined Microprocessor Control. In Proceedings of International Conference on Computer-Aided Design, pages 68\u201380, June 1994.","DOI":"10.1007\/3-540-58179-0_44"},{"key":"28_CR5","unstructured":"O. Coudert, C. Berthet, and J.-C. Madre. Verification of Sequential Machines Using Boolean Functional Vectors. In Proceedings of the IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, November 1990."},{"key":"28_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1007\/3-540-58179-0_59","volume-title":"Ground temporal logic: A logic for hardware verification","author":"D. Cyrluk","year":"1994","unstructured":"D. Cyrluk and P. Narendran. Ground temporal logic: A logic for hardware verification. In Conference on Computer-Aided Verification, LNCS 818, pages 247\u2013259, July 1994."},{"key":"28_CR7","doi-asserted-by":"crossref","unstructured":"S. Devadas and K. Keutzer. An Automata-Theoretic Approach to Behavioral Equivalence. In Proc. of ICCAD, pages 30\u201333, 1990.","DOI":"10.1109\/ICCAD.1990.129832"},{"key":"28_CR8","doi-asserted-by":"crossref","unstructured":"M. Genoe, L. Claesen, E. Verlind, F. Proesmans, and H. De Man. Illustration of the SFG-Tracing Multi-Level Behavioral Verification Methodology, by the Correctness Proof of a High to Low Level Synthesis Application in CATHEDRAL-II. In Proc. of IEEE International Conference on Computers and Design, pages 338\u2013341, 1991.","DOI":"10.1109\/ICCD.1991.139913"},{"key":"28_CR9","doi-asserted-by":"crossref","unstructured":"M. Genoe, L. Claesen, E. Verlind, F. Proesmans, and H. De Man. Automatic Formal Verification of Cathedral-II Circuits from Transistor Switch Level Implementations up to High Level Behavioral Specifications by the SFG-Tracing Methodology. In Proc. of European Conference on Design Automation (EDAC-92), pages 16\u201319, 1992.","DOI":"10.1109\/EDAC.1992.205893"},{"key":"28_CR10","unstructured":"J. L. Henny and D. A. Paterson. Computer Architecture: A Quantitative Approach. Morgan Kaufmann, 1990."},{"key":"28_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1007\/BFb0031810","volume-title":"Formal Methods in Computer-Aided Design","author":"R. Hojati","year":"1996","unstructured":"R. Hojati, A. Isles, D. Kirkpatrick, and R. K. Brayton. Verification using uninterpreted functions and finite instantiations. In Formal Methods in Computer-Aided Design, LNCS 1166, pages 218\u2013232, November 1996."},{"key":"28_CR12","doi-asserted-by":"crossref","unstructured":"M. Imai, Y. Takeuchi, N. Ohtsuki, and N. Hikichi. Compiler Generation Techniques for Embedded Processors and Their Application to HW\/SW Codesign. In Ahmed A. Jerraya and Jean Mermet, editors, System-Level Synthesis, pages 293\u2013320. Kluwer Academic Publishers, 1999.","DOI":"10.1007\/978-94-011-4698-2_9"},{"key":"28_CR13","doi-asserted-by":"crossref","unstructured":"R. B. Jones, D. L. Dill, and J. R. Burch. Efficient Validity Checking for Processor Verification. In Proceedings of International Conference on Computer-Aided Design, pages 2\u20136, November 1995.","DOI":"10.1109\/ICCAD.1995.479877"},{"key":"28_CR14","doi-asserted-by":"crossref","unstructured":"N. Mansouri and R. Vemuri. A Methodology for Automated Verification of Syn-thesized RTL Designs and Its Integration with a High-Level Synthesis Tool. In Formal Methods in Computer-Aided Design (FMCAD 98), pages 204\u2013221, 1998.","DOI":"10.1007\/3-540-49519-3_15"},{"issue":"2","key":"28_CR15","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"G. Nelson and D. C. Oppen. Simplification by Cooperating Decision Procedure. ACM Trans. on Programming Languages and Systems, 1(2):245\u2013257, 1979.","journal-title":"ACM Trans. on Programming Languages and Systems"},{"issue":"2","key":"28_CR16","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1145\/322123.322137","volume":"26","author":"R. E. Shostak","year":"1979","unstructured":"R. E. Shostak. A Practical Decision Procedure for Arithmetic with Function Symbols. Journal of ACM, 26(2):351\u2013360, 1979.","journal-title":"Journal of ACM"},{"key":"28_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1007\/BFb0028747","volume-title":"Model checking for a first-order temporal logic using multiway decision graphs","author":"Y. Xu","year":"1998","unstructured":"Y. Xu, E. Cerny, X. Song, F. Corella, and O. Ait Mohamed. Model checking for a first-order temporal logic using multiway decision graphs. In Conference on Computer-Aided Verification, LNCS 1427, pages 219\u2013231, July 1998."}],"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_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,23]],"date-time":"2025-01-23T00:23:28Z","timestamp":1737591808000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-40922-X_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540412199","9783540409229"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-40922-x_28","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"}}]}}