Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Remove & rename duplicate word_width <-> bytes mappings #436

Merged
merged 1 commit into from
Apr 12, 2024
Merged

Remove & rename duplicate word_width <-> bytes mappings #436

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions model/riscv_insts_aext.sail
View file
Open in desktop
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
View file
Open in desktop
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
View file
Open in desktop
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
View file
Open in desktop
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
Loading