2つの等価性検証
(Conformal LECとJasperGold のSECアプリ)

ケイデンスから、2種類の等価性検証ツールをご提供していることはご存知でしょうか?Conformal®プロダクト・ファミリーのLEC (Logical Equivalence Checker)と、JasperGold®のSEC (Sequential Equivalence Checking)アプリです。


比較対象となる2つのデザインの等価性を証明する為に、フォーマル検証技術が使われていること、等価性を検証するためのテストベンチは不要であることは同じなのですが、LECは組合せ回路のみの論理等価を、SECは順序回路を含めた機能等価を証明する点で違いがあります。この2つの等価性検証について、ご紹介いたします。

まずConformal LECについてです。フルチップサイズの大規模デザインであっても、RTLと論理合成後のネットリストのように、デザイン記述の抽象度が異なっていても、網羅的に論理の等価を証明します。Conformal LECでは、比較対象となるそれぞれのデザインをDFFやLatchといったシーケンシャル・エレメントと、入出力ポートを2つのデザインの中から全て対応付け(マッピング)をし、マッピングされたポイントまでの組み合わせ回路同士の等価をそれぞれ証明していくという手法が取られています。全ての組合せ回路の等価が証明されることで、デザイン全体の等価を確認することが出来ます。

また、Conformal LECには、一般的にフォーマル検証が苦手とするデータパスに対して、データパス解析機能が実装されており、複雑な積和演算器を含むデザインの証明にもお使いいただけます。組み合わせ回路同士の証明方法を使った等価性検証は、論理合成やテスト回路挿入、レイアウト処理を行った後でも、RTLで検証された機能が、各処理によって壊されていないかを確認するためにも不可欠なツールです。

JasperGold は、フォーマル機能検証ツールとしてご活用いただいておりますが、検証用途に合わせた”アプリ“をお使い頂くことで、「与えられた仕様(プロパティ)を満たしているかを証明」するために必要となるプロパティ記述を、自動生成させることが出来ます。

そのアプリの中に、等価性検証用のSequential Equivalence Checking(SEC)アプリがあります。JasperGold のSECアプリを使った等価性検証では、入力ポートからのデータが、出力ポートへと伝播させるまでの動作を、網羅的に見ることが出来ます。下図で示しましたSPECとIMPが、比較したいDUTとすると、それぞれ対応する入力ポートに同じ値が与えられた時に、対応する出力ポートに伝播してくるデータは、常に同じであるかを証明します。


前述のConformal LECのようにDFFやLatchの入力と出力を分断して、組み合わせ(コンビネーシャル)回路の証明を行うために必要であったDFFやLatchのマッピングを、JasperGold SECアプリでは気にする必要がありません。DFFの数が異なってくるリタイミングされたデザインの処理前後の等価や、レジスタの名称が異なるデザインにも、特別な指定をせずにお使いいただけます。更に、プロパティ検証がベースとなっておりますので、ある条件が成立するタイミング時だけ出力が一致することを確認したいというケースにもお使い頂くことが出来ます。

機能追加や論理を少し変更したようなデザインで、変更に無関係な回路の等価性の証明や、VHDLからVerilogへ言語を変更した場合、可読性を上げるためにモディファイしたデザインの変更前後など、RTLの設計・検証フェーズでの様々なケースの等価性を証明する際に威力を発揮いたします。また、SECアプリを使うことで、機能等価の検証に最適なエンジンが選ばれ、通常のプロパティ検証よりも高速に証明が行えるメリットもあります。 

Conformal のLECとJasperGold のSECアプリ、それぞれの違いについて、おわかりいただけましたでしょうか?
SECとLECのそれぞれの特徴を活かして頂き、効率的で有効な検証に、どちらもお役立て頂けると幸いです。

フィールドエンジニアリング&サービス本部
志賀 玲子

Page Top