なぜフォーマルなのか?

最新のプロセッサは、消費電力、性能、面積のために数多くの最適化が行われています。パイプライン化、インターロック、データ転送などの最適化により、多くのデータ依存関係やハザードが発生し、プロセッサがデッドロックを起こしたり、誤った結果を出力したりします。命令のインターリーブや複数のレジスタファイル、オペランドとともに、命令の組合わせ数が多いため、シミュレーションに基づく検証を網羅的に行うことは不可能です。

フォーマル検証の課題

フォーマル検証は、正しさを網羅的に証明し、設計実装におけるコーナーケースのバグを発見します。しかしながら、フォーマル検証には以下のような課題があります。

• • 収束が保証されない
  • 異なるフォーマル検証ツール間におけるフォーマルカバレッジのモデルの一貫性がない
  • フォーマルカバレッジモデルとシミュレーションとの間に整合性がない

RISC-Vプロセッサの自動フォーマル検証

 formalISA®アプリは、このような課題をすべてフォーマル検証のメソドロジで解決する検証IPです。Axiomiseの第一世代ISAフォーマル検証プルーフキット上に構築された formalISA®アプリは、クリーンなグラフィカルユーザーインターフェイスを備えており、エンドユーザーはいくつかのボタンを押すだけで、商用フォーマル検証ツールを使って、好みのRISC-Vコアのフォーマル検証結果を得ることができます。

プッシュボタン式の “Proove”や”Cover”のソリューションを使用することで、以下を行う必要がなくなります：

• •  １つのテストケースを記述する
  •  複雑なテストシーケンスを記述する
  •  スコアボードまたはチェッカーを記述する
  •  制約を記述する
  •  スティミュラスをランダム化する

アーキテクチャコンプライアンス

• • RISC-Vプロセッサの数学的証明によるISAコンプライアンスの確立

網羅的な証明

• • アーキテクチャおよびマイクロアーキテクチャのチェックとカバレッジを用いてRISC-Vプロセッサにバグが存在しないことを数学的に証明

バグハンティング

• • 32ビットおよび64ビットプロセッサのプロセッサ実装におけるバグやコーナーケースのバグを特定

自動化

• • 簡単なセットアップと使用
  • プッシュボタン
  • GUIベース
  • ベンダーニュートラル – 任意のフォーマル検証ツールを使用可能
  • シナリオカバレッジのソリューションを使用した命令セットの動作の可視化

マイクロアーキテクチャ非依存

• • インオーダーおよびアウトオブオーダーのコア
  • アプリはインオーダーコアおよびアウトオブオーダーコアでテスト済み
  • RV32IMCZb*およびRV64IMCZb*命令セットのサポート準備完了
  • 予測可能かつスケーラブルなランタイム

デバッグ

• • i-RADARによるインテリジェントなデバッグにより、デバッグ時間と設計者に引渡す時間を短縮

カバレッジ

• • シナリオカバレッジは自動生成される
  • SURF（Scheduler and Reporter for Formal）は、ダッシュボードにおいてすべての重要なサマリーを提供