A verification method for systolic arrays using induction-based theorem provers

Boyer RS, Moore JS. A computational logic handbook. New York: Academic Press, 1988. Bronstein A, Talcott CL. Formal verification of synchronous circuits based on string-functional semantics: the 7 Paillet circuits in Boyer–Moore. In: Sifakis J, editor. Automatic verification methods for finite state systems. Springer, 1989:317–333. Bryant, 1986, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, C35, 677, 10.1109/TC.1986.1676819 German SM, Wang Y. Formal verification of parameterized hardware designs. In: Proceedings of the International Conference on Computer Design. IEEE, 1985:549–552. 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–364. 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–128. Hunt Jr WA. FM8501: A verified microprocessor, PhD thesis, University of Texas at Austin, 1985 (Also available through Computational Logic Inc). 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–34. Kinniment DJ, Koelmans AM. Modelling and verification of timing conditions with Boyer–Moore Prover. In: Stavridou V, Melham T, Boute RT, editors. Theorem provers in circuit design. Amsterdam: Elsevier/North-Holland, 1992:111–127. Kropf T. Benchmark-circuits for hardware-verification. In: Theorem provers in circuit design 1995:1–12, http://goete.ira.uka.de/benchmarks, TPCD Benchmarks. Kung, 1982, Why systolic architectures?, IEEE Computer, X, 37, 10.1109/MC.1982.1653825 Owre S, Rushby JM, Shankar N. PVS: a prototype verification system. In: 11th International Conference on Automated Deduction. New York: Springer, 1992:748–752. Purushothaman, 1989, Mechanical certification of systolic algorithms, Journal of Automated Reasoning, 5, 67, 10.1007/BF00245022 Takahashi K, Fujita H. Time parameterized function method: a new method for hardware verification with the Boyer–Moore Theorem Prover. In: Proceedings of CHDL'95 (IFIP Conference on Hardware Description Languages and Their Applications). Chiba, Japan, 1995:545–552. Takahashi, 1998, TPF: an effective method for verifying synchronous circuits with induction-based provers, IEICE Transactions on Information and Systems, E81D, 12 Takahashi K, Fujita H. Verification of systolic arrays using induction-based theorem provers. Journal of Information Processing 1998;39:2323-–2330 (in Japanese). Verkest D, Vandenbergh J, Claesen L, de Man H. A description methodology for parameterized modules in the Boyer–Moore logic. In: Stavridou V, Melham T, Boute RT, editors. Theorem provers in circuit design. Amsterdam: Elsevier/North-Holland, 1992:37–57.