Skip to content

Commit

Permalink
Add Zacas extension
Browse files Browse the repository at this point in the history
  • Loading branch information
@ved-rivos
ved-rivos committed Apr 14, 2024
1 parent ac3ae36 commit acdf844
Show file tree
Hide file tree
Showing 3 changed files with 168 additions and 57 deletions.
7 changes: 7 additions & 0 deletions model/riscv_addr_checks.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -59,6 +59,13 @@ function ext_data_get_addr(base : regidx, offset : xlenbits, acc : AccessType(ex
let addr = X(base) + offset in
Ext_DataAddr_OK(addr)

/* Default AMO data addr is just base register.
Extensions might override and add additional checks. */
function ext_data_get_amo_addr(base : regidx, acc : AccessType(ext_access_type), width : amo_word_width)
-> Ext_DataAddr_Check(ext_data_addr_error) =
let addr = X(base) in
Ext_DataAddr_OK(addr)

function ext_handle_data_check_error(err : ext_data_addr_error) -> unit =
()

Expand Down
215 changes: 158 additions & 57 deletions model/riscv_insts_aext.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,7 @@ function lrsc_width_str(width : word_width) -> string =
* RISC-V only appears to define LR / SC / AMOs for word and double, although
* there seem to be encodings reserved for other widths.
*/
function amo_width_valid(size : word_width) -> bool = {
function lrsc_width_valid(size : word_width) -> bool = {
match(size) {
WORD => true,
DOUBLE => sizeof(xlen) >= 64,
Expand All @@ -43,9 +43,8 @@ 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_enc(size) @ rd @ 0b0101111 if amo_width_valid(size)

mapping clause encdec = LOADRES(aq, rl, rs1, size, rd) if lrsc_width_valid(size)
<-> 0b00010 @ bool_bits(aq) @ bool_bits(rl) @ 0b00000 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if lrsc_width_valid(size)

/* We could set load-reservations on physical or virtual addresses.
* For now we set them on virtual addresses, since it makes the
Expand Down Expand Up @@ -108,8 +107,8 @@ 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_enc(size) @ rd @ 0b0101111 if amo_width_valid(size)
mapping clause encdec = STORECON(aq, rl, rs2, rs1, size, rd) if lrsc_width_valid(size)
<-> 0b00011 @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if lrsc_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 @@ -192,7 +191,7 @@ mapping clause assembly = STORECON(aq, rl, rs2, rs1, size, rd)
<-> "sc." ^ size_mnemonic(size) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs2) ^ sep() ^ "(" ^ reg_name(rs1) ^ ")"

/* ****************************************************************** */
union clause ast = AMO : (amoop, bool, bool, regidx, regidx, word_width, regidx)
union clause ast = AMO : (amoop, bool, bool, regidx, regidx, amo_word_width, regidx)

mapping encdec_amoop : amoop <-> bits(5) = {
AMOSWAP <-> 0b00001,
Expand All @@ -203,11 +202,33 @@ mapping encdec_amoop : amoop <-> bits(5) = {
AMOMIN <-> 0b10000,
AMOMAX <-> 0b10100,
AMOMINU <-> 0b11000,
AMOMAXU <-> 0b11100
AMOMAXU <-> 0b11100,
AMOCAS <-> 0b00101
}

/**
* RISC-V only appears to define AMO for word and double, although
* there seem to be encodings reserved for other widths.
* zacas: amocas.d supported for RV32 and amocas.q for RV64
* amocas that operate on 2*XLEN data requires the first register
* of the register pair to be even numbered. RV32 supports amocas.d.
*/
function amo_encoding_valid(size : amo_word_width, op : amoop, rs2 : regidx, rd : regidx ) -> bool = {
match(size, sizeof(xlen), op) {
(AMO_WORD, 32, AMOCAS) => haveZacas(),
(AMO_WORD, 64, AMOCAS) => haveZacas(),
(AMO_WORD, _, _) => true,
(AMO_DOUBLE, 32, AMOCAS) => if rs2[0..0] != 0b0 | rd[0..0] != 0b0 then false else haveZacas(),
(AMO_DOUBLE, 64, AMOCAS) => haveZacas(),
(AMO_DOUBLE, _, _) => sizeof(xlen) >= 64,
(AMO_QUAD, 64, AMOCAS) => if rs2[0..0] != 0b0 | rd[0..0] != 0b0 then false else haveZacas(),
(AMO_QUAD, _, _) => false,
_ => false
}
}

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_enc(size) @ rd @ 0b0101111 if amo_width_valid(size)
mapping clause encdec = AMO(op, aq, rl, rs2, rs1, size, rd) if amo_encoding_valid(size, op, rs2, rd)
<-> encdec_amoop(op) @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ amo_size_enc(size) @ rd @ 0b0101111 if amo_encoding_valid(size, op, rs2, rd)

/* NOTE: Currently, we only EA if address translation is successful.
This may need revisiting. */
Expand All @@ -216,76 +237,155 @@ 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_amo_addr(rs1, ReadWrite(Data, Data), width) {
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),
(AMO_BYTE, _) => mem_write_ea(addr, 1, aq & rl, rl, true),
(AMO_HALF, _) => mem_write_ea(addr, 2, aq & rl, rl, true),
(AMO_WORD, _) => mem_write_ea(addr, 4, aq & rl, rl, true),
(AMO_DOUBLE, _) => mem_write_ea(addr, 8, aq & rl, rl, true),
(AMO_QUAD, 64) => mem_write_ea(addr, 16, aq & rl, rl, true),
_ => internal_error(__FILE__, __LINE__, "Unexpected AMO width")
};
let is_unsigned : bool = match op {
AMOMINU => true,
AMOMAXU => true,
_ => false
};
let rd_val : xlenbits = match width {
AMO_BYTE => if is_unsigned then zero_extend(X(rd)[7..0]) else sign_extend(X(rd)[7..0]),
AMO_HALF => if is_unsigned then zero_extend(X(rd)[15..0]) else sign_extend(X(rd)[15..0]),
AMO_WORD => if is_unsigned then zero_extend(X(rd)[31..0]) else sign_extend(X(rd)[31..0]),
AMO_DOUBLE => X(rd),
AMO_QUAD => X(rd)
};
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)
AMO_BYTE => if is_unsigned then zero_extend(X(rs2)[7..0]) else sign_extend(X(rs2)[7..0]),
AMO_HALF => if is_unsigned then zero_extend(X(rs2)[15..0]) else sign_extend(X(rs2)[15..0]),
AMO_WORD => if is_unsigned then zero_extend(X(rs2)[31..0]) else sign_extend(X(rs2)[31..0]),
AMO_DOUBLE => X(rs2),
AMO_QUAD => X(rs2)
};
/* AMOCAS.W for RV32 and AMOCAS.Q for RV64 operate on a pair of
* register. When the first register of a source register pair is
* x0, then both halves of the pair read as zero.
*/
let rd_plus_one : regidx =
match (width, sizeof(xlen), op) {
(AMO_DOUBLE, 32, AMOCAS) => if (rd != zreg) then (rd + 1) else zeros(),
(AMO_QUAD, 64, AMOCAS) => if (rd != zreg) then (rd + 1) else zeros(),
_ => zeros()
};
let rs2_plus_one : regidx =
match (width, sizeof(xlen), op) {
(AMO_DOUBLE, 32, AMOCAS) => if (rs2 != zreg) then (rs2 + 1) else zeros(),
(AMO_QUAD, 64, AMOCAS) => if (rs2 != zreg) then (rs2 + 1) else zeros(),
_ => zeros()
};
let rd_plus_one_val : xlenbits = zero_extend(X(rd_plus_one));
let rs2_plus_one_val : xlenbits = zero_extend(X(rs2_plus_one));
/* AMOCAS has release semantics only if AMOCAS is successful */
let amo_rd_rl : bool = match op {
AMOCAS => false,
_ => aq & rl
};
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)),
(AMO_BYTE, _) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 1, aq, amo_rd_rl, true)),
(AMO_HALF, _) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 2, aq, amo_rd_rl, true)),
(AMO_WORD, _) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 4, aq, amo_rd_rl, true)),
(AMO_DOUBLE, 64) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 8, aq, amo_rd_rl, true)),
(AMO_DOUBLE, 32) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 4, aq, amo_rd_rl, true)),
(AMO_QUAD, 64) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr, 8, aq, amo_rd_rl, true)),
_ => internal_error(__FILE__, __LINE__, "Unexpected AMO width")
};
let mval_high : MemoryOpResult(xlenbits) = match (width, sizeof(xlen)) {
(AMO_DOUBLE, 32) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr+4, 4, aq, amo_rd_rl, true)),
(AMO_QUAD, 64) => extend_value(is_unsigned, mem_read(ReadWrite(Data, Data), addr+8, 8, aq, amo_rd_rl, true)),
_ => MemValue(zeros())
};
match (mval) {
MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
MemValue(loaded) => {
let result : xlenbits =
match op {
AMOSWAP => rs2_val,
AMOADD => rs2_val + loaded,
AMOXOR => rs2_val ^ loaded,
AMOAND => rs2_val & loaded,
AMOOR => rs2_val | loaded,
match (mval_high) {
MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL },
MemValue(loaded_high) => {
let result : xlenbits =
match op {
AMOSWAP => rs2_val,
AMOADD => rs2_val + loaded,
AMOXOR => rs2_val ^ loaded,
AMOAND => rs2_val & loaded,
AMOOR => rs2_val | loaded,
AMOCAS => rs2_val,

/* 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)))
};
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 },
MemValue(false) => { internal_error(__FILE__, __LINE__, "AMO got false from mem_write_value") },
MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }
/* 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)))
};
let result_high : xlenbits =
match op {
AMOCAS => rs2_plus_one_val,
_ => zeros(),
};
let amo_does_write : bool =
match (op, sizeof(xlen), width) {
(AMOCAS, 32, AMO_WORD) => if ( loaded == rd_val ) then true else false,
(AMOCAS, 32, AMO_DOUBLE) => if ( loaded == rd_val & loaded_high == rd_plus_one_val ) then true else false,
(AMOCAS, 64, AMO_WORD) => if ( loaded == rd_val ) then true else false,
(AMOCAS, 64, AMO_DOUBLE) => if ( loaded == rd_val ) then true else false,
(AMOCAS, 64, AMO_QUAD) => if ( loaded == rd_val & loaded_high == rd_plus_one_val ) then true else false,
(_, _, _) => true
};
let rval : xlenbits = match width {
AMO_BYTE => sign_extend(loaded[7..0]),
AMO_HALF => sign_extend(loaded[15..0]),
AMO_WORD => sign_extend(loaded[31..0]),
AMO_DOUBLE => loaded,
AMO_QUAD => loaded
};
let rval_high : xlenbits = match width {
AMO_DOUBLE => loaded_high,
AMO_QUAD => loaded_high,
_ => zeros()
};
let wval : MemoryOpResult(bool) = match (width, sizeof(xlen), amo_does_write) {
(AMO_BYTE, _, true) => mem_write_value(addr, 1, result[7..0], aq & rl, rl, true),
(AMO_HALF, _, true) => mem_write_value(addr, 2, result[15..0], aq & rl, rl, true),
(AMO_WORD, _, true) => mem_write_value(addr, 4, result[31..0], aq & rl, rl, true),
(AMO_DOUBLE, 32, true) => mem_write_value(addr, 4, result, aq & rl, rl, true),
(AMO_DOUBLE, 64, true) => mem_write_value(addr, 8, result, aq & rl, rl, true),
(AMO_QUAD, 64, true) => mem_write_value(addr, 8, result, aq & rl, rl, true),
_ => MemValue(true)
};
match (wval) {
MemValue(true) => {
let wval_high : MemoryOpResult(bool) =
match (width, sizeof(xlen), amo_does_write) {
(AMO_DOUBLE, 32, true) => mem_write_value(addr+4, 4, result_high, aq & rl, rl, true),
(AMO_QUAD, 64, true) => mem_write_value(addr+8, 8, result_high, aq & rl, rl, true),
_ => MemValue(true)
};
match (wval_high) {
MemValue(true) => { X(rd) = rval; X(rd_plus_one) = rval_high; RETIRE_SUCCESS},
MemValue(false) => { internal_error(__FILE__, __LINE__, "AMO got false from mem_write_value") },
MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }
}
},
MemValue(false) => { internal_error(__FILE__, __LINE__, "AMO got false from mem_write_value") },
MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }
}
}
}
}
}
Expand All @@ -310,8 +410,9 @@ mapping amo_mnemonic : amoop <-> string = {
AMOMIN <-> "amomin",
AMOMAX <-> "amomax",
AMOMINU <-> "amominu",
AMOMAXU <-> "amomaxu"
AMOMAXU <-> "amomaxu",
AMOCAS <-> "amocas"
}

mapping clause assembly = AMO(op, aq, rl, rs2, rs1, width, rd)
<-> amo_mnemonic(op) ^ "." ^ size_mnemonic(width) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs2) ^ sep() ^ "(" ^ reg_name(rs1) ^ ")"
<-> amo_mnemonic(op) ^ "." ^ amo_size_mnemonic(width) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs2) ^ sep() ^ "(" ^ reg_name(rs1) ^ ")"
3 changes: 3 additions & 0 deletions model/riscv_sys_regs.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -160,6 +160,9 @@ function haveZmmul() -> bool = true
/* Zicond extension support */
function haveZicond() -> bool = true

/* Zacas extension support. */
function haveZacas() -> bool = true

bitfield Mstatush : bits(32) = {
MBE : 5,
SBE : 4
Expand Down

0 comments on commit acdf844

Please sign in to comment.