Japan
サイト内の現在位置を表示しています。
静的検証
Cレベル・プロパティ・チェッカ
CyberWorkBenchでは、Cソース(動作記述)のプロパティを検証する「Cレベル・プロパティ・チェッカ」を用意しています。
- ・プロパティ記述にC記述の変数名を使用可能
- ・反例パターンをC変数で表示
- ・静的(数学的)に検証するため、テスト・ベクタは不要
- ・RTLを検証しているため、RTLの品質を保証
- ・動作合成情報を利用して、サイクル精度のプロパティ検証を実行
プロパティの種類
組み込みプロパティ |
|
---|---|
ユーザ・プロパティ |
|
アサーション | 通常のCプログラムのassert()文を、形式検証に適用可能 |