Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add human-readable instruction name annotations #520

Open
wants to merge 3 commits into
base: master
Choose a base branch
from
+65 −6
Open

Add human-readable instruction name annotations #520

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
1da5e7c
Add names for some base instructions
jriyyya Apr 18, 2024
0b5ab31
Add more names for base instructions
Linda-Njau Jul 23, 2024
6670d78
Add names for mnemonic suffixes
ThinkOpenly Sep 9, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
67 changes: 61 additions & 6 deletions model/riscv_insts_base.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,14 +34,17 @@ function clause execute UTYPE(imm, rd, op) = {
}

mapping utype_mnemonic : uop <-> string = {
$[name "load upper immediate"]
RISCV_LUI <-> "lui",
$[name "add upper immediate to PC"]
RISCV_AUIPC <-> "auipc"
}

mapping clause assembly = UTYPE(imm, rd, op)
<-> utype_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_signed_20(imm)

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

mapping clause encdec = RISCV_JAL(imm_19 @ imm_7_0 @ imm_8 @ imm_18_13 @ imm_12_9 @ 0b0, rd)
Expand Down Expand Up @@ -88,6 +91,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 +103,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 @@ -146,11 +151,17 @@ function clause execute (BTYPE(imm, rs2, rs1, op)) = {
}

mapping btype_mnemonic : bop <-> string = {
$[name "branch if equal"]
RISCV_BEQ <-> "beq",
$[name "branch if not equal"]
RISCV_BNE <-> "bne",
$[name "branch if less than"]
RISCV_BLT <-> "blt",
$[name "branch if greater than"]
RISCV_BGE <-> "bge",
$[name "branch if less than (unsigned)"]
RISCV_BLTU <-> "bltu",
$[name "branch if greater than or equal to (unsigned)"]
RISCV_BGEU <-> "bgeu"
}

Expand Down Expand Up @@ -188,18 +199,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 @@ -231,8 +249,11 @@ function clause execute (SHIFTIOP(shamt, rs1, rd, op)) = {
}

mapping shiftiop_mnemonic : sop <-> string = {
$[name "shift left (logical) immediate"]
RISCV_SLLI <-> "slli",
$[name "shift right (logical) immediate"]
RISCV_SRLI <-> "srli",
$[name "shift right (arithmetic) immediate"]
RISCV_SRAI <-> "srai"
}

Expand Down Expand Up @@ -279,22 +300,33 @@ function clause execute (RTYPE(rs2, rs1, rd, op)) = {
}

mapping rtype_mnemonic : rop <-> string = {
$[name "add"]
RISCV_ADD <-> "add",
$[name "set less than"]
RISCV_SLT <-> "slt",
$[name "set less than (unsigned)"]
RISCV_SLTU <-> "sltu",
$[name "AND"]
RISCV_AND <-> "and",
$[name "OR"]
RISCV_OR <-> "or",
$[name "exclusive OR"]
RISCV_XOR <-> "xor",
$[name "shift left (logical)"]
RISCV_SLL <-> "sll",
$[name "shift right (logical)"]
RISCV_SRL <-> "srl",
$[name "subtract"]
RISCV_SUB <-> "sub",
$[name "shift right (arithmetic)"]
RISCV_SRA <-> "sra"
}

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 @@ -346,18 +378,21 @@ function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = {

val maybe_aq : bool <-> string
mapping maybe_aq = {
$[name "acquire"]
true <-> ".aq",
false <-> ""
}

val maybe_rl : bool <-> string
mapping maybe_rl = {
$[name "release"]
true <-> ".rl",
false <-> ""
}

val maybe_u : bool <-> string
mapping maybe_u = {
$[name "unsigned"]
true <-> "u",
false <-> ""
}
Expand All @@ -366,6 +401,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 +447,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 @@ -468,10 +505,15 @@ function clause execute (RTYPEW(rs2, rs1, rd, op)) = {
}

mapping rtypew_mnemonic : ropw <-> string = {
$[name "add word (RV64)"]
RISCV_ADDW <-> "addw",
$[name "subtract word (RV64)"]
RISCV_SUBW <-> "subw",
$[name "shift left (logical) word (RV64)"]
RISCV_SLLW <-> "sllw",
$[name "shift right (logical) word (RV64)"]
RISCV_SRLW <-> "srlw",
$[name "shift right (arithmetic) word (RV64)"]
RISCV_SRAW <-> "sraw"
}

Expand All @@ -481,6 +523,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 @@ -508,8 +551,11 @@ function clause execute (SHIFTIWOP(shamt, rs1, rd, op)) = {
}

mapping shiftiwop_mnemonic : sopw <-> string = {
$[name "shift left (logical) immediate word (RV64)"]
RISCV_SLLIW <-> "slliw",
$[name "shift right (logical) immediate word (RV64)"]
RISCV_SRLIW <-> "srliw",
$[name "shift right (arithmetic) immediate word (RV64)"]
RISCV_SRAIW <-> "sraiw"
}

Expand All @@ -519,6 +565,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 +632,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 +653,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 +665,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 +687,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 +707,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 +732,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 +746,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 +764,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
4 changes: 4 additions & 0 deletions model/riscv_types.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -376,9 +376,13 @@ mapping size_enc : word_width <-> bits(2) = {
}

mapping size_mnemonic : word_width <-> string = {
$[name "byte"]
BYTE <-> "b",
$[name "halfword"]
HALF <-> "h",
$[name "word"]
WORD <-> "w",
$[name "doubleword"]
DOUBLE <-> "d"
}

Expand Down
Loading