aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--model/riscv_insts_base.sail65
-rw-r--r--model/riscv_insts_cext.sail58
-rw-r--r--model/riscv_insts_mext.sail15
3 files changed, 111 insertions, 27 deletions
diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail
index 8a9af81..4367233 100644
--- a/model/riscv_insts_base.sail
+++ b/model/riscv_insts_base.sail
@@ -373,7 +373,9 @@ mapping clause assembly = STORE(imm, rs1, rd, size, aq, rl)
union clause ast = ADDIW : (bits(12), regbits, regbits)
mapping clause encdec = ADDIW(imm, rs1, rd)
+ if xlen_val == 64
<-> imm @ rs1 @ 0b000 @ rd @ 0b0011011
+ if xlen_val == 64
function clause execute (ADDIW(imm, rs1, rd)) = {
let result : xlenbits = EXTS(imm) + X(rs1);
@@ -382,14 +384,25 @@ function clause execute (ADDIW(imm, rs1, rd)) = {
}
mapping clause assembly = ADDIW(imm, rs1, rd)
+ if xlen_val == 64
<-> "addiw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_12(imm)
+ if xlen_val == 64
/* ****************************************************************** */
union clause ast = SHIFTW : (bits(5), regbits, regbits, sop)
-mapping clause encdec = SHIFTW(shamt, rs1, rd, RISCV_SLLI) <-> 0b0000000 @ shamt @ rs1 @ 0b001 @ rd @ 0b0011011
-mapping clause encdec = SHIFTW(shamt, rs1, rd, RISCV_SRLI) <-> 0b0000000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011
-mapping clause encdec = SHIFTW(shamt, rs1, rd, RISCV_SRAI) <-> 0b0100000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011
+mapping clause encdec = SHIFTW(shamt, rs1, rd, RISCV_SLLI)
+ if xlen_val == 64
+ <-> 0b0000000 @ shamt @ rs1 @ 0b001 @ rd @ 0b0011011
+ if xlen_val == 64
+mapping clause encdec = SHIFTW(shamt, rs1, rd, RISCV_SRLI)
+ if xlen_val == 64
+ <-> 0b0000000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011
+ if xlen_val == 64
+mapping clause encdec = SHIFTW(shamt, rs1, rd, RISCV_SRAI)
+ if xlen_val == 64
+ <-> 0b0100000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011
+ if xlen_val == 64
function clause execute (SHIFTW(shamt, rs1, rd, op)) = {
let rs1_val = (X(rs1))[31..0];
@@ -409,16 +422,33 @@ mapping shiftw_mnemonic : sop <-> string = {
}
mapping clause assembly = SHIFTW(shamt, rs1, rd, op)
+ if xlen_val == 64
<-> shiftw_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_5(shamt)
+ if xlen_val == 64
/* ****************************************************************** */
union clause ast = RTYPEW : (regbits, regbits, regbits, ropw)
-mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_ADDW) <-> 0b0000000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011
-mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_SUBW) <-> 0b0100000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011
-mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_SLLW) <-> 0b0000000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0111011
-mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_SRLW) <-> 0b0000000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0111011
-mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_SRAW) <-> 0b0100000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0111011
+mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_ADDW)
+ if xlen_val == 64
+ <-> 0b0000000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011
+ if xlen_val == 64
+mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_SUBW)
+ if xlen_val == 64
+ <-> 0b0100000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011
+ if xlen_val == 64
+mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_SLLW)
+ if xlen_val == 64
+ <-> 0b0000000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0111011
+ if xlen_val == 64
+mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_SRLW)
+ if xlen_val == 64
+ <-> 0b0000000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0111011
+ if xlen_val == 64
+mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_SRAW)
+ if xlen_val == 64
+ <-> 0b0100000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0111011
+ if xlen_val == 64
function clause execute (RTYPEW(rs2, rs1, rd, op)) = {
let rs1_val = (X(rs1))[31..0];
@@ -443,14 +473,25 @@ mapping rtypew_mnemonic : ropw <-> string = {
}
mapping clause assembly = RTYPEW(rs2, rs1, rd, op)
+ if xlen_val == 64
<-> rtypew_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
+ if xlen_val == 64
/* ****************************************************************** */
union clause ast = SHIFTIWOP : (bits(5), regbits, regbits, sopw)
-mapping clause encdec = SHIFTIWOP(shamt, rs1, rd, RISCV_SLLIW) <-> 0b0000000 @ shamt @ rs1 @ 0b001 @ rd @ 0b0011011
-mapping clause encdec = SHIFTIWOP(shamt, rs1, rd, RISCV_SRLIW) <-> 0b0000000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011
-mapping clause encdec = SHIFTIWOP(shamt, rs1, rd, RISCV_SRAIW) <-> 0b0100000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011
+mapping clause encdec = SHIFTIWOP(shamt, rs1, rd, RISCV_SLLIW)
+ if xlen_val == 64
+ <-> 0b0000000 @ shamt @ rs1 @ 0b001 @ rd @ 0b0011011
+ if xlen_val == 64
+mapping clause encdec = SHIFTIWOP(shamt, rs1, rd, RISCV_SRLIW)
+ if xlen_val == 64
+ <-> 0b0000000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011
+ if xlen_val == 64
+mapping clause encdec = SHIFTIWOP(shamt, rs1, rd, RISCV_SRAIW)
+ if xlen_val == 64
+ <-> 0b0100000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011
+ if xlen_val == 64
function clause execute (SHIFTIWOP(shamt, rs1, rd, op)) = {
let rs1_val = X(rs1);
@@ -470,7 +511,9 @@ mapping shiftiwop_mnemonic : sopw <-> string = {
}
mapping clause assembly = SHIFTIWOP(shamt, rs1, rd, op)
+ if xlen_val == 64
<-> shiftiwop_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ hex_bits_5(shamt)
+ if xlen_val == 64
/* ****************************************************************** */
union clause ast = FENCE : (bits(4), bits(4))
diff --git a/model/riscv_insts_cext.sail b/model/riscv_insts_cext.sail
index 9feced0..d2b0695 100644
--- a/model/riscv_insts_cext.sail
+++ b/model/riscv_insts_cext.sail
@@ -56,7 +56,9 @@ mapping clause assembly = C_LW(uimm, rsc, rdc)
union clause ast = C_LD : (bits(5), cregbits, cregbits)
mapping clause encdec_compressed = C_LD(ui76 @ ui53, rs1, rd)
+ if xlen_val == 64
<-> 0b011 @ ui53 : bits(3) @ rs1 : cregbits @ ui76 : bits(2) @ rd : cregbits @ 0b00
+ if xlen_val == 64
function clause execute (C_LD(uimm, rsc, rdc)) = {
let imm : bits(12) = EXTZ(uimm @ 0b000);
@@ -66,7 +68,9 @@ function clause execute (C_LD(uimm, rsc, rdc)) = {
}
mapping clause assembly = C_LD(uimm, rsc, rdc)
+ if xlen_val == 64
<-> "c.ld" ^ spc() ^ creg_name(rdc) ^ sep() ^ creg_name(rsc) ^ sep() ^ hex_bits_8(uimm @ 0b000)
+ if xlen_val == 64
/* ****************************************************************** */
union clause ast = C_SW : (bits(5), cregbits, cregbits)
@@ -88,7 +92,9 @@ mapping clause assembly = C_SW(uimm, rsc1, rsc2)
union clause ast = C_SD : (bits(5), cregbits, cregbits)
mapping clause encdec_compressed = C_SD(ui76 @ ui53, rs1, rs2)
+ if xlen_val == 64
<-> 0b111 @ ui53 : bits(3) @ rs1 : bits(3) @ ui76 : bits(2) @ rs2 : bits(3) @ 0b00
+ if xlen_val == 64
function clause execute (C_SD(uimm, rsc1, rsc2)) = {
let imm : bits(12) = EXTZ(uimm @ 0b000);
@@ -98,7 +104,9 @@ function clause execute (C_SD(uimm, rsc1, rsc2)) = {
}
mapping clause assembly = C_SD(uimm, rsc1, rsc2)
+ if xlen_val == 64
<-> "c.sd" ^ spc() ^ creg_name(rsc1) ^ sep() ^ creg_name(rsc2) ^ sep() ^ hex_bits_8(uimm @ 0b000)
+ if xlen_val == 64
/* ****************************************************************** */
union clause ast = C_ADDI : (bits(6), regbits)
@@ -120,19 +128,28 @@ mapping clause assembly = C_ADDI(nzi, rsd)
/* ****************************************************************** */
union clause ast = C_JAL : (bits(11))
-union clause ast = C_ADDIW : (bits(6), regbits)
-/* FIXME: decoding differs for RVC32/RVC64. Below, we are assuming
- * RV64, and C_JAL is RV32 only. */
-
-mapping clause encdec_compressed = C_ADDIW(imm5 @ imm40, rsd)
- if rsd != zreg
- <-> 0b001 @ imm5 : bits(1) @ rsd : regbits @ imm40 : bits(5) @ 0b01
- if rsd != zreg
+mapping clause encdec_compressed = C_JAL(i11 @ i10 @ i98 @ i7 @ i6 @ i5 @ i4 @ i31)
+ if xlen_val == 32
+ <-> 0b001 @ i11 : bits(1) @ i4 : bits(1) @ i98 : bits(2) @ i10 : bits(1) @ i6 : bits(1) @ i7 : bits(1) @ i31 : bits(3) @ i5 : bits(1) @ 0b01
+ if xlen_val == 32
function clause execute (C_JAL(imm)) =
execute(RISCV_JAL(EXTS(imm @ 0b0), ra))
+mapping clause assembly = C_JAL(imm)
+ if xlen_val == 32
+ <-> "c.jal" ^ spc() ^ hex_bits_12(imm @ 0b0)
+ if xlen_val == 32
+
+/* ****************************************************************** */
+union clause ast = C_ADDIW : (bits(6), regbits)
+
+mapping clause encdec_compressed = C_ADDIW(imm5 @ imm40, rsd)
+ if rsd != zreg & xlen_val == 64
+ <-> 0b001 @ imm5 : bits(1) @ rsd : regbits @ imm40 : bits(5) @ 0b01
+ if rsd != zreg & xlen_val == 64
+
function clause execute (C_ADDIW(imm, rsd)) = {
let imm : bits(32) = EXTS(imm);
let rs_val = X(rsd);
@@ -141,11 +158,10 @@ function clause execute (C_ADDIW(imm, rsd)) = {
true
}
-mapping clause assembly = C_JAL(imm)
- <-> "c.jal" ^ spc() ^ hex_bits_12(imm @ 0b0)
-
mapping clause assembly = C_ADDIW(imm, rsd)
+ if xlen_val == 64
<-> "c.addiw" ^ spc() ^ reg_name(rsd) ^ sep() ^ hex_bits_6(imm)
+ if xlen_val == 64
/* ****************************************************************** */
union clause ast = C_LI : (bits(6), regbits)
@@ -316,7 +332,9 @@ union clause ast = C_SUBW : (cregbits, cregbits)
/* TODO: invalid on RV32 */
mapping clause encdec_compressed = C_SUBW(rsd, rs2)
+ if xlen_val == 64
<-> 0b100 @ 0b1 @ 0b11 @ rsd : cregbits @ 0b00 @ rs2 : cregbits @ 0b01
+ if xlen_val == 64
function clause execute (C_SUBW(rsd, rs2)) = {
let rsd = creg2reg_bits(rsd);
@@ -325,14 +343,18 @@ function clause execute (C_SUBW(rsd, rs2)) = {
}
mapping clause assembly = C_SUBW(rsd, rs2)
+ if xlen_val == 64
<-> "c.subw" ^ spc() ^ creg_name(rsd) ^ sep() ^ creg_name(rs2)
+ if xlen_val == 64
/* ****************************************************************** */
union clause ast = C_ADDW : (cregbits, cregbits)
/* TODO: invalid on RV32 */
mapping clause encdec_compressed = C_ADDW(rsd, rs2)
+ if xlen_val == 64
<-> 0b100 @ 0b1 @ 0b11 @ rsd : cregbits @ 0b01 @ rs2 : cregbits @ 0b01
+ if xlen_val == 64
function clause execute (C_ADDW(rsd, rs2)) = {
let rsd = creg2reg_bits(rsd);
@@ -341,7 +363,9 @@ function clause execute (C_ADDW(rsd, rs2)) = {
}
mapping clause assembly = C_ADDW(rsd, rs2)
+ if xlen_val == 64
<-> "c.addw" ^ spc() ^ creg_name(rsd) ^ sep() ^ creg_name(rs2)
+ if xlen_val == 64
/* ****************************************************************** */
union clause ast = C_J : (bits(11))
@@ -412,9 +436,9 @@ mapping clause assembly = C_LWSP(uimm, rd)
union clause ast = C_LDSP : (bits(6), regbits)
mapping clause encdec_compressed = C_LDSP(ui86 @ ui5 @ ui43, rd)
- if rd != zreg
+ if rd != zreg & xlen_val == 64
<-> 0b011 @ ui5 : bits(1) @ rd : regbits @ ui43 : bits(2) @ ui86 : bits(3) @ 0b10
- if rd != zreg
+ if rd != zreg & xlen_val == 64
function clause execute (C_LDSP(uimm, rd)) = {
let imm : bits(12) = EXTZ(uimm @ 0b000);
@@ -422,9 +446,9 @@ function clause execute (C_LDSP(uimm, rd)) = {
}
mapping clause assembly = C_LDSP(uimm, rd)
- if rd != zreg
+ if rd != zreg & xlen_val == 64
<-> "c.ldsp" ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_6(uimm)
- if rd != zreg
+ if rd != zreg & xlen_val == 64
/* ****************************************************************** */
union clause ast = C_SWSP : (bits(6), regbits)
@@ -444,7 +468,9 @@ mapping clause assembly = C_SWSP(uimm, rd)
union clause ast = C_SDSP : (bits(6), regbits)
mapping clause encdec_compressed = C_SDSP(ui86 @ ui53, rs2)
+ if xlen_val == 64
<-> 0b111 @ ui53 : bits(3) @ ui86 : bits(3) @ rs2 : regbits @ 0b10
+ if xlen_val == 64
function clause execute (C_SDSP(uimm, rs2)) = {
let imm : bits(12) = EXTZ(uimm @ 0b000);
@@ -452,7 +478,9 @@ function clause execute (C_SDSP(uimm, rs2)) = {
}
mapping clause assembly = C_SDSP(uimm, rs2)
+ if xlen_val == 64
<-> "c.sdsp" ^ spc() ^ reg_name(rs2) ^ sep() ^ hex_bits_6(uimm)
+ if xlen_val == 64
/* ****************************************************************** */
union clause ast = C_JR : (regbits)
diff --git a/model/riscv_insts_mext.sail b/model/riscv_insts_mext.sail
index c36b677..c4ca7e5 100644
--- a/model/riscv_insts_mext.sail
+++ b/model/riscv_insts_mext.sail
@@ -103,7 +103,10 @@ mapping clause assembly = REM(rs2, rs1, rd, s)
/* ****************************************************************** */
union clause ast = MULW : (regbits, regbits, regbits)
-mapping clause encdec = MULW(rs2, rs1, rd) <-> 0b0000001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011
+mapping clause encdec = MULW(rs2, rs1, rd)
+ if xlen_val == 64
+ <-> 0b0000001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011
+ if xlen_val == 64
function clause execute (MULW(rs2, rs1, rd)) = {
if haveMulDiv() then {
@@ -123,13 +126,17 @@ function clause execute (MULW(rs2, rs1, rd)) = {
}
mapping clause assembly = MULW(rs2, rs1, rd)
+ if xlen_val == 64
<-> "mulw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
+ if xlen_val == 64
/* ****************************************************************** */
union clause ast = DIVW : (regbits, regbits, regbits, bool)
mapping clause encdec = DIVW(rs2, rs1, rd, s)
+ if xlen_val == 64
<-> 0b0000001 @ rs2 @ rs1 @ 0b10 @ bool_not_bits(s) @ rd @ 0b0111011
+ if xlen_val == 64
function clause execute (DIVW(rs2, rs1, rd, s)) = {
if haveMulDiv() then {
@@ -149,13 +156,17 @@ function clause execute (DIVW(rs2, rs1, rd, s)) = {
}
mapping clause assembly = DIVW(rs2, rs1, rd, s)
+ if xlen_val == 64
<-> "div" ^ maybe_not_u(s) ^ "w" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
+ if xlen_val == 64
/* ****************************************************************** */
union clause ast = REMW : (regbits, regbits, regbits, bool)
mapping clause encdec = REMW(rs2, rs1, rd, s)
+ if xlen_val == 64
<-> 0b0000001 @ rs2 @ rs1 @ 0b11 @ bool_not_bits(s) @ rd @ 0b0111011
+ if xlen_val == 64
function clause execute (REMW(rs2, rs1, rd, s)) = {
if haveMulDiv() then {
@@ -174,4 +185,6 @@ function clause execute (REMW(rs2, rs1, rd, s)) = {
}
mapping clause assembly = REMW(rs2, rs1, rd, s)
+ if xlen_val == 64
<-> "rem" ^ maybe_not_u(s) ^ "w" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
+ if xlen_val == 64
generated by cgit v1.1 at 2024-10-04 08:18:06 +0000