プロパティ・チェッキング
出典: くみこみックス
版間での差分
M (1 版) |
|||
| （間の 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用語辞典，CQ出版社，2000年5月．
