ページの先頭です。
サイト内の現在位置を表示しています。
  1. ホーム
  2. ソリューション・サービス
  3. 組込みシステムソリューション
  4. プリント基板・LSI設計
  5. CyberWorkBench
  6. 機能紹介
  7. 静的検証
ここから本文です。

静的検証

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

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

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

プロパティの種類

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

C-RTL等価性プルーバ

CyberWorkBenchでは、動作合成前後のC記述とRTL記述の動作が等価であることをテスト・ベクタなしで完全証明できる「C-RTL等価性プルーバ」を用意しています。

  • ・動作合成と連携
  • ・中間信号の対応情報を利用し、高速に検証可能
  • ・追加情報や、特別な準備や習熟が必要なく、簡単に利用可能

ページの先頭へ戻る