{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T11:24:34Z","timestamp":1649157874780},"reference-count":17,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Artificial Intelligence in Engineering"],"published-print":{"date-parts":[[1999,1]]},"DOI":"10.1016\/s0954-1810(98)00010-7","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T19:37:38Z","timestamp":1027625858000},"page":"43-53","source":"Crossref","is-referenced-by-count":0,"title":["A verification method for systolic arrays using induction-based theorem provers"],"prefix":"10.1016","volume":"13","author":[{"given":"Kazuko","family":"Takahashi","sequence":"first","affiliation":[]},{"given":"Hiroshi","family":"Fujita","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S0954-1810(98)00010-7_BIB1","unstructured":"Boyer RS, Moore JS. A computational logic handbook. New York: Academic Press, 1988."},{"key":"10.1016\/S0954-1810(98)00010-7_BIB2","unstructured":"Bronstein A, Talcott CL. Formal verification of synchronous circuits based on string-functional semantics: the 7 Paillet circuits in Boyer\u2013Moore. In: Sifakis J, editor. Automatic verification methods for finite state systems. Springer, 1989:317\u2013333."},{"key":"10.1016\/S0954-1810(98)00010-7_BIB3","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","article-title":"Graph-based algorithms for Boolean function manipulation","volume":"C35","author":"Bryant","year":"1986","journal-title":"IEEE Transactions on Computers"},{"key":"10.1016\/S0954-1810(98)00010-7_BIB4","unstructured":"German SM, Wang Y. Formal verification of parameterized hardware designs. In: Proceedings of the International Conference on Computer Design. IEEE, 1985:549\u2013552."},{"key":"10.1016\/S0954-1810(98)00010-7_BIB5","unstructured":"Goldschlag DM. Mechanically verifying safety and liveness property of delay insensitive circuits. In: Larsen KG, Skou A, editors. Computer aided verification. Berlin: Springer, 1991:354\u2013364."},{"key":"10.1016\/S0954-1810(98)00010-7_BIB6","doi-asserted-by":"crossref","unstructured":"Gordon MJC. HOL: A proof generating system for higher-order logic. In: Birtwistle G, Subrahmanyam PA, editors. VLSI Specification, verification and synthesis. Boston, MA: Kluwer Academic Publishers, 1988:73\u2013128.","DOI":"10.1007\/978-1-4613-2007-4_3"},{"key":"10.1016\/S0954-1810(98)00010-7_BIB7","unstructured":"Hunt Jr WA. FM8501: A verified microprocessor, PhD thesis, University of Texas at Austin, 1985 (Also available through Computational Logic Inc)."},{"key":"10.1016\/S0954-1810(98)00010-7_BIB8","doi-asserted-by":"crossref","unstructured":"Kaufmann M, Moore JS. ACL2: An industrial strength version of Nqthm. In: Proceedings of Eleventh Annual Conference on Computer Assurance. IEEE Computer Society Press, 1996:23\u201334.","DOI":"10.1109\/CMPASS.1996.507872"},{"key":"10.1016\/S0954-1810(98)00010-7_BIB9","unstructured":"Kinniment DJ, Koelmans AM. Modelling and verification of timing conditions with Boyer\u2013Moore Prover. In: Stavridou V, Melham T, Boute RT, editors. Theorem provers in circuit design. Amsterdam: Elsevier\/North-Holland, 1992:111\u2013127."},{"key":"10.1016\/S0954-1810(98)00010-7_BIB10","doi-asserted-by":"crossref","unstructured":"Kropf T. Benchmark-circuits for hardware-verification. In: Theorem provers in circuit design 1995:1\u201312, http:\/\/goete.ira.uka.de\/benchmarks, TPCD Benchmarks.","DOI":"10.1007\/3-540-59047-1_39"},{"key":"10.1016\/S0954-1810(98)00010-7_BIB11","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1109\/MC.1982.1653825","article-title":"Why systolic architectures?","volume":"X","author":"Kung","year":"1982","journal-title":"IEEE Computer"},{"key":"10.1016\/S0954-1810(98)00010-7_BIB12","doi-asserted-by":"crossref","unstructured":"Owre S, Rushby JM, Shankar N. PVS: a prototype verification system. In: 11th International Conference on Automated Deduction. New York: Springer, 1992:748\u2013752.","DOI":"10.1007\/3-540-55602-8_217"},{"key":"10.1016\/S0954-1810(98)00010-7_BIB13","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1007\/BF00245022","article-title":"Mechanical certification of systolic algorithms","volume":"5","author":"Purushothaman","year":"1989","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/S0954-1810(98)00010-7_BIB14","doi-asserted-by":"crossref","unstructured":"Takahashi K, Fujita H. Time parameterized function method: a new method for hardware verification with the Boyer\u2013Moore Theorem Prover. In: Proceedings of CHDL'95 (IFIP Conference on Hardware Description Languages and Their Applications). Chiba, Japan, 1995:545\u2013552.","DOI":"10.1109\/ASPDAC.1995.486368"},{"key":"10.1016\/S0954-1810(98)00010-7_BIB15","first-page":"12","article-title":"TPF: an effective method for verifying synchronous circuits with induction-based provers","volume":"E81D","author":"Takahashi","year":"1998","journal-title":"IEICE Transactions on Information and Systems"},{"key":"10.1016\/S0954-1810(98)00010-7_BIB16","unstructured":"Takahashi K, Fujita H. Verification of systolic arrays using induction-based theorem provers. Journal of Information Processing 1998;39:2323-\u20132330 (in Japanese)."},{"key":"10.1016\/S0954-1810(98)00010-7_BIB17","unstructured":"Verkest D, Vandenbergh J, Claesen L, de Man H. A description methodology for parameterized modules in the Boyer\u2013Moore logic. In: Stavridou V, Melham T, Boute RT, editors. Theorem provers in circuit design. Amsterdam: Elsevier\/North-Holland, 1992:37\u201357."}],"container-title":["Artificial Intelligence in Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0954181098000107?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0954181098000107?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,17]],"date-time":"2019-04-17T17:56:48Z","timestamp":1555523808000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0954181098000107"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999,1]]},"references-count":17,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1999,1]]}},"alternative-id":["S0954181098000107"],"URL":"https:\/\/doi.org\/10.1016\/s0954-1810(98)00010-7","relation":{},"ISSN":["0954-1810"],"issn-type":[{"value":"0954-1810","type":"print"}],"subject":[],"published":{"date-parts":[[1999,1]]}}}