Skip to content

Commit

Permalink
Remove & rename duplicate word_width <-> bytes mappings
Browse files Browse the repository at this point in the history
* 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
  • Loading branch information
Timmmm authored and billmcspadden-riscv committed Apr 12, 2024
1 parent 5c7d1f2 commit e187e02
Show file tree
Hide file tree
Showing 4 changed files with 22 additions and 29 deletions.
6 changes: 3 additions & 3 deletions model/riscv_insts_aext.sail
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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)) = {
Expand Down Expand Up @@ -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. */
Expand Down
8 changes: 4 additions & 4 deletions model/riscv_insts_base.sail
Original file line number Diff line number Diff line change
Expand Up @@ -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) {
Expand Down Expand Up @@ -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. */
Expand Down
23 changes: 8 additions & 15 deletions model/riscv_insts_vext_mem.sail
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand All @@ -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);

Expand Down Expand Up @@ -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();
Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -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)));
Expand Down Expand Up @@ -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)));
Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -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;
Expand Down
14 changes: 7 additions & 7 deletions model/riscv_types.sail
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand All @@ -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,
}

/*!
Expand Down

0 comments on commit e187e02

Please sign in to comment.