Edited at

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

More than 1 year has passed since last update.


目的

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も十分実用レベルになっていることが確認できました。

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