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:
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
GitHub - sifive/Kami: Kami - a DSL for designing Hardware in Coq, and the associated semantics and theorems for proving its correctness. Kami is inspired by Bluespec. It is actually a complete rewrite of an older version from MIT
