aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--model/riscv_ext_regs.sail2
-rw-r--r--model/riscv_insts_aext.sail337
-rw-r--r--model/riscv_insts_mext.sail54
-rw-r--r--model/riscv_insts_vext_vset.sail178
-rw-r--r--model/riscv_insts_zbb.sail24
-rw-r--r--model/riscv_insts_zbc.sail6
-rw-r--r--model/riscv_insts_zbkb.sail6
-rw-r--r--model/riscv_insts_zbkx.sail4
-rw-r--r--model/riscv_insts_zicsr.sail2
-rw-r--r--model/riscv_pmp_control.sail43
-rwxr-xr-xmodel/riscv_vreg_type.sail1
11 files changed, 318 insertions, 339 deletions
diff --git a/model/riscv_ext_regs.sail b/model/riscv_ext_regs.sail
index 28ed111..efe9bae 100644
--- a/model/riscv_ext_regs.sail
+++ b/model/riscv_ext_regs.sail
@@ -28,7 +28,7 @@ function ext_rvfi_init () = {
THIS(csrno, priv, isWrite) allows an extension to block access to csrno,
at Privilege level priv. It should return true if the access is allowed.
*/
-val ext_check_CSR : (bits(12), Privilege, bool) -> bool
+val ext_check_CSR : (csreg, Privilege, bool) -> bool
function ext_check_CSR (csrno, p, isWrite) = true
/*!
diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail
index 0f4da83..2e0eb9c 100644
--- a/model/riscv_insts_aext.sail
+++ b/model/riscv_insts_aext.sail
@@ -43,8 +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 haveAtomics() & amo_width_valid(size)
+ <-> 0b00010 @ bool_bits(aq) @ bool_bits(rl) @ 0b00000 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if haveAtomics() & amo_width_valid(size)
/* We could set load-reservations on physical or virtual addresses.
@@ -61,44 +61,39 @@ function process_loadres(rd, addr, value, is_unsigned) =
}
function clause execute(LOADRES(aq, rl, rs1, width, rd)) = {
- if haveAtomics() then {
- /* 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) {
- 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)
- 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")
- }
- }
- }
+ /* 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) {
+ 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)
+ 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")
+ }
+ }
}
- } else {
- handle_illegal();
- RETIRE_FAIL
}
}
@@ -108,8 +103,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 haveAtomics() & amo_width_valid(size)
+ <-> 0b00011 @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if haveAtomics() & 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)) = {
@@ -119,60 +114,58 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
*/
X(rd) = zero_extend(0b1); RETIRE_SUCCESS
} else {
- if haveAtomics() then {
- /* normal non-rmem case
- * rmem: SC is allowed to succeed (but might fail later)
- */
- /* 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) {
- 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)
- then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL }
- else {
- if match_reservation(vaddr) == false then {
- /* cannot happen in rmem */
- X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS
- } else {
- match translateAddr(vaddr, Write(Data)) { /* Write and ReadWrite are equivalent here:
- * 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")
- };
- 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) {
- 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 }
- }
+ /* normal non-rmem case
+ * rmem: SC is allowed to succeed (but might fail later)
+ */
+ /* 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) {
+ 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)
+ then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL }
+ else {
+ if match_reservation(vaddr) == false then {
+ /* cannot happen in rmem */
+ X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS
+ } else {
+ match translateAddr(vaddr, Write(Data)) { /* Write and ReadWrite are equivalent here:
+ * 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")
+ };
+ 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) {
+ 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 }
}
}
}
@@ -181,9 +174,6 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
}
}
}
- } else {
- handle_illegal();
- RETIRE_FAIL
}
}
}
@@ -206,87 +196,85 @@ mapping encdec_amoop : amoop <-> bits(5) = {
AMOMAXU <-> 0b11100
}
-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 haveAtomics() & amo_width_valid(size)
+ <-> encdec_amoop(op) @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if haveAtomics() & amo_width_valid(size)
/* 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)) = {
- if haveAtomics() then {
- /* 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) {
- 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)
- };
- 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) {
- 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,
+ /* 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) {
+ 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)
+ };
+ 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) {
+ 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,
- /* 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
+ /* 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 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 }
- }
+ 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 }
}
}
}
@@ -295,9 +283,6 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
}
}
}
- } else {
- handle_illegal();
- RETIRE_FAIL
}
}
diff --git a/model/riscv_insts_mext.sail b/model/riscv_insts_mext.sail
index 6bf94ee..d7f9dc7 100644
--- a/model/riscv_insts_mext.sail
+++ b/model/riscv_insts_mext.sail
@@ -20,11 +20,10 @@ mapping encdec_mul_op : mul_op <-> bits(3) = {
struct { high = true, signed_rs1 = false, signed_rs2 = false } <-> 0b011
}
-mapping clause encdec = MUL(rs2, rs1, rd, mul_op)
- <-> 0b0000001 @ rs2 @ rs1 @ encdec_mul_op(mul_op) @ rd @ 0b0110011
+mapping clause encdec = MUL(rs2, rs1, rd, mul_op) if haveMulDiv() | haveZmmul()
+ <-> 0b0000001 @ rs2 @ rs1 @ encdec_mul_op(mul_op) @ rd @ 0b0110011 if haveMulDiv() | haveZmmul()
function clause execute (MUL(rs2, rs1, rd, mul_op)) = {
- if haveMulDiv() | haveZmmul() then {
let rs1_val = X(rs1);
let rs2_val = X(rs2);
let rs1_int : int = if mul_op.signed_rs1 then signed(rs1_val) else unsigned(rs1_val);
@@ -35,10 +34,6 @@ function clause execute (MUL(rs2, rs1, rd, mul_op)) = {
else result_wide[(sizeof(xlen) - 1) .. 0];
X(rd) = result;
RETIRE_SUCCESS
- } else {
- handle_illegal();
- RETIRE_FAIL
- }
}
mapping mul_mnemonic : mul_op <-> string = {
@@ -54,11 +49,10 @@ mapping clause assembly = MUL(rs2, rs1, rd, mul_op)
/* ****************************************************************** */
union clause ast = DIV : (regidx, regidx, regidx, bool)
-mapping clause encdec = DIV(rs2, rs1, rd, s)
- <-> 0b0000001 @ rs2 @ rs1 @ 0b10 @ bool_not_bits(s) @ rd @ 0b0110011
+mapping clause encdec = DIV(rs2, rs1, rd, s) if haveMulDiv()
+ <-> 0b0000001 @ rs2 @ rs1 @ 0b10 @ bool_not_bits(s) @ rd @ 0b0110011 if haveMulDiv()
function clause execute (DIV(rs2, rs1, rd, s)) = {
- if haveMulDiv() then {
let rs1_val = X(rs1);
let rs2_val = X(rs2);
let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val);
@@ -68,10 +62,6 @@ function clause execute (DIV(rs2, rs1, rd, s)) = {
let q': int = if s & q > xlen_max_signed then xlen_min_signed else q;
X(rd) = to_bits(sizeof(xlen), q');
RETIRE_SUCCESS
- } else {
- handle_illegal();
- RETIRE_FAIL
- }
}
mapping maybe_not_u : bool <-> string = {
@@ -85,11 +75,10 @@ mapping clause assembly = DIV(rs2, rs1, rd, s)
/* ****************************************************************** */
union clause ast = REM : (regidx, regidx, regidx, bool)
-mapping clause encdec = REM(rs2, rs1, rd, s)
- <-> 0b0000001 @ rs2 @ rs1 @ 0b11 @ bool_not_bits(s) @ rd @ 0b0110011
+mapping clause encdec = REM(rs2, rs1, rd, s) if haveMulDiv()
+ <-> 0b0000001 @ rs2 @ rs1 @ 0b11 @ bool_not_bits(s) @ rd @ 0b0110011 if haveMulDiv()
function clause execute (REM(rs2, rs1, rd, s)) = {
- if haveMulDiv() then {
let rs1_val = X(rs1);
let rs2_val = X(rs2);
let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val);
@@ -98,10 +87,6 @@ function clause execute (REM(rs2, rs1, rd, s)) = {
/* signed overflow case returns zero naturally as required due to -1 divisor */
X(rd) = to_bits(sizeof(xlen), r);
RETIRE_SUCCESS
- } else {
- handle_illegal();
- RETIRE_FAIL
- }
}
mapping clause assembly = REM(rs2, rs1, rd, s)
@@ -111,12 +96,11 @@ mapping clause assembly = REM(rs2, rs1, rd, s)
union clause ast = MULW : (regidx, regidx, regidx)
mapping clause encdec = MULW(rs2, rs1, rd)
- if sizeof(xlen) == 64
+ if sizeof(xlen) == 64 & (haveMulDiv() | haveZmmul())
<-> 0b0000001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011
- if sizeof(xlen) == 64
+ if sizeof(xlen) == 64 & (haveMulDiv() | haveZmmul())
function clause execute (MULW(rs2, rs1, rd)) = {
- if haveMulDiv() | haveZmmul() then {
let rs1_val = X(rs1)[31..0];
let rs2_val = X(rs2)[31..0];
let rs1_int : int = signed(rs1_val);
@@ -126,10 +110,6 @@ function clause execute (MULW(rs2, rs1, rd)) = {
let result : xlenbits = sign_extend(result32);
X(rd) = result;
RETIRE_SUCCESS
- } else {
- handle_illegal();
- RETIRE_FAIL
- }
}
mapping clause assembly = MULW(rs2, rs1, rd)
@@ -141,12 +121,11 @@ mapping clause assembly = MULW(rs2, rs1, rd)
union clause ast = DIVW : (regidx, regidx, regidx, bool)
mapping clause encdec = DIVW(rs2, rs1, rd, s)
- if sizeof(xlen) == 64
+ if sizeof(xlen) == 64 & haveMulDiv()
<-> 0b0000001 @ rs2 @ rs1 @ 0b10 @ bool_not_bits(s) @ rd @ 0b0111011
- if sizeof(xlen) == 64
+ if sizeof(xlen) == 64 & haveMulDiv()
function clause execute (DIVW(rs2, rs1, rd, s)) = {
- if haveMulDiv() then {
let rs1_val = X(rs1)[31..0];
let rs2_val = X(rs2)[31..0];
let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val);
@@ -156,10 +135,6 @@ function clause execute (DIVW(rs2, rs1, rd, s)) = {
let q': int = if s & q > (2 ^ 31 - 1) then (0 - 2^31) else q;
X(rd) = sign_extend(to_bits(32, q'));
RETIRE_SUCCESS
- } else {
- handle_illegal();
- RETIRE_FAIL
- }
}
mapping clause assembly = DIVW(rs2, rs1, rd, s)
@@ -171,12 +146,11 @@ mapping clause assembly = DIVW(rs2, rs1, rd, s)
union clause ast = REMW : (regidx, regidx, regidx, bool)
mapping clause encdec = REMW(rs2, rs1, rd, s)
- if sizeof(xlen) == 64
+ if sizeof(xlen) == 64 & haveMulDiv()
<-> 0b0000001 @ rs2 @ rs1 @ 0b11 @ bool_not_bits(s) @ rd @ 0b0111011
- if sizeof(xlen) == 64
+ if sizeof(xlen) == 64 & haveMulDiv()
function clause execute (REMW(rs2, rs1, rd, s)) = {
- if haveMulDiv() then {
let rs1_val = X(rs1)[31..0];
let rs2_val = X(rs2)[31..0];
let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val);
@@ -185,10 +159,6 @@ function clause execute (REMW(rs2, rs1, rd, s)) = {
/* signed overflow case returns zero naturally as required due to -1 divisor */
X(rd) = sign_extend(to_bits(32, r));
RETIRE_SUCCESS
- } else {
- handle_illegal();
- RETIRE_FAIL
- }
}
mapping clause assembly = REMW(rs2, rs1, rd, s)
diff --git a/model/riscv_insts_vext_vset.sail b/model/riscv_insts_vext_vset.sail
index abd5587..40a7ea9 100644
--- a/model/riscv_insts_vext_vset.sail
+++ b/model/riscv_insts_vext_vset.sail
@@ -41,60 +41,54 @@ mapping maybe_ma_flag : string <-> bits(1) = {
sep() ^ "mu" <-> 0b0
}
-/* ****************************** vsetvli & vsetvl ******************************* */
-union clause ast = VSET_TYPE : (vsetop, bits(1), bits(1), bits(3), bits(3), regidx, regidx)
+val handle_illegal_vtype : unit -> unit
+function handle_illegal_vtype() = {
+ /* Note: Implementations can set vill or trap if the vtype setting is not supported.
+ * TODO: configuration support for both solutions
+ */
+ vtype.bits = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */
+ vl = zeros();
+ print_reg("CSR vtype <- " ^ BitStr(vtype.bits));
+ print_reg("CSR vl <- " ^ BitStr(vl))
+}
-mapping encdec_vsetop : vsetop <-> bits(4) ={
- VSETVLI <-> 0b0000,
- VSETVL <-> 0b1000
+val calculate_new_vl : (int, int) -> xlenbits
+function calculate_new_vl(AVL, VLMAX) = {
+ /* Note: ceil(AVL / 2) ≤ vl ≤ VLMAX when VLMAX < AVL < (2 * VLMAX)
+ * TODO: configuration support for either using ceil(AVL / 2) or VLMAX
+ */
+ if AVL <= VLMAX then to_bits(sizeof(xlen), AVL)
+ else if AVL < 2 * VLMAX then to_bits(sizeof(xlen), (AVL + 1) / 2)
+ else to_bits(sizeof(xlen), VLMAX)
}
-mapping clause encdec = VSET_TYPE(op, ma, ta, sew, lmul, rs1, rd) if haveVExt()
- <-> encdec_vsetop(op) @ ma @ ta @ sew @ lmul @ rs1 @ 0b111 @ rd @ 0b1010111 if haveVExt()
+/* *********************************** vsetvli *********************************** */
+union clause ast = VSETVLI : (bits(1), bits(1), bits(3), bits(3), regidx, regidx)
-function clause execute VSET_TYPE(op, ma, ta, sew, lmul, rs1, rd) = {
- let VLEN_pow = get_vlen_pow();
- let ELEN_pow = get_elen_pow();
+mapping clause encdec = VSETVLI(ma, ta, sew, lmul, rs1, rd) if haveVExt()
+ <-> 0b0000 @ ma @ ta @ sew @ lmul @ rs1 @ 0b111 @ rd @ 0b1010111 if haveVExt()
+
+function clause execute VSETVLI(ma, ta, sew, lmul, rs1, rd) = {
let LMUL_pow_ori = get_lmul_pow();
let SEW_pow_ori = get_sew_pow();
let ratio_pow_ori = SEW_pow_ori - LMUL_pow_ori;
/* set vtype */
- match op {
- VSETVLI => {
- vtype.bits = 0b0 @ zeros(sizeof(xlen) - 9) @ ma @ ta @ sew @ lmul
- },
- VSETVL => {
- let rs2 : regidx = sew[1 .. 0] @ lmul;
- vtype.bits = X(rs2)
- }
- };
+ vtype.bits = 0b0 @ zeros(sizeof(xlen) - 9) @ ma @ ta @ sew @ lmul;
- /* check legal SEW and LMUL and calculate VLMAX */
+ /* check new SEW and LMUL are legal and calculate VLMAX */
+ let VLEN_pow = get_vlen_pow();
+ let ELEN_pow = get_elen_pow();
let LMUL_pow_new = get_lmul_pow();
let SEW_pow_new = get_sew_pow();
- if SEW_pow_new > LMUL_pow_new + ELEN_pow then {
- /* Note: Implementations can set vill or trap if the vtype setting is not supported.
- * TODO: configuration support for both solutions
- */
- vtype.bits = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */
- vl = zeros();
- print_reg("CSR vtype <- " ^ BitStr(vtype.bits));
- print_reg("CSR vl <- " ^ BitStr(vl));
- return RETIRE_SUCCESS
- };
+ if SEW_pow_new > (LMUL_pow_new + ELEN_pow) then { handle_illegal_vtype(); return RETIRE_SUCCESS };
let VLMAX = int_power(2, VLEN_pow + LMUL_pow_new - SEW_pow_new);
/* set vl according to VLMAX and AVL */
if (rs1 != 0b00000) then { /* normal stripmining */
let rs1_val = X(rs1);
let AVL = unsigned(rs1_val);
- vl = if AVL <= VLMAX then to_bits(sizeof(xlen), AVL)
- else if AVL < 2 * VLMAX then to_bits(sizeof(xlen), (AVL + 1) / 2)
- else to_bits(sizeof(xlen), VLMAX);
- /* Note: ceil(AVL / 2) ≤ vl ≤ VLMAX when VLMAX < AVL < (2 * VLMAX)
- * TODO: configuration support for either using ceil(AVL / 2) or VLMAX
- */
+ vl = calculate_new_vl(AVL, VLMAX);
X(rd) = vl;
} else if (rd != 0b00000) then { /* set vl to VLMAX */
let AVL = unsigned(ones(sizeof(xlen)));
@@ -103,81 +97,105 @@ function clause execute VSET_TYPE(op, ma, ta, sew, lmul, rs1, rd) = {
} else { /* keep existing vl */
let AVL = unsigned(vl);
let ratio_pow_new = SEW_pow_new - LMUL_pow_new;
- if (ratio_pow_new != ratio_pow_ori) then {
- /* Note: Implementations can set vill or trap if the vtype setting is not supported.
- * TODO: configuration support for both solutions
- */
- vtype.bits = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */
- vl = zeros();
- }
+ if (ratio_pow_new != ratio_pow_ori) then { handle_illegal_vtype(); return RETIRE_SUCCESS }
};
- print_reg("CSR vtype <- " ^ BitStr(vtype.bits));
- print_reg("CSR vl <- " ^ BitStr(vl));
/* reset vstart to 0 */
vstart = zeros();
+
+ print_reg("CSR vtype <- " ^ BitStr(vtype.bits));
+ print_reg("CSR vl <- " ^ BitStr(vl));
print_reg("CSR vstart <- " ^ BitStr(vstart));
RETIRE_SUCCESS
}
-mapping vsettype_mnemonic : vsetop <-> string ={
- VSETVLI <-> "vsetvli",
- VSETVL <-> "vsetvli"
-}
+mapping clause assembly = VSETVLI(ma, ta, sew, lmul, rs1, rd)
+ <-> "vsetvli" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ sew_flag(sew) ^ maybe_lmul_flag(lmul) ^ maybe_ta_flag(ta) ^ maybe_ma_flag(ma)
-mapping clause assembly = VSET_TYPE(op, ma, ta, sew, lmul, rs1, rd)
- <-> vsettype_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ sew_flag(sew) ^ maybe_lmul_flag(lmul) ^ maybe_ta_flag(ta) ^ maybe_ma_flag(ma)
+/* *********************************** vsetvl ************************************ */
+union clause ast = VSETVL : (regidx, regidx, regidx)
-/* ********************************* vsetivli ************************************ */
-union clause ast = VSETI_TYPE : ( bits(1), bits(1), bits(3), bits(3), regidx, regidx)
+mapping clause encdec = VSETVL(rs2, rs1, rd) if haveVExt()
+ <-> 0b1000000 @ rs2 @ rs1 @ 0b111 @ rd @ 0b1010111 if haveVExt()
-mapping clause encdec = VSETI_TYPE(ma, ta, sew, lmul, uimm, rd) if haveVExt()
- <-> 0b1100 @ ma @ ta @ sew @ lmul @ uimm @ 0b111 @ rd @ 0b1010111 if haveVExt()
-
-function clause execute VSETI_TYPE(ma, ta, sew, lmul, uimm, rd) = {
- let VLEN_pow = get_vlen_pow();
- let ELEN_pow = get_elen_pow();
+function clause execute VSETVL(rs2, rs1, rd) = {
let LMUL_pow_ori = get_lmul_pow();
let SEW_pow_ori = get_sew_pow();
let ratio_pow_ori = SEW_pow_ori - LMUL_pow_ori;
/* set vtype */
- vtype.bits = 0b0 @ zeros(sizeof(xlen) - 9) @ ma @ ta @ sew @ lmul;
+ vtype.bits = X(rs2);
- /* check legal SEW and LMUL and calculate VLMAX */
+ /* check new SEW and LMUL are legal and calculate VLMAX */
+ let VLEN_pow = get_vlen_pow();
+ let ELEN_pow = get_elen_pow();
let LMUL_pow_new = get_lmul_pow();
let SEW_pow_new = get_sew_pow();
- if SEW_pow_new > LMUL_pow_new + ELEN_pow then {
- /* Note: Implementations can set vill or trap if the vtype setting is not supported.
- * TODO: configuration support for both solutions
- */
- vtype.bits = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */
- vl = zeros();
- print_reg("CSR vtype <- " ^ BitStr(vtype.bits));
- print_reg("CSR vl <- " ^ BitStr(vl));
- return RETIRE_SUCCESS
- };
+ if SEW_pow_new > (LMUL_pow_new + ELEN_pow) then { handle_illegal_vtype(); return RETIRE_SUCCESS };
let VLMAX = int_power(2, VLEN_pow + LMUL_pow_new - SEW_pow_new);
- let AVL = unsigned(uimm); /* AVL is encoded as 5-bit zero-extended imm in the rs1 field */
/* set vl according to VLMAX and AVL */
- vl = if AVL <= VLMAX then to_bits(sizeof(xlen), AVL)
- else if AVL < 2 * VLMAX then to_bits(sizeof(xlen), (AVL + 1) / 2)
- else to_bits(sizeof(xlen), VLMAX);
- /* Note: ceil(AVL / 2) ≤ vl ≤ VLMAX when VLMAX < AVL < (2 * VLMAX)
- * TODO: configuration support for either using ceil(AVL / 2) or VLMAX
- */
- X(rd) = vl;
+ if (rs1 != 0b00000) then { /* normal stripmining */
+ let rs1_val = X(rs1);
+ let AVL = unsigned(rs1_val);
+ vl = calculate_new_vl(AVL, VLMAX);
+ X(rd) = vl;
+ } else if (rd != 0b00000) then { /* set vl to VLMAX */
+ let AVL = unsigned(ones(sizeof(xlen)));
+ vl = to_bits(sizeof(xlen), VLMAX);
+ X(rd) = vl;
+ } else { /* keep existing vl */
+ let AVL = unsigned(vl);
+ let ratio_pow_new = SEW_pow_new - LMUL_pow_new;
+ if (ratio_pow_new != ratio_pow_ori) then { handle_illegal_vtype(); return RETIRE_SUCCESS }
+ };
+
+ /* reset vstart to 0 */
+ vstart = zeros();
+
print_reg("CSR vtype <- " ^ BitStr(vtype.bits));
print_reg("CSR vl <- " ^ BitStr(vl));
+ print_reg("CSR vstart <- " ^ BitStr(vstart));
+
+ RETIRE_SUCCESS
+}
+
+mapping clause assembly = VSETVL(rs2, rs1, rd)
+ <-> "vsetvl" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
+
+/* ********************************** vsetivli *********************************** */
+union clause ast = VSETIVLI : ( bits(1), bits(1), bits(3), bits(3), regidx, regidx)
+
+mapping clause encdec = VSETIVLI(ma, ta, sew, lmul, uimm, rd) if haveVExt()
+ <-> 0b1100 @ ma @ ta @ sew @ lmul @ uimm @ 0b111 @ rd @ 0b1010111 if haveVExt()
+
+function clause execute VSETIVLI(ma, ta, sew, lmul, uimm, rd) = {
+ /* set vtype */
+ vtype.bits = 0b0 @ zeros(sizeof(xlen) - 9) @ ma @ ta @ sew @ lmul;
+
+ /* check new SEW and LMUL are legal and calculate VLMAX */
+ let VLEN_pow = get_vlen_pow();
+ let ELEN_pow = get_elen_pow();
+ let LMUL_pow_new = get_lmul_pow();
+ let SEW_pow_new = get_sew_pow();
+ if SEW_pow_new > (LMUL_pow_new + ELEN_pow) then { handle_illegal_vtype(); return RETIRE_SUCCESS };
+ let VLMAX = int_power(2, VLEN_pow + LMUL_pow_new - SEW_pow_new);
+
+ /* set vl according to VLMAX and AVL */
+ let AVL = unsigned(uimm); /* AVL is encoded as 5-bit zero-extended imm in the rs1 field */
+ vl = calculate_new_vl(AVL, VLMAX);
+ X(rd) = vl;
/* reset vstart to 0 */
vstart = zeros();
+
+ print_reg("CSR vtype <- " ^ BitStr(vtype.bits));
+ print_reg("CSR vl <- " ^ BitStr(vl));
print_reg("CSR vstart <- " ^ BitStr(vstart));
RETIRE_SUCCESS
}
-mapping clause assembly = VSETI_TYPE(ma, ta, sew, lmul, uimm, rd)
+mapping clause assembly = VSETIVLI(ma, ta, sew, lmul, uimm, rd)
<-> "vsetivli" ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_5(uimm) ^ sep() ^ sew_flag(sew) ^ maybe_lmul_flag(lmul) ^ maybe_ta_flag(ta) ^ maybe_ma_flag(ma)
diff --git a/model/riscv_insts_zbb.sail b/model/riscv_insts_zbb.sail
index c7671a6..d39afc0 100644
--- a/model/riscv_insts_zbb.sail
+++ b/model/riscv_insts_zbb.sail
@@ -184,7 +184,7 @@ mapping clause assembly = RISCV_REV8(rs1, rd)
function clause execute (RISCV_REV8(rs1, rd)) = {
let rs1_val = X(rs1);
- result : xlenbits = zeros();
+ var result : xlenbits = zeros();
foreach (i from 0 to (sizeof(xlen) - 8) by 8)
result[(i + 7) .. i] = rs1_val[(sizeof(xlen) - i - 1) .. (sizeof(xlen) - i - 8)];
X(rd) = result;
@@ -202,7 +202,7 @@ mapping clause assembly = RISCV_ORCB(rs1, rd)
function clause execute (RISCV_ORCB(rs1, rd)) = {
let rs1_val = X(rs1);
- result : xlenbits = zeros();
+ var result : xlenbits = zeros();
foreach (i from 0 to (sizeof(xlen) - 8) by 8)
result[(i + 7) .. i] = if rs1_val[(i + 7) .. i] == zeros()
then 0x00
@@ -222,7 +222,7 @@ mapping clause assembly = RISCV_CPOP(rs1, rd)
function clause execute (RISCV_CPOP(rs1, rd)) = {
let rs1_val = X(rs1);
- result : nat = 0;
+ var result : nat = 0;
foreach (i from 0 to (xlen_val - 1))
if rs1_val[i] == bitone then result = result + 1;
X(rd) = to_bits(sizeof(xlen), result);
@@ -240,7 +240,7 @@ mapping clause assembly = RISCV_CPOPW(rs1, rd)
function clause execute (RISCV_CPOPW(rs1, rd)) = {
let rs1_val = X(rs1);
- result : nat = 0;
+ var result : nat = 0;
foreach (i from 0 to 31)
if rs1_val[i] == bitone then result = result + 1;
X(rd) = to_bits(sizeof(xlen), result);
@@ -258,8 +258,8 @@ mapping clause assembly = RISCV_CLZ(rs1, rd)
function clause execute (RISCV_CLZ(rs1, rd)) = {
let rs1_val = X(rs1);
- result : nat = 0;
- done : bool = false;
+ var result : nat = 0;
+ var done : bool = false;
foreach (i from (sizeof(xlen) - 1) downto 0)
if not(done) then if rs1_val[i] == bitzero
then result = result + 1
@@ -279,8 +279,8 @@ mapping clause assembly = RISCV_CLZW(rs1, rd)
function clause execute (RISCV_CLZW(rs1, rd)) = {
let rs1_val = X(rs1);
- result : nat = 0;
- done : bool = false;
+ var result : nat = 0;
+ var done : bool = false;
foreach (i from 31 downto 0)
if not(done) then if rs1_val[i] == bitzero
then result = result + 1
@@ -300,8 +300,8 @@ mapping clause assembly = RISCV_CTZ(rs1, rd)
function clause execute (RISCV_CTZ(rs1, rd)) = {
let rs1_val = X(rs1);
- result : nat = 0;
- done : bool = false;
+ var result : nat = 0;
+ var done : bool = false;
foreach (i from 0 to (sizeof(xlen) - 1))
if not(done) then if rs1_val[i] == bitzero
then result = result + 1
@@ -321,8 +321,8 @@ mapping clause assembly = RISCV_CTZW(rs1, rd)
function clause execute (RISCV_CTZW(rs1, rd)) = {
let rs1_val = X(rs1);
- result : nat = 0;
- done : bool = false;
+ var result : nat = 0;
+ var done : bool = false;
foreach (i from 0 to 31)
if not(done) then if rs1_val[i] == bitzero
then result = result + 1
diff --git a/model/riscv_insts_zbc.sail b/model/riscv_insts_zbc.sail
index 910db1b..458b9fa 100644
--- a/model/riscv_insts_zbc.sail
+++ b/model/riscv_insts_zbc.sail
@@ -18,7 +18,7 @@ mapping clause assembly = RISCV_CLMUL(rs2, rs1, rd)
function clause execute (RISCV_CLMUL(rs2, rs1, rd)) = {
let rs1_val = X(rs1);
let rs2_val = X(rs2);
- result : xlenbits = zeros();
+ var result : xlenbits = zeros();
foreach (i from 0 to (xlen_val - 1))
if rs2_val[i] == bitone then result = result ^ (rs1_val << i);
X(rd) = result;
@@ -37,7 +37,7 @@ mapping clause assembly = RISCV_CLMULH(rs2, rs1, rd)
function clause execute (RISCV_CLMULH(rs2, rs1, rd)) = {
let rs1_val = X(rs1);
let rs2_val = X(rs2);
- result : xlenbits = zeros();
+ var result : xlenbits = zeros();
foreach (i from 0 to (xlen_val - 1))
if rs2_val[i] == bitone then result = result ^ (rs1_val >> (xlen_val - i));
X(rd) = result;
@@ -56,7 +56,7 @@ mapping clause assembly = RISCV_CLMULR(rs2, rs1, rd)
function clause execute (RISCV_CLMULR(rs2, rs1, rd)) = {
let rs1_val = X(rs1);
let rs2_val = X(rs2);
- result : xlenbits = zeros();
+ var result : xlenbits = zeros();
foreach (i from 0 to (xlen_val - 1))
if rs2_val[i] == bitone then result = result ^ (rs1_val >> (xlen_val - i - 1));
X(rd) = result;
diff --git a/model/riscv_insts_zbkb.sail b/model/riscv_insts_zbkb.sail
index 76190f0..f6246d1 100644
--- a/model/riscv_insts_zbkb.sail
+++ b/model/riscv_insts_zbkb.sail
@@ -64,7 +64,7 @@ mapping clause assembly = RISCV_ZIP(rs1, rd)
function clause execute (RISCV_ZIP(rs1, rd)) = {
assert(sizeof(xlen) == 32);
let rs1_val = X(rs1);
- result : xlenbits = zeros();
+ var result : xlenbits = zeros();
foreach (i from 0 to (sizeof(xlen_bytes)*4 - 1)) {
result[i*2] = rs1_val[i];
result[i*2 + 1] = rs1_val[i + sizeof(xlen_bytes)*4];
@@ -85,7 +85,7 @@ mapping clause assembly = RISCV_UNZIP(rs1, rd)
function clause execute (RISCV_UNZIP(rs1, rd)) = {
assert(sizeof(xlen) == 32);
let rs1_val = X(rs1);
- result : xlenbits = zeros();
+ var result : xlenbits = zeros();
foreach (i from 0 to (sizeof(xlen_bytes)*4 - 1)) {
result[i] = rs1_val[i*2];
result[i + sizeof(xlen_bytes)*4] = rs1_val[i*2 + 1];
@@ -105,7 +105,7 @@ mapping clause assembly = RISCV_BREV8(rs1, rd)
function clause execute (RISCV_BREV8(rs1, rd)) = {
let rs1_val = X(rs1);
- result : xlenbits = zeros();
+ var result : xlenbits = zeros();
foreach (i from 0 to (sizeof(xlen) - 8) by 8)
result[i+7..i] = reverse(rs1_val[i+7..i]);
X(rd) = result;
diff --git a/model/riscv_insts_zbkx.sail b/model/riscv_insts_zbkx.sail
index 59a90c6..d19a2b1 100644
--- a/model/riscv_insts_zbkx.sail
+++ b/model/riscv_insts_zbkx.sail
@@ -18,7 +18,7 @@ mapping clause assembly = RISCV_XPERM8(rs2, rs1, rd)
function clause execute (RISCV_XPERM8(rs2, rs1, rd)) = {
let rs1_val = X(rs1);
let rs2_val = X(rs2);
- result : xlenbits = zeros();
+ var result : xlenbits = zeros();
foreach (i from 0 to (sizeof(xlen) - 8) by 8) {
let index = unsigned(rs2_val[i+7..i]);
result[i+7..i] = if 8*index < sizeof(xlen)
@@ -41,7 +41,7 @@ mapping clause assembly = RISCV_XPERM4(rs2, rs1, rd)
function clause execute (RISCV_XPERM4(rs2, rs1, rd)) = {
let rs1_val = X(rs1);
let rs2_val = X(rs2);
- result : xlenbits = zeros();
+ var result : xlenbits = zeros();
foreach (i from 0 to (sizeof(xlen) - 4) by 4) {
let index = unsigned(rs2_val[i+3..i]);
result[i+3..i] = if 4*index < sizeof(xlen)
diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail
index 7c52abd..f2980fb 100644
--- a/model/riscv_insts_zicsr.sail
+++ b/model/riscv_insts_zicsr.sail
@@ -10,7 +10,7 @@
/* This file specifies the instructions in the 'Zicsr' extension. */
/* ****************************************************************** */
-union clause ast = CSR : (bits(12), regidx, regidx, bool, csrop)
+union clause ast = CSR : (csreg, regidx, regidx, bool, csrop)
mapping encdec_csrop : csrop <-> bits(2) = {
CSRRW <-> 0b01,
diff --git a/model/riscv_pmp_control.sail b/model/riscv_pmp_control.sail
index 1e4cb77..ce53caf 100644
--- a/model/riscv_pmp_control.sail
+++ b/model/riscv_pmp_control.sail
@@ -8,19 +8,17 @@
/* address ranges */
-// TODO: handle the 34-bit paddr32 on RV32
+// [min, max) of the matching range, in units of 4 bytes.
+type pmp_addr_range_in_words = option((xlenbits, xlenbits))
-/* [min, max) of the matching range. */
-type pmp_addr_range = option((xlenbits, xlenbits))
-
-function pmpAddrRange(cfg: Pmpcfg_ent, pmpaddr: xlenbits, prev_pmpaddr: xlenbits) -> pmp_addr_range = {
+function pmpAddrRange(cfg: Pmpcfg_ent, pmpaddr: xlenbits, prev_pmpaddr: xlenbits) -> pmp_addr_range_in_words = {
match pmpAddrMatchType_of_bits(cfg[A]) {
OFF => None(),
- TOR => { Some ((prev_pmpaddr << 2, pmpaddr << 2)) },
+ TOR => { Some ((prev_pmpaddr, pmpaddr)) },
NA4 => {
// NA4 is not selectable when the PMP grain G >= 1. See pmpWriteCfg().
assert(sys_pmp_grain() < 1, "NA4 cannot be selected when PMP grain G >= 1.");
- let lo = pmpaddr << 2;
+ let lo = pmpaddr;
Some((lo, lo + 4))
},
NAPOT => {
@@ -33,7 +31,7 @@ function pmpAddrRange(cfg: Pmpcfg_ent, pmpaddr: xlenbits, prev_pmpaddr: xlenbits
let lo = pmpaddr & (~ (mask));
// mask + 1: 0b00000100000
let len = mask + 1;
- Some((lo << 2, (lo + len) << 2))
+ Some((lo, (lo + len)))
}
}
}
@@ -65,18 +63,27 @@ function pmpCheckPerms(ent, acc, priv) = {
enum pmpAddrMatch = {PMP_NoMatch, PMP_PartialMatch, PMP_Match}
-function pmpMatchAddr(addr: xlenbits, width: xlenbits, rng: pmp_addr_range) -> pmpAddrMatch = {
+function pmpMatchAddr(addr: xlenbits, width: xlenbits, rng: pmp_addr_range_in_words) -> pmpAddrMatch = {
match rng {
None() => PMP_NoMatch,
- Some((lo, hi)) => if hi <=_u lo /* to handle mis-configuration */
- then PMP_NoMatch
- else {
- if (addr + width <=_u lo) | (hi <=_u addr)
- then PMP_NoMatch
- else if (lo <=_u addr) & (addr + width <=_u hi)
- then PMP_Match
- else PMP_PartialMatch
- }
+ Some((lo, hi)) => {
+ // Convert to integers.
+ let addr = unsigned(addr);
+ let width = unsigned(width);
+ // These are in units of 4 bytes.
+ let lo = unsigned(lo) * 4;
+ let hi = unsigned(hi) * 4;
+
+ if hi <= lo /* to handle mis-configuration */
+ then PMP_NoMatch
+ else {
+ if (addr + width <= lo) | (hi <= addr)
+ then PMP_NoMatch
+ else if (lo <= addr) & (addr + width <= hi)
+ then PMP_Match
+ else PMP_PartialMatch
+ }
+ },
}
}
diff --git a/model/riscv_vreg_type.sail b/model/riscv_vreg_type.sail
index a1f292a..2ab211b 100755
--- a/model/riscv_vreg_type.sail
+++ b/model/riscv_vreg_type.sail
@@ -14,7 +14,6 @@ type vreglenbits = bits(vlenmax) /* use the largest possible register length */
type vregtype = vreglenbits
/* vector instruction types */
-enum vsetop = { VSETVLI, VSETVL }
enum vvfunct6 = { VV_VADD, VV_VSUB, VV_VMINU, VV_VMIN, VV_VMAXU, VV_VMAX, VV_VAND, VV_VOR, VV_VXOR,
VV_VRGATHER, VV_VRGATHEREI16, VV_VSADDU, VV_VSADD, VV_VSSUBU, VV_VSSUB, VV_VSLL, VV_VSMUL,
generated by cgit v1.1 at 2024-07-10 03:32:38 +0000