diff options
| author | Thomas Bauereiss | 2017-11-07 15:39:44 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2017-11-07 15:39:44 +0000 |
| commit | a06fef246172dd97d68e4fef77132a375554db73 (patch) | |
| tree | 4f9574e9c9e46c9d7b6ecec349b84943b1ace2d6 /mips_new_tc | |
| parent | 1dbf01cafae9aba80582754f17d831c8bc11cdba (diff) | |
Add builtin for reversing endianness
Diffstat (limited to 'mips_new_tc')
| -rw-r--r-- | mips_new_tc/mips_prelude.sail | 4 | ||||
| -rw-r--r-- | mips_new_tc/mips_wrappers.sail | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/mips_new_tc/mips_prelude.sail b/mips_new_tc/mips_prelude.sail index 128c63d8..c026c85f 100644 --- a/mips_new_tc/mips_prelude.sail +++ b/mips_new_tc/mips_prelude.sail @@ -577,7 +577,7 @@ function (bool) isAddressAligned ((bit[64]) addr, (WordType) wordType) = let a = unsigned(addr) in ((a quot alignment_width) == (a + wordWidthBytes(wordType) - 1) quot alignment_width) -val forall Nat 'W, 'W >= 1. ([:'W:], bit[8 * 'W]) -> bit[8 * 'W] effect pure reverse_endianness' +(*val forall Nat 'W, 'W >= 1. ([:'W:], bit[8 * 'W]) -> bit[8 * 'W] effect pure reverse_endianness' function rec forall Nat 'W, 'W >= 1. bit[8 * 'W] reverse_endianness' (w, value) = { @@ -592,7 +592,7 @@ val forall Nat 'W, 'W >= 1. bit[8 * 'W] -> bit[8 * 'W] effect pure reverse_endia function rec forall Nat 'W, 'W >= 1. bit[8 * 'W] reverse_endianness ((bit[8 * 'W]) value) = { reverse_endianness'(sizeof 'W, value) -} +}*) function forall Nat 'n, 1 <= 'n, 'n <= 8. (bit[8 * 'n]) effect { rmem } MEMr_wrapper ((bit[64]) addr, ([:'n:]) size) = if (addr == 0x000000007f000000) then diff --git a/mips_new_tc/mips_wrappers.sail b/mips_new_tc/mips_wrappers.sail index c5eb6cf4..70033977 100644 --- a/mips_new_tc/mips_wrappers.sail +++ b/mips_new_tc/mips_wrappers.sail @@ -38,7 +38,7 @@ val forall Nat 'n, 'n >= 1, 'n <= 8. (bit[64], [:'n:], bit[8 * 'n]) -> unit effect {eamem, wmv, wreg} MEMw_wrapper function unit MEMw_wrapper((bit[64]) addr, ([:'n:]) size, (bit[8 * 'n]) data) = - let ledata = reverse_endianness'(sizeof 'n, data) in + let ledata = reverse_endianness(data) in if (addr == 0x000000007f000000) then { UART_WDATA := ledata[7..0]; @@ -53,7 +53,7 @@ val forall Nat 'n, 'n >= 1, 'n <= 8. (bit[64], [:'n:], bit[8 * 'n]) -> bool effe function bool MEMw_conditional_wrapper(addr, size, data) = { MEMea_conditional(addr, size); - MEMval_conditional(addr, size, reverse_endianness'(sizeof 'n, data)) + MEMval_conditional(addr, size, reverse_endianness(data)) } function bit[64] addrWrapper((bit[64]) addr, (MemAccessType) accessType, (WordType) width) = |