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
Reflection is ready to be merged into master. There already is a Notations_rewrites.v file in the Kami directory. I merged in the changes from the ProcessorCoreWellFormed_part5 branch to this file. I have not merged in WfMod_Helper.v as yet. This will be the next task.
Reflection is ready to be merged into master. There already is a Notations_rewrites.v file in the Kami directory. I merged in the changes from the ProcessorCoreWellFormed_part5 branch to this file. I have not merged in WfMod_Helper.v as yet. This will be the next task.