Yosys と arachne-pnr は何をしているのか、中を覗いてみる

投稿者: | 2019/11/28

Looking into what Yosys and arachne-pnr are doing under the hood.

昨日、初めて Yosys と arachne-pnr で論理合成をしてみましたが、折角のフリーソフトですので、それらが裏で何をしているのか、もう少し探ってみたいと思います。特に、途中で生成している BLIF(Berkeley Logic Interchange Format )ファイルというのが気になりますよね。

非常に小さな回路を合成してみる

先日のサンプルコード(LED で SOS を送る)は、ややコードが大きめで、Yosys が出力する BLIF ファイルも若干大きめです。中を覗いてもチンプンカンプンでした。そこで、もっと小さなコードから試してみましょう。(私は FPGA も HDL も初心者ですので、変なコードは乞う御容赦。)

module test(
    input a,
    input b,
    output x
);
    assign x = a & b;
endmodule

こんな Verilog コードを用意してみました。(ただの 2入力論理積ゲートですね。) それでは、Yosys で synth_ice40 コマンドを使わずに、単純に -S オプションで論理合成してみましょう。yosys のヘルプによると

The option -S is an shortcut for calling the "synth" command, a default script for transforming the Verilog input to a gate-level netlist.

だそうです。実行してみます。

$ yosys -o test.blif -S test.v

test.blif を覗いてみます。

# Generated by Yosys 0.8 (Apio build) (git sha1 ebe5a35, clang 9.1.0 -fPIC -Os)

.model test
.inputs a b
.outputs x
.names $false
.names $true
1
.names $undef
.names b a x
11 1
.end

なんだか暗号のような出力ですが、意外とコンパクトです。内容を読解してみましょう。BLIF の構文に関しては、こちらが詳しいです。

上記ドキュメントは 11ページと短いので、気合いがあれば半日で理解できるでしょうが、私はずぼらなので、ペラペラとめくっただけで誤魔化します。ぱっと見た理解としては、BLIF というのは論理回路をテキスト形式で表現するためのもので、論理ゲート(.names)、ラッチ(.latch)といったコマンドがあるようです。さらにその接続も記述できるので、ネットリスト的な意味合いもあるようです。他のコマンドは、取りあえず無視します。

上記 test.blif では、次の部分が該当します。

.names b a x
11 1

意味ですが、b と a が入力、x が出力の論理ゲートを .names  コマンドで定義しており、「11 1」というのは、真理値表のようです。つまり、b と a が 1 と 1 のときに、x が 1 になりますよ、ということですね。

論理和ゲートも試してみます。(Verilog ソースは略)

.names b a x
1- 1
-1 1

今度出てきた「-」は、上述の構文書によると「not used」だそうです。つまり don't care ですね。つまり、b が 1 で a が don't care なら x は 1、また b が don't care で a が 1 なら x は 1、という意味です。

ここまでは簡単ですね。つまり Yosys は、デフォルト動作では、Verilog 記述の論理回路を、論理ゲートとラッチの組み合わせ、さらにそのネットリストに変換してくれるという訳です。

iCE40 FPGA 用に合成するとどうなるか

さて、上記で出力した BLIF ですが、これを arachne-pnr で合成することはできるのでしょうか。私もよく分かっていないのですが、とりあえずやってみます。

test.blif:10: fatal error: invalid .names directive: expected 1 or 2 arguments, got 3

だめでした。単純に BLIF に変換した結果を、arachne-pnr は placing できないようです。そこで、当初の Yosys の使い方のように、synth_ice40 を使って BLIF を生成し直してみます。論理和のほうを示します。

.gate SB_LUT4 I0=a I1=b I2=$false I3=$false O=x
.attr src "/Users/yokoyama/.apio/packages/toolchain-icestorm/bin/../share/yosys/ice40/cells_map.v:44"
.param LUT_INIT 1110

なんか新しいコマンド .gate とか .attr とか .param を使っています。これは上記の構文書には掲載がなくて、こちらのサイトに説明がありました。どうも、Extended BLIF という拡張フォーマットのようですね。Yosys のマニュアルを読み込まないと分からない点が多いのですが、どうも SB_LUT4 というライブラリを使うようになっていて、そのライブラリが .attr src 後続のファイルで定義されているようです。つまり arachne-pnr には対して、「iCE40 FPGA が持っている LUT4 を使うんだよ。その LUT の真理値表は 1110 だよ」と伝えているようです。

こちらを読んでもう少し調べたところ、Yosys が持っている techmap(technology mapper)という機能を使い、ある構文(論理?)を、(Verilog で書かれている)ライブラリで定義したデバイス特有の機能(LUT や block RAM)などに置き換えるということをしているようです。ちょっとこの辺まで来ると重箱つつきで、しばくらは詳細に踏み込まないようにしたいと思います。

後で arachne-pnr を実行すると、その記述を読み取り、最適な場所にある logic cell に上記 LUT を配置し、結線をしてくれる、ということのようです。(本当に理解しようとしたら、Yosys のマニュアルを読まないとダメですね。私はハッカーにはなれそうもないです。)

ところで、上記 Verilog の回路を論理積に戻してから合成し直すと、以下のような出力になります。

.param LUT_INIT 1000

いずれにしても、真理値表には 4ビットの情報しかないですね。LUT4 は 4ビットのメモリと等価のはずですので、16行(?)の真理値表が必要のはずですが、上記では 4行しかありません。これはおそらく、2入力のゲートでは 2ビットのメモリと等価なので、4行(2 の二乗)の真理値表があれば十分、ということなのでしょう。

まず最初に、x = a & b の真理値表を考えてみましょう。

a b x
0 0 0
0 1 0
1 0 0
1 1 1

なるほど、という感じですね。次に x = a | b です。

a b x
0 0 0
0 1 1
1 0 1
1 1 1

パラメタの順番はともあれ、2入力の論理回路を 2入力の LUT にマップしているということは分かりました。試しに 4入力の論理回路を合成してみましょう。

assign x = (a & b | c) ^ d;

あまり面白くありませんが、iCE40 用に合成すると、

.gate SB_LUT4 I0=a I1=b I2=c I3=d O=x
.attr src "/Users/yokoyama/.apio/packages/toolchain-icestorm/bin/../share/yosys/ice40/cells_map.v:52"
.param LUT_INIT 0000011111111000

となりました。真理値表がちゃんと 16行になってますね。

さらに実験として 5入力にしてみましょう。

assign x = (a & b | c) ^ (d & e);

iCE40 には LUT4 しかありませんので、

.gate SB_LUT4 I0=d I1=e I2=$abc$72$n9 I3=$false O=x
.attr src "/Users/yokoyama/.apio/packages/toolchain-icestorm/bin/../share/yosys/ice40/cells_map.v:48"
.param LUT_INIT 10000111
.gate SB_LUT4 I0=b I1=a I2=c I3=$false O=$abc$72$n9
.attr src "/Users/yokoyama/.apio/packages/toolchain-icestorm/bin/../share/yosys/ice40/cells_map.v:48"
.param LUT_INIT 00000111

はい。2つの LUT4 に分割されて実装されました。

D-FF を入れてみよう

組み合わせ回路はだいたい雰囲気が分かったので、次に stateful な回路を実装してみましょう。シンプルさ重視でこんなのです。(バカにされそう。)

module test(
    input a,
    input clk,
    output x
);
    always @(posedge clk)
        x <= a;
endmodule

まずは、-S オプションで合成したバージョンです。

.names $undef
.latch a x re clk 2

前述の BLIF 構文書を見ると、これはラッチ回路として実装され、入力が a、出力が x、re は resing edge の意味で、クロック入力が clk です。最後の 2 というのは何でしょう?  これはラッチ回路の初期値(内部状態)だそうですが、2とは!?  実は、2 というのは don't care だそうです。つまり、未定義ですね。

synth_ice40 したバージョンはどうでしょうか。

.gate SB_DFF C=clk D=a Q=x
.attr src "test.v:7|/Users/yokoyama/.apio/packages/toolchain-icestorm/bin/../share/yosys/ice40/cells_map.v:2"

いとも簡単に、logic cell の D-FF にマップされてしまいました。ところで、この SB_DFF というのは register primitive というものだそうで、後述の SiliconBlue ICE™ Technology Library に出てきます。

最後にもう少し複雑(?)な回路です。先ほどの D-FF に非同期リセットを入れてみました。(これでいいのかな?)

module test(
    input a,
    input async_rst,
    input clk,
    output x
);
    always @(posedge clk, posedge async_rst)
    begin
        if (async_rst)
            x <= 0;
        else
            x <= a;
    end
endmodule

今回は、sync_ice40 の結果だけにしておきましょう。

.gate SB_DFFR C=clk D=a Q=x R=async_rst
.attr src "test.v:8|/Users/yokoyama/.apio/packages/toolchain-icestorm/bin/../share/yosys/ice40/cells_map.v:17"

iCE40 の logic cell で実現される register primitive SB_DFFR には、非同期リセット入力があるようです。

ちなみに調子づいて、非同期 set/reset 付きの D-FF を合成したところ、

.gate $_DFFSR_PPP_ C=clk D=$true Q=x R=$abc$84$n6 S=$abc$84$n3
.attr src "test.v:9"

という出力が出てきました。これを arachne-pnr にかけたところ、見事(?)に

fatal error: unknown model `$_DFFSR_PPP_'

というエラーになりました。Clifford Wolf さんに依ると(ここの議論)、「大抵の FPGA は SR-FF をサポートしてないから無理だよん」ということでした。ちなみに iCE40 の logic cell はどのような設計になっているのでしょう。内部実装までは見つかりませんでしたが、以下のような資料を見つけました。

非同期 set と 非同期 reset はできるようですが、両方同時は無理、ということでした。面白いですね。

余談ですが、SiliconBlue というのは iCE40 FPGA を開発した会社の名前です。2011 年に Lattice に買収されたそうです。

今日はここまでにしましょう。なんだか知恵熱が出そうです。 🙂