※本記事はInterface誌2023年3月号に掲載されたものの原稿版になります
今回はプロセッサ開発における機能検証についてご紹介します．ハードウェアやソフトウェアに限らず，製品開発においては検証に多くの工数をかけます．もちろんプロセッサ開発も例外ではありません．プロセッサの機能はプログラムの命令列を実行することです．もしプロセッサにバグがあってプログラムを正常に実行することができないと，システム全体が正常動作しないことになります．検証の重要性は明らかで，決して不十分であってはならない開発フェーズです．一方で，製品開発には開発期間や予算といった制約があります．製品に求められる品質を検証で担保すると共に，開発コストやリリース日程を守って計画通りに開発を完了することもまた製品開発に求められます．
プロセッサの検証は何が大変か
大変でない検証はありませんが，プロセッサの検証も大変なものになりがちです．その要因は数多くありますが，ここではデータパスの構造に起因する例をご紹介します．下の命令はRISC-V(1)の整数加算命令で，レジスタt0，t1の加算結果をレジスタt2に格納します．
add t2, t0, t1
プロセッサがこの命令を正しく実行することを検証するには，ソースレジスタであるt0，t1に値を入力してこの命令を実行し，ディスティネーションレジスタt2に期待値が格納されることを確認します．RISC-Vでは命令の動作を確認する検証プログラムとしてriscv-tests(2)やRISC-V Architecture Test SIG(3)などGitHubで公開されているオープンソースのものや商用のテストスイートなど多数あり，これらを活用することができます．しかし，多くのパイプライン構造のプロセッサではそのような検証だけでは不十分です．その理由を説明するために，少しだけプロセッサのデータパス構造の例について触れます．図1と図2は5段パイプラインプロセッサのデータパスの例です．下のように① sub命令の結果を② add命令がレジスタt0経由で参照するケースを考えます．
① sub t0, t3, t4 ② add t2, t0, t1
図1のデータパス構造では，① sub命令の結果を一度レジスタファイルのレジスタt0に書き込んだ後に，レジスタファイルからレジスタt0の値を読み出して② add命令を実行する動作となります．この場合，レジスタt0のレジスタファイルへの書き込みと読み出しで3クロックサイクルのパイプラインストールが発生するため，② add命令はクロックサイクル#9で完了することになります．パイプラインストールの間プロセッサは命令を実行することなく時間だけが過ぎていくため，性能の低いプロセッサとなります．一方，図2のデータパス構造では，① sub命令の演算結果をEXステージのALU(算術論理演算器)の出力から② add命令のIDステージにバイパスすることができます．② add命令は① sub命令の結果を必ずしもレジスタファイルから読み出す必要はありません．クロックサイクル#3の① sub命令の演算結果を次のクロックサイクル#4で② add命令が参照して演算できれば，パイプラインストールを発生させることなく② add命令をクロックサイクル#6で完了することができ，より性能の高いプロセッサとすることができます．これは一例であり，多段パイプラインステージを備えるプロセッサやALUを複数備えるスーパースカラプロセッサでは，より多くのバイパス経路を備えます．さらに，割り込みや分岐予測ミスによるパイプラインフラッシュなどの命令実行制御，高性能化のためのキャッシュなど複雑化する構造は多数あり，検証ではこの組み合わせも考慮する必要があります．全ての組み合わせを挙げると気の遠くなるような膨大な検証ケースを考慮しなければならないことがイメージできるかと思います．そして，それはプロセッサの構造に依存するために前述のriscv-testsやRISC-V Architecture Test SIGなどRISC-V命令の動作結果のみを確認する検証プログラムでは不十分で，内部構造を全て確認する検証プログラムを作成する必要があります．
図1： 5段パイプライン・プロセッサ(バイパスなし)
図2： 5段パイプライン・プロセッサ(バイパスあり)
こういった機能検証は，機能仕様や実装仕様をインプットとしてプロセッサに発生しうる内部状態を網羅した検証項目を作成し，それに従ってサブユニット毎の検証やプロセッサ全体結合で検証することになります．以下で，プロセッサ全体の結合検証における検証手法の一部をご紹介します．
プログラムを動かす動的検証
図3はプロセッサの動的検証を行う論理シミュレーション環境の構成例で，実際のマイコンやSoCと同様にプロセッサとメモリモデル，割り込みコントローラなどをバスで接続した環境です．この検証環境のシミュレーション制御部が検証プログラムバイナリをメモリモデルに読み込んだ後にリセットを解除し，検証対象であるプロセッサがメモリモデルから検証プログラムを命令フェッチして実行，といった実際のプロセッサの動作を確認することができます．
図3： 論理シミュレーション環境
重要なのは，プロセッサの動作結果が期待通りであることのチェックです．プロセッサの検証ケース数は非常に多く，検証プログラム全てを論理シミュレーション環境が出力する信号波形で正常動作を確認するのは，たとえ小規模のプロセッサでも大変非効率です．また，一度検証プログラムで動作を確認した後に，デザインを変更するたびに再び全ての検証プログラム実行の信号波形を確認するのは非現実的です．そこで検証環境で正常動作をチェックする機構を用意しておきます．ここでは，メモリデータのチェックと命令毎の実行結果ログのチェックの2つの方法をご紹介します．1つ目のメモリデータのチェックとは，検証プログラムの中に検証結果をメモリモデルに書き込む処理を仕込んでおき，検証プログラムの動作完了後に期待値チェッカがメモリモデル上の値と予め用意した期待値を一致確認するものです．2つ目の命令毎の実行結果ログのチェックとは，検証プログラムのアセンブラ1命令毎に実行結果がプロセッサと命令セットシミュレータとで一致することを確認するものです．命令セットシミュレータとはC++などでプロセッサの機能仕様を実装したもので，RISC-VではGitHubで公開されているspike(4)や商用のものがあります．例えばspikeでは，図4のようなプログラムの実行結果ログを1命令毎に出力することができます．開発したプロセッサにも同様に1命令毎に実行結果ログを出力させることで，実行結果の一致比較をすることができます．検証担当者はこのように動的検証環境を整備した上で，プロセッサの内部状態も含めて確認する検証プログラムを作成して検証します．
図4： spikeの命令実行結果ログ
プログラムを動かさない静的検証
20年ほど前に筆者が新卒入社してすぐに従事したプロセッサ開発では，検証担当者はまだ論理シミュレーションのみで機能検証を行っており膨大な数の検証プログラムを作成していました．前述したように検証は構造の複雑化に伴って必要な検証ケースが増加するので，大規模化，高性能化したプロセッサの開発においては動的検証のみでは限られた期間で検証を完遂することは困難です．そこで近年では，静的検証の1つであるフォーマル検証を組み入れる開発が行われています．フォーマル検証は，論理シミュレーションで動作させることなく機能仕様や実装仕様と回路の間に矛盾ないことをツールが静的に解析して回路の実装が正しいことを確認する検証手法です．検証担当者は，フォーマル検証を活用することで大量の検証プログラムを作成することなくプロセッサの多数の内部状態の組み合わせを確認することができます．フォーマル検証を行うツールはEDA(Electronic Design Automation)ツールベンダーからリリースされており，弊社のハードウェア開発でも広く適用している検証手法となっています．フォーマル検証の詳細な説明については他を参照していただくとして，ここではSVA(SystemVerilogアサーション)を用いたフォーマル検証の例をご紹介します．
図5は，SVAを用いたフォーマル検証の例です．フォーマル検証ツールは，検証対象のデザインと仕様書を元に作成したSVAを入力として，証明結果を出力します．証明結果は，証明できた／指定した探索範囲で証明も反例発見もできなかった／反例を発見した，と主に3種類になります．反例とは，SVAで記載した期待と異なる動作をするバグケースです．フォーマル検証ツールは，期待と異なる動作を検出したクロックサイクルからその原因になる動作のクロックサイクルまで遡って波形を出力します．設計者はこの反例の波形を確認してバグ解析することができます．
図5： SVAを用いたフォーマル検証
図6は，プロセッサの命令処理を確認する例です．ここでは検証対象を図2のようなシングルスカラ，インオーダーパイプラインのプロセッサとし，下の命令の動作を確認するケースを考えます．
and t5, t0, t1
and命令のWBステージ時点ではそれより前の命令は実行完了して結果が全てレジスタファイルに反映されているため，and命令のWBステージとその次のクロックサイクルの間の変化が期待通りであることを確認します．図6に記載したSVAこの確認内容に従ったもので，and命令のWBステージ時点でのレジスタファイル上のソースレジスタt0,t1を参照し，そのAND論理演算の結果が次のクロックサイクルでのディスティネーションレジスタt5の値と一致することを確認するものとなっています．一方，検証対象プロセッサのパイプライン処理ではIDステージでソースレジスタt0,t1の値をレジスタファイルかEX,MEM,WBステージからのバイパス経由で取得し，EXステージでAND論理演算を処理した後にWBステージで演算結果をレジスタファイルにライトバックします．フォーマル検証ツールはVerilogやVHDLといったRTL(Register Transfer Level)記述のプロセッサデザインとSVAを入力として，ディスティネーションレジスタt5の結果が常に一致することを証明します．フォーマル検証ツールはクロックサイクルを遡ってWBステージより前の処理の状態も探索するため，この証明ができると，and命令の演算結果のみでなくソースレジスタのリード元の選択やWBステージに至るまでのパイプラインストール制御などand命令の処理が正しく実装されていると判断することができます．
図6： 命令処理の確認
検証プログラムを用いた動的検証で同様のバイパスやパイプラインストール制御など全ての状態の組み合わせを確認するには，時間をかけて多くのプログラムを作成する必要があります．このことから，フォーマル検証が少ない工数で検証するのに有効であることがお分かり頂けるかと思います．しかしフォーマル検証も万能ではありません．フォーマル検証ツールはデザインの内部状態をデータや制御の区別なく網羅的に探索するため，検証対象のデザインの規模に従って探索範囲が膨大になります．探索範囲の規模に伴って多くの計算機リソースと時間を必要とするため，デザインの規模次第では検証できない結果となることもあります．その場合は探索を検証可能な範囲に限定するために，内部状態を制限する制約記述を追加して検証します．図6に示したような比較的小規模なプロセッサを検証する場合でも，検証ケース別に探索範囲を限定する制約を追加する必要があるでしょう．例えばプロセッサのレジスタや演算器の幅は32ビットもしくは64ビットが一般的ですが，パイプライン制御を検証する場合はその全ての値を網羅する必要はありません．この場合，探索範囲を限定するためにレジスタの値に制約を追加します．また，図6に示したSVAでは割り込みや分岐予測失敗といった要因によるand命令のパイプラインキャンセル制御は対象外となるため，それらは別のSVAもしくは論理シミュレーションなどで検証を補完する必要があります．
おわりに
今回は，プロセッサ開発で用いられる検証手法のうち論理シミュレーション検証とフォーマル検証の例をご紹介しました．これら検証の一端のみのご紹介でしたが，それぞれ一長一短あることがお分かり頂けたかと思います．他にも多くの検証手法があり，EDAベンダーは様々な検証ツールをリリースしています．工数が大きいプロセッサ検証において，検証のポイントと各種検証手法の性質をしっかり把握して検証全体で複数の手法をうまく使い分けた検証戦略を立案するところは，プロセッサ開発全体の腕の見せ所の1つになるでしょう．
****
やました はじめ
****
[参考文献]
(1)RISC-V.
https://riscv.org/
(2)Unit tests for RISC-V processors, GitHub.
https://github.com/riscv-software-src/riscv-tests
(3)RISC-V Foundation Architecture Test SIG, GitHub.
https://github.com/riscv-non-isa/riscv-arch-test
(4)Spike; RISC-V instruction set architecture simulator, GitHub.
https://github.com/riscv-software-src/riscv-isa-sim