Skip to content

Commit

Permalink
Merge branch 'riscv:master' into sdtrig_support
Browse files Browse the repository at this point in the history
  • Loading branch information
@Mudassir10X
Mudassir10X authored Jun 7, 2024
2 parents d865d0f + 7ff6d94 commit 4fbb701
Show file tree
Hide file tree
Showing 6 changed files with 97 additions and 173 deletions.
11 changes: 9 additions & 2 deletions model/prelude_mem.sail
View file
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
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
148 changes: 40 additions & 108 deletions model/riscv_insts_aext.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -53,46 +53,31 @@ mapping clause encdec = LOADRES(aq, rl, rs1, size, rd)
* call to load_reservation in LR and cancel_reservation in SC.
*/

val process_loadres : forall 'n, 0 < 'n <= xlen_bytes. (regidx, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> Retired
function process_loadres(rd, addr, value, is_unsigned) =
match extend_value(is_unsigned, value) {
MemValue(result) => { load_reservation(addr); X(rd) = result; RETIRE_SUCCESS },
MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL }
}

function clause execute(LOADRES(aq, rl, rs1, width, rd)) = {
let width_bytes = size_bytes(width);

// This is checked during decoding.
assert(width_bytes <= sizeof(xlen_bytes));

/* 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), width_bytes) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) => {
let aligned : bool =
/* BYTE and HALF would only occur due to invalid decodes, but it doesn't hurt
* to treat them as valid here; otherwise we'd need to throw an internal_error.
*/
match width {
BYTE => true,
HALF => vaddr[0..0] == 0b0,
WORD => vaddr[1..0] == 0b00,
DOUBLE => vaddr[2..0] == 0b000
};
/* "LR faults like a normal load, even though it's in the AMO major opcode space."
* - Andrew Waterman, isa-dev, 10 Jul 2018.
*/
if not(aligned)
if not(is_aligned(vaddr, width))
then { handle_mem_exception(vaddr, E_Load_Addr_Align()); RETIRE_FAIL }
else match translateAddr(vaddr, Read(Data)) {
TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
TR_Address(addr, _) =>
match (width, sizeof(xlen)) {
(BYTE, _) => process_loadres(rd, vaddr, mem_read(Read(Data), addr, 1, aq, aq & rl, true), false),
(HALF, _) => process_loadres(rd, vaddr, mem_read(Read(Data), addr, 2, aq, aq & rl, true), false),
(WORD, _) => process_loadres(rd, vaddr, mem_read(Read(Data), addr, 4, aq, aq & rl, true), false),
(DOUBLE, 64) => process_loadres(rd, vaddr, mem_read(Read(Data), addr, 8, aq, aq & rl, true), false),
_ => internal_error(__FILE__, __LINE__, "Unexpected AMO width")
}
}
TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
TR_Address(addr, _) =>
match mem_read(Read(Data), addr, width_bytes, aq, aq & rl, true) {
MemValue(result) => { load_reservation(vaddr); X(rd) = sign_extend(result); RETIRE_SUCCESS },
MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }
},
}
}
}
}
Expand All @@ -108,6 +93,11 @@ mapping clause encdec = STORECON(aq, rl, rs2, rs1, size, rd)

/* NOTE: Currently, we only EA if address translation is successful. This may need revisiting. */
function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
let width_bytes = size_bytes(width);

// This is checked during decoding.
assert(width_bytes <= sizeof(xlen_bytes));

if speculate_conditional () == false then {
/* should only happen in rmem
* rmem: allow SC to fail very early
Expand All @@ -120,20 +110,10 @@ 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), width_bytes) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) => {
let aligned : bool =
/* BYTE and HALF would only occur due to invalid decodes, but it doesn't hurt
* to treat them as valid here; otherwise we'd need to throw an internal_error.
*/
match width {
BYTE => true,
HALF => vaddr[0..0] == 0b0,
WORD => vaddr[1..0] == 0b00,
DOUBLE => vaddr[2..0] == 0b000
};
if not(aligned)
if not(is_aligned(vaddr, width))
then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL }
else {
if match_reservation(vaddr) == false then {
Expand All @@ -144,25 +124,12 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
* both result in a SAMO exception */
TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
TR_Address(addr, _) => {
let eares : MemoryOpResult(unit) = match (width, sizeof(xlen)) {
(BYTE, _) => mem_write_ea(addr, 1, aq & rl, rl, true),
(HALF, _) => mem_write_ea(addr, 2, aq & rl, rl, true),
(WORD, _) => mem_write_ea(addr, 4, aq & rl, rl, true),
(DOUBLE, 64) => mem_write_ea(addr, 8, aq & rl, rl, true),
_ => internal_error(__FILE__, __LINE__, "STORECON expected word or double")
};
let eares = mem_write_ea(addr, width_bytes, aq & rl, rl, true);
match (eares) {
MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
MemValue(_) => {
rs2_val = X(rs2);
let res : MemoryOpResult(bool) = match (width, sizeof(xlen)) {
(BYTE, _) => mem_write_value(addr, 1, rs2_val[7..0], aq & rl, rl, true),
(HALF, _) => mem_write_value(addr, 2, rs2_val[15..0], aq & rl, rl, true),
(WORD, _) => mem_write_value(addr, 4, rs2_val[31..0], aq & rl, rl, true),
(DOUBLE, 64) => mem_write_value(addr, 8, rs2_val, aq & rl, rl, true),
_ => internal_error(__FILE__, __LINE__, "STORECON expected word or double")
};
match (res) {
let rs2_val = X(rs2);
match mem_write_value(addr, width_bytes, rs2_val[width_bytes * 8 - 1 .. 0], aq & rl, rl, true) {
MemValue(true) => { X(rd) = zero_extend(0b0); cancel_reservation(); RETIRE_SUCCESS },
MemValue(false) => { X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS },
MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }
Expand Down Expand Up @@ -202,77 +169,42 @@ mapping clause encdec = AMO(op, aq, rl, rs2, rs1, size, rd)
/* NOTE: Currently, we only EA if address translation is successful.
This may need revisiting. */
function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
let 'width_bytes = size_bytes(width);

// This is checked during decoding.
assert(width_bytes <= sizeof(xlen_bytes));

/* 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), width_bytes) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) => {
match translateAddr(vaddr, ReadWrite(Data, Data)) {
TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
TR_Address(addr, _) => {
let eares : MemoryOpResult(unit) = match (width, sizeof(xlen)) {
(BYTE, _) => mem_write_ea(addr, 1, aq & rl, rl, true),
(HALF, _) => mem_write_ea(addr, 2, aq & rl, rl, true),
(WORD, _) => mem_write_ea(addr, 4, aq & rl, rl, true),
(DOUBLE, 64) => mem_write_ea(addr, 8, aq & rl, rl, true),
_ => internal_error(__FILE__, __LINE__, "Unexpected AMO width")
};
let is_unsigned : bool = match op {
AMOMINU => true,
AMOMAXU => true,
_ => false
};
let rs2_val : xlenbits = match width {
BYTE => if is_unsigned then zero_extend(X(rs2)[7..0]) else sign_extend(X(rs2)[7..0]),
HALF => if is_unsigned then zero_extend(X(rs2)[15..0]) else sign_extend(X(rs2)[15..0]),
WORD => if is_unsigned then zero_extend(X(rs2)[31..0]) else sign_extend(X(rs2)[31..0]),
DOUBLE => X(rs2)
};
let eares = mem_write_ea(addr, width_bytes, aq & rl, rl, true);
let rs2_val = X(rs2)[width_bytes * 8 - 1 .. 0];
match (eares) {
MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
MemValue(_) => {
let mval : MemoryOpResult(xlenbits) = match (width, sizeof(xlen)) {
(BYTE, _) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 1, aq, aq & rl, true)),
(HALF, _) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 2, aq, aq & rl, true)),
(WORD, _) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 4, aq, aq & rl, true)),
(DOUBLE, 64) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 8, aq, aq & rl, true)),
_ => internal_error(__FILE__, __LINE__, "Unexpected AMO width")
};
match (mval) {
match mem_read(ReadWrite(Data, Data), addr, width_bytes, aq, aq & rl, true) {
MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
MemValue(loaded) => {
let result : xlenbits =
let result : bits('width_bytes * 8) =
match op {
AMOSWAP => rs2_val,
AMOADD => rs2_val + loaded,
AMOXOR => rs2_val ^ loaded,
AMOAND => rs2_val & loaded,
AMOOR => rs2_val | loaded,

/* These operations convert bitvectors to integer values using [un]signed,
* and back using to_bits().
*/
AMOMIN => to_bits(sizeof(xlen), min(signed(rs2_val), signed(loaded))),
AMOMAX => to_bits(sizeof(xlen), max(signed(rs2_val), signed(loaded))),
AMOMINU => to_bits(sizeof(xlen), min(unsigned(rs2_val), unsigned(loaded))),
AMOMAXU => to_bits(sizeof(xlen), max(unsigned(rs2_val), unsigned(loaded)))
AMOMIN => if rs2_val <_s loaded then rs2_val else loaded,
AMOMAX => if rs2_val >_s loaded then rs2_val else loaded,
AMOMINU => if rs2_val <_u loaded then rs2_val else loaded,
AMOMAXU => if rs2_val >_u loaded then rs2_val else loaded,
};
let rval : xlenbits = match width {
BYTE => sign_extend(loaded[7..0]),
HALF => sign_extend(loaded[15..0]),
WORD => sign_extend(loaded[31..0]),
DOUBLE => loaded
};
let wval : MemoryOpResult(bool) = match (width, sizeof(xlen)) {
(BYTE, _) => mem_write_value(addr, 1, result[7..0], aq & rl, rl, true),
(HALF, _) => mem_write_value(addr, 2, result[15..0], aq & rl, rl, true),
(WORD, _) => mem_write_value(addr, 4, result[31..0], aq & rl, rl, true),
(DOUBLE, 64) => mem_write_value(addr, 8, result, aq & rl, rl, true),
_ => internal_error(__FILE__, __LINE__, "Unexpected AMO width")
};
match (wval) {
MemValue(true) => { X(rd) = rval; RETIRE_SUCCESS },
match mem_write_value(addr, width_bytes, sign_extend(result), aq & rl, rl, true) {
MemValue(true) => { X(rd) = sign_extend(loaded); RETIRE_SUCCESS },
MemValue(false) => { internal_error(__FILE__, __LINE__, "AMO got false from mem_write_value") },
MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }
}
Expand Down
Loading

0 comments on commit 4fbb701

Please sign in to comment.