著者

森岡 澄夫 柴田 直樹 東野 輝夫 谷口 健一

出版者

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

雑誌

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

巻号頁・発行日

vol.96, no.299, pp.49-56, 1996-10-18

被引用文献数

5

---

加算器, 乗算器, ALUなど, 算術演算を行う組み合わせ論理回路が, そのワードレベル仕様F (整数上の論理式として書かれた入出力関係の記述) を正しく実現している事を, プレスブルガー文真偽判定手続きを用いて自動証明する方法と, 証明例について述べる. 証明は, いわゆるビットレベル検証 (各回路モジュールM_jごと, そのワードレベル仕様F_jがゲートレベルで正しく実現されていることの証明) とワードレベル検証 (各M_jの接続関係および各ワードレベル仕様F_jのもとで, Fが満たされることの証明) に分けて行う. 乗算など, プレスブルガー算術で直接扱えない演算を行う回路についても, その演算に関して数学的に成り立つ性質等を仮定することにより, 証明できる場合がある. 本手法の特徴は, 幾つかの工夫を行ったプレスブルガー真偽判定ルーチンを用いることにより, 各モジュールの演算ビット長 n が増えても, 回路中のモジュールの数や組合せ方が同じで, かつ仕様記述のサイズが n 依存していなければ, ワードレベル検証にかかる時間がほとんど増加しないことである. 例えば n ビット乗算器から 2n ビット乗算器を構成した場合のワードレベル検証を, 2分程度のCPU時間で行えた. ビットレベル検証についても, 演算ビット長が4ビット程度であれば, 例えば加減算・論理演算を行うALU (74382) について6分程度のCPU時間で行えた.