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

Change ext_data_get_addr to use bytes for width #468

Merged
merged 1 commit into from
Jun 3, 2024
Merged

Change ext_data_get_addr to use bytes for width #468

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
11 changes: 9 additions & 2 deletions model/prelude_mem.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -80,8 +80,15 @@ instantiation sail_mem_write with
because it means width argument can be fast native integer. It
would be even better if it could be <= 8 bytes so that data can
also be a 64-bit int but CHERI needs 128-bit accesses for
capabilities and SIMD / vector instructions will also need more. */
type max_mem_access : Int = 16
capabilities and SIMD / vector instructions will also need more.

The specific value does not matter (if it is >8) since anything up
to 2^64-1 will result in a native int being used for the width type.

4096 was chosen because it is a page size, and a reasonable maximum
for cbo.zero.
*/
type max_mem_access : Int = 4096

val write_ram : forall 'n, 0 < 'n <= max_mem_access. (write_kind, xlenbits, int('n), bits(8 * 'n), mem_meta) -> bool

Expand Down
2 changes: 1 addition & 1 deletion model/riscv_addr_checks.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,7 @@ type ext_data_addr_error = unit

/* Default data addr is just base register + immediate offset (may be zero).
Extensions might override and add additional checks. */
function ext_data_get_addr(base : regidx, offset : xlenbits, acc : AccessType(ext_access_type), width : word_width)
function ext_data_get_addr(base : regidx, offset : xlenbits, acc : AccessType(ext_access_type), width : range(1, max_mem_access))
-> Ext_DataAddr_Check(ext_data_addr_error) =
let addr = X(base) + offset in
Ext_DataAddr_OK(addr)
Expand Down
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 @@ -64,7 +64,7 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = {
/* Get the address, X(rs1) (no offset).
* Extensions might perform additional checks on address validity.
*/
match ext_data_get_addr(rs1, zeros(), Read(Data), width) {
match ext_data_get_addr(rs1, zeros(), Read(Data), size_bytes(width)) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) => {
let aligned : bool =
Expand Down Expand Up @@ -120,7 +120,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
/* Get the address, X(rs1) (no offset).
* Extensions might perform additional checks on address validity.
*/
match ext_data_get_addr(rs1, zeros(), Write(Data), width) {
match ext_data_get_addr(rs1, zeros(), Write(Data), size_bytes(width)) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) => {
let aligned : bool =
Expand Down Expand Up @@ -205,7 +205,7 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
/* Get the address, X(rs1) (no offset).
* Some extensions perform additional checks on address validity.
*/
match ext_data_get_addr(rs1, zeros(), ReadWrite(Data, Data), width) {
match ext_data_get_addr(rs1, zeros(), ReadWrite(Data, Data), size_bytes(width)) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) => {
match translateAddr(vaddr, ReadWrite(Data, Data)) {
Expand Down
4 changes: 2 additions & 2 deletions model/riscv_insts_base.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -326,7 +326,7 @@ function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = {
let offset : xlenbits = sign_extend(imm);
/* Get the address, X(rs1) + offset.
Some extensions perform additional checks on address validity. */
match ext_data_get_addr(rs1, offset, Read(Data), width) {
match ext_data_get_addr(rs1, offset, Read(Data), size_bytes(width)) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
if check_misaligned(vaddr, width)
Expand Down Expand Up @@ -382,7 +382,7 @@ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = {
let offset : xlenbits = sign_extend(imm);
/* Get the address, X(rs1) + offset.
Some extensions perform additional checks on address validity. */
match ext_data_get_addr(rs1, offset, Write(Data), width) {
match ext_data_get_addr(rs1, offset, Write(Data), size_bytes(width)) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
if check_misaligned(vaddr, width)
Expand Down
4 changes: 2 additions & 2 deletions model/riscv_insts_fext.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -315,7 +315,7 @@ function clause execute(LOAD_FP(imm, rs1, rd, width)) = {
let offset : xlenbits = sign_extend(imm);
/* Get the address, X(rs1) + offset.
Some extensions perform additional checks on address validity. */
match ext_data_get_addr(rs1, offset, Read(Data), width) {
match ext_data_get_addr(rs1, offset, Read(Data), size_bytes(width)) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
if check_misaligned(vaddr, width)
Expand Down Expand Up @@ -381,7 +381,7 @@ function clause execute (STORE_FP(imm, rs2, rs1, width)) = {
let (aq, rl, con) = (false, false, false);
/* Get the address, X(rs1) + offset.
Some extensions perform additional checks on address validity. */
match ext_data_get_addr(rs1, offset, Write(Data), width) {
match ext_data_get_addr(rs1, offset, Write(Data), size_bytes(width)) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
if check_misaligned(vaddr, width)
Expand Down
26 changes: 13 additions & 13 deletions model/riscv_insts_vext_mem.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -81,7 +81,7 @@ function process_vlseg (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) =
vstart = to_bits(16, i);
foreach (j from 0 to (nf - 1)) {
let elem_offset = (i * nf + j) * load_width_bytes;
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), width_type) {
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), load_width_bytes) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
if check_misaligned(vaddr, width_type)
Expand Down Expand Up @@ -149,7 +149,7 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem)
if vm_val[i] then { /* active segments */
foreach (j from 0 to (nf - 1)) {
let elem_offset = (i * nf + j) * load_width_bytes;
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), width_type) {
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), load_width_bytes) {
Ext_DataAddr_Error(e) => {
if i == 0 then { ext_handle_data_check_error(e); return RETIRE_FAIL }
else {
Expand Down Expand Up @@ -251,7 +251,7 @@ function process_vsseg (nf, vm, vs3, load_width_bytes, rs1, EMUL_pow, num_elem)
vstart = to_bits(16, i);
foreach (j from 0 to (nf - 1)) {
let elem_offset = (i * nf + j) * load_width_bytes;
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), width_type) {
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), load_width_bytes) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
if check_misaligned(vaddr, width_type)
Expand Down Expand Up @@ -322,7 +322,7 @@ function process_vlsseg (nf, vm, vd, load_width_bytes, rs1, rs2, EMUL_pow, num_e
vstart = to_bits(16, i);
foreach (j from 0 to (nf - 1)) {
let elem_offset = i * rs2_val + j * load_width_bytes;
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), width_type) {
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), load_width_bytes) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
if check_misaligned(vaddr, width_type)
Expand Down Expand Up @@ -388,7 +388,7 @@ function process_vssseg (nf, vm, vs3, load_width_bytes, rs1, rs2, EMUL_pow, num_
vstart = to_bits(16, i);
foreach (j from 0 to (nf - 1)) {
let elem_offset = i * rs2_val + j * load_width_bytes;
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), width_type) {
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), load_width_bytes) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
if check_misaligned(vaddr, width_type)
Expand Down Expand Up @@ -460,7 +460,7 @@ function process_vlxseg (nf, vm, vd, EEW_index_bytes, EEW_data_bytes, EMUL_index
vstart = to_bits(16, i);
foreach (j from 0 to (nf - 1)) {
let elem_offset : int = signed(vs2_val[i]) + j * EEW_data_bytes;
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), width_type) {
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), EEW_data_bytes) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
if check_misaligned(vaddr, width_type)
Expand Down Expand Up @@ -551,7 +551,7 @@ function process_vsxseg (nf, vm, vs3, EEW_index_bytes, EEW_data_bytes, EMUL_inde
vstart = to_bits(16, i);
foreach (j from 0 to (nf - 1)) {
let elem_offset : int = signed(vs2_val[i]) + j * EEW_data_bytes;
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), width_type) {
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), EEW_data_bytes) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
if check_misaligned(vaddr, width_type)
Expand Down Expand Up @@ -644,7 +644,7 @@ function process_vlre (nf, vd, load_width_bytes, rs1, elem_per_reg) = {
foreach (i from elem_to_align to (elem_per_reg - 1)) {
vstart = to_bits(16, cur_elem);
let elem_offset = cur_elem * load_width_bytes;
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), width_type) {
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), load_width_bytes) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
if check_misaligned(vaddr, width_type)
Expand All @@ -668,7 +668,7 @@ function process_vlre (nf, vd, load_width_bytes, rs1, elem_per_reg) = {
foreach (i from 0 to (elem_per_reg - 1)) {
vstart = to_bits(16, cur_elem);
let elem_offset = cur_elem * load_width_bytes;
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), width_type) {
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), load_width_bytes) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
if check_misaligned(vaddr, width_type)
Expand Down Expand Up @@ -726,7 +726,7 @@ function process_vsre (nf, load_width_bytes, rs1, vs3, elem_per_reg) = {
foreach (i from elem_to_align to (elem_per_reg - 1)) {
vstart = to_bits(16, cur_elem);
let elem_offset : int = cur_elem * load_width_bytes;
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), width_type) {
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), load_width_bytes) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
if check_misaligned(vaddr, width_type)
Expand Down Expand Up @@ -760,7 +760,7 @@ function process_vsre (nf, load_width_bytes, rs1, vs3, elem_per_reg) = {
foreach (i from 0 to (elem_per_reg - 1)) {
vstart = to_bits(16, cur_elem);
let elem_offset = cur_elem * load_width_bytes;
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), width_type) {
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), load_width_bytes) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
if check_misaligned(vaddr, width_type)
Expand Down Expand Up @@ -828,7 +828,7 @@ function process_vm(vd_or_vs3, rs1, num_elem, evl, op) = {
if i < evl then { /* active elements */
vstart = to_bits(16, i);
if op == VLM then { /* load */
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), i), Read(Data), width_type) {
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), i), Read(Data), 1) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
if check_misaligned(vaddr, width_type)
Expand All @@ -844,7 +844,7 @@ function process_vm(vd_or_vs3, rs1, num_elem, evl, op) = {
}
}
} else if op == VSM then { /* store */
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), i), Write(Data), width_type) {
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), i), Write(Data), 1) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
if check_misaligned(vaddr, width_type)
Expand Down
Loading