From a67bf16aa5d0773984c43ff8159ee9c580488b28 Mon Sep 17 00:00:00 2001 From: "Paul A. Clarke" Date: Tue, 18 Jun 2024 10:24:35 -0500 Subject: [PATCH] tweaks after rebase --- model/riscv_insts_svinval.sail | 12 ++++----- model/riscv_insts_zcb.sail | 48 +++++++++++++++++----------------- model/riscv_sys_control.sail | 2 +- model/riscv_sys_regs.sail | 7 +++-- 4 files changed, 36 insertions(+), 33 deletions(-) diff --git a/model/riscv_insts_svinval.sail b/model/riscv_insts_svinval.sail index 168fb17ff..66eaafe2e 100644 --- a/model/riscv_insts_svinval.sail +++ b/model/riscv_insts_svinval.sail @@ -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)) @@ -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 @@ -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 diff --git a/model/riscv_insts_zcb.sail b/model/riscv_insts_zcb.sail index 86253bff4..0fac41077 100644 --- a/model/riscv_insts_zcb.sail +++ b/model/riscv_insts_zcb.sail @@ -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() ^ ")" @@ -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() ^ ")" @@ -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() ^ ")" @@ -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() ^ ")" @@ -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() ^ ")" @@ -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) @@ -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) @@ -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) @@ -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) @@ -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) @@ -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) @@ -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) diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 3797cbc37..a71759cbd 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -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; diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index cd1e7d6ce..de1db68c6 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -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, @@ -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])