Tim Hutt

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...

There's tons of code like this: ``` let res : MemoryOpResult(bool) = match (width) { BYTE => mem_write_value(paddr, 1, rs2_val[7..0], aq, rl, false), HALF => mem_write_value(paddr, 2, rs2_val[15..0], aq, rl,...

Refactor duplicated floating point code for 16/32/64 bit floats

1

The floating point code is full of copy/pasted functions for 16/32/64 bit values. This is unnecessary since Sail has amazing support for generic code that works on all sizes. For...

Use result type instead of `MemoryOpResult`, `TR_Result`, and `PTW_Result`

9

Sail has a standard `result` type in it's library now so we should replace these: ``` union PTW_Result('paddr : Type, 'pte : Type) = { PTW_Success: ('paddr, 'pte, 'paddr, nat,...

For clarify and to avoid mixing them up, we can use Sail's `newtype` feature to create distinct types for physical and virtual addresses. For example: ``` newtype physaddr = physaddr...

VM code doesn't check reserved bits of PTEs are zero

5

From the Sv39 spec: > The PTE format for Sv39 is shown in Figure 60. Bits 9-0 have the same meaning as for Sv32. Bit 63 is reserved for use...

VM code reads 8 bytes even for 4-byte PTEs

2

In `pt_walk`: ``` // Read this-level PTE from mem let mem_result = mem_read_priv(Read(Data), // AccessType Supervisor, // Privilege pte_phys_addr, 8, // atom (8) false, // aq false, // rl false);...

Deduplicate some floating point code

12

This is an initial effort to deduplicate the floating point code (see #432). Currently all the floating point code is copy/pasted for every size of float (f16, f32, f64). That's...

Regardless of whether p-ext is enabled or not, some insns (i.e. `add32`) are not available on rv32. Still it is possible to provide generic code for their immediates, as it...