riscv-semantics
riscv-semantics copied to clipboard
mit-plv
A formal semantics of the RISC-V ISA in Haskell
I am interested in working on riscv-semantics codebase. Is there an interest in adding the support for "C" compressed instructions extension to riscv-semantics? If one is to add the support,...
I must not have "riscv-none-embed-gcc" in my install path, because when I ran ./install.sh, the make got to "make[1]: riscv-none-embed-gcc: Command not found" A more explicit description about where riscv-none-embed-gcc...
Currently, one `RiscvMachine` only runs one hart (RISC-V compatible hardware thread), but implementations of the RISC-V spec may support multiple harts. The interactions between harts and the restrictions on these...
the fmadd group of instructions should use f32MulAdd rather than f32Mul then f32Add
It would be great if trying to execute an instruction from an address that was written to after the last `FENCE.I` instruction was executed was undefined behavior. I am requesting...
Hi -- I'm having trouble following the installation instructions. Even after doing ```~/h/riscv-semantics> ./install_riscv_gcc.sh Downloading riscv-gcc... ######################################################################### 100.0% Riscv-gcc has been installed. ~/h/riscv-semantics> . setup.sh ``` I get this: ```~/h/riscv-semantics>...
### Problem Description I was trying to run the tests compiled in 32-bit mode with the simulator. Some of the tests work fine (e.g. `test/src/add.c` returns the result correctly) but...
I've installed git head of clash (see instructions at https://github.com/clash-lang/clash-compiler/wiki/Getting-started) and used `stack install` to install that version of clash in `~/.local/bin`. I can use `stack exec -- clash ...`...
Reads and writes to illegal CSRs should raise an Illegal Instruction exception. Since the commit ca2b76e7ef5794ccc8190ce68395b3c0d278563f, reads to illegal (or unimplemented) CSRs return 0, and writes do nothing. Before that...
