aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorTim Hutt <timothy.hutt@codasip.com>2024-03-06 10:59:42 +0000
committerBill McSpadden <bill@riscv.org>2024-04-12 10:00:00 -0500
commite187e0220352e731dc15dbc7375adb3dccac8138 (patch)
tree2ef68c90489fbf607d1fe2749e7c7f4158da81e8
parent5c7d1f2a024390897f2471b34abed4b144f000d8 (diff)
downloadsail-riscv-e187e0220352e731dc15dbc7375adb3dccac8138.zip
sail-riscv-e187e0220352e731dc15dbc7375adb3dccac8138.tar.gz
sail-riscv-e187e0220352e731dc15dbc7375adb3dccac8138.tar.bz2
Remove & rename duplicate word_width <-> bytes mappings
* Remove the duplicate mapping functions. * Rename to `size_bytes` for consistency with the other two functions. * Rename `size_bits` to `size_enc`, otherwise it's quite confusing that `size_bits` is not just `8 * size_bytes`. Fixes #423
-rw-r--r--model/riscv_insts_aext.sail6
-rw-r--r--model/riscv_insts_base.sail8
-rw-r--r--model/riscv_insts_vext_mem.sail23
-rw-r--r--model/riscv_types.sail14
4 files changed, 22 insertions, 29 deletions
diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail
index e72f912..0f4da83 100644
--- a/model/riscv_insts_aext.sail
+++ b/model/riscv_insts_aext.sail
@@ -44,7 +44,7 @@ function amo_width_valid(size : word_width) -> bool = {
union clause ast = LOADRES : (bool, bool, regidx, word_width, regidx)
mapping clause encdec = LOADRES(aq, rl, rs1, size, rd) if amo_width_valid(size)
- <-> 0b00010 @ bool_bits(aq) @ bool_bits(rl) @ 0b00000 @ rs1 @ 0b0 @ size_bits(size) @ rd @ 0b0101111 if amo_width_valid(size)
+ <-> 0b00010 @ bool_bits(aq) @ bool_bits(rl) @ 0b00000 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if amo_width_valid(size)
/* We could set load-reservations on physical or virtual addresses.
@@ -109,7 +109,7 @@ mapping clause assembly = LOADRES(aq, rl, rs1, size, rd)
union clause ast = STORECON : (bool, bool, regidx, regidx, word_width, regidx)
mapping clause encdec = STORECON(aq, rl, rs2, rs1, size, rd) if amo_width_valid(size)
- <-> 0b00011 @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_bits(size) @ rd @ 0b0101111 if amo_width_valid(size)
+ <-> 0b00011 @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if amo_width_valid(size)
/* NOTE: Currently, we only EA if address translation is successful. This may need revisiting. */
function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
@@ -207,7 +207,7 @@ mapping encdec_amoop : amoop <-> bits(5) = {
}
mapping clause encdec = AMO(op, aq, rl, rs2, rs1, size, rd) if amo_width_valid(size)
- <-> encdec_amoop(op) @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_bits(size) @ rd @ 0b0101111 if amo_width_valid(size)
+ <-> encdec_amoop(op) @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if amo_width_valid(size)
/* NOTE: Currently, we only EA if address translation is successful.
This may need revisiting. */
diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail
index caea73a..9c4630b 100644
--- a/model/riscv_insts_base.sail
+++ b/model/riscv_insts_base.sail
@@ -297,8 +297,8 @@ union clause ast = LOAD : (bits(12), regidx, regidx, bool, word_width, bool, boo
/* unsigned loads are only present for widths strictly less than xlen,
signed loads also present for widths equal to xlen */
-mapping clause encdec = LOAD(imm, rs1, rd, is_unsigned, size, false, false) if (word_width_bytes(size) < sizeof(xlen_bytes)) | (not(is_unsigned) & word_width_bytes(size) <= sizeof(xlen_bytes))
- <-> imm @ rs1 @ bool_bits(is_unsigned) @ size_bits(size) @ rd @ 0b0000011 if (word_width_bytes(size) < sizeof(xlen_bytes)) | (not(is_unsigned) & word_width_bytes(size) <= sizeof(xlen_bytes))
+mapping clause encdec = LOAD(imm, rs1, rd, is_unsigned, size, false, false) if (size_bytes(size) < sizeof(xlen_bytes)) | (not(is_unsigned) & size_bytes(size) <= sizeof(xlen_bytes))
+ <-> imm @ rs1 @ bool_bits(is_unsigned) @ size_enc(size) @ rd @ 0b0000011 if (size_bytes(size) < sizeof(xlen_bytes)) | (not(is_unsigned) & size_bytes(size) <= sizeof(xlen_bytes))
val extend_value : forall 'n, 0 < 'n <= xlen_bytes. (bool, MemoryOpResult(bits(8 * 'n))) -> MemoryOpResult(xlenbits)
function extend_value(is_unsigned, value) = match (value) {
@@ -373,8 +373,8 @@ mapping clause assembly = LOAD(imm, rs1, rd, is_unsigned, size, aq, rl)
/* ****************************************************************** */
union clause ast = STORE : (bits(12), regidx, regidx, word_width, bool, bool)
-mapping clause encdec = STORE(imm7 @ imm5, rs2, rs1, size, false, false) if word_width_bytes(size) <= sizeof(xlen_bytes)
- <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b0 @ size_bits(size) @ imm5 : bits(5) @ 0b0100011 if word_width_bytes(size) <= sizeof(xlen_bytes)
+mapping clause encdec = STORE(imm7 @ imm5, rs2, rs1, size, false, false) if size_bytes(size) <= sizeof(xlen_bytes)
+ <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ imm5 : bits(5) @ 0b0100011 if size_bytes(size) <= sizeof(xlen_bytes)
/* NOTE: Currently, we only EA if address translation is successful.
This may need revisiting. */
diff --git a/model/riscv_insts_vext_mem.sail b/model/riscv_insts_vext_mem.sail
index 942fbaf..0f1dfee 100644
--- a/model/riscv_insts_vext_mem.sail
+++ b/model/riscv_insts_vext_mem.sail
@@ -61,13 +61,6 @@ mapping vlewidth_pow : vlewidth <-> {|3, 4, 5, 6|} = {
VLE64 <-> 6
}
-mapping bytes_wordwidth : {|1, 2, 4, 8|} <-> word_width = {
- 1 <-> BYTE,
- 2 <-> HALF,
- 4 <-> WORD,
- 8 <-> DOUBLE
-}
-
/* ******************** Vector Load Unit-Stride Normal & Segment (mop=0b00, lumop=0b00000) ********************* */
union clause ast = VLSEGTYPE : (bits(3), bits(1), regidx, vlewidth, regidx)
@@ -77,7 +70,7 @@ mapping clause encdec = VLSEGTYPE(nf, vm, rs1, width, vd) if haveVExt()
val process_vlseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('b), regidx, int('p), int('n)) -> Retired
function process_vlseg (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) = {
let EMUL_reg : int = if EMUL_pow <= 0 then 1 else int_power(2, EMUL_pow);
- let width_type : word_width = bytes_wordwidth(load_width_bytes);
+ let width_type : word_width = size_bytes(load_width_bytes);
let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000);
let vd_seg : vector('n, dec, bits('f * 'b * 8)) = read_vreg_seg(num_elem, load_width_bytes * 8, EMUL_pow, nf, vd);
@@ -143,7 +136,7 @@ mapping clause encdec = VLSEGFFTYPE(nf, vm, rs1, width, vd) if haveVExt()
val process_vlsegff : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('b), regidx, int('p), int('n)) -> Retired
function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) = {
let EMUL_reg : int = if EMUL_pow <= 0 then 1 else int_power(2, EMUL_pow);
- let width_type : word_width = bytes_wordwidth(load_width_bytes);
+ let width_type : word_width = size_bytes(load_width_bytes);
let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000);
let vd_seg : vector('n, dec, bits('f * 'b * 8)) = read_vreg_seg(num_elem, load_width_bytes * 8, EMUL_pow, nf, vd);
let tail_ag : agtype = get_vtype_vta();
@@ -248,7 +241,7 @@ mapping clause encdec = VSSEGTYPE(nf, vm, rs1, width, vs3) if haveVExt()
val process_vsseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('b), regidx, int('p), int('n)) -> Retired
function process_vsseg (nf, vm, vs3, load_width_bytes, rs1, EMUL_pow, num_elem) = {
let EMUL_reg : int = if EMUL_pow <= 0 then 1 else int_power(2, EMUL_pow);
- let width_type : word_width = bytes_wordwidth(load_width_bytes);
+ let width_type : word_width = size_bytes(load_width_bytes);
let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000);
let vs3_seg : vector('n, dec, bits('f * 'b * 8)) = read_vreg_seg(num_elem, load_width_bytes * 8, EMUL_pow, nf, vs3);
let mask : vector('n, dec, bool) = init_masked_source(num_elem, EMUL_pow, vm_val);
@@ -317,7 +310,7 @@ mapping clause encdec = VLSSEGTYPE(nf, vm, rs2, rs1, width, vd) if haveVExt()
val process_vlsseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('b), regidx, regidx, int('p), int('n)) -> Retired
function process_vlsseg (nf, vm, vd, load_width_bytes, rs1, rs2, EMUL_pow, num_elem) = {
let EMUL_reg : int = if EMUL_pow <= 0 then 1 else int_power(2, EMUL_pow);
- let width_type : word_width = bytes_wordwidth(load_width_bytes);
+ let width_type : word_width = size_bytes(load_width_bytes);
let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000);
let vd_seg : vector('n, dec, bits('f * 'b * 8)) = read_vreg_seg(num_elem, load_width_bytes * 8, EMUL_pow, nf, vd);
let rs2_val : int = signed(get_scalar(rs2, sizeof(xlen)));
@@ -384,7 +377,7 @@ mapping clause encdec = VSSSEGTYPE(nf, vm, rs2, rs1, width, vs3) if haveVExt()
val process_vssseg : forall 'f 'b 'n 'p, (0 < 'f & 'f <= 8) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('b), regidx, regidx, int('p), int('n)) -> Retired
function process_vssseg (nf, vm, vs3, load_width_bytes, rs1, rs2, EMUL_pow, num_elem) = {
let EMUL_reg : int = if EMUL_pow <= 0 then 1 else int_power(2, EMUL_pow);
- let width_type : word_width = bytes_wordwidth(load_width_bytes);
+ let width_type : word_width = size_bytes(load_width_bytes);
let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000);
let vs3_seg : vector('n, dec, bits('f * 'b * 8)) = read_vreg_seg(num_elem, load_width_bytes * 8, EMUL_pow, nf, vs3);
let rs2_val : int = signed(get_scalar(rs2, sizeof(xlen)));
@@ -454,7 +447,7 @@ mapping clause encdec = VLUXSEGTYPE(nf, vm, vs2, rs1, width, vd) if haveVExt()
val process_vlxseg : forall 'f 'ib 'db 'ip 'dp 'n, (0 < 'f & 'f <= 8) & ('ib in {1, 2, 4, 8}) & ('db in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('ib), int('db), int('ip), int('dp), regidx, regidx, int('n), int) -> Retired
function process_vlxseg (nf, vm, vd, EEW_index_bytes, EEW_data_bytes, EMUL_index_pow, EMUL_data_pow, rs1, vs2, num_elem, mop) = {
let EMUL_data_reg : int = if EMUL_data_pow <= 0 then 1 else int_power(2, EMUL_data_pow);
- let width_type : word_width = bytes_wordwidth(EEW_data_bytes);
+ let width_type : word_width = size_bytes(EEW_data_bytes);
let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000);
let vd_seg : vector('n, dec, bits('f * 'db * 8)) = read_vreg_seg(num_elem, EEW_data_bytes * 8, EMUL_data_pow, nf, vd);
let vs2_val : vector('n, dec, bits('ib * 8)) = read_vreg(num_elem, EEW_index_bytes * 8, EMUL_index_pow, vs2);
@@ -546,7 +539,7 @@ mapping clause encdec = VSUXSEGTYPE(nf, vm, vs2, rs1, width, vs3) if haveVExt()
val process_vsxseg : forall 'f 'ib 'db 'ip 'dp 'n, (0 < 'f & 'f <= 8) & ('ib in {1, 2, 4, 8}) & ('db in {1, 2, 4, 8}) & ('n >= 0). (int('f), bits(1), regidx, int('ib), int('db), int('ip), int('dp), regidx, regidx, int('n), int) -> Retired
function process_vsxseg (nf, vm, vs3, EEW_index_bytes, EEW_data_bytes, EMUL_index_pow, EMUL_data_pow, rs1, vs2, num_elem, mop) = {
let EMUL_data_reg : int = if EMUL_data_pow <= 0 then 1 else int_power(2, EMUL_data_pow);
- let width_type : word_width = bytes_wordwidth(EEW_data_bytes);
+ let width_type : word_width = size_bytes(EEW_data_bytes);
let vm_val : vector('n, dec, bool) = read_vmask(num_elem, vm, 0b00000);
let vs3_seg : vector('n, dec, bits('f * 'db * 8)) = read_vreg_seg(num_elem, EEW_data_bytes * 8, EMUL_data_pow, nf, vs3);
let vs2_val : vector('n, dec, bits('ib * 8)) = read_vreg(num_elem, EEW_index_bytes * 8, EMUL_index_pow, vs2);
@@ -640,7 +633,7 @@ mapping clause encdec = VLRETYPE(nf, rs1, width, vd) if haveVExt()
val process_vlre : forall 'f 'b 'n, ('f in {1, 2, 4, 8}) & ('b in {1, 2, 4, 8}) & ('n >= 0). (int('f), regidx, int('b), regidx, int('n)) -> Retired
function process_vlre (nf, vd, load_width_bytes, rs1, elem_per_reg) = {
- let width_type : word_width = bytes_wordwidth(load_width_bytes);
+ let width_type : word_width = size_bytes(load_width_bytes);
let start_element = get_start_element();
if start_element >= nf * elem_per_reg then return RETIRE_SUCCESS; /* no elements are written if vstart >= evl */
let elem_to_align : int = start_element % elem_per_reg;
diff --git a/model/riscv_types.sail b/model/riscv_types.sail
index 59172cf..e9a5a19 100644
--- a/model/riscv_types.sail
+++ b/model/riscv_types.sail
@@ -367,7 +367,8 @@ mapping bool_not_bits : bool <-> bits(1) = {
false <-> 0b1
}
-mapping size_bits : word_width <-> bits(2) = {
+// Get the bit encoding of word_width.
+mapping size_enc : word_width <-> bits(2) = {
BYTE <-> 0b00,
HALF <-> 0b01,
WORD <-> 0b10,
@@ -381,12 +382,11 @@ mapping size_mnemonic : word_width <-> string = {
DOUBLE <-> "d"
}
-val word_width_bytes : word_width -> {'s, 's == 1 | 's == 2 | 's == 4 | 's == 8 . int('s)}
-function word_width_bytes width = match width {
- BYTE => 1,
- HALF => 2,
- WORD => 4,
- DOUBLE => 8
+mapping size_bytes : word_width <-> {1, 2, 4, 8} = {
+ BYTE <-> 1,
+ HALF <-> 2,
+ WORD <-> 4,
+ DOUBLE <-> 8,
}
/*!