Coqをベースとしたハードウェア表現および生成プラットフォーム"Kami"を試す

MITのプログラム言語を研究しているグループの検証プラットフォーム「Kami」の論文を読んでいる。

KamiとはCoqをベースとしたDSLで、ハードウェアを表現するための言語およびそのプラットフォーム。KamiはCoqのハードウェア記述から検証、ハードウェア生成までを行うことを目的とする。

論文は以下に掲載されている。30ページもあり長い。

• Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification
  • http://plv.csail.mit.edu/kami/papers/icfp17.pdf

とりあえず動かしてみる。以下のリポジトリを使おう。

github.com

# Revision : ed1d6cd
$ git clone git@github.com:sifive/Kami.git

ツールチェインを用意する。まずはCoqの最新バージョンをインストールしよう。KamiはCoqの比較的最新バージョンが必要となる。

$ cd /tmp
$ curl -L https://github.com/coq/coq/archive/V8.11.0.tar.gz | tar xz
$ cd coq-8.11.0
$ ./configure
$ make -j$(nproc)
$ sudo make install

$ coqtop --version

The Coq Proof Assistant, version 8.11.0 (February 2020)
compiled on Feb 7 2020 2:49:57 with OCaml 4.05.0

次にライブラリをインストールする。以下のCoqの追加ライブラリが必要だ。

$ git clone git@github.com:mit-plv/bbv.git
$ cd bbv
$ make

$ git clone git@github.com:tchajed/coq-record-update.git
$ cd coq-record-update
$ make

最終的に以下のようなディレクトリ構造になっていればOK。

.
|-- Kami
|-- bbv
`-- coq-record-update

さて、とりあえずMakeを実行してみよう。

$ make -j8

coq_makefile -f _CoqProject ./All.v ./AllDefn.v ./AllNotations.v ./Compiler/Compiler.v ./Compiler/CompilerDoubleWrites.v ./Compiler/CompilerProps.v ./Compiler/CompilerSimple.v ./Compiler/CompilerSimpleProps.v ./Compiler/CompilerSimpleSem.v ./Compiler/Rtl.v ./Compiler/Test.v ./Compiler/UnverifiedIncompleteCompiler.v ./Extraction.v ./Guard.v ./Lib/EclecticLib.v ./Lib/Fold.v ./Lib/HexNotation.v ./Lib/HexNotationWord.v ./Lib/VectorFacts.v ./Lib/Word.v ./Lib/WordProperties.v ./LibStruct.v ./Notations.v ./NotationsTest.v ./Notations_rewrites.v ./PPlusProperties.v ./PProperties.v ./Properties.v ./Simulator/CoqSim/Eval.v ./Simulator/CoqSim/HaskellTypes.v ./Simulator/CoqSim/Misc.v ./Simulator/CoqSim/RegisterFile.v ./Simulator/CoqSim/SimTypes.v ./Simulator/CoqSim/Simulator.v ./Simulator/CoqSim/TransparentProofs.v ./Simulator/NativeTest.v ./StateMonad.v ./Syntax.v ./SyntaxDoubleWrites.v ./Tactics.v ./Tutorial/ExtractEx.v ./Tutorial/GallinaActionEx.v ./Tutorial/PhoasEx.v ./Tutorial/SyntaxEx.v ./Tutorial/TacticsEx.v ./Utila.v ./WfMod_Helper.v -o Makefile.coq.all
Warning: no common logical root
Warning: in such case INSTALLDEFAULTROOT must be defined
Warning: the install-doc target is going to install files
Warning: in orphan_Kami_bbv_RecordUpdate
make -f Makefile.coq.all
make[1]: Entering directory '/home/msyksphinz/work/riscv/kami/Kami'
COQDEP VFILES
COQC Lib/Fold.v
COQC Lib/EclecticLib.v
COQC Lib/VectorFacts.v
COQC StateMonad.v
COQC Lib/HexNotation.v
COQC Lib/Word.v
COQC Tutorial/PhoasEx.v
...
implEq cannot be defined because the projections counterImpl, isSending were
not defined. [cannot-define-projection,records]
File "./Tutorial/TacticsEx.v", line 46, characters 2-641:
Warning:
specEq cannot be defined because the projections isSending, counterImpl,
counterImpl were not defined. [cannot-define-projection,records]
COQC Tutorial/ExtractEx.v
COQC Tutorial/GallinaActionEx.v
COQC Tutorial/PhoasEx.v
     = "let xO := (true || false) in let xSO := true in (xO && xSO)"
     : string
COQC Tutorial/SyntaxEx.v
COQC WfMod_Helper.v

とりあえずエラー無くコンパイルが完了した。内部を解析していこう。