by Ashish Darbari on 08-29-2021 at 6:00 am
Categories: Axiomise, Cadence, EDA, Semiconductor Services

オープンソースのRISC-V命令セットアーキテクチャ（ISA）の登場により、プロセッサ・アーキテクチャおよび設計開発は完全に自由化され、RISC-Vシリコンを入手する競争が激化している。今後5年以内に、RISC-Vベースのラップトップやデスクトップが市場に出回ることは間違いないだろう。しかし、これらのプロセッサは高品質なのだろうか？90年代半ばに発覚した有名なIntel社のFDIVバグのような不具合はないのだろうか？私たちは、セーフティクリティカルなドメイン、セキュリティ、機能性について、プロセッサをロバストに検証するために必要なことを学んだのだろうか？

この記事では、オープンソースRISC-Vアーキテクチャの観点から、検証のトレンド、プロセッサ検証を困難にする要素、そして特にAxiomise社が提供する完全自動化されベンダー非依存のformalISA ®アプリとCadence社のJasperGold®フォーマル検証プラットフォームの組合わせにより、フォーマルメソドロジ適用をいかに容易化できるかについて見ていく。またAxiomise社のデバッグ、解析、レポーティングを自動化する新たなソリューション（i-RADARTM）についても議論する。

プロセッサ検証はなぜ困難なのか？

設計者は、RISC-V ISAを採用し、消費電力と性能面から最適化された多くの異なるプロセッサアーキテクチャを幅広いデバイス、つまりモバイル、IoTエッジからハイエンドのサーバーに至るまで適用を始めている。しかし、それぞれの異なる実装であっても、ISAのすべての命令を完全に機能的に一貫して実行できなくてはならない。この機能の一貫性は、デバイスが遭遇する可能性のある幅広い未知のデータセットに対しても完全な検証が求められ、従来の検証手法では実現が困難である。

加えて複雑なマルチスレッドを持つパイプラインアーキテクチャやアウトオブオーダーの実行は、検証にとって大きな課題である。シミュレーションでは容易に捕えることができない一般的な検証バグは、同時実行、ストール、割込み、レース条件、アービトレーション、メモリ順序によるものが多い。デバッグはさらに大きな課題となり、セキュリティ上のリークを発生させないようにすることは、設計者にとって別の頭痛の種となる。

業界はどのように対応しているのか？

UVMを使用したシミュレーションベースの検証は、検証立ち上げ時のスティミュラスのランダム化に大きく依存し、サインオフには機能カバレッジを使用する。 プロセッサが複雑化し大規模化する中で、マイクロアーキテクチャ内部のステートマシンの相互作用という深いポイントにまで到達できるスティミュラスをモデル化し、プロセッサのすべてのバグを顕在化することは容易ではない。機能カバレッジは、まさに同じスティミュラスとランダム化に大きく依存するため、サインオフの能力は限られており、シミュレーションベースでは網羅的な検証は無理なのだ。許容可能な機能カバレッジの達成率を得るために、UVMインフラストラクチャを人の努力によって向上させることは有名な話である。Harry Foster氏によるWilson Researchのレポートでは、プロセッサのデザインハウスでは設計者1人に対して5人の検証エンジニアを雇用していると指摘している。また同レポートではシミュレーションが検証手法の主流であることが明確に示されているが、ASICの68％、FPGAの83％が初回シリコンで失敗していると指摘している。

そのため、業界の大半がシミュレーションベースの検証を理解し、常に自分が最もよく知る方法で突き進めるのは簡単であることは十分に理解できるが、検証課題の複雑さとUVMベースの検証の不十分さにより、業界はフォーマル検証を採用せざるを得なくなっている。ArmやIntelのような確立したISAの所有者は、検証も含めてリードしてきた。彼ら業界のリーダーたちは、ISAの動作の一貫性が、無数の実装アーキテクチャにわたり、ISAを中心としたソフトウェアのエコシステムを発展させるために不可欠であることを理解している。RISC-Vの場合、ISAの整合性に責任を持つ単一の組織が存在しないため、RISC-Vにリソースを投入する企業にとって、ISAの検証はさらに重要であると言える。さらに歴史から学ぶべきことがあるとすれば、Intel FDIVや、より最近のセキュリティ欠陥であるSpecter/Meltdownの問題は、目からウロコのはずである。あなたが開発するシリコンは、最初に動作した時のように、何年経っても、ロックすることなく、ハッカーにさらされることなく、期待通りに動作しなくてはならない。

フォーマル検証：網羅的な保証を提供する唯一の方法

高品質な検証を低コストで実現するためには、フォーマル検証しかないだろう。フォーマル・プロパティを記述する時間は、UVMテストベンチのインスツルメンテーションに比べればほんのわずかである。これらのフォーマル・プロパティを検証する実行時間はさらに短くなる。ここ2年間で、Axiomiseのフォーマル検証ソリューションにより、cv32e40p、ibex、0riscy、そして最近では6段のインオーダーパイプラインを持つWARP-Vファミリなどのプロセッサ上で27,000以上のプロパティを数時間で網羅的に証明できることが繰り返し示されている。

確かに、フォーマルプロパティをコーディングするには人的努力が必要であり、何をコーディングすべきか、どのように効率的にプロパティをコーディングするかを知るには経験が必要になる。これこそが、まさにAxiomiseがフォーマル検証コースを教える理由で、コースオンラインのセルフペースで学習できるものと、インストラクタによるコースの両者がある。

AxiomiseはCadence社と提携し、業界をリードするJasperGoldフォーマル検証プラットフォームを使用する顧客向けに、これらのコースを提供している。しかしフォーマル検証を学び、高品質なフォーマル検証済みデザインを必要な時間内に顧客に届けるリソースがない場合、AxiomiseのRISC-V向けの既製のフォーマル検証ソリューションを購入することもできる。

WARP-Vのケーススタディ

WARP-Vは、RedWood EDAのCEOであるSteve Hooverが、TL-Verilog（Verilogに新たにトランザクションレベル機能を追加したもの）を推進するために考案したもので、設計者が効率的にバグを抑えた設計を実現し、最終的にRTLをコレクトバイコンストラクションで構築できるように設計されている。このインフラストラクチャの優れた点は、高位TL Verilogモデルで多段パイプライン設計を簡単に行えることである。実際、Verilogを抽出することもでき、抽出されたVerilogでも非常に優れた可読性が保持されている。

WARP-Vのフォーマル検証

SteveがWARP-Vプロセッサーを設計したとき、SteveとAkos Hadnagyがどのようにプロセッサーをフォーマル検証したかを含め、これらのコンセプトを実証するために多くの記事が書かれている。Steveはオープンソースのソリューションを使用していた。SteveがWARP-Vの検証にそれを採用したと発表したとき、私を含め誰もがバグがないことを確信していた。

formalISA® を用いたWARP-Vのフォーマル検証

そこでShivani ShahがAxiomiseのformalISAソリューションを使い、AxiomiseとともにWARP-Vプロセッサーのフォーマル検証を始めたとき、その時点ではバグが見つかるとは思っていなかった。すでにフォーマル検証を使っているのに、バグが見つかるわけないと思っていたのだ。

そのため、WARP-Vコアをアプリに統合してから数分も経たないうちにプロパティに障害が発生したときは、本当に驚きだった。最初の直感は、私たちの検証ソリューションに問題があるのではないか、あるいは実際に統合が正しく行われておらず、アプリの設定に使用したマッピング・ファイルに不一致があるのではないか、というものだった。

Shivaniがさらに深く掘り下げ、チケットを開き、Steveに問い合わせを始めたとき、私たちが発見した問題はまさに真の設計バグであることが判明した。これらのバグの初期セットはすべて、RISC-V ISAの仕様に準拠したformalISAで分岐命令のセマンティクスがどのように解釈されているか、また、たまたま一致したSteveの設計モデルとオープンソースのRISC-Vフォーマルテストベンチがアーキテクチャ仕様に準拠していないことに起因していたた。つまり、WARP-Vプロセッサーはプロセッサーとしては動作するが、RISC-V ISAが提示する要件を満たしていなかった。ソフトウェアはコンパイラを通してある動作をするが、ハードウェアは別の動作をしていた。私たちは、SteveAkosとアコスと直接ミーティングを予定し、両者ともこれが設計上のバグであることを確認した。

そもそもなぜこのようなバグが発生したのかをSteveに尋ねたところ、Steveは設計当時、仕様のいくつかの側面が明確でなかったため、オープンソースのRISC-Vのフォーマルなセマンティクスの解釈に頼ったと述べた。Steveが自分でバグを発見しなかったことは驚くことではないが、驚いたのは、彼らが使用したフォーマルモデルにこのバグがあったことだ。

注意点について記載するならば、オープンソースの公式ソリューションと同じ分岐命令のセマンティクスをコアで使っているなら、コアに同じバグがある可能性があるということだ。

Shivaniが彼女の仕事の範囲を拡大し、私たちのアプリにM-extensionsを追加し始めたとき、さらに多くのバグが特定された。この完全なリストは私たちのGithubページから見ることができる。

formalISA®を用いたこれまでの検証

我々は以前、他のプロセッサの検証にも我々のアプリを使用している。RISC-V summit 2019では、検証をどのように開始し、チェックをどのようにフォーマルモデル化するかについて詳細を説明し、検証メソドロジについて概説した。そこでは0riscyとibexの検証結果を提供している。どちらも2ステージ・パイプラインを持つ小規模な組込みデザインであり、0riscyはすでに検証済みで、すでにシリコンの工程に入っていたが、アプリによりデッドロックを含む65以上のバグが特定された。Ibexは0riscyのクローンに近いものだったが、その開発が開始し、初期段階で検証を行い、多数の命令に影響を及ぼすコーナーケースのバグをいくつか特定している。

2020年には、OpenHWグループと協力しcv32e40pコアをフォーマルで検証した。広範囲なカバレッジを含む約27,000のプロパティを数時間で検証することができた。これらの結果は、2020年のRISC-Vサミットや2021年3月のウェビナーで発表された。また、公開されているRISC-V ISA仕様の不整合問題を含むいくつかのバグを発見した。

formalISAで特定された仕様のバグの例

公開されているRISC-V ISAの仕様v2.2では、30ページでimm[5]が0でない場合、シフト命令SLLI、SRLI、SRAIに対してイリーガルなインストラクション例外の生成を要求している。しかし、仕様書の104ページには、SLLI、SRLI、SRAIの命令に対するオペコードを提供しており、でコードされた命令がこれらのいずれかである場合、imm[5]が0でないことはあり得ない。

シナリオカバレッジ

従来のマイクロプロセッサの検証は、シミュレーションを用いたアーキテクチャテストに大きく依存している。このためシミュレーションによる機能カバレッジでは、さまざまな命令間の相互作用をテストするが、検証品質の結果は特定のスティミュラスパターンに限定されてしまう。私たちのシナリオカバレッジでは、フォワーディング、パイプライン命令インターリーブ、ストール、割り込み、デバッグの相互作用などの最適化をターゲットとした、興味深いシナリオの範囲を検証するためのassertとcoverを自動生成する。

どのように機能するか

formalISAアプリは、Excelスプレッドシートからユーザー定義の仕様を読み込み、波形とともにプロパティのアサーションとカバレッジ、そしてそのプルーフを生成し、これらの仕様項目が到達可能なすべての状態で常にホールドすることを疑う余地なく立証する。下の図は、リセットから4サイクル後にSUB命令が 2回発行され、その1サイクル後にOR命令が発行され、その1サイクル後にAND命令が発行されることを指定するユーザー・エントリを示している。このエントリは、フォーマル・ツールで証明されるカバレッジ・ターゲット（アサートとカバー）の範囲をトリガする。以下の波形は、フォワーディングを示すこのエントリを満たすシナリオを示している。

アーキテクチャ検証のプランニングとステータスのダッシュボード

formalISAアプリを用いる私たちのソリューションの優れた点は、ユーザーがRTLや仕様のバグを発見し、プルーフへと導き、ワンプッシュのボタンで検証プランニング、ステータス、カバレッジ結果全体を自動生成できるということである。プランニングとステータスは、RISC-VInternationalが発行するRISC-V仕様に直接リンクされている。

Cadence JasperGold®のようなツールを使用すると、JasperGoldの機能を活用した豊富なカバレッジのダッシュボードを生成することができる。

i-RADAR – Intelligent Rapid Analysis Debug and Reporting

Shivaniがバグを発見し、私たちが一緒にその根本原因を探っていたとき、私たちはフォーマルメソドロジとフォーマル検証のデバッガの１つであるJasperGold® Visualizeを使用していたものの、そのデバッグには大変な労力を要した。JasperGold®は、プロパティの不具合に関連する正確な一連の信号を特定するが、多くの場合、特定された信号は、プルーフコアにリンクされており、正確すぎるのだ。

この意味は、信号の特定のビット、たとえば分岐アドレスのビット [1:0] がフェイルの原因である場合、それが表示され、ユーザーはトレースを体系的に追跡する必要がある。これはすべて正しいことではあるが、デバッグを行う人が、何かがフェイルした理由をまとめ、それがバグである理由を理解してから設計者に返すには時間を要してしまう。

トレースに関する説明だけでは、設計者は何がデバッグされているのか分からないと不満を漏らすことがよくある。この問題を克服するために、私たちはAxiomiseでi-RADAR™️と呼ばれる新しいインテリジェントなデバッグソリューションを設計した。i-RADAR™️はIntelligent Rapid Analysis, Debug and Reportingの略で、formalISAアプリを購入するとJasperGoldのプラグインソリューションとしてAxiomiseから提供される。

JasperGoldとformalISAアプリを使用している場合、JasperGoldにGUIボタンが表示される。このボタンをクリックすると、Axiomiseのインテリジェント解析が実行され、フェイルしたプロパティに対して、設計者へのデバッグのハンドオフのためにVCDと共にデバッグレポートが生成される。つまり、デバッグ、トラブルシューティング、レポート作成などに人手をかける必要がない。

i-RADERの活用

i-RADAR™️をCadence JasperGold®で使用した場合の波形イメージを表示している。トレースは、WARP-VのBEQ命令のフェイル・プロパティを示している。コーズアリティ関係の正確な連鎖がデバッガに注釈されている。また設計バグである理由を説明するレポートも以下のファイルに出力される。

——————————————————————————————-

formalISA generated cover report for the instruction beq

Generated on 2021-08-22 17:07:44 %

beq.fsdb, beq.vcd, and beq.shm written on disk

——————————————————————————————-

The waveform is for the RISC-V instruction: BEQ

BEQ was triggered for execution and commit (u_isa.beq_instr_trigger) in cycle: 23

Design computes the branch target address in cycle 23 = 32’h00000034

Formal model computes the branch target address in cycle 23 = 32’h00000030

The formal model computes target address in cycle 23 using the PC (32’h00000001) and the offset (32’h00000030)

The value computed by the design 32’h00000034 does not match with the value computed by the formal model 32’h00000030

——————————————————————————————-

なぜAxiomiseフォーマル検証ソリューションが重要なのか？

Axiomiseは、通常の命令だけでなく特権命令もサポートするRISC-V ISAのアーキテクチャモデルの構築に投資してきた。プロセッサの検証に何年もの経験値をもつAxiomiseチームは、キーとなる抽象化技術をformalISA®アプリに落とし込み、独立したレビューを受け、異なるプロセッサに対しても適用できるようにした。Cadence社とのパートナーシップにより、JasperGold®ユーザー向けにformalISA®アプリを用いた検証と最適化を行うことができる。Axiomiseは、6次元カバレッジソリューションの一部として、業界初のシナリオカバレッジベースのソリューションも構築している。当社のソリューションは、すべてのフォーマル検証ツールで動作し、プッシュボタン式で、最初のプルーフの実行からインテリジェントなデバッグ、6次元を使用した包括的なカバレッジの取得まで、スマートに自動化できる市場で唯一のソリューションである。

さらに詳細については、以下のリンクを確認していただきたい。

まとめ

プロセッサを設計することと、それをFPGAで実現し、プログラムの実行例を示すことは別のことである。しかし、このプロセッサが機能的、安全性、セキュリティ上の欠陥を持つことなく、期待通りにシリコン上で正しく動作することを保証することは、まったく別の課題である。

欠陥ゼロのシリコンを構築することは容易ではなく、ベストの検証技術を結集して集中的に取り組む必要がある。そして検証を推し進める各人の政治的なマイルストーンではなく、検証の関心事に焦点を当てる必要がある。UVMを使用したシミュレーションベースの検証では、プロセッサを高品質に検証することはできない。その事を気にする必要はなく、誰もが徹底的な検証に近づくことすらできないのだ。Intel、IBM、Arm、AMDのような有名なプロセッサ・デザイン・ハウスは、過去30年以上にわたって、フォーマルメソドロジによって検証作業をどのように補完・補足してきたかを示す数多くの論文を発表している。フォーマルメソドロジは、網羅的な検証結果を得る唯一の方法であり、これによってシリコンをサインオフすることで、誰もが安心して眠れるようになる。フォーマルメソドロジを使うことで、バグがないことを証明し、コーナーケース（100万分の1の確率）のバグを数秒で浮かび上がらせることができる。また、さまざまなカバレッジ手法を使い、フォーマルメソドロジで完了と言われたら、本当に完了したのだと証明を通して納得させることができる。

AxiomiseのRISC-Vフォーマル検証アプリであるformalISA®は、Cadence社のJasperGold®のようなトップエンドのフォーマル検証ツールと組み合わせて使用することで、特注のテストベンチを立ち上げる人的コストを削減し、網羅的なサインオフへのパスを加速する完全なソリューションを提供する。新たなデバッグ・ソリューションを組み合わせることで、設計者へのデバッグ・ハンドオフのための自動化されたインテリジェント解析を実行し、デバッグ時間とコストを削減することができる。

著者:
Axiomise, Ashish Darbari
Cadence Design Systems, Pete Hardee