サイバーテック、誰もが即活用できるフォーマル検証手法の新たな提案「InFormal」とは？

EDSF2007に出展していた、サーバーテック社のブースレポート。

サイバーテックは、昨年同様、米Jasper Design Automation社のフォーマル検証ツール「JasperGold」を展示。単なる製品の機能説明というよりも、「JasperGold」を用いたフォーマル検証の活用方法を前面に押し出す展示内容で、「InFormal」、「Light Formal」、「Deep Formal」という、3種類の検証手法を提案していた。

説明によると、「InFormal」は、RTL設計者がブロック設計のフェーズで設計しながら利用する、検証の入り口「In」となる最も手軽なフォーマル検証手法。「Light Formal」は、設計したブロックの初期検証フェーズで利用するアサーションベースの検証手法で、設計者及び検証エンジニアによる利用を想定。そして「Deep Formal」は、検証エンジニア向けのプロパティを用いた徹底的な網羅検証の手法で、ブロック検証の完成フェーズで適用するというもの。

中でも面白いのは「InFormal」で、この手法はテストベンチ不要は当然ながら、フォーマル検証では必須と思われているアサーション記述も必要とせず、RTLコードさえ有れば、すぐにRTLの基本的な動作を確認する事が可能。

例えば、FSMの最後のステートや転送終了信号の変化など、確認したいRTLの状態を指定すれば、その状態の波形データをツールが生成。入力信号の状態を変えて様々な波形で動作確認したり、指定した状態に到達できない状況を発見したりする事ができるという。

このようなフォーマル検証ツールの使い方は、フォーマル検証に敷居の高さを感じている設計者にとって非常に入りやすい手法で、コーディングしたRTLをすぐにブロックレベルで検証しバグを発見できるほか、他人の書いたRTLの動作確認などにも利用できるため、RTL設計者にとってのメリットは大きい。

※記事提供：EDA Express

Verilog‐HDLによるテストベンチ―アサーション検証の効率化のために

SystemVerilogアサーション・ハンドブック