diff --git a/README.md b/README.md index 51419c019..c1cff1633 100644 --- a/README.md +++ b/README.md @@ -109,7 +109,7 @@ Supported RISC-V ISA features - Zfa extension for additional floating-point instructions, v1.0 - Zfinx, Zdinx, and Zhinx extensions for floating-point in integer registers, v1.0 - C extension for compressed instructions, v2.0 -- Zca, Zcf, Zcd, and Zcb extensions for code size reduction, v1.0 +- Zca, Zcf, Zcd, Zcb, and Zcmt extensions for code size reduction, v1.0 - Zcmop extension for compressed May-Be-Operations, v1.0 - B (Zba, Zbb, Zbs) and Zbc extensions for bit manipulation, v1.0 - Zbkb, Zbkc, and Zbkx extensions for bit manipulation for cryptography, v1.0 diff --git a/config/default.json b/config/default.json index 2b66a6250..c274f9446 100644 --- a/config/default.json +++ b/config/default.json @@ -119,6 +119,9 @@ "Zcb" : { "supported" : true }, + "Zcmt" : { + "supported" : false + }, "Zcmop" : { "supported" : true }, diff --git a/model/CMakeLists.txt b/model/CMakeLists.txt index d10a57043..ea705c364 100644 --- a/model/CMakeLists.txt +++ b/model/CMakeLists.txt @@ -72,6 +72,7 @@ foreach (xlen IN ITEMS 32 64) "riscv_insts_zba.sail" "riscv_insts_zbb.sail" "riscv_insts_zbc.sail" + "riscv_insts_zcmt.sail" "riscv_insts_zbs.sail" "riscv_insts_zcb.sail" "riscv_insts_zfh.sail" diff --git a/model/riscv_addr_checks.sail b/model/riscv_addr_checks.sail index e7cb9cb82..69e7a8ef7 100644 --- a/model/riscv_addr_checks.sail +++ b/model/riscv_addr_checks.sail @@ -59,6 +59,11 @@ function ext_data_get_addr(base : regidx, offset : xlenbits, acc : AccessType(ex let addr = Virtaddr(X(base) + offset) in Ext_DataAddr_OK(addr) +function ext_data_get_addr_from_bits(addr_ext : xlenbits, acc : AccessType(ext_access_type), width : mem_access_width) + -> Ext_DataAddr_Check(ext_data_addr_error) = + let addr = Virtaddr(addr_ext) in + Ext_DataAddr_OK(addr) + function ext_handle_data_check_error(err : ext_data_addr_error) -> unit = () diff --git a/model/riscv_extensions.sail b/model/riscv_extensions.sail index c5ff1466b..c65f943e1 100644 --- a/model/riscv_extensions.sail +++ b/model/riscv_extensions.sail @@ -108,6 +108,9 @@ function clause hartSupports(Ext_Zca) = config extensions.Zca.supported // Code Size Reduction: additional 16-bit aliases enum clause extension = Ext_Zcb function clause hartSupports(Ext_Zcb) = config extensions.Zcb.supported +// Code Size Reduction: compressed table jump instructions +enum clause extension = Ext_Zcmt +function clause hartSupports(Ext_Zcmt) = config extensions.Zcmt.supported // Code Size Reduction: compressed double precision floating point loads and stores enum clause extension = Ext_Zcd function clause hartSupports(Ext_Zcd) = config extensions.Zcd.supported diff --git a/model/riscv_insts_zcd.sail b/model/riscv_insts_zcd.sail index 685244a7f..8d346a94c 100644 --- a/model/riscv_insts_zcd.sail +++ b/model/riscv_insts_zcd.sail @@ -6,7 +6,7 @@ /* SPDX-License-Identifier: BSD-2-Clause */ /*=======================================================================================*/ -function clause currentlyEnabled(Ext_Zcd) = hartSupports(Ext_Zcd) & currentlyEnabled(Ext_D) & currentlyEnabled(Ext_Zca) & (currentlyEnabled(Ext_C) | not(hartSupports(Ext_C))) +function clause currentlyEnabled(Ext_Zcd) = hartSupports(Ext_Zcd) & currentlyEnabled(Ext_D) & currentlyEnabled(Ext_Zca) & not(currentlyEnabled(Ext_Zcmt)) & (currentlyEnabled(Ext_C) | not(hartSupports(Ext_C))) union clause ast = C_FLDSP : (bits(6), fregidx) diff --git a/model/riscv_insts_zcmt.sail b/model/riscv_insts_zcmt.sail new file mode 100644 index 000000000..573e2d386 --- /dev/null +++ b/model/riscv_insts_zcmt.sail @@ -0,0 +1,86 @@ +/*=======================================================================================*/ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except where otherwise noted is subject the BSD */ +/* two-clause license in the LICENSE file. */ +/* */ +/* SPDX-License-Identifier: BSD-2-Clause */ +/*=======================================================================================*/ + +function clause currentlyEnabled(Ext_Zcmt) = hartSupports(Ext_Zcmt) & currentlyEnabled(Ext_Zca) & not(currentlyEnabled(Ext_Zcd)) + +type target_address = xlenbits + +function fetch_jump_table(table_address : xlenbits) -> result(target_address, unit) = { + /* Executable permission required to fetch jump table address */ + match ext_data_get_addr_from_bits(table_address, Execute(), xlen_bytes) { + Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); Err() }, + Ext_DataAddr_OK(vaddr) => { + if check_misaligned(vaddr, size_bytes(xlen_bytes)) + then { handle_mem_exception(vaddr, E_Load_Addr_Align()); Err() } + else match translateAddr(vaddr, Execute()) { + TR_Failure(e, _) => { handle_mem_exception(vaddr, e); Err() }, + TR_Address(paddr, _) => + match mem_read(Execute(), paddr, xlen_bytes, false, false, false) { + Ok(result) => { Ok(result) }, + Err(e) => { handle_mem_exception(vaddr, e); Err() }, + } + } + } + } +} + +union clause ast = CM_JALT : (bits(8)) + +mapping clause encdec_compressed = CM_JALT(index) + <-> 0b101 @ 0b000 @ index : bits(8) @ 0b10 + when currentlyEnabled(Ext_Zcmt) & 32 <= unsigned(index) + +function clause execute (CM_JALT(index)) = { + let base : bits(xlen) = jvt[base] @ 0b000000; + let index : bits(xlen) = zero_extend(index); + if jvt[mode] == 0b000000 then { + let table_address = base + (index << log2_xlen_bytes); + match fetch_jump_table(table_address) { + Err(_) => { RETIRE_FAIL }, + Ok(target_address) => { + X(ra) = get_next_pc(); + set_next_pc([target_address with 0 = bitzero]); + RETIRE_SUCCESS + } + }; + } else { + handle_illegal(); + RETIRE_FAIL + }; +} + +mapping clause assembly = CM_JALT(index) + <-> "cm.jalt" ^ spc() ^ hex_bits_8(index) + +/* ****************************************************************** */ +union clause ast = CM_JT : (bits(8)) + +mapping clause encdec_compressed = CM_JT(index) + <-> 0b101 @ 0b000 @ index : bits(8) @ 0b10 + when currentlyEnabled(Ext_Zcmt) & unsigned(index) < 32 + +function clause execute (CM_JT(index)) = { + let base : bits(xlen) = jvt[base] @ 0b000000; + let index : bits(xlen) = zero_extend(index); + if jvt[mode] == 0b000000 then { + let table_address = base + (index << log2_xlen_bytes); + match fetch_jump_table(table_address) { + Err(_) => { RETIRE_FAIL }, + Ok(target_address) => { + set_next_pc([target_address with 0 = bitzero]); + RETIRE_SUCCESS + } + }; + } else { + handle_illegal(); + RETIRE_FAIL + }; +} + +mapping clause assembly = CM_JT(index) + <-> "cm.jt" ^ spc() ^ hex_bits_8(index) diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index fb952121f..53a7d487f 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -978,3 +978,24 @@ function get_vtype_vma() = decode_agtype(vtype[vma]) val get_vtype_vta : unit -> agtype function get_vtype_vta() = decode_agtype(vtype[vta]) + +/* Zcmt register */ + +bitfield Jvt : xlenbits = { + base : xlen - 1 .. 6, + mode : 5 .. 0 +} +register jvt : Jvt + +function legalize_jvt(o : Jvt, v : xlenbits) -> Jvt = { + let v = Mk_Jvt(v); + [o with + base = v[base], + mode = 0b000000 + ] +} + +mapping clause csr_name_map = 0x017 <-> "jvt" +function clause is_CSR_defined (0x017) = currentlyEnabled(Ext_Zcmt) +function clause write_CSR(0x017, value) = { jvt = legalize_jvt(jvt, value); jvt.bits } +function clause read_CSR(0x017) = jvt.bits