Skip to content

Commit

Permalink
tweaks after rebase
Browse files Browse the repository at this point in the history
  • Loading branch information
@ThinkOpenly
ThinkOpenly committed Jun 18, 2024
1 parent 9e0a892 commit a67bf16
Show file tree
Hide file tree
Showing 4 changed files with 36 additions and 33 deletions.
12 changes: 6 additions & 6 deletions model/riscv_insts_svinval.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,8 +9,8 @@
union clause ast = SINVAL_VMA : (regidx, regidx)

mapping clause encdec =
SINVAL_VMA(rs1, rs2) if haveSvinval()
<-> 0b0001011 @ rs2 : regidx @ rs1 : regidx @ 0b000 @ 0b00000 @ 0b1110011 if haveSvinval()
SINVAL_VMA(rs1, rs2) if extension("Svinval")
<-> 0b0001011 @ rs2 : regidx @ rs1 : regidx @ 0b000 @ 0b00000 @ 0b1110011 if extension("Svinval")

function clause execute SINVAL_VMA(rs1, rs2) = {
execute(SFENCE_VMA(rs1, rs2))
Expand All @@ -24,8 +24,8 @@ mapping clause assembly = SINVAL_VMA(rs1, rs2)
union clause ast = SFENCE_W_INVAL : unit

mapping clause encdec =
SFENCE_W_INVAL() if haveSvinval()
<-> 0b0001100 @ 0b00000 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 if haveSvinval()
SFENCE_W_INVAL() if extension("Svinval")
<-> 0b0001100 @ 0b00000 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 if extension("Svinval")

function clause execute SFENCE_W_INVAL() = {
if cur_privilege == User
Expand All @@ -40,8 +40,8 @@ mapping clause assembly = SFENCE_W_INVAL() <-> "sfence.w.inval"
union clause ast = SFENCE_INVAL_IR : unit

mapping clause encdec =
SFENCE_INVAL_IR() if haveSvinval()
<-> 0b0001100 @ 0b00001 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 if haveSvinval()
SFENCE_INVAL_IR() if extension("Svinval")
<-> 0b0001100 @ 0b00001 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 if extension("Svinval")

function clause execute SFENCE_INVAL_IR() = {
if cur_privilege == User
Expand Down
48 changes: 24 additions & 24 deletions model/riscv_insts_zcb.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,8 +9,8 @@
union clause ast = C_LBU : (bits(2), cregidx, cregidx)

mapping clause encdec_compressed =
C_LBU(uimm1 @ uimm0, rdc, rs1c) if haveZcb()
<-> 0b100 @ 0b000 @ rs1c : cregidx @ uimm0 : bits(1) @ uimm1 : bits(1) @ rdc : cregidx @ 0b00 if haveZcb()
C_LBU(uimm1 @ uimm0, rdc, rs1c) if extension("Zcb")
<-> 0b100 @ 0b000 @ rs1c : cregidx @ uimm0 : bits(1) @ uimm1 : bits(1) @ rdc : cregidx @ 0b00 if extension("Zcb")

mapping clause assembly = C_LBU(uimm, rdc, rs1c) <->
"c.lbu" ^ spc() ^ creg_name(rdc) ^ sep() ^ hex_bits_2(uimm) ^ opt_spc() ^ "(" ^ opt_spc() ^ creg_name(rs1c) ^ opt_spc() ^ ")"
Expand All @@ -27,8 +27,8 @@ function clause execute C_LBU(uimm, rdc, rs1c) = {
union clause ast = C_LHU : (bits(2), cregidx, cregidx)

mapping clause encdec_compressed =
C_LHU(uimm1 @ 0b0, rdc, rs1c) if haveZcb()
<-> 0b100 @ 0b001 @ rs1c : cregidx @ 0b0 @ uimm1 : bits(1) @ rdc : cregidx @ 0b00 if haveZcb()
C_LHU(uimm1 @ 0b0, rdc, rs1c) if extension("Zcb")
<-> 0b100 @ 0b001 @ rs1c : cregidx @ 0b0 @ uimm1 : bits(1) @ rdc : cregidx @ 0b00 if extension("Zcb")

mapping clause assembly = C_LHU(uimm, rdc, rs1c) <->
"c.lhu" ^ spc() ^ creg_name(rdc) ^ sep() ^ hex_bits_2(uimm) ^ opt_spc() ^ "(" ^ opt_spc() ^ creg_name(rs1c) ^ opt_spc() ^ ")"
Expand All @@ -45,8 +45,8 @@ function clause execute C_LHU(uimm, rdc, rs1c) = {
union clause ast = C_LH : (bits(2), cregidx, cregidx)

mapping clause encdec_compressed =
C_LH(uimm1 @ 0b0, rdc, rs1c) if haveZcb()
<-> 0b100 @ 0b001 @ rs1c : cregidx @ 0b1 @ uimm1 : bits(1) @ rdc : cregidx @ 0b00 if haveZcb()
C_LH(uimm1 @ 0b0, rdc, rs1c) if extension("Zcb")
<-> 0b100 @ 0b001 @ rs1c : cregidx @ 0b1 @ uimm1 : bits(1) @ rdc : cregidx @ 0b00 if extension("Zcb")

mapping clause assembly = C_LH(uimm, rdc, rs1c) <->
"c.lh" ^ spc() ^ creg_name(rdc) ^ sep() ^ hex_bits_2(uimm) ^ opt_spc() ^ "(" ^ opt_spc() ^ creg_name(rs1c) ^ opt_spc() ^ ")"
Expand All @@ -63,8 +63,8 @@ function clause execute C_LH(uimm, rdc, rs1c) = {
union clause ast = C_SB : (bits(2), cregidx, cregidx)

mapping clause encdec_compressed =
C_SB(uimm1 @ uimm0, rs1c, rs2c) if haveZcb()
<-> 0b100 @ 0b010 @ rs1c : cregidx @ uimm0 : bits(1) @ uimm1 : bits(1) @ rs2c @ 0b00 if haveZcb()
C_SB(uimm1 @ uimm0, rs1c, rs2c) if extension("Zcb")
<-> 0b100 @ 0b010 @ rs1c : cregidx @ uimm0 : bits(1) @ uimm1 : bits(1) @ rs2c @ 0b00 if extension("Zcb")

mapping clause assembly = C_SB(uimm, rs1c, rs2c) <->
"c.sb" ^ spc() ^ creg_name(rs2c) ^ sep() ^ hex_bits_2(uimm) ^ opt_spc() ^ "(" ^ opt_spc() ^ creg_name(rs1c) ^ opt_spc() ^ ")"
Expand All @@ -81,8 +81,8 @@ function clause execute C_SB(uimm, rs1c, rs2c) = {
union clause ast = C_SH : (bits(2), cregidx, cregidx)

mapping clause encdec_compressed =
C_SH(uimm1 @ 0b0, rs1c, rs2c) if haveZcb()
<-> 0b100 @ 0b011 @ rs1c : cregidx @ 0b0 @ uimm1 : bits(1) @ rs2c : cregidx @ 0b00 if haveZcb()
C_SH(uimm1 @ 0b0, rs1c, rs2c) if extension("Zcb")
<-> 0b100 @ 0b011 @ rs1c : cregidx @ 0b0 @ uimm1 : bits(1) @ rs2c : cregidx @ 0b00 if extension("Zcb")

mapping clause assembly = C_SH(uimm, rs1c, rs2c) <->
"c.sh" ^ spc() ^ creg_name(rs1c) ^ sep() ^ hex_bits_2(uimm) ^ opt_spc() ^ "(" ^ opt_spc() ^ creg_name(rs2c) ^ opt_spc() ^ ")"
Expand All @@ -99,8 +99,8 @@ function clause execute C_SH(uimm, rs1c, rs2c) = {
union clause ast = C_ZEXT_B : (cregidx)

mapping clause encdec_compressed =
C_ZEXT_B(rsdc) if haveZcb()
<-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b000 @ 0b01 if haveZcb()
C_ZEXT_B(rsdc) if extension("Zcb")
<-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b000 @ 0b01 if extension("Zcb")

mapping clause assembly = C_ZEXT_B(rsdc) <->
"c.zext.b" ^ spc() ^ creg_name(rsdc)
Expand All @@ -116,8 +116,8 @@ function clause execute C_ZEXT_B(rsdc) = {
union clause ast = C_SEXT_B : (cregidx)

mapping clause encdec_compressed =
C_SEXT_B(rsdc) if haveZcb() & haveZbb()
<-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b001 @ 0b01 if haveZcb() & haveZbb()
C_SEXT_B(rsdc) if extension("Zcb") & extension("Zbb")
<-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b001 @ 0b01 if extension("Zcb") & extension("Zbb")

mapping clause assembly = C_SEXT_B(rsdc) <->
"c.sext.b" ^ spc() ^ creg_name(rsdc)
Expand All @@ -132,8 +132,8 @@ function clause execute C_SEXT_B(rsdc) = {
union clause ast = C_ZEXT_H : (cregidx)

mapping clause encdec_compressed =
C_ZEXT_H(rsdc) if haveZcb() & haveZbb()
<-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b010 @ 0b01 if haveZcb() & haveZbb()
C_ZEXT_H(rsdc) if extension("Zcb") & extension("Zbb")
<-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b010 @ 0b01 if extension("Zcb") & extension("Zbb")

mapping clause assembly = C_ZEXT_H(rsdc) <->
"c.zext.h" ^ spc() ^ creg_name(rsdc)
Expand All @@ -148,8 +148,8 @@ function clause execute C_ZEXT_H(rsdc) = {
union clause ast = C_SEXT_H : (cregidx)

mapping clause encdec_compressed =
C_SEXT_H(rsdc) if haveZcb() & haveZbb()
<-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b011 @ 0b01 if haveZcb() & haveZbb()
C_SEXT_H(rsdc) if extension("Zcb") & extension("Zbb")
<-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b011 @ 0b01 if extension("Zcb") & extension("Zbb")

mapping clause assembly = C_SEXT_H(rsdc) <->
"c.sext.h" ^ spc() ^ creg_name(rsdc)
Expand All @@ -164,8 +164,8 @@ function clause execute C_SEXT_H(rsdc) = {
union clause ast = C_ZEXT_W : (cregidx)

mapping clause encdec_compressed =
C_ZEXT_W(rsdc) if haveZcb() & haveZba() & sizeof(xlen) == 64
<-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b100 @ 0b01 if haveZcb() & haveZba() & sizeof(xlen) == 64
C_ZEXT_W(rsdc) if extension("Zcb") & extension("Zba") & sizeof(xlen) == 64
<-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b100 @ 0b01 if extension("Zcb") & extension("Zba") & sizeof(xlen) == 64

mapping clause assembly = C_ZEXT_W(rsdc) <->
"c.zext.w" ^ spc() ^ creg_name(rsdc)
Expand All @@ -180,8 +180,8 @@ function clause execute C_ZEXT_W(rsdc) = {
union clause ast = C_NOT : (cregidx)

mapping clause encdec_compressed =
C_NOT(rsdc) if haveZcb()
<-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b101 @ 0b01 if haveZcb()
C_NOT(rsdc) if extension("Zcb")
<-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b101 @ 0b01 if extension("Zcb")

mapping clause assembly = C_NOT(rsdc) <->
"c.not" ^ spc() ^ creg_name(rsdc)
Expand All @@ -197,8 +197,8 @@ function clause execute C_NOT(rsdc) = {
union clause ast = C_MUL : (cregidx, cregidx)

mapping clause encdec_compressed =
C_MUL(rsdc, rs2c) if haveZcb() & (haveMulDiv() | haveZmmul())
<-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b10 @ rs2c : cregidx @ 0b01 if haveZcb() & (haveMulDiv() | haveZmmul())
C_MUL(rsdc, rs2c) if extension("Zcb") & (extension("M") | extension("Zmmul"))
<-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b10 @ rs2c : cregidx @ 0b01 if extension("Zcb") & (extension("M") | extension("Zmmul"))

mapping clause assembly = C_MUL(rsdc, rs2c) <->
"c.mul" ^ spc() ^ creg_name(rsdc) ^ sep() ^ creg_name(rs2c)
Expand Down
2 changes: 1 addition & 1 deletion model/riscv_sys_control.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -170,7 +170,7 @@ function exception_delegatee(e : ExceptionType, p : Privilege) -> Privilege = {
/* if S-mode is absent, medeleg delegates to U-mode if 'N' is supported. */
let user = if extension("S")
then super & extension("N") & bit_to_bool(sedeleg.bits[idx])
else super & extension("N")
else super & extension("N");
let deleg = if extension("U") & user then User
else if extension("S") & super then Supervisor
else Machine;
Expand Down
7 changes: 5 additions & 2 deletions model/riscv_sys_regs.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -227,8 +227,8 @@ function extension(ext) = {
/* V extension has to enable both via misa.V as well as mstatus.VS */
"V" => (misa[V] == 0b1) & (mstatus[VS] != 0b00),

"Zaamo" => haveAtomics(),
"Zalrsc" => haveAtomics(),
"Zaamo" => extension("A"),
"Zalrsc" => extension("A"),

/* BitManip extension support. */
"Zba" => true,
Expand Down Expand Up @@ -927,3 +927,6 @@ function decode_agtype(ag) = {

val get_vtype_vma : unit -> agtype
function get_vtype_vma() = decode_agtype(vtype[vma])

val get_vtype_vta : unit -> agtype
function get_vtype_vta() = decode_agtype(vtype[vta])

0 comments on commit a67bf16

Please sign in to comment.