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
Stars
216
Forks
13
Watchers
216
Open Issues
12
Overall repository health assessment
No package.json found
This might not be a Node.js project
184
commits
104
commits
57
commits
24
commits
11
commits
9
commits
6
commits
4
commits
2
commits
1
commits
Issue 121: moved import statement for NatStr into AllDefn. Removed deprecated code. Converted functions in CoqSim to use natHexStr rather than natDecStr.
f57d2c4View on GitHubMoved the nat to string conversion functions and associated proofs to a new file named Lib/NatStr.v
fe91e90View on GitHubIssue 121: moved all deprecated definitions to the end of Kami.Notations.
c063114View on GitHubIssue 121: Proved that nat_decimal_string, nat_binary_string, and nat_hex_string are injective. Rewrote the nat to string conversion functions.
f65f33dView on GitHub