プロパティ・チェッキング

出典: くみこみックス

版間での差分
M (1 版)
最新版 (2009年3月16日 (月) 07:30) (ソースを表示)
 
(間の 1 版分が非表示です)
4 行 4 行
 設計された順序回路が,特定の設計仕様(プロパティ)を満たしているかどうかを判定すること.モデル・チェッキングと呼ぶ場合もある.
 設計された順序回路が,特定の設計仕様(プロパティ)を満たしているかどうかを判定すること.モデル・チェッキングと呼ぶ場合もある.
 ある状態遷移表現で記述された設計に対して,別の状態遷移の形式で与えられた仕様,あるいは時相論理で表現された仕様をつき合わせて検証する.実際には,設計の遷移状態を一つずつたどり,各状態が与えられた仕様を満たしているかどうかを確認する.プロパティ・チェッキングの検証対象回路は,動作が複雑で論理シミュレーションだけでは検証が困難な制御回路などである.
 ある状態遷移表現で記述された設計に対して,別の状態遷移の形式で与えられた仕様,あるいは時相論理で表現された仕様をつき合わせて検証する.実際には,設計の遷移状態を一つずつたどり,各状態が与えられた仕様を満たしているかどうかを確認する.プロパティ・チェッキングの検証対象回路は,動作が複雑で論理シミュレーションだけでは検証が困難な制御回路などである.
 +
<br>
 +
<br>
 +
<br>
 +
<center>
 +
[[画像:lsi_f77.gif]]<br>
 +
<br>
 +
'''図 プロパティ・チェッキング'''
 +
</center>
<br>
<br>
<br>
<br>
14 行 22 行
* [[フォーマル・ベリファイア]]
* [[フォーマル・ベリファイア]]
-
[[Category:組み込み技術全般]] [[Category:LSI]]
+
[[Category:組み込み技術全般|フロハティチェッキンク]] [[Category:LSI|フロハティチェッキンク]]

最新版

プロパティ・チェッキング【Property Checking】

 設計された順序回路が,特定の設計仕様(プロパティ)を満たしているかどうかを判定すること.モデル・チェッキングと呼ぶ場合もある.  ある状態遷移表現で記述された設計に対して,別の状態遷移の形式で与えられた仕様,あるいは時相論理で表現された仕様をつき合わせて検証する.実際には,設計の遷移状態を一つずつたどり,各状態が与えられた仕様を満たしているかどうかを確認する.プロパティ・チェッキングの検証対象回路は,動作が複雑で論理シミュレーションだけでは検証が困難な制御回路などである.


画像:lsi_f77.gif

図 プロパティ・チェッキング



【出典】西久保 靖彦;基本システムLSI用語辞典,CQ出版社,2000年5月.

関連項目

表示