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

Add ratified Zacas extension #285

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
Open

Add ratified Zacas extension #285

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
ac3ae36
fix merge conflicts
ved-rivos Apr 14, 2024
acdf844
Add Zacas extension
ved-rivos Jul 14, 2023
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
7 changes: 7 additions & 0 deletions model/riscv_addr_checks.sail
View file
Open in desktop
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
Open in desktop
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
Open in desktop
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
Loading
Loading