diff options
Diffstat (limited to 'model')
| -rw-r--r-- | model/riscv_regs.sail | 24 | ||||
| -rw-r--r-- | model/riscv_sys_control.sail | 5 | ||||
| -rw-r--r-- | model/riscv_sys_regs.sail | 4 | ||||
| -rw-r--r-- | model/riscv_types.sail | 27 |
4 files changed, 39 insertions, 21 deletions
diff --git a/model/riscv_regs.sail b/model/riscv_regs.sail index dd7d888..90ecc75 100644 --- a/model/riscv_regs.sail +++ b/model/riscv_regs.sail @@ -11,6 +11,15 @@ register PC : xlenbits register nextPC : xlenbits +/* Mappings for encoding */ + +mapping encdec_reg : regidx <-> bits(5) = { + forwards Regidx(r) => zero_extend(r), + backwards r if not(base_E_enabled) | r[4] == bitzero => Regidx(r[regidx_bit_width - 1 .. 0]), +} + +mapping encdec_creg : cregidx <-> bits(3) = { Cregidx(r) <-> r } + /* mappings for assembly */ mapping reg_abi_name_raw : bits(5) <-> string = { @@ -84,9 +93,11 @@ mapping reg_arch_name_raw : bits(5) <-> string = { 0b11111 <-> "x31", } +// Mapping from 4/5 back to 5 bits here makes the name mapping much easier. +// If you call `reg_name("t6")` on an E hart you'll get a mapping failure. mapping reg_name : regidx <-> string = { - Regidx(i) if get_config_use_abi_names() <-> reg_abi_name_raw(i), - Regidx(i) if not(get_config_use_abi_names()) <-> reg_arch_name_raw(i), + encdec_reg(i) if get_config_use_abi_names() <-> reg_abi_name_raw(i), + encdec_reg(i) if not(get_config_use_abi_names()) <-> reg_arch_name_raw(i), } // Special mapping for the sp register for use in assembly for sp-relative @@ -96,7 +107,7 @@ mapping sp_reg_name : unit <-> string = { () if not(get_config_use_abi_names()) <-> "x2", } -mapping creg_name : cregidx <-> string = { Cregidx(i) <-> reg_name(Regidx(0b01 @ i)) } +mapping creg_name : cregidx <-> string = { Cregidx(i) <-> reg_name(encdec_reg(0b01 @ i)) } function xreg_write_callback(reg : regidx, value : xlenbits) -> unit = { let name = reg_name(reg); @@ -236,10 +247,3 @@ function wX_pair_bits(i : regidx, data : bits(xlen * 2)) -> unit = } overload X_pair = {rX_pair_bits, wX_pair_bits} - - -/* Mappings for encoding */ - -mapping encdec_reg : regidx <-> bits(5) = { Regidx(r) <-> r } - -mapping encdec_creg : cregidx <-> bits(3) = { Cregidx(r) <-> r } diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 6edd4a9..e7e3dd9 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -275,12 +275,15 @@ function reset_misa() -> unit = { misa[A] = bool_to_bits(hartSupports(Ext_A)); /* atomics */ misa[C] = bool_to_bits(hartSupports(Ext_C)); /* RVC */ misa[B] = bool_to_bits(hartSupports(Ext_B)); /* Bit-manipulation */ - misa[I] = 0b1; /* base integer ISA */ misa[M] = bool_to_bits(hartSupports(Ext_M)); /* integer multiply/divide */ misa[U] = bool_to_bits(hartSupports(Ext_U)); /* user-mode */ misa[S] = bool_to_bits(hartSupports(Ext_S)); /* supervisor-mode */ misa[V] = bool_to_bits(hartSupports(Ext_V)); /* vector extension */ + // Base integer ISA (disabled if we only support the 16-register E base). + misa[E] = bool_to_bits(base_E_enabled); + misa[I] = ~(misa[E]); + if hartSupports(Ext_F) & hartSupports(Ext_Zfinx) then internal_error(__FILE__, __LINE__, "F and Zfinx cannot both be enabled!"); diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 71be271..5a8ae56 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -112,7 +112,9 @@ function legalize_misa(m : Misa, v : xlenbits) -> Misa = { D = if hartSupports(Ext_D) & v[F] == 0b1 then v[D] else 0b0, F = if hartSupports(Ext_F) then v[F] else 0b0, H = if hartSupports(Ext_H) then v[H] else 0b0, // TODO: Not fully supported yet - I = 0b1, // I is currently always supported + // Writable I is not currently supported. + I = bool_to_bits(not(base_E_enabled)), + E = bool_to_bits(base_E_enabled), M = if hartSupports(Ext_M) then v[M] else 0b0, // Q = if hartSupports(Ext_Q) then v[Q] else 0b0, TODO: Not supported yet S = if hartSupports(Ext_S) & v[U] == 0b1 then v[S] else 0b0, diff --git a/model/riscv_types.sail b/model/riscv_types.sail index 400ff9e..27e1186 100644 --- a/model/riscv_types.sail +++ b/model/riscv_types.sail @@ -17,28 +17,37 @@ type instbits = bits(32) type pagesize_bits : Int = 12 let pagesize_bits = sizeof(pagesize_bits) +// RV32E and RV64E Base Integer Instruction Sets. If this enabled then +// the model will only support E (16 integer registers). It is allowed +// to have a design where `misa[I]` is writable to turn E on and off, +// but this model does not support that. +type base_E_enabled : Bool = config base.E +let base_E_enabled = constraint(base_E_enabled) + /* register identifiers */ -newtype regidx = Regidx : bits(5) /* uncompressed register identifiers */ +type regidx_bit_width = if base_E_enabled then 4 else 5 +let regidx_bit_width = sizeof(regidx_bit_width) + +newtype regidx = Regidx : bits(regidx_bit_width) /* uncompressed register identifiers */ newtype cregidx = Cregidx : bits(3) /* identifiers in RVC instructions */ type csreg = bits(12) /* CSR addressing */ -function regidx_offset(Regidx(r) : regidx, o : bits(5)) -> regidx = Regidx(r + o) +function regidx_offset(Regidx(r) : regidx, o : bits(regidx_bit_width)) -> regidx = Regidx(r + o) function regidx_offset_range(Regidx(r) : regidx, o : range(0, 31)) -> regidx = Regidx(r + o) -function regidx_bits(Regidx(b) : regidx) -> bits(5) = b +function regidx_bits(Regidx(b) : regidx) -> bits(regidx_bit_width) = b overload operator + = { regidx_offset, regidx_offset_range } /* register file indexing */ -newtype regno = Regno : range(0, 31) +newtype regno = Regno : range(0, 2 ^ regidx_bit_width - 1) /* mapping RVC register indices into normal indices */ -val creg2reg_idx : cregidx -> regidx -function creg2reg_idx(Cregidx(i)) = Regidx(0b01 @ i) +function creg2reg_idx(Cregidx(i) : cregidx) -> regidx = Regidx(zero_extend(0b1 @ i)) /* some architecture and ABI relevant register identifiers */ -let zreg : regidx = Regidx(0b00000) /* x0, zero register */ -let ra : regidx = Regidx(0b00001) /* x1, return address */ -let sp : regidx = Regidx(0b00010) /* x2, stack pointer */ +let zreg : regidx = Regidx(zero_extend(0b00)) /* x0, zero register */ +let ra : regidx = Regidx(zero_extend(0b01)) /* x1, return address */ +let sp : regidx = Regidx(zero_extend(0b10)) /* x2, stack pointer */ /* base architecture definitions */ |