サイト内の現在位置を表示しています。

静的検証

Cレベル・プロパティ・チェッカ

CyberWorkBenchでは、Cソース(動作記述)のプロパティを検証する「Cレベル・プロパティ・チェッカ」を用意しています。

  • ・プロパティ記述にC記述の変数名を使用可能
  • ・反例パターンをC変数で表示
  • ・静的(数学的)に検証するため、テスト・ベクタは不要
  • ・RTLを検証しているため、RTLの品質を保証
  • ・動作合成情報を利用して、サイクル精度のプロパティ検証を実行

プロパティの種類

組み込みプロパティ
  • 配列アクセス・チェック
  • if、switch文デッド・コード・チェック
  • 並列if文条件排他性チェック
  • 多重代入チェック
  • ステート・マシン・デッド・ロック・チェック など
ユーザ・プロパティ
  • 言語形式(PSL、LTL)
  • 組み込みテンプレート
アサーション 通常のCプログラムのassert()文を、形式検証に適用可能