著者

鈴木 一哉 吉田 たけお 三浦 幸也

出版者

一般社団法人電子情報通信学会

雑誌

電子情報通信学会技術研究報告. VLD, VLSI設計技術

巻号頁・発行日

vol.96, no.425, pp.41-48, 1996-12-13

参考文献数

10

---

本稿では設計されたハードウェアの構造がその動作仕様を満たしているかどうかを検証する方法を提案する.従来の検証法で用いられている一階述語論理は再帰的な表現ができないため,順序回路を含むようなハードウェアを表現できない.本稿では高階述語論理を用いることによってこの問題を解決する.本稿ではまず仕様である動作記述およびその設計である構造記述をそれぞれ高階述語論理式に変換する方法を示す.仕様記述および設計記述を表す論理式から"設計が仕様を満たしている"という意味を表す論理式を作り,この論理式を証明することによって検証を行なう.さらに本稿ではこの論理式を定理証明系を用いて証明する際の手順も示す.