Verification method for systolic arrays using induction-based theorem provers

Kazuko Takahashi, Hiroshi Fujita

研究成果: ジャーナルへの寄稿学術誌査読

抄録

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.

本文言語英語
ページ(範囲)43-53
ページ数11
ジャーナルArtificial Intelligence in Engineering
13
1
DOI
出版ステータス出版済み - 1999

!!!All Science Journal Classification (ASJC) codes

  • コンピュータサイエンス一般
  • 工学一般

フィンガープリント

「Verification method for systolic arrays using induction-based theorem provers」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル