Tim Hutt
Tim Hutt
Support PMAs
Currently the thing close to PMAs in the model is this: ``` val phys_mem_segments : unit -> list((xlenbits, xlenbits)) function phys_mem_segments() = (plat_rom_base (), plat_rom_size ()) :: (plat_ram_base (), plat_ram_size...
Currently to choose between F support or F&D you need to compile the model differently - using `riscv_flen_D.sail` or `riscv_flen_F.sail`. This is unfortunate because now to support all the different...
Currently the model doesn't have very clear or rigorous handling of chip reset. I think we should do the following: 1. Rename all of these `init` functions to `reset`. This...
`is_CSR_defined` has a ton of `p == Machine` etc. checks that should be replaced by `true`, since the permission check is already handled in a generic way by this: ```...
This is quite annoying. If you run this command ``` ARCH=RV64 make ocaml_emulator/riscv_ocaml_sim_RV64 ``` and you have some error in your OCaml code it will do the expected thing, compile...
As far as I can see there's no reason to have this: ``` register x1 : regtype register x2 : regtype register x3 : regtype register x4 : regtype register...
The CSR code is a bit odd. For example `readCSR()` uses a `match`: ``` function readCSR csr : csreg -> xlenbits = { let res : xlenbits = match (csr,...
Currently there's a global register: ``` /* internal state to hold instruction bits for faulting instructions */ register instbits : xlenbits ``` Which is saved after fetch: ``` F_Base(w) =>...
It just has some stuff about adding copyright headers to files but they header has changed and it's short enough to easily do manually now.
``` /* NOTE: Currently, we only EA if address translation is successful. This may need revisiting. */ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { if speculate_conditional...