Skip to content

Commit

Permalink
Use extension discriminator for "A" and "M" extensions
Browse files Browse the repository at this point in the history
More support for #4.
Using the `extension()` function in `mapping clause encdec` expressions for extensions allows a parser to clearly know when a function is part of an extension (or set of extensions).
  • Loading branch information
Bakugo90 authored and ThinkOpenly committed Jun 17, 2024
1 parent cc680e5 commit edb07a9
Show file tree
Hide file tree
Showing 3 changed files with 22 additions and 20 deletions.
12 changes: 6 additions & 6 deletions model/riscv_insts_aext.sail
Original file line number Diff line number Diff line change
Expand Up @@ -43,8 +43,8 @@ function amo_width_valid(size : word_width) -> bool = {
/* ****************************************************************** */
union clause ast = LOADRES : (bool, bool, regidx, word_width, regidx)

mapping clause encdec = LOADRES(aq, rl, rs1, size, rd) if haveZalrsc() & amo_width_valid(size)
<-> 0b00010 @ bool_bits(aq) @ bool_bits(rl) @ 0b00000 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if haveZalrsc() & amo_width_valid(size)
mapping clause encdec = LOADRES(aq, rl, rs1, size, rd) if extension("Zalrsc") & amo_width_valid(size)
<-> 0b00010 @ bool_bits(aq) @ bool_bits(rl) @ 0b00000 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if extension("Zalrsc") & amo_width_valid(size)


/* We could set load-reservations on physical or virtual addresses.
Expand Down Expand Up @@ -88,8 +88,8 @@ mapping clause assembly = LOADRES(aq, rl, rs1, size, rd)
/* ****************************************************************** */
union clause ast = STORECON : (bool, bool, regidx, regidx, word_width, regidx)

mapping clause encdec = STORECON(aq, rl, rs2, rs1, size, rd) if haveZalrsc() & amo_width_valid(size)
<-> 0b00011 @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if haveZalrsc() & amo_width_valid(size)
mapping clause encdec = STORECON(aq, rl, rs2, rs1, size, rd) if extension("Zalrsc") & amo_width_valid(size)
<-> 0b00011 @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if extension("Zalrsc") & amo_width_valid(size)

/* NOTE: Currently, we only EA if address translation is successful. This may need revisiting. */
function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
Expand Down Expand Up @@ -163,8 +163,8 @@ mapping encdec_amoop : amoop <-> bits(5) = {
AMOMAXU <-> 0b11100
}

mapping clause encdec = AMO(op, aq, rl, rs2, rs1, size, rd) if haveZaamo() & amo_width_valid(size)
<-> encdec_amoop(op) @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if haveZaamo() & amo_width_valid(size)
mapping clause encdec = AMO(op, aq, rl, rs2, rs1, size, rd) if extension("Zaamo") & amo_width_valid(size)
<-> encdec_amoop(op) @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if extension("Zaamo") & amo_width_valid(size)

/* NOTE: Currently, we only EA if address translation is successful.
This may need revisiting. */
Expand Down
24 changes: 12 additions & 12 deletions model/riscv_insts_mext.sail
Original file line number Diff line number Diff line change
Expand Up @@ -20,8 +20,8 @@ mapping encdec_mul_op : mul_op <-> bits(3) = {
struct { high = true, signed_rs1 = false, signed_rs2 = false } <-> 0b011
}

mapping clause encdec = MUL(rs2, rs1, rd, mul_op) if haveMulDiv() | haveZmmul()
<-> 0b0000001 @ rs2 @ rs1 @ encdec_mul_op(mul_op) @ rd @ 0b0110011 if haveMulDiv() | haveZmmul()
mapping clause encdec = MUL(rs2, rs1, rd, mul_op) if extension("M") | extension("Zmmul")
<-> 0b0000001 @ rs2 @ rs1 @ encdec_mul_op(mul_op) @ rd @ 0b0110011 if extension("M") | extension("Zmmul")

function clause execute (MUL(rs2, rs1, rd, mul_op)) = {
let rs1_val = X(rs1);
Expand Down Expand Up @@ -49,8 +49,8 @@ mapping clause assembly = MUL(rs2, rs1, rd, mul_op)
/* ****************************************************************** */
union clause ast = DIV : (regidx, regidx, regidx, bool)

mapping clause encdec = DIV(rs2, rs1, rd, s) if haveMulDiv()
<-> 0b0000001 @ rs2 @ rs1 @ 0b10 @ bool_not_bits(s) @ rd @ 0b0110011 if haveMulDiv()
mapping clause encdec = DIV(rs2, rs1, rd, s) if extension("M")
<-> 0b0000001 @ rs2 @ rs1 @ 0b10 @ bool_not_bits(s) @ rd @ 0b0110011 if extension("M")

function clause execute (DIV(rs2, rs1, rd, s)) = {
let rs1_val = X(rs1);
Expand All @@ -75,8 +75,8 @@ mapping clause assembly = DIV(rs2, rs1, rd, s)
/* ****************************************************************** */
union clause ast = REM : (regidx, regidx, regidx, bool)

mapping clause encdec = REM(rs2, rs1, rd, s) if haveMulDiv()
<-> 0b0000001 @ rs2 @ rs1 @ 0b11 @ bool_not_bits(s) @ rd @ 0b0110011 if haveMulDiv()
mapping clause encdec = REM(rs2, rs1, rd, s) if extension("M")
<-> 0b0000001 @ rs2 @ rs1 @ 0b11 @ bool_not_bits(s) @ rd @ 0b0110011 if extension("M")

function clause execute (REM(rs2, rs1, rd, s)) = {
let rs1_val = X(rs1);
Expand All @@ -96,9 +96,9 @@ mapping clause assembly = REM(rs2, rs1, rd, s)
union clause ast = MULW : (regidx, regidx, regidx)

mapping clause encdec = MULW(rs2, rs1, rd)
if sizeof(xlen) == 64 & (haveMulDiv() | haveZmmul())
if sizeof(xlen) == 64 & (extension("M") | extension("Zmmul"))
<-> 0b0000001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011
if sizeof(xlen) == 64 & (haveMulDiv() | haveZmmul())
if sizeof(xlen) == 64 & (extension("M") | extension("Zmmul"))

function clause execute (MULW(rs2, rs1, rd)) = {
let rs1_val = X(rs1)[31..0];
Expand All @@ -121,9 +121,9 @@ mapping clause assembly = MULW(rs2, rs1, rd)
union clause ast = DIVW : (regidx, regidx, regidx, bool)

mapping clause encdec = DIVW(rs2, rs1, rd, s)
if sizeof(xlen) == 64 & haveMulDiv()
if sizeof(xlen) == 64 & extension("M")
<-> 0b0000001 @ rs2 @ rs1 @ 0b10 @ bool_not_bits(s) @ rd @ 0b0111011
if sizeof(xlen) == 64 & haveMulDiv()
if sizeof(xlen) == 64 & extension("M")

function clause execute (DIVW(rs2, rs1, rd, s)) = {
let rs1_val = X(rs1)[31..0];
Expand All @@ -146,9 +146,9 @@ mapping clause assembly = DIVW(rs2, rs1, rd, s)
union clause ast = REMW : (regidx, regidx, regidx, bool)

mapping clause encdec = REMW(rs2, rs1, rd, s)
if sizeof(xlen) == 64 & haveMulDiv()
if sizeof(xlen) == 64 & extension("M")
<-> 0b0000001 @ rs2 @ rs1 @ 0b11 @ bool_not_bits(s) @ rd @ 0b0111011
if sizeof(xlen) == 64 & haveMulDiv()
if sizeof(xlen) == 64 & extension("M")

function clause execute (REMW(rs2, rs1, rd, s)) = {
let rs1_val = X(rs1)[31..0];
Expand Down
6 changes: 4 additions & 2 deletions model/riscv_sys_regs.sail
Original file line number Diff line number Diff line change
Expand Up @@ -928,15 +928,17 @@ val extension : (string) -> bool

function extension(ext) = {
match ext {
"A" => misa.A() == 0b1,
"A" => misa[A] == 0b1,
"C" => misa.C() == 0b1,
"D" => (misa.D() == 0b1) & (mstatus.FS() != 0b00),
"F" => (misa.F() == 0b1) & (mstatus.FS() != 0b00),
"M" => misa.M() == 0b1,
"M" => misa[A] == 0b1,
"N" => misa.N() == 0b1,
"U" => misa.U() == 0b1,
"S" => misa.S() == 0b1,
"V" => (misa.V() == 0b1) & (mstatus.VS() != 0b00),
"Zaamo" => haveAtomics(),
"Zalrsc" => haveAtomics(),
"Zba" => true,
"Zbb" => true,
"Zbc" => true,
Expand Down

0 comments on commit edb07a9

Please sign in to comment.