|
| 1 | +/*=======================================================================================*/ |
| 2 | +/* This Sail RISC-V architecture model, comprising all files and */ |
| 3 | +/* directories except where otherwise noted is subject the BSD */ |
| 4 | +/* two-clause license in the LICENSE file. */ |
| 5 | +/* */ |
| 6 | +/* SPDX-License-Identifier: BSD-2-Clause */ |
| 7 | +/*=======================================================================================*/ |
| 8 | + |
| 9 | +function clause currentlyEnabled(Ext_Zcmt) = hartSupports(Ext_Zcmt) & currentlyEnabled(Ext_Zca) & not(currentlyEnabled(Ext_Zcd)) |
| 10 | + |
| 11 | +type target_address = xlenbits |
| 12 | + |
| 13 | +function fetch_jump_table(table_address : xlenbits) -> result(target_address, unit) = { |
| 14 | + /* Executable permission required to fetch jump table address */ |
| 15 | + match ext_data_get_addr_from_bits(table_address, Execute(), xlen_bytes) { |
| 16 | + Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); Err() }, |
| 17 | + Ext_DataAddr_OK(vaddr) => { |
| 18 | + if check_misaligned(vaddr, size_bytes(xlen_bytes)) |
| 19 | + then { handle_mem_exception(vaddr, E_Load_Addr_Align()); Err() } |
| 20 | + else match translateAddr(vaddr, Execute()) { |
| 21 | + TR_Failure(e, _) => { handle_mem_exception(vaddr, e); Err() }, |
| 22 | + TR_Address(paddr, _) => |
| 23 | + match mem_read(Execute(), paddr, xlen_bytes, false, false, false) { |
| 24 | + Ok(result) => { Ok(result) }, |
| 25 | + Err(e) => { handle_mem_exception(vaddr, e); Err() }, |
| 26 | + } |
| 27 | + } |
| 28 | + } |
| 29 | + } |
| 30 | +} |
| 31 | + |
| 32 | +union clause ast = CM_JALT : (bits(8)) |
| 33 | + |
| 34 | +mapping clause encdec_compressed = CM_JALT(index) |
| 35 | + <-> 0b101 @ 0b000 @ index : bits(8) @ 0b10 |
| 36 | + when currentlyEnabled(Ext_Zcmt) & 32 <= unsigned(index) |
| 37 | + |
| 38 | +function clause execute (CM_JALT(index)) = { |
| 39 | + let base : bits(xlen) = jvt[base] @ 0b000000; |
| 40 | + let index : bits(xlen) = zero_extend(index); |
| 41 | + if jvt[mode] == 0b000000 then { |
| 42 | + let table_address = base + (index << log2_xlen_bytes); |
| 43 | + match fetch_jump_table(table_address) { |
| 44 | + Err(_) => { RETIRE_FAIL }, |
| 45 | + Ok(target_address) => { |
| 46 | + X(ra) = get_next_pc(); |
| 47 | + set_next_pc([target_address with 0 = bitzero]); |
| 48 | + RETIRE_SUCCESS |
| 49 | + } |
| 50 | + }; |
| 51 | + } else { |
| 52 | + handle_illegal(); |
| 53 | + RETIRE_FAIL |
| 54 | + }; |
| 55 | +} |
| 56 | + |
| 57 | +mapping clause assembly = CM_JALT(index) |
| 58 | + <-> "cm.jalt" ^ spc() ^ hex_bits_8(index) |
| 59 | + |
| 60 | +/* ****************************************************************** */ |
| 61 | +union clause ast = CM_JT : (bits(8)) |
| 62 | + |
| 63 | +mapping clause encdec_compressed = CM_JT(index) |
| 64 | + <-> 0b101 @ 0b000 @ index : bits(8) @ 0b10 |
| 65 | + when currentlyEnabled(Ext_Zcmt) & unsigned(index) < 32 |
| 66 | + |
| 67 | +function clause execute (CM_JT(index)) = { |
| 68 | + let base : bits(xlen) = jvt[base] @ 0b000000; |
| 69 | + let index : bits(xlen) = zero_extend(index); |
| 70 | + if jvt[mode] == 0b000000 then { |
| 71 | + let table_address = base + (index << log2_xlen_bytes); |
| 72 | + match fetch_jump_table(table_address) { |
| 73 | + Err(_) => { RETIRE_FAIL }, |
| 74 | + Ok(target_address) => { |
| 75 | + set_next_pc([target_address with 0 = bitzero]); |
| 76 | + RETIRE_SUCCESS |
| 77 | + } |
| 78 | + }; |
| 79 | + } else { |
| 80 | + handle_illegal(); |
| 81 | + RETIRE_FAIL |
| 82 | + }; |
| 83 | +} |
| 84 | + |
| 85 | +mapping clause assembly = CM_JT(index) |
| 86 | + <-> "cm.jt" ^ spc() ^ hex_bits_8(index) |
0 commit comments