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
Bakugo90 authored Mar 7, 2024
1 parent a13f2e2 commit 4808a16
Show file tree
Hide file tree
Showing 2 changed files with 21 additions and 21 deletions.
12 changes: 6 additions & 6 deletions model/riscv_insts_aext.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -105,7 +105,7 @@ 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 amo_width_valid(size)
mapping clause encdec = LOADRES(aq, rl, rs1, size, rd) if extension("A") & amo_width_valid(size)
<-> 0b00010 @ bool_bits(aq) @ bool_bits(rl) @ 0b00000 @ rs1 @ 0b0 @ size_bits(size) @ rd @ 0b0101111 if amo_width_valid(size)


Expand All @@ -123,7 +123,7 @@ function process_loadres(rd, addr, value, is_unsigned) =
}

function clause execute(LOADRES(aq, rl, rs1, width, rd)) = {
if haveAtomics() then {
if extension("A") then {
/* Get the address, X(rs1) (no offset).
* Extensions might perform additional checks on address validity.
*/
Expand Down Expand Up @@ -170,7 +170,7 @@ 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 amo_width_valid(size)
mapping clause encdec = STORECON(aq, rl, rs2, rs1, size, rd) if extension("A") & amo_width_valid(size)
<-> 0b00011 @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_bits(size) @ rd @ 0b0101111 if amo_width_valid(size)

/* NOTE: Currently, we only EA if address translation is successful. This may need revisiting. */
Expand All @@ -181,7 +181,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
*/
X(rd) = zero_extend(0b1); RETIRE_SUCCESS
} else {
if haveAtomics() then {
if extension("A") then {
/* normal non-rmem case
* rmem: SC is allowed to succeed (but might fail later)
*/
Expand Down Expand Up @@ -268,13 +268,13 @@ mapping encdec_amoop : amoop <-> bits(5) = {
AMOMAXU <-> 0b11100
}

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

/* NOTE: Currently, we only EA if address translation is successful.
This may need revisiting. */
function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
if haveAtomics() then {
if extension("A") then {
/* Get the address, X(rs1) (no offset).
* Some extensions perform additional checks on address validity.
*/
Expand Down
30 changes: 15 additions & 15 deletions model/riscv_insts_mext.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -83,11 +83,11 @@ mapping encdec_mul_op : (bool, bool, bool) <-> bits(3) = {
}

/* for some reason the : bits(3) here is still necessary - BUG */
mapping clause encdec = MUL(rs2, rs1, rd, high, signed1, signed2)
mapping clause encdec = MUL(rs2, rs1, rd, high, signed1, signed2) if extension("M")
<-> 0b0000001 @ rs2 @ rs1 @ encdec_mul_op(high, signed1, signed2) : bits(3) @ rd @ 0b0110011

function clause execute (MUL(rs2, rs1, rd, high, signed1, signed2)) = {
if haveMulDiv() | haveZmmul() then {
if extension("M") | haveZmmul() then {
let rs1_val = X(rs1);
let rs2_val = X(rs2);
let rs1_int : int = if signed1 then signed(rs1_val) else unsigned(rs1_val);
Expand Down Expand Up @@ -117,11 +117,11 @@ mapping clause assembly = MUL(rs2, rs1, rd, high, signed1, signed2)
/* ****************************************************************** */
union clause ast = DIV : (regidx, regidx, regidx, bool)

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

function clause execute (DIV(rs2, rs1, rd, s)) = {
if haveMulDiv() then {
if extension("M") then {
let rs1_val = X(rs1);
let rs2_val = X(rs2);
let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val);
Expand All @@ -148,11 +148,11 @@ mapping clause assembly = DIV(rs2, rs1, rd, s)
/* ****************************************************************** */
union clause ast = REM : (regidx, regidx, regidx, bool)

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

function clause execute (REM(rs2, rs1, rd, s)) = {
if haveMulDiv() then {
if extension("M") then {
let rs1_val = X(rs1);
let rs2_val = X(rs2);
let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val);
Expand All @@ -174,12 +174,12 @@ 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
if extension("M") & sizeof(xlen) == 64
<-> 0b0000001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011
if sizeof(xlen) == 64
if extension("M") & sizeof(xlen) == 64

function clause execute (MULW(rs2, rs1, rd)) = {
if haveMulDiv() | haveZmmul() then {
if extension("M") | haveZmmul() then {
let rs1_val = X(rs1)[31..0];
let rs2_val = X(rs2)[31..0];
let rs1_int : int = signed(rs1_val);
Expand All @@ -204,12 +204,12 @@ 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
if extension("M") & sizeof(xlen) == 64
<-> 0b0000001 @ rs2 @ rs1 @ 0b10 @ bool_not_bits(s) @ rd @ 0b0111011
if sizeof(xlen) == 64
if extension("M") & sizeof(xlen) == 64

function clause execute (DIVW(rs2, rs1, rd, s)) = {
if haveMulDiv() then {
if extension("M") then {
let rs1_val = X(rs1)[31..0];
let rs2_val = X(rs2)[31..0];
let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val);
Expand All @@ -234,12 +234,12 @@ 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
if extension("M") & sizeof(xlen) == 64
<-> 0b0000001 @ rs2 @ rs1 @ 0b11 @ bool_not_bits(s) @ rd @ 0b0111011
if sizeof(xlen) == 64
if extension("M") & sizeof(xlen) == 64

function clause execute (REMW(rs2, rs1, rd, s)) = {
if haveMulDiv() then {
if extension("M") then {
let rs1_val = X(rs1)[31..0];
let rs2_val = X(rs2)[31..0];
let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val);
Expand Down

0 comments on commit 4808a16

Please sign in to comment.