Coqをベースとしたハードウェア表現および生成プラットフォーム"Kami"を試す - FPGA開発日記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:
