Verification method for systolic arrays using induction-based theorem provers

Kazuko Takahashi, Hiroshi Fujita

Research output: Contribution to journalArticlepeer-review


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
Issue number1
Publication statusPublished - 1999

All Science Journal Classification (ASJC) codes

  • General Computer Science
  • General Engineering


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

Cite this