{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,16]],"date-time":"2025-04-16T05:36:03Z","timestamp":1744781763320},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540662020"},{"type":"electronic","value":"9783540486831"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"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":[[1999]]},"DOI":"10.1007\/3-540-48683-6_33","type":"book-chapter","created":{"date-parts":[[2007,10,7]],"date-time":"2007-10-07T03:22:18Z","timestamp":1191727338000},"page":"380-393","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Automatic Verification of Combinational and Pipelined FFT Circuits"],"prefix":"10.1007","author":[{"given":"Per","family":"Bjesse","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,1,14]]},"reference":[{"key":"33_CR1","doi-asserted-by":"crossref","unstructured":"Per Bjesse, Koen Claessen, Mary Sheeran, and Satnam Singh. Lava: Hardware Design in Haskell. In Proceedings of the third International Conference on Functional Programming. ACM SIGPLAN, acm press, September 1998.","DOI":"10.1145\/289423.289440"},{"key":"33_CR2","doi-asserted-by":"crossref","unstructured":"Jerry Burch and David Dill. Automatic Verification of Microprocessor Control. In Proceedings of the Computer Aided Verification Conference, July 1994.","DOI":"10.1007\/3-540-58179-0_44"},{"key":"33_CR3","doi-asserted-by":"crossref","unstructured":"Clark Barrett, David Dill, and Jeremy Levitt. Validity checking for combinations of theories with equality. In Mandayam Srivas and Albert Camilleri, editors, Formal Methods In Computer-Aided Design, volume 1166 of Lecture Notes in Computer Science, pages 187\u2013201. Springer Verlag, November 1996. Palo Alto, California, November 6-8.","DOI":"10.1007\/BFb0031808"},{"key":"33_CR4","unstructured":"David Cyrluk. Microprocessor verification in PVS. Technical Report SRI-CSL-93-12, SRI Computer Science Laboratory, December 1993."},{"key":"33_CR5","doi-asserted-by":"crossref","unstructured":"Ruben Gamboa. Mechanically verifying the correctness of the Fast Fourier Transform in ACL2. In Third International Workshop on Formal Methods for Parallel Programming: Theory and Applications, 1998.","DOI":"10.1007\/3-540-64359-1_743"},{"key":"33_CR6","unstructured":"Shousheng He. Concurrent VLSI Architectures for DFT Computing and Algorithms for Multi-output Logic Decomposition. PhD thesis, Lund Institute of Technology, 1995."},{"issue":"2","key":"33_CR7","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1023\/A:1005843632307","volume":"18","author":"W. W. McCune","year":"1997","unstructured":"William W. McCune and L. Wos. Otter: The CADE-13 competition incarnations. Journal of Automated Reasoning, 18(2):211\u2013220, 1997.","journal-title":"Journal of Automated Reasoning"},{"key":"33_CR8","unstructured":"John Proakis and Dimitris Manolakis. Digital Signal Processing. Macmillan, 1992."},{"key":"33_CR9","unstructured":"Gunnar St\u00e5almarck. A System for Determining Propositional Logic Theorems by Applying Values and Rules to Triplets that are Generated from a Formula, 1989. Swedish Patent No. 467 076 (approved 1992), U.S. Patent No. 5 276 897 (1994), European Patent No. 0403 454 (1995)."},{"issue":"2","key":"33_CR10","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1023\/A:1005887414560","volume":"18","author":"T. Tammet","year":"1997","unstructured":"Tanel Tammet. Gandalf. Journal of Automated Reasoning, 18(2):199\u2013204, 1997.","journal-title":"Journal of Automated Reasoning"},{"key":"33_CR11","unstructured":"[TZS+96]_ Sofi\u00e8ne Tahar, Zijian Zhou, Xiaoyu Song, Eduard Cerny, and Michel Langevin. Formal verification of an ATM switch fabric using Multiway Decision Graphs. In IEEE Proceedings of Sixth Great Lakes Symposium on VLSI, March 1996."},{"key":"33_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/3-540-49519-3_3","volume-title":"Formal Methods in Computer-Aided Design","author":"M. Velev","year":"1998","unstructured":"Miroslav Velev and Randal Bryant. Bit-Level Abstraction in the Verification of Pipelined Microprocessors by Correspondence Checking. In Formal Methods in Computer-Aided Design, volume 1522 of LNCS, pages 18\u201335, Palo Alto, November 1998. Springer Verlag."},{"key":"33_CR13","unstructured":"[ZSC+95]_ Zijian Zhou, Xiaoyu Song, Fransisco Corella, Eduard Cerny, and Michel Langevin. Description and Verification of RTL Designs Using Multiway Decision Graphs. In Proceedings of the Conference on Hardware Description Languages and their applications, August 1995."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48683-6_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,6]],"date-time":"2020-04-06T06:08:05Z","timestamp":1586153285000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48683-6_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540662020","9783540486831"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-48683-6_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]},"assertion":[{"value":"14 January 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}