"The MIPS R10000 Superscalar Microprocessor" のパイプラインをまとめる

"The MIPS R10000 Superscalar Microprocessor" の論文をもう一度読み直してみている。

1. 概要

MIPS R10000 は、シリコン・グラフィックス社 (Silicon Graphics, Inc.) によって開発された 64 ビットスーパースカラマイクロプロセッサである。動的アウトオブオーダ実行機能を備え、MIPS IV 命令セットアーキテクチャを実装しており、複雑な実アプリケーションにおいて高いパフォーマンスを発揮するよう設計されている。

主要な特徴

• アウトオブオーダ・スーパースカラ: キャッシュミスによる停止を回避し、先行命令を継続的に実行することでレイテンシを隠蔽する。
• MIPS IV ISA の 64 ビット実装: フル 64 ビットの命令セットを実現。
• 高帯域幅の命令フェッチ: サイクルあたり 4 命令をフェッチ・デコードし、5 本の低レイテンシ実行ユニットへ発行する。
• 投機的実行: 分岐予測を用いた投機的フェッチと実行を可能とする。
• 順序通りのグラデュエーション: 実行はアウトオブオーダだが、完了は順序通りに処理される。
• 正確な例外処理とメモリ一貫性: シーケンシャルメモリ一貫性と正確な例外を保証。
• 階層型ノンブロッキングキャッシュ: 2 レベルのライトバックキャッシュによりメモリレイテンシを軽減。
• モジュラーデザイン: アクティブリスト、レジスタマップテーブル、命令キューを規則的構造に組み込み、設計の複雑さを軽減。
• 製造技術: 0.35μm CMOS 技術、680 万トランジスタ (うち 440 万はキャッシュアレイ)、ダイサイズ 16.64 × 17.934 mm。

---

2. 設計理念

R10000 はメモリ帯域幅およびレイテンシが性能を律することを前提に設計された。

• レジスタマッピングとノンブロッキングキャッシュ: キャッシュミス中でも他命令を継続実行可能とし、リソース効率を最大化する。
• 動的命令リオーダ: オペランドの準備状況に基づき実行順を変更し、キャッシュミス時も即座に適応する。
• 命令ウィンドウ: 最大 32 命令を先読みし並列実行機会を探索、セカンダリキャッシュレイテンシをほぼ隠蔽する。

---

3. パイプラインと命令実行

R10000 は 6 本の独立パイプラインを備える。

• 整数パイプライン × 2 (レイテンシ 1)
• 浮動小数点パイプライン × 2 (レイテンシ 2–3)
• ロード・ストアパイプライン × 2 (レイテンシ 1–2)

Figure.2 にそれぞれのパイプラインが図示されている。

• 浮動小数点パイプライン1
  • FPキュー(16エントリ)に格納され、発行されるとFPレジスタファイルにアクセスする。2つのデータを読み込んで、FP adderに渡され、その結果をFPレジスタに書き込む
• 浮動小数点パイプライン2
  • FPキュー(16エントリ)に格納され、発行されるとFPレジスタファイルにアクセスする。2つのデータを読み込んで、FP multiplierに渡され、その結果をFPレジスタに書き込む
• 浮動小数点メモリアクセス命令
  • Address Queue (16エントリ) に格納され、FPレジスタファイルにアクセスしている(2ポート使われているが、これはなんで？)。その後、データキャッシュにアクセスしている。
• 整数メモリアクセス命令
  • Address Queue (16エントリ) に格納され、整数レジスタファイルにアクセスしたのち、Address Calculationを行い、TLBにアクセスしている。
• 整数命令1
  • Integer Queue (16エントリ) に格納され、整数レジスタファイルにアクセスしたのち、Integer ALU1に格納し、整数レジスタファイルに書き込む。
• 整数命令2
  • Integer Queue (16エントリ) に格納され、整数レジスタファイルにアクセスしたのち、Integer ALU2に格納し、整数レジスタファイルに書き込む。

"The MIPS R10000 Superscalar Microprocessor" を NotebookLM でまとめさせてみる (2)

前回の続き：

msyksphinz.hatenablog.com

"The MIPS R10000 Superscalar Microprocessor" の論文を改めて読んでみて、NotebookLMを使ってまとめてみた。すごく便利だ。便利すぎて頭に入らないよ。

以下の文章は全部AIで生成してもらったので注意です。

---

レジスタリネーミング

アウトオブオーダー実行を実現するために、R10000はレジスタリネーミングを使用する。

論理レジスタと物理レジスタ

プログラマには見えない形で、命令フィールドで参照される論理レジスタ番号が、ハードウェアレジスタファイル内の物理レジスタ番号に動的にマップされる。

物理レジスタの数

物理レジスタは論理レジスタよりも多く、コミットされた値と、完了したがグラデュエートしていない命令の一時的な結果の両方を保持する。

• 整数レジスタ: 33の論理レジスタ（1～31、Hi、Lo）と64の物理レジスタ
• 浮動小数点レジスタ: 32の論理レジスタ（0～31）と64の物理レジスタ

レジスタマップテーブル

論理レジスタから物理レジスタへの現在の割り当てを保持する。整数用と浮動小数点用で独立している。

フリーリスト

現在割り当てられていない物理レジスタのリストを保持する。

アクティブリスト

プロセッサ内で現在アクティブなすべての命令を記録する。グラデュエーションまたは例外/誤予測分岐によるアボート時に命令がリストから削除される。最大32命令がアクティブである可能性があり、アクティブリストは4つの並列、8段の循環FIFOで構成されている。

ビジービットテーブル

各物理レジスタが現在有効な値を含んでいるかを示すビットを保持する。

命令キュー

R10000は、命令タイプに応じて3つの命令キューに命令を配置する。

整数キュー

16エントリを持ち、ALUへの発行時にエントリを解放する。オペランドの準備状況に基づいてアウトオブオーダーで発行される。

アドレスキュー

16エントリの循環FIFOで、オリジナルのプログラム順序を維持する。ロード/ストア命令を処理し、メモリ依存性を判断する。アドレスキューはロード/ストア命令を元の順序とは異なる順序で実行するが、逐次メモリ一貫性を維持する。

逐次メモリ一貫性の維持

外部インターフェースがキャッシュラインを無効化した後に、そのデータがレジスタにロードされ、しかしそのロード命令がグラデュエートする前にデータが使用された場合、キューはロード命令にソフト例外を生成する。これによりパイプラインがフラッシュされ、ロード命令とその後のすべての命令がアボートされ、古いデータが使用されないようにする。その後、例外を継続するのではなく、プロセッサはアボートされたロード命令から通常の実行を再開する。

ロードリンク (LL) およびストア条件付き (SC) 命令

MIPSアーキテクチャは、ロードリンク (LL) とストア条件付き (SC) 命令ペアでアトミックメモリ操作をシミュレートする。これらの命令はメモリへのロックアクセスを必要としないため、システム設計を複雑にしない。SC命令は、競合がなくリンクワードがキャッシュに残っている場合にのみメモリに書き込む。

浮動小数点キュー

16エントリを持ち、整数キューと似ているが、即値は含まれない。

実行ユニット

整数実行ユニット

ALU1とALU2

それぞれ64ビット加算器と論理ユニットを含む。ALU1はシフタと分岐条件ロジックを、ALU2は部分整数乗算アレイと整数除算ロジックを含む。

乗算と除算

ALU2で反復的に計算される。乗算はBoothのアルゴリズムを、除算は非回復型アルゴリズムを使用する。

浮動小数点実行ユニット

加算器と乗算器

3ステージパイプラインで、単一サイクル繰り返しレートのフルパイプラインである。

除算と平方根

独立した反復ユニットが、SRTアルゴリズムを使用してサイクルあたり2ビット生成する。除算ユニットはサイクルあたり4ビット生成するために2つのステージをカスケード接続する。

メモリ階層

R10000は、ノンブロッキングの2レベルセットアソシアティブキャッシュメモリ階層を実装している。

プライマリキャッシュ (オンチップ)

命令キャッシュ (32KB)

8,192命令ワードを格納し、各ワードは36ビット形式にプリデコードされる。同時に両方のキャッシュウェイから4つの命令をフェッチし、キャッシュヒットロジックが目的の命令を選択する。

データキャッシュ (32KB)

帯域幅を増やすために2つの16KBバンクをインターリーブする。

セカンダリキャッシュ (外部)

基本仕様

512KBから16MBまでの外部同期SRAMチップで実装された2ウェイセットアソシアティブキャッシュである。ラインサイズは16または32ワードに構成可能である。

疑似セットアソシアティブ

標準SRAMと1つの追加アドレスピンで2ウェイの疑似セットアソシアティブを実現する。

エラー訂正コード (ECC)

データ整合性のため、各データクワッドワードに9ビットのECCコードとパリティビットを格納する。

システムインターフェース

R10000は、64ビットのスプリットトランザクションシステムバスを使用して外部と通信する。

クラスター接続

最大4つのR10000チップを直接クラスター接続できる。

ノンブロッキングキャッシュリフィル

最大4つの未処理の読み取り要求をサポートする。

キャッシュコヒーレンシ

8エントリのクラスターバッファが未処理の操作を追跡し、キャッシュコヒーレンシを確保する。

クロック

オンチップのPLLが、外部システムインターフェースクロックと同期してすべてのタイミングを生成する。システム設計の柔軟性のため、セカンダリキャッシュとシステムインターフェースのクロック周波数を独立して設定できる。

パイプラインクロックの2倍で動作するPLLクロックを基準としている。パイプラインが200MHzで動作する場合、PLLは400MHzで動作し、ユーザーはシステムインターフェースを200、133、100、80、66.7、57、または50MHzで設定できる。また、セカンダリキャッシュを200MHzから66.7MHzの間で独立して設定できる。

出力ドライバー

4つのバッファグループがあり、LVCMOSまたはHSTL規格に個別に設定可能である。キャッシュアドレスバッファは大きなトーテムポールトランジスタを使用して複数の分散負荷を高速駆動する。キャッシュクロックバッファは最小出力遅延で低インピーダンス差動信号を駆動する。低ジッタ遅延要素がこれらのクロックを精密にアライメントし、プリント基板のクロックネットでの伝播遅延に合わせて静的に設定されるため、クロックの立ち上がりエッジがプロセッサの内部クロックと同時にキャッシュに到達する。

パフォーマンス

200MHzのR10000マイクロプロセッサ、4MBセカンダリキャッシュ（200MHz）、100MHzシステムインターフェースバス、および180nsメモリレイテンシを持つシステムでの予測パフォーマンスは以下の通りである。

• SPEC95int (ピーク): 9
• SPEC95fp (ピーク): 19

まとめ

MIPS R10000は、当時の最先端のアウトオブオーダー実行技術を駆使した革新的なプロセッサであった。レジスタリネーミング、投機的実行、ノンブロッキングキャッシュなどの技術により、高い命令レベルの並列性を実現し、複雑なリアルワールドアプリケーションにおいて優れたパフォーマンスを発揮した。

特に注目すべきは、逐次メモリ一貫性を保ちながらアウトオブオーダー実行を実現した点である。これにより、プログラマには逐次実行と同じ見た目を提供しつつ、内部では高い並列性を実現するという、理想的な設計を実現している。

R10000の設計思想と技術は、その後のプロセッサ設計に大きな影響を与え、現代の高性能プロセッサの基礎となっている。

"The MIPS R10000 Superscalar Microprocessor" を NotebookLM でまとめさせてみる (1)

"The MIPS R10000 Superscalar Microprocessor" の論文を改めて読んでみて、NotebookLMを使ってまとめてみた。すごく便利だ。便利すぎて頭に入らないよ。

以下の文章は全部AIで生成してもらったので注意です。

---

はじめに

MIPS R10000は、シリコン・グラフィックス社（Silicon Graphics, Inc.）によって開発された、動的なアウトオブオーダー実行機能を備えた64ビットのスーパースカラーマイクロプロセッサである。 MIPS IV命令セットアーキテクチャを実装しており、複雑なリアルワールドアプリケーションにおいて高いパフォーマンスを発揮するように設計されている。

主要な特徴

アウトオブオーダー・スーパースカラー実行

R10000の最大の特徴は、アウトオブオーダー・スーパースカラー実行である。 キャッシュミスによって停止した命令のさらに先の命令を実行することで、レイテンシによる時間ロスを最小限に抑える。 これにより、他の命令を完了させ、後続のキャッシュ・リフィルを早期に開始することができる。

MIPS IV ISAの64ビット実装

64ビットのMIPS IV命令セットアーキテクチャを完全に実装しており、当時の最新の命令セット機能を活用している。

高性能な命令フェッチとデコード

サイクルあたり4つの命令をフェッチおよびデコードし、5つのフルパイプライン、低レイテンシの実行ユニットに動的に発行する。 これにより、高い命令レベルの並列性を実現している。

投機的実行

分岐を超えて投機的に命令をフェッチし、実行することができる。分岐予測の精度が高い場合、パイプラインの停止を大幅に削減できる。

順序通りのグラデュエーション

命令は完了時に順序通りにグラデュエート（完了）する。 これにより、プログラムの意味論を保ちながら、アウトオブオーダー実行の利点を享受できる。

逐次メモリ一貫性と正確な例外処理

実行はアウトオブオーダーであるが、逐次メモリ一貫性と正確な例外処理を提供する。 これにより、プログラマには逐次実行と同じ見た目を提供しつつ、内部では高い並列性を実現している。

階層型ノンブロッキングメモリシステム

2レベルのセットアソシアティブ、ライトバックキャッシュにより、メモリレイテンシを隠蔽する。 この階層型のノンブロッキングメモリシステムは、メモリレイテンシを効果的に隠蔽する。

モジュラーデザイン

複雑性に対処するため、アクティブリスト、レジスタマップテーブル、命令キューなど、多くの制御ロジックを規則的な構造内に配置したモジュラーデザインを採用している。

製造技術

0.35μm CMOS技術を使用し、16.64x17.934mmのチップ上に680万個のトランジスタ（プライマリキャッシュアレイに440万個）を搭載している。この298 mm²のチップは、当時の最先端の製造技術を活用している。

設計理念

メモリ帯域幅とレイテンシが多くのプログラムのパフォーマンスを制限するため、R10000はこれらのリソースを効率的に利用するように設計されている。

レジスタマッピングとノンブロッキングキャッシュ

キャッシュリフィル操作をオーバーラップさせるために相互に補完する仕組みを採用している。これにより、命令がキャッシュミスした場合でも、他の命令はアウトオブオーダーで実行を継続できる。

動的命令リオーダー

オペランドの可用性に基づいて命令実行を動的にリオーダーする複雑なハードウェアを備えている。これはキャッシュミスが命令を遅延させる際に即座に適応する仕組みである。

命令ウィンドウ

最大32命令を先読みし、並列処理の可能性を探す。 これはセカンダリキャッシュからのリフィルレイテンシのほとんどを隠蔽するのに十分な大きさであるが、メインメモリのレイテンシの一部しか隠蔽できない。 メインメモリのレイテンシは通常、セカンダリキャッシュよりもはるかに長いためである。

パイプラインと命令実行

R10000は、6つのほぼ独立したパイプラインを持っている。

命令フェッチパイプライン (ステージ1-3)

ステージ1: 命令フェッチとアライメント

次の4つの命令をフェッチしてアラインする。

ステージ2: デコードとリネーム

命令をデコードおよびリネームし、ジャンプおよび分岐命令のターゲットアドレスを計算する。

ステージ3: キューへの書き込み

リネームされた命令をキューに書き込み、オペランドが最初にビジーであるかを判断するためにビジービットテーブルを読み取る。オペランドがすべて準備できるまで、命令はキューで待機する。

実行パイプライン (ステージ3-X)

ステージ3 (後半): 命令発行とオペランド読み取り

キューが命令を発行し、レジスタファイルからオペランドを読み取る。5つの実行パイプラインは、ステージ3でキューが命令を発行したときに開始される。プロセッサはステージ3の後半にレジスタファイルからオペランドを読み取り、ステージ4で実行を開始する。

ステージ4: 実行開始

実際の命令実行が開始される。

レイテンシ

• 整数パイプライン: 1ステージ
• ロードパイプライン: 2ステージ
• 浮動小数点パイプライン: 3ステージ

結果の書き込み

結果は次のステージの前半にレジスタファイルに書き込まれる。

独立した整数/浮動小数点セクション

最大限の並列操作を可能にするために、独立した命令キュー、レジスタファイル、データパスを持っている。

命令フェッチと分岐予測

高帯域幅のフェッチ

プロセッサは、実行できるよりも高い帯域幅で命令をフェッチおよびデコードする必要がある。これにより、分岐予測ミスやキャッシュミスによる停止を最小限に抑えることができる。

投機的フェッチ

分岐予測に基づいて、投機的に命令をフェッチする。誤予測された分岐の後の命令は破棄される。この仕組みにより、分岐予測が成功した場合のパフォーマンス向上を実現している。

分岐予測

512エントリの分岐履歴テーブルに基づいた2ビットアルゴリズムを使用する。Spec92整数プログラムでは87%の予測精度を示す。この高い予測精度により、投機的実行の効果を最大化している。

アラインされていない命令フェッチ

16ワードの命令キャッシュライン内の任意のワードアラインメントで、4つの命令を並行してフェッチする。これにより、命令の配置に関係なく、高いフェッチ帯域幅を維持できる。

RISC-Vの「Svvptc拡張」について調査する

RISC-Vの仕様書を読んで、Svvptc拡張について内容を読んでみる。

この拡張機能は、オペレーティングシステムのメモリ管理処理を大幅に簡略化する可能性を秘めているものである。

Svvptc 拡張の基本概念

Svvptcは、ページ・テーブル・エントリ(PTE)の無効状態から有効状態への変更を扱う際の振る舞いを最適化する。

• PTEのValidビットが0から1に変更された場合、その変更が明示的なメモリ管理命令なしで、一定時間内にHARTのアドレス変換キャッシュに自動的に反映されることを保証する。

従来のメモリ管理の課題

これまでのRISC-V実装では、OSがPTEを無効から有効に変更した後、その変更をHARTのアドレス変換キャッシュに反映させるために、以下のような処理が必要だった：

1. PTEを更新 (Invalid → Valid)
2. SFENCE.VMAやSINVAL.VMAなどのメモリ管理命令を実行
3. アドレス変換キャッシュの同期完了を待つ

これらの同期命令はかなりのオーバーヘッドをもたらし、特にコンテキスト・スイッチやメモリ・マッピング操作が頻繁に発生するワークロードでは、システム全体のパフォーマンスに影響を与えていた。

Svvptcによる最適化

Svvptc 拡張では、PTEのValidビットが0から1に変更されると、その変更は一定時間内に自動的にアドレス変換キャッシュに反映される。これにより：

• メモリ管理命令(SFENCE.VMA/SINVAL.VMA)の実行が省略可能になる
• システムコールやページフォールト処理の効率化が実現する
• メモリマッピング操作のレイテンシが削減される

想定される実装方法

Svvptc拡張をハードウェアとして実装するためのアプローチはいくつか考えられる：

• アドレス変換キャッシュそのものを持たない設計
• 無効なPTEをアドレス変換キャッシュに格納しない方式
• タイマーを使って定期的に無効なPTEを自動的に排除する機構
• PTEを更新するストア命令とアドレス変換キャッシュをコヒーレントにする設計

制限事項と注意点

重要なのは、Svvptcが対象とするのは「InvalidからValidへの変更」のみという点である。PTEに対する他の変更、特にValidからInvalidへの変更については、従来通りメモリ管理命令が必要になる。

パフォーマンスとトレードオフ

Svvptc拡張は、メモリ管理命令の省略によるパフォーマンス向上と、稀に発生する可能性のある追加のページフォールトのコストのトレードオフを最適化している。

• キャッシュの反映がタイムラグで遅れ、OSが意図していないページフォールトが一時的に起きる可能性はあるが、仕様上これは許容される。

仕様書でも明記されているように、「メモリ管理命令を省略することによるパフォーマンス上の利点は、時折発生する可能性のある無駄なページフォールトのコストを上回る」という判断に基づいている。

RISC-V「SVADU」拡張：PTE A/Dビットのハードウェア更新機能

SVADUというRISC-V拡張は、ページ・テーブル・エントリのAccessedビットとDirtyビットの管理を行うための命令拡張だ。 まずは、ページ・テーブル・エントリ(PTE)のA/Dビットについてまとめる。

Accessed（A）ビット

• ページが読み取り、書き込み、または実行されたかどうかを示す
• ページへの最初のアクセス時にハードウェアによって自動的に1に設定される
• ページ置換アルゴリズム（LRU等）での参照頻度の追跡

Dirty（D）ビット

• ページが書き込まれたかどうかを示す
• ページへの最初の書き込み時にハードウェアによって自動的に1に設定される
• ページアウト時の書き戻しの必要性判断

例えば、新たに作成されたページに対してデータをストアするとどうなるか。

• Accessedビット（A）：1にセットされる（ページがアクセスされたため）
• Dirtyビット（D）：1にセットされる（書き込みが発生したため）

このPTE.Dビットへの設定は、SVADU拡張が有効ではない場合は例外を発生させ、例外処理ルーチンによってソフトウェアが手動で設定する。

一方、SVADU拡張が実装されている場合、ハードウェアによるA/Dビット自動更新が可能になる。つまり、メモリアクセス時に、ハードウェアが自動的にPTEのA/Dビットを設定する。

SVADU拡張は、さらにいくつかのCSRレジスタを追加する。

menvcfg.ADUEフィールド

• Machine Environment Configurationレジスタ
• M-modeでのA/Dビットハードウェア更新の制御

henvcfg.ADUEフィールド

• Hypervisor Environment Configurationレジスタ
• HS-modeでのA/Dビットハードウェア更新の制御

ちなみに、このPTE.Dへの書き込みのテストを行っているのが riscv-tests の rv64si-p-dirty だ。

github.com

rv64si-p-dirty（dirty.S）がテストしている主な内容は以下の通りである。

1. Dirtyビットの初期状態の確認

   • ページ・テーブル・エントリ（PTE）のDirtyビット（D）がクリアされた状態でページにアクセスした場合、例外が発生することを確認している。

2. ストア命令によるDirtyビットの自動セット

   • Dirtyビットが0のページに対してストア命令（書き込み）を実行した際、ハードウェアまたはソフトウェアによってDirtyビットが1にセットされることを確認している。

3. 例外ハンドラによるDirtyビットのソフトウェア更新

   • ハードウェアで自動的にDirtyビットがセットされない場合、ストアアクセス例外が発生し、例外ハンドラがPTE.Dを1にセットしてリトライする処理が正しく動作するかを検証している。

4. Dirtyビットが1のときのストアアクセス

   • Dirtyビットが既に1になっているページに対してストア命令を実行しても、例外が発生せず正常に書き込みができることを確認している。

5. Aビット（Accessedビット）との連携動作

   • Dirtyビットのテストと同時に、Accessedビット（A）が正しくセットされるかも併せて確認している。

SymbiYosysを使ったBooth乗算器のフォーマル検証を試行する

より複雑なBooth乗算器に対して同様のフォーマル検証を試行してみる。

Booth乗算器は、符号付き数の乗算を効率的に実行するためのアルゴリズムであり、部分積の数を削減することで高速化を図る手法である。 このような複雑な設計に対してフォーマル検証がどこまで有効に機能するかを確認してみたい。

Booth乗算器の設計

module booth_mult
  (
   input         clk,
   input         reset,
   input         req_valid,
   input         req_in_1_signed,
   input         req_in_2_signed,
   input [31:0]  req_in_1,
   input [31:0]  req_in_2,
   output [63:0] resp_result
   );

フォーマル検証の設定

Booth乗算器の検証には、以下の設定ファイルを使用した：

[options]
mode bmc
depth 40

[engines]
smtbmc z3

[script]
read -sv -formal booth_mult.v
prep -top booth_mult

[files]
booth_mult.v

アサーションの定義

一発で32ビットの乗算器を検証することはどう考えてもできないので、ステップ・バイ・ステップで検証をできないか試してみる。

1. 下位の8ビットは検証できているものとする
2. 次の8ビットは、下位が検証できているものとして検証する

logic        [15: 0] x_u, y_u;
logic signed [15: 0] x_s, y_s;
logic signed [15: 0] model_result;

always_comb begin
  x_u = {8'b0, x[ 7: 0]};
  y_u = {8'b0, y[ 7: 0]};
  x_s = x_signed ? $signed({{8{x[7]}}, x}) : $signed(x_u);
  y_s = y_signed ? $signed({{8{y[7]}}, y}) : $signed(y_u);
  model_result = x_s * y_s;

  assume (resp_result[ 7: 0] == model_result[ 7: 0]);
  assert (resp_result[15: 8] == model_result[15: 8]);
end

検証の実行

検証を実行すると、以下のような状態になるのだが、まだ検証は完了していない。

SBY 16:23:49 [booth_mult_bmc] prep: finished (returncode=0)
SBY 16:23:49 [booth_mult_bmc] smt2: starting process "cd booth_mult_bmc/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 16:23:49 [booth_mult_bmc] engine_0: starting process "cd booth_mult_bmc; yosys-smtbmc -s z3 --presat --noprogress -t 40  --append 0 --dump-vcd engine_0/trace.vcd --dump-yw engine_0/trace.yw --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2"
SBY 16:23:49 [booth_mult_bmc] engine_0: ##   0:00:00  Solver: z3
SBY 16:23:49 [booth_mult_bmc] engine_0: ##   0:00:00  Checking assumptions in step 0..
SBY 16:24:49 [booth_mult_bmc] engine_0: ##   0:01:00  waiting for solver (1 minute)

EmacsのVerilog-Modeではstruct/interfaceが扱える

知らなかったのだが、EmacsのVerilog-Modeでは structやinterfaceが扱えるようだ。長年の悩みが解決される！

qiita.com

module auto_connect_struct
  (
   input logic i_clk,

   input  input_t in,
   output output_t out
   );

assign out.c = in.a + in.b;

endmodule // auto_connect_struct                                                                                                                                                                                                                                                                                                                                                          

module auto_connect_struct2
  (
   /*AUTOINPUT*/
   /*AUTOOUTPUT*/
   );

auto_connect_struct u_struct
  (/*AUTOINST*/);

endmodule // auto_connect_struct2                                                                                                                                                                                                                                                                                                                                                         

これをVerilog-Modeで自動的に接続してもうまくいかない。 このように、out / in の信号が外に出ていかない。

module auto_connect_struct2
  (
   /*AUTOINPUT*/
   // Beginning of automatic inputs (from unused autoinst inputs)                                                                                                                                                                                                                                                                                                                         
   input logic          i_clk                  // To u_struct of auto_connect_struct.v                                                                                                                                                                                                                                                                                                    
   // End of automatics                                                                                                                                                                                                                                                                                                                                                                   
   /*AUTOOUTPUT*/
   );

auto_connect_struct u_struct
  (/*AUTOINST*/
   // Interfaces                                                                                                                                                                                                                                                                                                                                                                          
   .in                                  (in),
   .out                                 (out),
   // Inputs                                                                                                                                                                                                                                                                                                                                                                              
   .i_clk                               (i_clk));

endmodule // auto_connect_struct2                                                                                                                                                                                                                                                                                                                                                         

これを解決するためには、 verilog-typedef-regexp を使って、どの型がstruct/unionであるかを定義してやる。

module auto_connect_struct2
  (
   /*AUTOINPUT*/
   // Beginning of automatic inputs (from unused autoinst inputs)                                                                                                                                                                                                                                                                                                                         
   input logic          i_clk,                  // To u_struct of auto_connect_struct.v                                                                                                                                                                                                                                                                                                   
   input input_t        in,                     // To u_struct of auto_connect_struct.v                                                                                                                                                                                                                                                                                                   
   // End of automatics                                                                                                                                                                                                                                                                                                                                                                   
   /*AUTOOUTPUT*/
   // Beginning of automatic outputs (from unused autoinst outputs)                                                                                                                                                                                                                                                                                                                       
   output output_t      out                    // From u_struct of auto_connect_struct.v                                                                                                                                                                                                                                                                                                  
   // End of automatics                                                                                                                                                                                                                                                                                                                                                                   
   );

auto_connect_struct u_struct
  (/*AUTOINST*/
   // Outputs                                                                                                                                                                                                                                                                                                                                                                             
   .out                                 (out),
   // Inputs                                                                                                                                                                                                                                                                                                                                                                              
   .i_clk                               (i_clk),
   .in                                  (in));

endmodule // auto_connect_struct2                                                                                                                                                                                                                                                                                                                                                         

// Local Variables:                                                                                                                                                                                                                                                                                                                                                                       
// verilog-typedef-regexp:"_t$"                                                                                                                                                                                                                                                                                                                                                           
// End:                                                                                                                                                                                                                                                                                                                                                                                   

このように、無事にin / out を structとして定義することで無事に入出力として接続できる。