Lava メモ

Haskell ベースで内部 DSL として実装された HDL である Lava に関するメモです。

バージョン等は 2011 年 11 月現在

Lava とは

Lava はハードウェア記述言語で、Haskell ベースの内部 DSL として実装されています。Chalmers (ちゃーまーず、ないし、しゃるめる、などと日本では読んでいるようです) 大学 (関数型言語の研究が盛んで HBC と HBI という Haskell 処理系などを作ったりしています) 版が本家? らしく、他に機能の追加と削除などがされている派生版がいくつかあります。

Lava のバリエーション

Chalmers -- chalmers-lava2000 という Hackage があるのでそれを使えばよいでしょう
Xilinx -- xilinx-lava / FoP の Lava の章の執筆者のひとりである Satnam Singh さんの Lava のページ ( http://raintown.org/lava/ ) で紹介しているのはこちらのバージョンのようですが、微妙に現在のバージョンに追いついていないようなので本稿で解説（の予定）。
York -- york-lava
Kansas -- kansas-lava
- Kansas Lava で xor2 を使って、このページで紹介している方法で VHDL を生成する方は、バグがありますのでソースを修正して上書きインストールしてから VHDL を生成してください。バグの詳細とパッチは https://github.com/ku-fpg/kansas-lava/issues/2 にあります

Hackage にあるものとしては、以上のようになります。他に Wired という Hackage の一部に含まれているものがあります。

FoP

とりあえずのイントロダクションとしては、FoP こと『関数プログラミングの楽しみ』の 8 章をやってみるとよいでしょう。定理証明器についてなど、まずは最新の情報をサポートサイト（ http://fop.sampou.org/chap08.html ）で確認することから始めるのがよいと思います。

本文中での解説に使われているのは Chalmers 版から Xilinx 版への途中頃のバージョンのもののようです。訳注などに従い、Chalmers 版を使って試してみるのがよいでしょう。サポートサイトや訳注に書かれている通りやれば、どれも実行して確認できました。

ライブラリの衝突

前述の Lava を複数 cabal でインストールしてあると import Lava でどれを選べばよいかわからないということでエラーになります（ Language.KansasLava という名前になっている Kansas Lava を除く）。Haskell 処理系に毎回オプションを指定しても良いでしょうが、ghc-pkg hide chalmers-lava2000 などのようにして使わないほうを見えなくしてしまうのが便利でしょう。

というか 3 つもあると面倒なので以下のようなスクリプトを作りました。

#!/bin/sh

ghc-pkg hide chalmers-lava2000
ghc-pkg hide xilinx-lava
ghc-pkg hide york-lava

case $1 in
-c )
	LAVA=chalmers-lava2000
	;;
-x )
	LAVA=xilinx-lava
	;;
-y )
	LAVA=york-lava
	;;
* )
	echo 'usage select_lava.sh (-c|-x|-y)'
	exit 1
	;;
esac

ghc-pkg expose $LAVA

各 Lava の違い

Chalmers 大のサイトのこちら → http://www.cse.chalmers.se/edu/course/TDA956/Slides/ にある Lava111.pdf （授業の最初の時間用のプレゼン資料のようです）の 8 ページ目に、各 Lava についての概観があります（この授業を取ると Bluespec の人をゲストに呼んで講義、とかあるのですねぇ）

ソースコードのファイル構成と行数を見ると以下のようになっています。

$ wc -l chalmers-lava2000-1.1.2/Lava/*.hs
      66 chalmers-lava2000-1.1.2/Lava/Arithmetic.hs
     151 chalmers-lava2000-1.1.2/Lava/Captain.hs
      39 chalmers-lava2000-1.1.2/Lava/Combinational.hs
     113 chalmers-lava2000-1.1.2/Lava/ConstructiveAnalysis.hs
     154 chalmers-lava2000-1.1.2/Lava/Eprover.hs
      47 chalmers-lava2000-1.1.2/Lava/Error.hs
     133 chalmers-lava2000-1.1.2/Lava/Fixit.hs
     420 chalmers-lava2000-1.1.2/Lava/Generic.hs
     144 chalmers-lava2000-1.1.2/Lava/HeerHugo.hs
      10 chalmers-lava2000-1.1.2/Lava/IOBuffering.hs
     173 chalmers-lava2000-1.1.2/Lava/Isc.hs
       7 chalmers-lava2000-1.1.2/Lava/LavaDir.hs
      18 chalmers-lava2000-1.1.2/Lava/LavaRandom.hs
     150 chalmers-lava2000-1.1.2/Lava/Limmat.hs
     150 chalmers-lava2000-1.1.2/Lava/Modoc.hs
      62 chalmers-lava2000-1.1.2/Lava/MyST.hs
      60 chalmers-lava2000-1.1.2/Lava/Netlist.hs
      96 chalmers-lava2000-1.1.2/Lava/Operators.hs
      96 chalmers-lava2000-1.1.2/Lava/Patterns.hs
     399 chalmers-lava2000-1.1.2/Lava/Property.hs
     181 chalmers-lava2000-1.1.2/Lava/Ref.hs
      59 chalmers-lava2000-1.1.2/Lava/Retime.hs
     150 chalmers-lava2000-1.1.2/Lava/Satnik.hs
     150 chalmers-lava2000-1.1.2/Lava/Satzoo.hs
      18 chalmers-lava2000-1.1.2/Lava/Sequent.hs
     137 chalmers-lava2000-1.1.2/Lava/Sequential.hs
      68 chalmers-lava2000-1.1.2/Lava/SequentialCircuits.hs
     173 chalmers-lava2000-1.1.2/Lava/SequentialConstructive.hs
     350 chalmers-lava2000-1.1.2/Lava/Signal.hs
      15 chalmers-lava2000-1.1.2/Lava/SignalTry.hs
     155 chalmers-lava2000-1.1.2/Lava/Smv.hs
      60 chalmers-lava2000-1.1.2/Lava/Stable.hs
      72 chalmers-lava2000-1.1.2/Lava/Table.hs
      23 chalmers-lava2000-1.1.2/Lava/Test.hs
     475 chalmers-lava2000-1.1.2/Lava/Verification.hs
     199 chalmers-lava2000-1.1.2/Lava/Vhdl.hs
     265 chalmers-lava2000-1.1.2/Lava/Vis.hs
     150 chalmers-lava2000-1.1.2/Lava/Zchaff.hs
    5188 total

$ wc -l kansas-lava-0.2.4/Language/KansasLava/*.hs kansas-lava-0.2.4/Language/KansasLava/*/*.hs
     101 kansas-lava-0.2.4/Language/KansasLava/DOT.hs
      28 kansas-lava-0.2.4/Language/KansasLava/Dynamic.hs
      61 kansas-lava-0.2.4/Language/KansasLava/Entity.hs
     412 kansas-lava-0.2.4/Language/KansasLava/Fabric.hs
      65 kansas-lava-0.2.4/Language/KansasLava/Internal.hs
     255 kansas-lava-0.2.4/Language/KansasLava/Optimization.hs
      96 kansas-lava-0.2.4/Language/KansasLava/Probes.hs
      16 kansas-lava-0.2.4/Language/KansasLava/Protocols.hs
     188 kansas-lava-0.2.4/Language/KansasLava/RTL.hs
     343 kansas-lava-0.2.4/Language/KansasLava/Rep.hs
     443 kansas-lava-0.2.4/Language/KansasLava/Signal.hs
      79 kansas-lava-0.2.4/Language/KansasLava/Stream.hs
     836 kansas-lava-0.2.4/Language/KansasLava/Test.hs
     694 kansas-lava-0.2.4/Language/KansasLava/Types.hs
     435 kansas-lava-0.2.4/Language/KansasLava/Utils.hs
     324 kansas-lava-0.2.4/Language/KansasLava/VCD.hs
     323 kansas-lava-0.2.4/Language/KansasLava/VHDL.hs
      75 kansas-lava-0.2.4/Language/KansasLava/Netlist/Decl.hs
     930 kansas-lava-0.2.4/Language/KansasLava/Netlist/Inst.hs
     392 kansas-lava-0.2.4/Language/KansasLava/Netlist/Utils.hs
     203 kansas-lava-0.2.4/Language/KansasLava/Protocols/AckBox.hs
      68 kansas-lava-0.2.4/Language/KansasLava/Protocols/Enabled.hs
     153 kansas-lava-0.2.4/Language/KansasLava/Protocols/Memory.hs
     824 kansas-lava-0.2.4/Language/KansasLava/Protocols/Patch.hs
     155 kansas-lava-0.2.4/Language/KansasLava/Protocols/ReadyBox.hs
      82 kansas-lava-0.2.4/Language/KansasLava/Protocols/Types.hs
     176 kansas-lava-0.2.4/Language/KansasLava/Rep/Class.hs
     128 kansas-lava-0.2.4/Language/KansasLava/Rep/TH.hs
     154 kansas-lava-0.2.4/Language/KansasLava/VCD/EventList.hs
    8039 total

$ wc -l xilinx-lava-5.0.1.5/Lava/*.hs
      24 xilinx-lava-5.0.1.5/Lava/Adder.hs
     102 xilinx-lava-5.0.1.5/Lava/ApplyLayout.hs
     415 xilinx-lava-5.0.1.5/Lava/CircuitGraphToVHDL.hs
      60 xilinx-lava-5.0.1.5/Lava/Col.hs
     414 xilinx-lava-5.0.1.5/Lava/Combinators.hs
      18 xilinx-lava-5.0.1.5/Lava/Comparator.hs
      21 xilinx-lava-5.0.1.5/Lava/Components.hs
      80 xilinx-lava-5.0.1.5/Lava/ComputeNetDrivers.hs
      50 xilinx-lava-5.0.1.5/Lava/ComputeNetlist.hs
       9 xilinx-lava-5.0.1.5/Lava/Diagnostics.hs
     594 xilinx-lava-5.0.1.5/Lava/Gates.hs
     171 xilinx-lava-5.0.1.5/Lava/ISE.hs
      60 xilinx-lava-5.0.1.5/Lava/Instantiate.hs
     274 xilinx-lava-5.0.1.5/Lava/LUTGates.hs
      21 xilinx-lava-5.0.1.5/Lava/Middle.hs
     234 xilinx-lava-5.0.1.5/Lava/Netlist.hs
     370 xilinx-lava-5.0.1.5/Lava/NetlistToEDIF.hs
      20 xilinx-lava-5.0.1.5/Lava/OneBitAdder.hs
      20 xilinx-lava-5.0.1.5/Lava/OneBitSubtractor.hs
      39 xilinx-lava-5.0.1.5/Lava/OverlayTile.hs
      21 xilinx-lava-5.0.1.5/Lava/PortRange.hs
     151 xilinx-lava-5.0.1.5/Lava/Ports.hs
      46 xilinx-lava-5.0.1.5/Lava/PrimitiveGates.hs
      34 xilinx-lava-5.0.1.5/Lava/RPM.hs
      24 xilinx-lava-5.0.1.5/Lava/Subtractor.hs
     301 xilinx-lava-5.0.1.5/Lava/Utils.hs
      19 xilinx-lava-5.0.1.5/Lava/Version.hs
      10 xilinx-lava-5.0.1.5/Lava/Virtex2.hs
      10 xilinx-lava-5.0.1.5/Lava/Virtex4.hs
      10 xilinx-lava-5.0.1.5/Lava/Virtex5.hs
      10 xilinx-lava-5.0.1.5/Lava/Virtex6.hs
    3632 total

$ wc -l york-lava-0.2/modules/Lava/*.hs
      59 york-lava-0.2/modules/Lava/Binary.hs
     596 york-lava-0.2/modules/Lava/Bit.hs
      68 york-lava-0.2/modules/Lava/JList.hs
     419 york-lava-0.2/modules/Lava/Prelude.hs
    1374 york-lava-0.2/modules/Lava/Vector.hs
     383 york-lava-0.2/modules/Lava/Vhdl.hs
    2899 total

FoP の内容をそれぞれの Lava で

Xilinx Lava で

FoP の内容を Xilinx Lava でやってみました。が、現在の Xilinx Lava は FPGA で (というより Xilinx の Virtex ファミリで) 高品質なマニュアル指定によるフロアプランを高水準かつ効率的におこなうことに特化しているようで、かなりの内容を飛ばしてあります。

Xilinx Lava 版の各コードは sect-8.lhs です（出力の型の Out が大きな変更点）。

一番最後の VHDL を生成するプログラムは別にしてあります。Main.lhs です。runghc Main で実行すればよいでしょう（ lavac コマンドは無くなっているようですが、Haskell Platform に cabal でインストールしていれば、特に問題なく runghc で実行できます）。生成される nandgate.vhd を見てみると、先頭にヘッダコメントとパッケージ宣言が付いていますが、その後は本文中の図8.12 とほぼ同様のリストが生成されています（FPGA のセル配置に関する情報の記法がちょっと変わっている）。

York Lava で

York Lava でもやってみました。ソースコードの規模は圧倒的に小さいようですが、Xilinx Lava と違いシミュレーションもできますし、順序回路を作るためのプリミティブである delay もあります（ == delay を作るための Generic がある）。

FoP 本文中のリストはほとんどそのまま変更なしで動くので、ファイルは上げません。主要な変更点などのポイントについて以下に書きます。

simulate のインタフェースは Chalmers とは違っています（simulateSeq は同じ）。

halfAdd のような組み合わせ論理回路のシミュレートは simulateN (型は simulateN :: Generic a => Int -> a -> [a] ) を simulateN 1 $ halfAdd (in0, in1) のようにして使います。出力結果の入った、中身がひとつだけのリストが得られます。

ghci での実行例を以下に示します。

$ ghci
GHCi, version 7.0.3: http://www.haskell.org/ghc/  :? for help
Loading ...(略)
Prelude> :l sect-8.lhs
[1 of 1] Compiling Main             ( sect-8.lhs, interpreted )
Ok, modules loaded: Main.
*Main> simulateN 1 $ halfAdd (low, low)
Loading ...(略)
[(low,low)]
*Main> simulateN 1 $ halfAdd (low, high)
[(high,low)]
*Main> simulateN 1 $ halfAdd (high, low)
[(high,low)]
*Main> simulateN 1 $ halfAdd (high, high)
[(low,high)]

また、simulate を使わなくても、関数に直接入力を与えると、出てくる出力が Chalmers Lava では可読性の低いものでしたが、York Lava では普通に見られる出力が出てきます。

Chalmers Lava

*Main> halfAdd (low, low)
(xorl[low,low],andl[low,low])

====

York Lava

*Main> halfAdd (low, low)
(low,low)

§8.5 verify ないし同様のものはないようです。

<==> 演算子はありませんが、代わりに 1 ビット 2 個の比較をおこなって 1 ビットを返す（意味的には inv . xor である）演算子 <=> と、Chalmers Lava の <==> と（ほぼ?）同じ意味の === 演算子があります。

§8.6 順序回路のシミュレーション方法は FoP 本文中のものと全く同じです。

*Main> simulateSeq edge [high, low, low, high]
[high,low,low,low]

（組み合わせ回路の時には式中にあった $ がこちらにはないことに注意）

counter で使っている zeroList は York Lava にはないので low の列を明示的に作ってやる必要があります。

> counter :: Int -> () -> [Bit]
> counter n () = number
>   where
>     number          = delay (replicate n low) number'
>     (number', cout) = bitAdder (high, number)

§8.7 8.8 TODO

§8.9

練習問題 8.24 8.25 については、York Lava の makeComponent のデモも兼ねて、というのとちょっと冗長なので別ファイルとします。こちら → sect-8_9.lhs

VHDL 生成については Main.lhs を参照してください。

Kansas Lava で

VHDL 生成以外についてのソースコードは sect-8.lhs です。

VHDL 生成については Main.lhs です。

Bit ではなく Bit i という型引数の付いた型を使う点以外は、ほとんど本文と同じです。simulate はありませんが直接値を与えて、組み合わせ論理回路はシミュレートできます。詳細はコメントを見てください。

VHDL 生成は他の Lava の例と同じように runghc Main で実行すると nandgate.vhd という VHDL ファイルが生成されます。

Xilinx Lava (書きかけ)

最新の Haskell Platform ではビルド中に haskell98 ライブラリでエラーになります。cabal unpack xilinx-lava として展開し、以下のパッチ xilinx-lava_patch.txt を当ててから cabal install してください。

チュートリアル（ http://raintown.org/lava/tutorials/index.htm ）の第 1 節の 5 ページにあるリストをバージョン 5.0.1.5 に対応させたものを置いておきます。

Tutrial1.lhs

変更点などについてのコメントは lhs にしてソースコード中に書いてあります。これをたとえば runghc で実行すると次のようになります。

$ runghc Tutrial1.lhs
Generating tutrial1.vhd ... [done]
Generating tutrial1.edif ... [done]
Generating tutrial1_package.vhd ... [done]

長くなるのでコメントでは割愛しましたが Out の詳細は以下のようなものになっています。（フリップフロップのようなたすきがけ回路を直接配線で記述してもうまく扱うため（たとえば PARTHENON ではループしてスタックが溢れます）の変更か何かなのでしょうか？）

$ ghci
GHCi, version 7.0.3: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Loading package ffi-1.0 ... linking ... done.
Prelude> :m Lava
Prelude Lava> :i Out
type Out a = Control.Monad.Trans.State.Lazy.State Netlist a
        -- Defined in xilinx-lava-5.0.1.5:Lava.Netlist

チップの選択

Xilinx Lava で、import して使うための Lava.Virtex2 等のモジュールがありますが、それらは中身を見るとわかりますが、単に Lava.Gates というパッケージを import するためのラッパーで、どれも同じものです（ Lava.Gates モジュールを直接 import しようとすると hidden module であるために import できません）。

Lava.Virtex2 等を import して Lava.Gates が import されると、FPGA のプリミティブを利用して定義されている and2 などが使えるようになります。

元々の設計では、恐らく import するモジュールを差し替えて、合成対象のチップを替えていたのだと思われます。

Xilinx Lava 5.0.1.5 では、computeNetlist の第 2 引数に与える値によって、合成対象を切り替えるようになっているようです。XilinxArchitecture という型です。そして、その値による実際の処理の振り分けは RPM.hs というソースファイルの中にあります。見ればわかりますがそんなにややこしいことはしていません。実験してみたところ、Spartan-3E 用には Virtex4 か Virtex5 を流用して合成できました。

York Lava (書きかけ)

Reduceron プロジェクトのメモ。チュートリアル → http://www.cs.york.ac.uk/fp/reduceron/memos/Memo23.txt