JasperGoldの悲観でも楽観でもない不定値Xの世界観

何回かにわけて、X伝搬問題に関する検証技術情報を紹介していこうと思います。
今回は、X伝搬における悲観評価と楽観評価の問題です。以下では簡単化のため、1'b1, 1'b0, 1'bx をそれぞれ、1, 0, x と表記する場合があります。また、X伝搬の悲観評価や楽観評価からくる問題を、X-Pessimism 問題とX-Optimmism と呼ぶ事にします。
皆様は、2入力のセレクタ回路、またはMUX回路をRTLに実装する際に、どのように実装しますか?例えば、if-else 文を使って、

などのように記述しますか?あるいは、三項(Ternary)演算子を用いて、

としますか?その他の方法でも実装可能でしょうが、だいたい上の二つが代表的な書き方ではないしょうか。では、X伝搬に関して、上の二つの振る舞いの違いを確認します。この二つを区別するために、前者を if-else 表記、後者を Ternary 表記と呼びます。

例えば、セレクト信号の cond が xになった場合を考えます。前提として、cond, a, b, y が全て1 bit だとします。

上の回路で cond が x になった時、この二つの表記の違いで、
RTLシミュレーション結果にどのような違いが生じますか?

Verilog LRMの定義によると、条件項が不定のXの場合、if-else 表記では条件評価は false 扱いで else 側を処理するため、上の例では y = b が選択されます。一方、Ternary 表記では、cond が x の場合でも論理的にこれを解決しようとします。つまり、a と b が同じ場合はどちらを選択しても同じ結果になるため y = a (=b)、それ以外では結果を特定できないため、 y は不定の x になります。この二つの違いを、下の表に整理します。

Inputs Output
cond a b if-else Ternary
x 0 0 0 0
x 0 1 1 x
x 1 0 0 x
x 1 1 1 1

今回の例において、RTLシミュレーションで cond が x になる条件で、シリコン内でたまたま 0 になるように合成されている場合には、実チップとRTLシミュレーションの結果は同じになります。でも、そうではない場合、つまり実チップでcond が 1 となった場合に、不具合が発生する可能性が残ります。
このように、RTLシミュレーションでは、不定の x を楽観的に x 以外(つまり、1bitの場合には1'b1 か1'b0 )におきかえしてまう X-Optimism 問題が生じる可能性があります。

X-OPTIMISM 問題を解決する手段として GATE LEVEL のシミュレーション

を行う方法があります。ただし、Gate Level シミュレーションでは、Xの悲観評価によるX伝搬誤検出のバグレポート対策が問題になります。例えば、上のMUX 回路が合成後に次のようなNANDで構成されたとします。

NANDでは片方の入力がxでもう片方が0以外の時に出力もxになります。従って、上の真理値表にNANDをもちいたGate Level シミュレーションの結果を追加すると、次のようになります。

Inputs Output
cond a b if-else Ternary NAND
x 0 0 0 0 0
x 0 1 1 x x
x 1 0 0 x x
x 1 1 1 1 x

お分かりの通り、実回路のシリコン内では a と b が共に 1'b1 の場合、セレクト信号 cond には無関係で y = 1 となるところ、NAND を用いた Gate Level シミュレーションでは y = x となり、実際より悲観的にXを伝搬させ、結果的に誤検出のバグレポートが大量に発生します。いわゆる、 X-Pessimism 問題です。この問題は、次のように、ANDやORを用いた組み合わせ論理で回路を記述すればRTLシミュレーションでも起こり得ます。

つまり、シミュレーションではこのようなX-Pessimism 問題が生じてしまいます。

弊社のJasperGold® では、このようなX-OPTIMISM問題や
X-PESSIMISM問題は生じません

なぜでしょう?一言で説明すると、JasperGold では、原因となるx が0 の場合と1の場合のそれぞれで検証を行うからです。0または1、どちらで検証しても検証ターゲットが同じ振る舞いをする場合にX伝搬問題は起こらず、異なるとX伝搬が検出されたと報告されます。結果、Xを過剰に伝搬させてログ解析を複雑にするX-Pessimism 問題も、必要なXを伝搬させないことでバグを見落としてしまうX-Optimism問題も起こりません。

JasperGold を用いたX伝搬問題の具体的な解決方法

JG-XPROPとJG-FPVを使った、二つの方法を紹介します。
JG-XPROP アプリを使いアサーションをツールに生成させて、特定のターゲットがXになり得るかを検証する方法があります。この方法ではユーザーはSVAやPSLといった検証言語を知らなくても簡単に検証を行う事ができます。アサーションを書く必要がないため、設計者がリントチェッカで文法や構造チェックを行うように手軽に、しかも早期にX伝搬関連のバグを見つける事ができます。一般に、後の工程で見つけるバグの方が解析やデバッグに伴うイタレーションにも時間がかかるので、JG-XPROPで早期に見つかるバグを早期に見つけて早期に対応する事で、全体の開発工数の削減につなげられます。

他の方法は、ユーザーが機能仕様書からアサーションを書いて、機能的な正しさを証明する方法です。いわゆる、一般的なフォーマル機能検証で、JG-FPVアプリでこれを行います。RTLで特定の信号がx になり得る場合、このxを、自由に0 または1になれる信号として扱うので、その両方を考慮してアサーションに違反する反例が存在するかどうかを検証します。 例えば、x が0なら正しいが1だと誤動作を引きおこす場合に、この誤動作で発火するアサーションがあれば、機能に影響するすべてのX伝搬の問題は JG-FPVで見つける事が可能です。ただし、機能仕様書があることは当然ですが、そこから検証プランを立て、これを正しくアサーションで書く必要があります。

JG-XPROP とJG-FPV、どちらも優れたアプリです。前者はアサーションを書かなくても検証できるメリットがありますが、機能には影響しないX伝搬による反例がレポートされてしまう場合もあります(X-Pessimism や X-Optimism 問題の事ではありません)。後者は、プランやアサーションにも依存しますが機能に影響する不具合のみをレポートするので、理想的には誤検出のバグレポートを0にする事が出来る反面、アサーションを書く必要があるためSVAやPSLなどのスキルが要求されます。また、場合によっては機能仕様書がない事でアサーションがかけない事もあるため、どのプロジェクトでも誰でも使いこなせる、というわけではないようです。

このような状況を踏まえて、我々は、お客様の組織の開発文化やスタイル、またはチームの役割(設計か検証か)にあわせたX伝搬問題のソリューションを、提案しています。

JasperGold のアプリ群スライドJasperGold のアプリ群スライド画像をクリックすると拡大表示されます

昨年2016年に弊社の北米本社で開催された
JUG (JasperGold USER GROUP CONFERENCE) で

韓国のSamsung社のYoungsik Kim様に発表いただいた、このスライドをご覧になりましたでしょうか?Samsung社では、すでに設計者のRTLサインオフとしてJG-XPROPによるX伝搬関連のバグがない事が条件になっております。弊社のJG-AFLによるリントチェック同様、幅広くご利用いただき品質や効率改善に役立てていただいております。

皆様におきましても、設計段階で無用なX伝搬問題を早期に解決していただき、品質と効率改善の両方を同時に達成していただくきっかけにしていただければと思い、簡単ですが弊社のJasperGoldを用いたX伝搬問題の解決方法を紹介させていただきました。

フィールドエンジニアリング&サービス本部
Jasper R&D, Sr Principal Product Engineer
渡口 和信

Page Top