Siemens EDA/シーメンス EDA
シミュレーションベースの検証を補間するフォーマル検証エンジン
シミュレーションベースの検証では、テストパターンを追加し、ターゲットとする検証箇所を活性化し、その反応を後段に伝播させて結果を観測します。あくまでもテスト記述の意図に従ってターゲットを活性化し、この生産性を上げる場合にはランダムにテストを振りながら活性化する範囲を広げていきます。これに対してフォーマル検証では、デザイン中のクロックを自動的に進めながら、静的にステート空間を探索し、網羅的に検証します。シミュレーションベースの検証とフォーマル検証を組み合わせることにより、より深く、より広いカバレッジを効率よく達成することができます。Questaではシミュレータとフォーマル検証において共通のコンパイラと共通のカバレッジデータベースが使用できるため、検証フロー全体で品質と生産性の向上を実現します。
フォーマル検証には、アサーションを駆使しながらステート空間を探索しバグの特定やデザインの正当性を証明するプロパティチェックと、特定の検証項目や限られた適用範囲に対して完全に自動化が可能なフォーマルアプリがあります。静的検証ではテストパターンが不要であるため、設計の初期段階から使用することが可能です。またフォーマル向けのアサーションライブラリを使用すると、AXIバスなどの標準的なプロトコルに対する完全遵守を証明することができます。
「アサーションベース設計 立ち上げ支援サービス」をご利用ください
Wilson Research Groupが実施した機能検証の市場調査によれば、アサーションを使用する大多数はSystemVerilog Assertions(SVA)を使用しています。SVAは2005年にIEEE標準となっています。新たな手法が登場したときに、それを開発フローに導入するには、言語の習得に始まり、その効果を評価しては改善するなど、多くの労力を要します。
PALTEKではこの労力を低減し、誰もがアサーションを使い始められるようにするための支援策として、「アサーションベース設計 立ち上げ支援サービス」を提供しています。