入力名標集合と制御条件を用いたレジスタ転送レベルの設計検証法

吉田 たけお  貴家 仁志  内藤 祥雄  

誌名
電子情報通信学会論文誌 D   Vol.J79-D1   No.1   pp.28-40
発行日: 1996/01/25
Online ISSN: 
DOI: 
Print ISSN: 0915-1915
論文種別: 論文
専門分野: フォールトトレランス
キーワード: 
ハードウェア記述言語(HDL),  設計検証,  帰能的関数,  依存入力集合,  パス・コンディション,  

本文: PDF(957.4KB)>>
論文を購入




あらまし: 
ハードウェア記述言語(HDL)による記述中には,計算機で計算可能な関数として知られている帰納的関数(Churchの提唱)が記述されていると考えられる.このとき,設計記述が正しいための必要条件として,仕様記述が表す帰納的関数とこれに対応する設計記述が表す帰納的関数とが等価であることが挙げられる.これらの帰納的関数が等価でない場合,設計記述には,演算の誤りが存在すると言われる.しかし,この必要条件を厳密に調べることは困難である.本論文では,演算の誤りの一部である,システムの入出力の依存関係の誤りを検出する検証法を提案する.そのために,本論文では,HDL記述が表すシステムの入力名標の集合と制御条件を用いた“機能”という概念を用いて正しい設計記述について考察する.本方法は,レジスタ転送レベル(RTL)を対象とした高レベルの検証法である.