Verification method for systolic arrays using induction-based theorem provers

Kazuko Takahashi, Hiroshi Fujita

Research output: Contribution to journalArticlepeer-review

Abstract

We propose a method for verifying hardware design with an induction-based theorem prover such as the Boyer-Moore Theorem Prover. As a case study, we apply the method to verification of the correctness of systolic array designs. In verifying circuits, we prove that an implementation satisfies a specification, in particular their functional equivalence. In proving the equivalence, induction is applied to the variables that denote time and position in the circuit. We discuss what lemmas should be used for appropriate application of induction. The lemmas we have found reflect the characteristics of the structure of the circuit. With these lemmas, the method provides a systematic way of verification for systolic arrays and eases the user's burden with respect to the hardware verification.

Original languageEnglish
Pages (from-to)43-53
Number of pages11
JournalArtificial Intelligence in Engineering
Volume13
Issue number1
DOIs
Publication statusPublished - Jan 1 1999
Externally publishedYes

All Science Journal Classification (ASJC) codes

  • Computer Science(all)
  • Engineering(all)

Fingerprint Dive into the research topics of 'Verification method for systolic arrays using induction-based theorem provers'. Together they form a unique fingerprint.

Cite this