Skip to content

Commit

Permalink
Add names for some base instructions
Browse files Browse the repository at this point in the history
  • Loading branch information
jriyyya authored and ThinkOpenly committed Aug 12, 2024
1 parent 2078d87 commit 1da5e7c
Showing 1 changed file with 28 additions and 6 deletions.
34 changes: 28 additions & 6 deletions model/riscv_insts_base.sail
Original file line number Diff line number Diff line change
Expand Up @@ -88,6 +88,7 @@ mapping clause assembly = RISCV_JAL(imm, rd)
<-> "jal" ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_signed_21(imm)

/* ****************************************************************** */
$[name "jump and link register"]
union clause ast = RISCV_JALR : (bits(12), regidx, regidx)

mapping clause encdec = RISCV_JALR(imm, rs1, rd)
Expand All @@ -99,6 +100,7 @@ mapping clause assembly = RISCV_JALR(imm, rs1, rd)
/* see riscv_jalr_seq.sail or riscv_jalr_rmem.sail for the execute clause. */

/* ****************************************************************** */
$[name "conditional branch"]
union clause ast = BTYPE : (bits(13), regidx, regidx, bop)

mapping encdec_bop : bop <-> bits(3) = {
Expand Down Expand Up @@ -188,18 +190,25 @@ function clause execute (ITYPE (imm, rs1, rd, op)) = {
}

mapping itype_mnemonic : iop <-> string = {
RISCV_ADDI <-> "addi",
RISCV_SLTI <-> "slti",
RISCV_SLTIU <-> "sltiu",
RISCV_XORI <-> "xori",
RISCV_ORI <-> "ori",
RISCV_ANDI <-> "andi"
$[name "add immediate"]
RISCV_ADDI <-> "addi",
$[name "set less than immediate"]
RISCV_SLTI <-> "slti",
$[name "set less than immediate unsigned"]
RISCV_SLTIU <-> "sltiu",
$[name "XOR immediate"]
RISCV_XORI <-> "xori",
$[name "OR immediate"]
RISCV_ORI <-> "ori",
$[name "AND immediate"]
RISCV_ANDI <-> "andi"
}

mapping clause assembly = ITYPE(imm, rs1, rd, op)
<-> itype_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_signed_12(imm)

/* ****************************************************************** */
$[name "Shift Immediate"]
union clause ast = SHIFTIOP : (bits(6), regidx, regidx, sop)

mapping encdec_sop : sop <-> bits(3) = {
Expand Down Expand Up @@ -295,6 +304,7 @@ mapping clause assembly = RTYPE(rs2, rs1, rd, op)
<-> rtype_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)

/* ****************************************************************** */
$[name "load"]
union clause ast = LOAD : (bits(12), regidx, regidx, bool, word_width, bool, bool)

/* unsigned loads are only present for widths strictly less than xlen,
Expand Down Expand Up @@ -366,6 +376,7 @@ mapping clause assembly = LOAD(imm, rs1, rd, is_unsigned, size, aq, rl)
<-> "l" ^ size_mnemonic(size) ^ maybe_u(is_unsigned) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_signed_12(imm) ^ "(" ^ reg_name(rs1) ^ ")"

/* ****************************************************************** */
$[name "store"]
union clause ast = STORE : (bits(12), regidx, regidx, word_width, bool, bool)

mapping clause encdec = STORE(imm7 @ imm5, rs2, rs1, size, false, false) if size_bytes(size) <= sizeof(xlen_bytes)
Expand Down Expand Up @@ -411,6 +422,7 @@ mapping clause assembly = STORE(imm, rs2, rs1, size, aq, rl)
<-> "s" ^ size_mnemonic(size) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rs2) ^ sep() ^ hex_bits_signed_12(imm) ^ opt_spc() ^ "(" ^ opt_spc() ^ reg_name(rs1) ^ opt_spc() ^ ")"

/* ****************************************************************** */
$[name "add immediate word"]
union clause ast = ADDIW : (bits(12), regidx, regidx)

mapping clause encdec = ADDIW(imm, rs1, rd)
Expand Down Expand Up @@ -481,6 +493,7 @@ mapping clause assembly = RTYPEW(rs2, rs1, rd, op)
if sizeof(xlen) == 64

/* ****************************************************************** */
$[name "shift immediate word"]
union clause ast = SHIFTIWOP : (bits(5), regidx, regidx, sopw)

mapping clause encdec = SHIFTIWOP(shamt, rs1, rd, RISCV_SLLIW)
Expand Down Expand Up @@ -519,6 +532,7 @@ mapping clause assembly = SHIFTIWOP(shamt, rs1, rd, op)
if sizeof(xlen) == 64

/* ****************************************************************** */
$[name "fence (memory)"]
union clause ast = FENCE : (bits(4), bits(4))

mapping clause encdec = FENCE(pred, succ)
Expand Down Expand Up @@ -585,6 +599,7 @@ mapping clause assembly = FENCE(pred, succ)
<-> "fence" ^ spc() ^ fence_bits(pred) ^ sep() ^ fence_bits(succ)

/* ****************************************************************** */
$[name "fence (total store order)"]
union clause ast = FENCE_TSO : (bits(4), bits(4))

mapping clause encdec = FENCE_TSO(pred, succ)
Expand All @@ -605,6 +620,7 @@ mapping clause assembly = FENCE_TSO(pred, succ)
<-> "fence.tso" ^ spc() ^ fence_bits(pred) ^ sep() ^ fence_bits(succ)

/* ****************************************************************** */
$[name "fence (instruction)"]
union clause ast = FENCEI : unit

mapping clause encdec = FENCEI()
Expand All @@ -616,6 +632,7 @@ function clause execute FENCEI() = { /* __barrier(Barrier_RISCV_i); */ RETIRE_SU
mapping clause assembly = FENCEI() <-> "fence.i"

/* ****************************************************************** */
$[name "environment call"]
union clause ast = ECALL : unit

mapping clause encdec = ECALL()
Expand All @@ -637,6 +654,7 @@ function clause execute ECALL() = {
mapping clause assembly = ECALL() <-> "ecall"

/* ****************************************************************** */
$[name "machine-level return"]
union clause ast = MRET : unit

mapping clause encdec = MRET()
Expand All @@ -656,6 +674,7 @@ function clause execute MRET() = {
mapping clause assembly = MRET() <-> "mret"

/* ****************************************************************** */
$[name "supervisor-level return"]
union clause ast = SRET : unit

mapping clause encdec = SRET()
Expand All @@ -680,6 +699,7 @@ function clause execute SRET() = {
mapping clause assembly = SRET() <-> "sret"

/* ****************************************************************** */
$[name "environment breakpoint"]
union clause ast = EBREAK : unit

mapping clause encdec = EBREAK()
Expand All @@ -693,6 +713,7 @@ function clause execute EBREAK() = {
mapping clause assembly = EBREAK() <-> "ebreak"

/* ****************************************************************** */
$[name "wait for interrupt"]
union clause ast = WFI : unit

mapping clause encdec = WFI()
Expand All @@ -710,6 +731,7 @@ function clause execute WFI() =
mapping clause assembly = WFI() <-> "wfi"

/* ****************************************************************** */
$[name "supervisor memory-management fence (virtual memory address)"]
union clause ast = SFENCE_VMA : (regidx, regidx)

mapping clause encdec = SFENCE_VMA(rs1, rs2)
Expand Down

0 comments on commit 1da5e7c

Please sign in to comment.