Haskell
Verilog
HDL
adventcalendar2017

依存型の紹介と応用としてのClashの紹介

目的

19番目の Advent Calender 2017 Haskell(その2)です。

依存型とは何か、何に役に立つのか、その応用としてのClashと
Clashを用いた論理回路の実装のトライアルの紹介をします。

依存型とは何か

Wikipediaの依存型リンク先に他の型の値に依存する型が依存型とあります。例えば、Boolの値はTrue,Falseがありますが、Boolが型なのはもちろんですが、TrueやFalseも型として扱えるようになります。

その代表的なものとして、リストの要素数を埋め込んだ型があります。例えば、普通のBoolのリストは[Bool]な感じで長さに決まりはないですが、Vector 5 Boolのように長さ5のBool型のリストが作れます。(vector-sizedパッケージで実際に作れます。)

型に値を埋め込むだけだとありがたみがないですが、カリー=ハワード同型対応で「プログラム=証明」(proofs-as-programs)・「型=命題」(formulae-as-types)といわれているので、証明をやるにはリッチな型が必要なのです。

依存型が何に役に立つのか

依存型の応用には以下のものがあります。他にもあると思いますが。

Clashとは、その近況

clashはhaskellで書けるハードウェア記述言語です。

ハードウェアの記述の階層は3つあります。

  1. ゲートレベル
    • スタンダードセルやFPGAの素子レベル
  2. レジスタトランスファーレベル(RTL)
    • クロックによるサイクル単位の設計
    • 記憶素子のレジスタと状態のない論理回路の世界
    • レジスタは設計者が明示する
    • 論理圧縮は論理合成ツールの仕事で合成ツールはRTLをゲートレベルに変換する。
    • Clashはこのレベル。
  3. 高位合成
    • レジスタは設計者が明示しない
    • コンパイラによって勝手にステートマシンができる
    • サイクルの指定がないとコンパイラが適当に設定する
    • c言語から回路を生成とかはこのレベル

ClashはRTLを記述し、verilog,VHDLなどの他のRTLを出力します。ghc-apiを使ってhaskellのコードをパースしてRTLに変換しているのでghc拡張が使えます。

単にRTLを記述するだけでなく、依存型を用いて、
8bitのビット列はBitVector 8
8bitのビット列を8つ束ねたものをVec 8 (BitVector 8)
と書けます。

副作用のない組み合わせ回路は下記のように書けます。

adder' :: BitVector 8 -> BitVector 8 -> BitVector 8
adder' a b = a + b

Systemクロックに同期する信号はSignal System (BitVector 8)
とし、下記のように書くとaとbを足したあとレジスタにいれる回路になります。

adder :: Signal System (BitVector 8) -> Signal System (BitVector 8) -> Signal System (BitVector 8)
adder a b = register 0 $ a + b

副作用ない組み合わせ回路をつかって、mealyマシンでステートを持つ回路が記述できます。
ただ、mealyマシンだとレジスタを内部のstateに割り当てるだけなので、回路の出力にレジスタを置きたいときには使いづらいです。

adder' :: (BitVector 8,BitVector 8) -> BitVector 8
adder' (a,b) = a + b

madder :: Signal System ((BitVector 8),(BitVector 8)) -> Signal System (BitVector 8)
madder = mealy (\state input -> ((adder' input),state))) 0

クロックを明示するスタイルと明示しないスタイル(Systemクロックが自動で使われる)が使い分けられ、haskellを使っているのでmapなどの高階関数が使えます。

Clashはそろそろghc 8.2に対応した1.0がリリースされます。
新しいバージョンでクロックだけでなく、リセット信号も型で明示できるようになります。
今hackageに挙がっているものとだいぶ記述の仕方が変わっているので、下記のようにしてgitのものを使いましょう。

> git clone git@github.com:clash-lang/clash-compiler.git
> cd clash-compiler
> git submodule init
> git submodule update
> stack install

I2C Slaveとステッピングモーターコントローラの実装

今回I2C SlaveになるステッピングモーターコントローラをClashで書いてみました。I2Cはチップ間のバスです。また、ステッピングモーターはプリンタに使われている位置決めが容易なモーターです。

ターゲットのデバイスはAlteraのCycloneII EP2C5T144のFPGAです。

今回の回路はモーター18個に対応しています。

こちらにhaskellのコードとそれから生成したverilogのファイルを置きました。テスト不足でまだ動かないですが、生成されたverilogの記述をみると人間がよめる形式(registerと組み合わせ回路が明示されていて)になっていて素晴らしいです。

合成結果

Quartus II 12.1で合成しました。(最新のものだとなぜかFPGAに書き込めなかったので古いものを使いました。)

結果は下記です。大変小さいデバイスですが、ロジックの利用率は8%で無駄なものはできてなさそうです。今回はピンネックでこれ以上のステッピングモーターコントローラーは詰め込めなさそうです。

Flow Status Successful - Tue Dec 19 19:23:39 2017
Quartus II 64-Bit Version   12.1 Build 177 11/07/2012 SJ Web Edition
Revision Name   stepper
Top-level Entity Name   Top_topEntity
Family  Cyclone II
Device  EP2C5T144C6
Timing Models   Final
Total logic elements    391 / 4,608 ( 8 % )
Total combinational functions   304 / 4,608 ( 7 % )
Dedicated logic registers   251 / 4,608 ( 5 % )
Total registers 251
Total pins  77 / 89 ( 87 % )
Total virtual pins  0
Total memory bits   0 / 119,808 ( 0 % )
Embedded Multiplier 9-bit elements  0 / 26 ( 0 % )
Total PLLs  0 / 2 ( 0 % )

まとめと今後

Haskellの依存型を用いたハードウェア記述言語のClashを紹介し、それを利用してI2C Slaveとステッピングモーターコントローラーを実装しました。依存型もClashも十分実用レベルになっていることが確認できました。

次回はちゃんとステッピングモーターが動いている動画を用意したいです。