Big endianness Support added #751
Conversation
model/prelude.sail
Outdated
| @@ -236,3 +236,6 @@ type max_mem_access : Int = 4096 | |||
|
|
|||
| // Type used for memory access widths. Zero byte accesses are not allowed. | |||
| type mem_access_width = range(1, max_mem_access) | |||
|
|
|||
| // Function to reverse endianness. | |||
| val reverse_endianness = pure {c: " reverse_endianness"} : forall 'n . (bits('n * 8)) -> bits('n * 8) | |||
There was a problem hiding this comment.
Any reason not to just use the existing sail reverse_endianness library? https://github.com/rems-project/sail/blob/6a8d444e41a3e04798e874325bf4ec0f813e3a3a/lib/reverse_endianness.sail#L47
Just put a $include <reverse_endianness.sail> at the top of the prelude.
There was a problem hiding this comment.
I actually tried this but was getting the following error:
This is because of the difference of types being passed by the function (bits(8 * 'n)) and type taken by the function bits('n).
Actually, this solution was suggested by @Timmmm and this method made the function accept values forall 'n instead of using contrained values.
|
I just noticed that |
|
The readme can also be updated to mention this support. |
| Ok(v, m) } | ||
| (_, Some(v, m)) => { | ||
| let temp_var: bits('n * 8) = match (t, is_big_endian(t)) { | ||
| (Execute(), _) => (v), |
There was a problem hiding this comment.
Why not move the check for an execute access into is_big_endian? It already needs to get AccessType to determine effective privilege, and if it is an execute type it will always be little endian.
| then print_mem("mem[" ^ to_str(t) ^ "," ^ BitStr(physaddr_bits(paddr)) ^ "] -> " ^ BitStr(v)); | ||
| Ok(v, m) } | ||
| (_, Some(v, m)) => { | ||
| let temp_var: bits('n * 8) = match (t, is_big_endian(t)) { |
There was a problem hiding this comment.
Let's use a more specific/significant name than temp_var. Especially as we move to include Sail code in the ISA manual, we want to make sure the meaning of everything is clear.
Hi @jordancarlin and @Timmmm
This PR adds the support for the big endianness in Sail RISC-V.
The test for the verification of this support is available here.