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 に買収されたそうです。
今日はここまでにしましょう。なんだか知恵熱が出そうです。 🙂