Skip to content

Commit

Permalink
Fix mext whitespace
Browse files Browse the repository at this point in the history
  • Loading branch information
@jordancarlin @Alasdair
jordancarlin authored and Alasdair committed May 20, 2024
1 parent 85a065e commit c2b5fb7
Showing 1 changed file with 53 additions and 53 deletions.
106 changes: 53 additions & 53 deletions model/riscv_insts_mext.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,16 +24,16 @@ mapping clause encdec = MUL(rs2, rs1, rd, mul_op) if haveMulD
<-> 0b0000001 @ rs2 @ rs1 @ encdec_mul_op(mul_op) @ rd @ 0b0110011 if haveMulDiv() | haveZmmul()

function clause execute (MUL(rs2, rs1, rd, mul_op)) = {
let rs1_val = X(rs1);
let rs2_val = X(rs2);
let rs1_int : int = if mul_op.signed_rs1 then signed(rs1_val) else unsigned(rs1_val);
let rs2_int : int = if mul_op.signed_rs2 then signed(rs2_val) else unsigned(rs2_val);
let result_wide = to_bits(2 * sizeof(xlen), rs1_int * rs2_int);
let result = if mul_op.high
then result_wide[(2 * sizeof(xlen) - 1) .. sizeof(xlen)]
else result_wide[(sizeof(xlen) - 1) .. 0];
X(rd) = result;
RETIRE_SUCCESS
let rs1_val = X(rs1);
let rs2_val = X(rs2);
let rs1_int : int = if mul_op.signed_rs1 then signed(rs1_val) else unsigned(rs1_val);
let rs2_int : int = if mul_op.signed_rs2 then signed(rs2_val) else unsigned(rs2_val);
let result_wide = to_bits(2 * sizeof(xlen), rs1_int * rs2_int);
let result = if mul_op.high
then result_wide[(2 * sizeof(xlen) - 1) .. sizeof(xlen)]
else result_wide[(sizeof(xlen) - 1) .. 0];
X(rd) = result;
RETIRE_SUCCESS
}

mapping mul_mnemonic : mul_op <-> string = {
Expand All @@ -53,15 +53,15 @@ mapping clause encdec = DIV(rs2, rs1, rd, s) if haveMu
<-> 0b0000001 @ rs2 @ rs1 @ 0b10 @ bool_not_bits(s) @ rd @ 0b0110011 if haveMulDiv()

function clause execute (DIV(rs2, rs1, rd, s)) = {
let rs1_val = X(rs1);
let rs2_val = X(rs2);
let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val);
let rs2_int : int = if s then signed(rs2_val) else unsigned(rs2_val);
let q : int = if rs2_int == 0 then -1 else quot_round_zero(rs1_int, rs2_int);
/* check for signed overflow */
let q': int = if s & q > xlen_max_signed then xlen_min_signed else q;
X(rd) = to_bits(sizeof(xlen), q');
RETIRE_SUCCESS
let rs1_val = X(rs1);
let rs2_val = X(rs2);
let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val);
let rs2_int : int = if s then signed(rs2_val) else unsigned(rs2_val);
let q : int = if rs2_int == 0 then -1 else quot_round_zero(rs1_int, rs2_int);
/* check for signed overflow */
let q': int = if s & q > xlen_max_signed then xlen_min_signed else q;
X(rd) = to_bits(sizeof(xlen), q');
RETIRE_SUCCESS
}

mapping maybe_not_u : bool <-> string = {
Expand All @@ -79,14 +79,14 @@ mapping clause encdec = REM(rs2, rs1, rd, s) if haveMu
<-> 0b0000001 @ rs2 @ rs1 @ 0b11 @ bool_not_bits(s) @ rd @ 0b0110011 if haveMulDiv()

function clause execute (REM(rs2, rs1, rd, s)) = {
let rs1_val = X(rs1);
let rs2_val = X(rs2);
let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val);
let rs2_int : int = if s then signed(rs2_val) else unsigned(rs2_val);
let r : int = if rs2_int == 0 then rs1_int else rem_round_zero(rs1_int, rs2_int);
/* signed overflow case returns zero naturally as required due to -1 divisor */
X(rd) = to_bits(sizeof(xlen), r);
RETIRE_SUCCESS
let rs1_val = X(rs1);
let rs2_val = X(rs2);
let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val);
let rs2_int : int = if s then signed(rs2_val) else unsigned(rs2_val);
let r : int = if rs2_int == 0 then rs1_int else rem_round_zero(rs1_int, rs2_int);
/* signed overflow case returns zero naturally as required due to -1 divisor */
X(rd) = to_bits(sizeof(xlen), r);
RETIRE_SUCCESS
}

mapping clause assembly = REM(rs2, rs1, rd, s)
Expand All @@ -101,15 +101,15 @@ mapping clause encdec = MULW(rs2, rs1, rd)
if sizeof(xlen) == 64 & (haveMulDiv() | haveZmmul())

function clause execute (MULW(rs2, rs1, rd)) = {
let rs1_val = X(rs1)[31..0];
let rs2_val = X(rs2)[31..0];
let rs1_int : int = signed(rs1_val);
let rs2_int : int = signed(rs2_val);
/* to_bits requires expansion to 64 bits followed by truncation */
let result32 = to_bits(64, rs1_int * rs2_int)[31..0];
let result : xlenbits = sign_extend(result32);
X(rd) = result;
RETIRE_SUCCESS
let rs1_val = X(rs1)[31..0];
let rs2_val = X(rs2)[31..0];
let rs1_int : int = signed(rs1_val);
let rs2_int : int = signed(rs2_val);
/* to_bits requires expansion to 64 bits followed by truncation */
let result32 = to_bits(64, rs1_int * rs2_int)[31..0];
let result : xlenbits = sign_extend(result32);
X(rd) = result;
RETIRE_SUCCESS
}

mapping clause assembly = MULW(rs2, rs1, rd)
Expand All @@ -126,15 +126,15 @@ mapping clause encdec = DIVW(rs2, rs1, rd, s)
if sizeof(xlen) == 64 & haveMulDiv()

function clause execute (DIVW(rs2, rs1, rd, s)) = {
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);
let rs2_int : int = if s then signed(rs2_val) else unsigned(rs2_val);
let q : int = if rs2_int == 0 then -1 else quot_round_zero(rs1_int, rs2_int);
/* check for signed overflow */
let q': int = if s & q > (2 ^ 31 - 1) then (0 - 2^31) else q;
X(rd) = sign_extend(to_bits(32, q'));
RETIRE_SUCCESS
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);
let rs2_int : int = if s then signed(rs2_val) else unsigned(rs2_val);
let q : int = if rs2_int == 0 then -1 else quot_round_zero(rs1_int, rs2_int);
/* check for signed overflow */
let q': int = if s & q > (2 ^ 31 - 1) then (0 - 2^31) else q;
X(rd) = sign_extend(to_bits(32, q'));
RETIRE_SUCCESS
}

mapping clause assembly = DIVW(rs2, rs1, rd, s)
Expand All @@ -151,14 +151,14 @@ mapping clause encdec = REMW(rs2, rs1, rd, s)
if sizeof(xlen) == 64 & haveMulDiv()

function clause execute (REMW(rs2, rs1, rd, s)) = {
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);
let rs2_int : int = if s then signed(rs2_val) else unsigned(rs2_val);
let r : int = if rs2_int == 0 then rs1_int else rem_round_zero(rs1_int, rs2_int);
/* signed overflow case returns zero naturally as required due to -1 divisor */
X(rd) = sign_extend(to_bits(32, r));
RETIRE_SUCCESS
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);
let rs2_int : int = if s then signed(rs2_val) else unsigned(rs2_val);
let r : int = if rs2_int == 0 then rs1_int else rem_round_zero(rs1_int, rs2_int);
/* signed overflow case returns zero naturally as required due to -1 divisor */
X(rd) = sign_extend(to_bits(32, r));
RETIRE_SUCCESS
}

mapping clause assembly = REMW(rs2, rs1, rd, s)
Expand Down

0 comments on commit c2b5fb7

Please sign in to comment.