riscv-coq
riscv-coq copied to clipboard
mit-plv
RISC-V Specification in Coq
This [commit](https://github.com/mit-plv/riscv-coq/commit/6072bd95d6899f2970c659db67834611fe7a408e) breaks the smoke test in the platform: https://github.com/coq/platform/actions/runs/8391869140/job/22983180597 Could you offer a new test ?
This unfortunately makes src/riscv/Spec/Decode.v a bit slower; I can speed it up if desired by setting boolean equality only for `InstructionSet`. This is to help with https://github.com/mit-plv/bedrock2/issues/285 ... which I...
I started working on a formalisation of the privileged specification, mostly the CSRs. The CSR branch on my repo contains the current code. Some splitting and reordering of the commits...
I created a branch 'doc' in my repo with some notes about the structure of the code. I’m beginning to decipher `Primitives.v` and would like to add my notes about...
To specify the behaviour of a risc-v processor with multiple harts, the follwing problems need to be solved. * The harts aren’t always in the same state. This requires a...
Adds leakage traces to the semantics. I'm unsure whether the leakage trace semantics actually belong in this repository; maybe they should go in [riscv-semantics](https://github.com/mit-plv/riscv-semantics/tree/master) instead. But this PR should be...
Adapt to https://github.com/coq/coq/pull/19530 This is an adaptation in anticipation of the day the temporary backward compatibility introduced in the upstream PR will be removed (probably a few years in the...
