Questa X-Check

 

網羅的な自動Xステート検証

Questa X-CheckはRTL設計を自動的に解析し、内蔵のフォーマルエンジンを使ってX値伝搬に関する問題を徹底的に洗い出すアプリケーションです。フォーマル検証の知識もプロパティ言語の知識も必要ありません。

不定値Xの問題

設計内のクリティカルな制御分岐上の信号が不定値であったり、レジスタに予期しない不正値が読み込まれたりすると、影響範囲が急拡大して、致命的なバグに姿を変えてしまうことがあります。特に論理合成とシミュレーションではX値信号の扱いが異なるので厄介です。論理合成では、Xは「任意の値」として取り扱われるのに対して、シミュレーションでは「不定の値」とされます。些細なことに見えますが、この解釈の違いのために、X値伝搬に関する問題はシミュレーションツールを使っては検出できず、見逃されてしまします。想定外のX値がローパワーのアイソレーション制御信号あるいは重要なクロックイネーブル信号に現れると、チップはたちまちハングアップしてしまいます。

Questa X-Check  

Questa X-Checkは、RTL記述と初期化シーケンス仕様さえあればアサーションを自動で生成して、チップにとって致命的なXステートの問題を素早く解析することができます。形式的仕様記述言語の知識もPSL(Property Specification Language)の知識も必要ありません。

ソリューション: Questa X-Check

Questa X-CheckはX値伝搬の問題を網羅的に特定するフォーマル解析を自動化するアプリケーションです。具体的には、RTL記述と初期化シーケンス仕様を入力として、フォーマルエンジンを使って解析を実施し、Xステート関連のすべての問題の原因(つまり初期化シーケンス直後のXステート、X値の設定、複数のドライバ、範囲外のインデックス、算術例外)を特定するものです。また、レジスタを楽観的に初期化したか悲観的に初期化したかを示すフラグを立てます。最終的には、X値の正確なセマンティクスを用いて、問題が未解決のレジスタと破損したレジスタを検知します。

特長

  • RTL記述に含まれるXのソースを網羅的に特定
  • X値楽観論とX値悲観論の動作を検出
  • X値の正確なセマンティクスを使って、問題が未解決のレジスタと破損したレジスタを識別
  • Questa Advanced Simulatorとの統合によりX値伝搬解析を補完

利点

  • Xステートに関わるすべての問題を徹底的に特定できる
  • プロパティ言語やフォーマル検証、アサーションベース検証の知識が不要な完全自動化解析フロー
製品情報リクエスト