aboutsummaryrefslogtreecommitdiff
path: root/model
diff options
context:
space:
mode:
Diffstat (limited to 'model')
-rw-r--r--model/riscv_insts_base.sail2
-rw-r--r--model/riscv_insts_cext.sail22
-rw-r--r--model/riscv_insts_mext.sail2
-rw-r--r--model/riscv_regs.sail3
4 files changed, 14 insertions, 15 deletions
diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail
index 7cf3044..7ac4294 100644
--- a/model/riscv_insts_base.sail
+++ b/model/riscv_insts_base.sail
@@ -288,7 +288,6 @@ mapping clause assembly = RTYPE(rs2, rs1, rd, op)
union clause ast = LOAD : (bits(12), regbits, regbits, bool, word_width, bool, bool)
/* Load unsigned double is only present in RV128I, not RV64I */
-/* TODO: aq/rl */
mapping clause encdec = LOAD(imm, rs1, rd, is_unsigned, size, false, false) if size_bits(size) != 0b11 | not_bool(is_unsigned)
<-> imm @ rs1 @ bool_bits(is_unsigned) @ size_bits(size) @ rd @ 0b0000011 if size_bits(size) != 0b11 | not_bool(is_unsigned)
@@ -364,7 +363,6 @@ mapping clause assembly = LOAD(imm, rs1, rd, is_unsigned, size, aq, rl)
/* ****************************************************************** */
union clause ast = STORE : (bits(12), regbits, regbits, word_width, bool, bool)
-/* TODO: aq/rl */
mapping clause encdec = STORE(imm7 @ imm5, rs2, rs1, size, false, false)
<-> imm7 : bits(7) @ rs2 @ rs1 @ 0b0 @ size_bits(size) @ imm5 : bits(5) @ 0b0100011
diff --git a/model/riscv_insts_cext.sail b/model/riscv_insts_cext.sail
index 4986278..d09a795 100644
--- a/model/riscv_insts_cext.sail
+++ b/model/riscv_insts_cext.sail
@@ -3,7 +3,7 @@
/* These instructions are only legal if misa.C() is true. Instead of
* checking this in every execute clause, we currently do the check in one place
- * in the fetch-execute logic. This may need revisiting for TestRig.
+ * in the fetch-execute logic.
*/
/* ****************************************************************** */
@@ -325,7 +325,6 @@ mapping clause assembly = C_AND(rsd, rs2)
/* ****************************************************************** */
union clause ast = C_SUBW : (cregbits, cregbits)
-/* TODO: invalid on RV32 */
mapping clause encdec_compressed = C_SUBW(rsd, rs2)
if sizeof(xlen) == 64
<-> 0b100 @ 0b1 @ 0b11 @ rsd : cregbits @ 0b00 @ rs2 : cregbits @ 0b01
@@ -345,7 +344,6 @@ mapping clause assembly = C_SUBW(rsd, rs2)
/* ****************************************************************** */
union clause ast = C_ADDW : (cregbits, cregbits)
-/* TODO: invalid on RV32 */
mapping clause encdec_compressed = C_ADDW(rsd, rs2)
if sizeof(xlen) == 64
<-> 0b100 @ 0b1 @ 0b11 @ rsd : cregbits @ 0b01 @ rs2 : cregbits @ 0b01
@@ -402,20 +400,26 @@ mapping clause assembly = C_BNEZ(imm, rs)
union clause ast = C_SLLI : (bits(6), regbits)
/* TODO: On RV32, also need shamt[5] == 0 */
-mapping clause encdec_compressed = C_SLLI(nzui5 @ nzui40, rsd) if nzui5 @ nzui40 != 0b000000 & rsd != zreg
- <-> 0b000 @ nzui5 : bits(1) @ rsd : regbits @ nzui40 : bits(5) @ 0b10 if nzui5 @ nzui40 != 0b000000 & rsd != zreg
+mapping clause encdec_compressed = C_SLLI(nzui5 @ nzui40, rsd)
+ if nzui5 @ nzui40 != 0b000000 & rsd != zreg
+ <-> 0b000 @ nzui5 : bits(1) @ rsd : regbits @ nzui40 : bits(5) @ 0b10
+ if nzui5 @ nzui40 != 0b000000 & rsd != zreg
function clause execute (C_SLLI(shamt, rsd)) =
execute(SHIFTIOP(shamt, rsd, rsd, RISCV_SLLI))
-mapping clause assembly = C_SLLI(shamt, rsd) if shamt != 0b000000 & rsd != zreg
- <-> "c.slli" ^ spc() ^ reg_name(rsd) ^ sep() ^ hex_bits_6(shamt) if shamt != 0b000000 & rsd != zreg
+mapping clause assembly = C_SLLI(shamt, rsd)
+ if shamt != 0b000000 & rsd != zreg
+ <-> "c.slli" ^ spc() ^ reg_name(rsd) ^ sep() ^ hex_bits_6(shamt)
+ if shamt != 0b000000 & rsd != zreg
/* ****************************************************************** */
union clause ast = C_LWSP : (bits(6), regbits)
-mapping clause encdec_compressed = C_LWSP(ui76 @ ui5 @ ui42, rd) if rd != zreg
- <-> 0b010 @ ui5 : bits(1) @ rd : regbits @ ui42 : bits(3) @ ui76 : bits(2) @ 0b10 if rd != zreg
+mapping clause encdec_compressed = C_LWSP(ui76 @ ui5 @ ui42, rd)
+ if rd != zreg
+ <-> 0b010 @ ui5 : bits(1) @ rd : regbits @ ui42 : bits(3) @ ui76 : bits(2) @ 0b10
+ if rd != zreg
function clause execute (C_LWSP(uimm, rd)) = {
let imm : bits(12) = EXTZ(uimm @ 0b00);
diff --git a/model/riscv_insts_mext.sail b/model/riscv_insts_mext.sail
index cab8d9c..b133ac2 100644
--- a/model/riscv_insts_mext.sail
+++ b/model/riscv_insts_mext.sail
@@ -2,7 +2,7 @@
/* This file specifies the instructions in the 'M' extension. */
/* ****************************************************************** */
-/* FIXME: separate these out into separate ast variants */
+
union clause ast = MUL : (regbits, regbits, regbits, bool, bool, bool)
mapping encdec_mul_op : (bool, bool, bool) <-> bits(3) = {
diff --git a/model/riscv_regs.sail b/model/riscv_regs.sail
index f865cd1..f866fab 100644
--- a/model/riscv_regs.sail
+++ b/model/riscv_regs.sail
@@ -43,8 +43,6 @@ register x30 : regtype
register x31 : regtype
val rX : forall 'n, 0 <= 'n < 32. regno('n) -> xlenbits effect {rreg, escape}
-/*function rX 0 = 0x0000000000000000
-and rX (r if r > 0) = Xs[r]*/
function rX r = {
let v : regtype =
match r {
@@ -136,7 +134,6 @@ function wX (r, in_v) = {
};
if (r != 0) then {
rvfi_wX(r, in_v);
- // Xs[r] = v;
print_reg("x" ^ string_of_int(r) ^ " <- " ^ RegStr(v));
}
}