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

replace fsplit and fmake with mapping fstruct #568

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

replace fsplit and fmake with mapping fstruct #568

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
63 changes: 35 additions & 28 deletions model/riscv_insts_dext.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,98 +32,105 @@
/* **************************************************************** */
/* S and D value structure (sign, exponent, mantissa) */

/* TODO: this should be a 'mapping' */
val fsplit_D : bits(64) -> (bits(1), bits(11), bits(52))
function fsplit_D x64 = (x64[63..63], x64[62..52], x64[51..0])

val fmake_D : (bits(1), bits(11), bits(52)) -> bits(64)
function fmake_D (sign, exp, mant) = sign @ exp @ mant

val fExtractor_D : bits(64) <-> (bits(1), bits(11), bits(52))
function fExtractor_D_forwards(x64) = fsplit_D(x64)
function fExtractor_D_forwards_matches(x64) = true
function fExtractor_D_backwards(sign, exp, mant) = fmake_D(sign, exp, mant)
function fExtractor_D_backwards_matches(sign, exp, mant) = true

mapping fstruct_D : bits(64) <-> (bits(1), bits(11), bits(52)) = {fExtractor_D(sign, exp, mant) <-> (sign, exp, mant)}

/* ---- Structure tests */

val f_is_neg_inf_D : bits(64) -> bool
function f_is_neg_inf_D x64 = {
let (sign, exp, mant) = fsplit_D (x64);
let (sign, exp, mant) = fstruct_D (x64);
( (sign == 0b1)
& (exp == ones())
& (mant == zeros()))
}

val f_is_neg_norm_D : bits(64) -> bool
function f_is_neg_norm_D x64 = {
let (sign, exp, mant) = fsplit_D (x64);
let (sign, exp, mant) = fstruct_D (x64);
( (sign == 0b1)
& (exp != zeros())
& (exp != ones()))
}

val f_is_neg_subnorm_D : bits(64) -> bool
function f_is_neg_subnorm_D x64 = {
let (sign, exp, mant) = fsplit_D (x64);
let (sign, exp, mant) = fstruct_D (x64);
( (sign == 0b1)
& (exp == zeros())
& (mant != zeros()))
}

val f_is_neg_zero_D : bits(64) -> bool
function f_is_neg_zero_D x64 = {
let (sign, exp, mant) = fsplit_D (x64);
let (sign, exp, mant) = fstruct_D (x64);
( (sign == ones())
& (exp == zeros())
& (mant == zeros()))
}

val f_is_pos_zero_D : bits(64) -> bool
function f_is_pos_zero_D x64 = {
let (sign, exp, mant) = fsplit_D (x64);
let (sign, exp, mant) = fstruct_D (x64);
( (sign == zeros())
& (exp == zeros())
& (mant == zeros()))
}

val f_is_pos_subnorm_D : bits(64) -> bool
function f_is_pos_subnorm_D x64 = {
let (sign, exp, mant) = fsplit_D (x64);
let (sign, exp, mant) = fstruct_D (x64);
( (sign == zeros())
& (exp == zeros())
& (mant != zeros()))
}

val f_is_pos_norm_D : bits(64) -> bool
function f_is_pos_norm_D x64 = {
let (sign, exp, mant) = fsplit_D (x64);
let (sign, exp, mant) = fstruct_D (x64);
( (sign == zeros())
& (exp != zeros())
& (exp != ones()))
}

val f_is_pos_inf_D : bits(64) -> bool
function f_is_pos_inf_D x64 = {
let (sign, exp, mant) = fsplit_D (x64);
let (sign, exp, mant) = fstruct_D (x64);
( (sign == zeros())
& (exp == ones())
& (mant == zeros()))
}

val f_is_SNaN_D : bits(64) -> bool
function f_is_SNaN_D x64 = {
let (sign, exp, mant) = fsplit_D (x64);
let (sign, exp, mant) = fstruct_D (x64);
( (exp == ones())
& (mant [51] == bitzero)
& (mant != zeros()))
}

val f_is_QNaN_D : bits(64) -> bool
function f_is_QNaN_D x64 = {
let (sign, exp, mant) = fsplit_D (x64);
let (sign, exp, mant) = fstruct_D (x64);
( (exp == ones())
& (mant [51] == bitone))
}

/* Either QNaN or SNan */
val f_is_NaN_D : bits(64) -> bool
function f_is_NaN_D x64 = {
let (sign, exp, mant) = fsplit_D (x64);
let (sign, exp, mant) = fstruct_D (x64);
( (exp == ones())
& (mant != zeros()))
}
Expand All @@ -134,15 +141,15 @@ function f_is_NaN_D x64 = {

val negate_D : bits(64) -> bits(64)
function negate_D (x64) = {
let (sign, exp, mant) = fsplit_D (x64);
let (sign, exp, mant) = fstruct_D (x64);
let new_sign = if (sign == 0b0) then 0b1 else 0b0;
fmake_D (new_sign, exp, mant)
}

val feq_quiet_D : (bits(64), bits (64)) -> (bool, bits(5))
function feq_quiet_D (v1, v2) = {
let (s1, e1, m1) = fsplit_D (v1);
let (s2, e2, m2) = fsplit_D (v2);
let (s1, e1, m1) = fstruct_D (v1);
let (s2, e2, m2) = fstruct_D (v2);

let v1Is0 = f_is_neg_zero_D(v1) | f_is_pos_zero_D(v1);
let v2Is0 = f_is_neg_zero_D(v2) | f_is_pos_zero_D(v2);
Expand All @@ -158,8 +165,8 @@ function feq_quiet_D (v1, v2) = {

val flt_D : (bits(64), bits (64), bool) -> (bool, bits(5))
function flt_D (v1, v2, is_quiet) = {
let (s1, e1, m1) = fsplit_D (v1);
let (s2, e2, m2) = fsplit_D (v2);
let (s1, e1, m1) = fstruct_D (v1);
let (s2, e2, m2) = fstruct_D (v2);

let result : bool =
if (s1 == 0b0) & (s2 == 0b0) then
Expand Down Expand Up @@ -189,8 +196,8 @@ function flt_D (v1, v2, is_quiet) = {

val fle_D : (bits(64), bits (64), bool) -> (bool, bits(5))
function fle_D (v1, v2, is_quiet) = {
let (s1, e1, m1) = fsplit_D (v1);
let (s2, e2, m2) = fsplit_D (v2);
let (s1, e1, m1) = fstruct_D (v1);
let (s2, e2, m2) = fstruct_D (v2);

let v1Is0 = f_is_neg_zero_D(v1) | f_is_pos_zero_D(v1);
let v2Is0 = f_is_neg_zero_D(v2) | f_is_pos_zero_D(v2);
Expand Down Expand Up @@ -726,9 +733,9 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FSGNJ_D)) = {
let rs1_val_D = F_or_X_D(rs1);
let rs2_val_D = F_or_X_D(rs2);

let (s1, e1, m1) = fsplit_D (rs1_val_D);
let (s2, e2, m2) = fsplit_D (rs2_val_D);
let rd_val_D = fmake_D (s2, e1, m1);
let (s1, e1, m1) = fstruct_D (rs1_val_D);
let (s2, e2, m2) = fstruct_D (rs2_val_D);
let rd_val_D = fstruct_D ((s2, e1, m1));

F_or_X_D(rd) = rd_val_D;
RETIRE_SUCCESS
Expand All @@ -737,9 +744,9 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FSGNJ_D)) = {
function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FSGNJN_D)) = {
let rs1_val_D = F_or_X_D(rs1);
let rs2_val_D = F_or_X_D(rs2);
let (s1, e1, m1) = fsplit_D (rs1_val_D);
let (s2, e2, m2) = fsplit_D (rs2_val_D);
let rd_val_D = fmake_D (0b1 ^ s2, e1, m1);
let (s1, e1, m1) = fstruct_D (rs1_val_D);
let (s2, e2, m2) = fstruct_D (rs2_val_D);
let rd_val_D = fstruct_D ((0b1 ^ s2, e1, m1));

F_or_X_D(rd) = rd_val_D;
RETIRE_SUCCESS
Expand All @@ -748,9 +755,9 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FSGNJN_D)) = {
function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FSGNJX_D)) = {
let rs1_val_D = F_or_X_D(rs1);
let rs2_val_D = F_or_X_D(rs2);
let (s1, e1, m1) = fsplit_D (rs1_val_D);
let (s2, e2, m2) = fsplit_D (rs2_val_D);
let rd_val_D = fmake_D (s1 ^ s2, e1, m1);
let (s1, e1, m1) = fstruct_D (rs1_val_D);
let (s2, e2, m2) = fstruct_D (rs2_val_D);
let rd_val_D = fstruct_D ((s1 ^ s2, e1, m1));

F_or_X_D(rd) = rd_val_D;
RETIRE_SUCCESS
Expand Down
65 changes: 36 additions & 29 deletions model/riscv_insts_fext.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -71,98 +71,105 @@ function nvFlag() -> bits(5) = 0b_10000
/* **************************************************************** */
/* S and D value structure (sign, exponent, mantissa) */

/* TODO: this should be a 'mapping' */
val fsplit_S : bits(32) -> (bits(1), bits(8), bits(23))
function fsplit_S x32 = (x32[31..31], x32[30..23], x32[22..0])

val fmake_S : (bits(1), bits(8), bits(23)) -> bits(32)
function fmake_S (sign, exp, mant) = sign @ exp @ mant

val fExtractor_S : bits(32) <-> (bits(1), bits(8), bits(23))
function fExtractor_S_forwards(x32) = fsplit_S(x32)
function fExtractor_S_forwards_matches(x32) = true
function fExtractor_S_backwards(sign, exp, mant) = fmake_S(sign, exp, mant)
function fExtractor_S_backwards_matches(sign, exp, mant) = true

mapping fstruct_S : bits(32) <-> (bits(1), bits(8), bits(23)) = {fExtractor_S(sign, exp, mant) <-> (sign, exp, mant)}

/* ---- Structure tests */

val f_is_neg_inf_S : bits(32) -> bool
function f_is_neg_inf_S x32 = {
let (sign, exp, mant) = fsplit_S (x32);
let (sign, exp, mant) = fstruct_S (x32);
( (sign == 0b1)
& (exp == ones())
& (mant == zeros()))
}

val f_is_neg_norm_S : bits(32) -> bool
function f_is_neg_norm_S x32 = {
let (sign, exp, mant) = fsplit_S (x32);
let (sign, exp, mant) = fstruct_S (x32);
( (sign == 0b1)
& (exp != zeros())
& (exp != ones()))
}

val f_is_neg_subnorm_S : bits(32) -> bool
function f_is_neg_subnorm_S x32 = {
let (sign, exp, mant) = fsplit_S (x32);
let (sign, exp, mant) = fstruct_S (x32);
( (sign == 0b1)
& (exp == zeros())
& (mant != zeros()))
}

val f_is_neg_zero_S : bits(32) -> bool
function f_is_neg_zero_S x32 = {
let (sign, exp, mant) = fsplit_S (x32);
let (sign, exp, mant) = fstruct_S (x32);
( (sign == ones())
& (exp == zeros())
& (mant == zeros()))
}

val f_is_pos_zero_S : bits(32) -> bool
function f_is_pos_zero_S x32 = {
let (sign, exp, mant) = fsplit_S (x32);
let (sign, exp, mant) = fstruct_S (x32);
( (sign == zeros())
& (exp == zeros())
& (mant == zeros()))
}

val f_is_pos_subnorm_S : bits(32) -> bool
function f_is_pos_subnorm_S x32 = {
let (sign, exp, mant) = fsplit_S (x32);
let (sign, exp, mant) = fstruct_S (x32);
( (sign == zeros())
& (exp == zeros())
& (mant != zeros()))
}

val f_is_pos_norm_S : bits(32) -> bool
function f_is_pos_norm_S x32 = {
let (sign, exp, mant) = fsplit_S (x32);
let (sign, exp, mant) = fstruct_S (x32);
( (sign == zeros())
& (exp != zeros())
& (exp != ones()))
}

val f_is_pos_inf_S : bits(32) -> bool
function f_is_pos_inf_S x32 = {
let (sign, exp, mant) = fsplit_S (x32);
let (sign, exp, mant) = fstruct_S (x32);
( (sign == zeros())
& (exp == ones())
& (mant == zeros()))
}

val f_is_SNaN_S : bits(32) -> bool
function f_is_SNaN_S x32 = {
let (sign, exp, mant) = fsplit_S (x32);
let (sign, exp, mant) = fstruct_S (x32);
( (exp == ones())
& (mant [22] == bitzero)
& (mant != zeros()))
}

val f_is_QNaN_S : bits(32) -> bool
function f_is_QNaN_S x32 = {
let (sign, exp, mant) = fsplit_S (x32);
let (sign, exp, mant) = fstruct_S (x32);
( (exp == ones())
& (mant [22] == bitone))
}

/* Either QNaN or SNan */
val f_is_NaN_S : bits(32) -> bool
function f_is_NaN_S x32 = {
let (sign, exp, mant) = fsplit_S (x32);
let (sign, exp, mant) = fstruct_S (x32);
( (exp == ones())
& (mant != zeros()))
}
Expand All @@ -172,15 +179,15 @@ function f_is_NaN_S x32 = {

val negate_S : bits(32) -> bits(32)
function negate_S (x32) = {
let (sign, exp, mant) = fsplit_S (x32);
let (sign, exp, mant) = fstruct_S (x32);
let new_sign = if (sign == 0b0) then 0b1 else 0b0;
fmake_S (new_sign, exp, mant)
fstruct_S ((new_sign, exp, mant))
}

val feq_quiet_S : (bits(32), bits (32)) -> (bool, bits(5))
function feq_quiet_S (v1, v2) = {
let (s1, e1, m1) = fsplit_S (v1);
let (s2, e2, m2) = fsplit_S (v2);
let (s1, e1, m1) = fstruct_S (v1);
let (s2, e2, m2) = fstruct_S (v2);

let v1Is0 = f_is_neg_zero_S(v1) | f_is_pos_zero_S(v1);
let v2Is0 = f_is_neg_zero_S(v2) | f_is_pos_zero_S(v2);
Expand All @@ -196,8 +203,8 @@ function feq_quiet_S (v1, v2) = {

val flt_S : (bits(32), bits (32), bool) -> (bool, bits(5))
function flt_S (v1, v2, is_quiet) = {
let (s1, e1, m1) = fsplit_S (v1);
let (s2, e2, m2) = fsplit_S (v2);
let (s1, e1, m1) = fstruct_S (v1);
let (s2, e2, m2) = fstruct_S (v2);

let result : bool =
if (s1 == 0b0) & (s2 == 0b0) then
Expand Down Expand Up @@ -227,8 +234,8 @@ function flt_S (v1, v2, is_quiet) = {

val fle_S : (bits(32), bits (32), bool) -> (bool, bits(5))
function fle_S (v1, v2, is_quiet) = {
let (s1, e1, m1) = fsplit_S (v1);
let (s2, e2, m2) = fsplit_S (v2);
let (s1, e1, m1) = fstruct_S (v1);
let (s2, e2, m2) = fstruct_S (v2);

let v1Is0 = f_is_neg_zero_S(v1) | f_is_pos_zero_S(v1);
let v2Is0 = f_is_neg_zero_S(v2) | f_is_pos_zero_S(v2);
Expand Down Expand Up @@ -850,9 +857,9 @@ mapping clause encdec = F_BIN_TYPE_S(rs2, rs1, rd, FLE_S) if hav
function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FSGNJ_S)) = {
let rs1_val_S = F_or_X_S(rs1);
let rs2_val_S = F_or_X_S(rs2);
let (s1, e1, m1) = fsplit_S (rs1_val_S);
let (s2, e2, m2) = fsplit_S (rs2_val_S);
let rd_val_S = fmake_S (s2, e1, m1);
let (s1, e1, m1) = fstruct_S (rs1_val_S);
let (s2, e2, m2) = fstruct_S (rs2_val_S);
let rd_val_S = fstruct_S ((s2, e1, m1));

F_or_X_S(rd) = rd_val_S;
RETIRE_SUCCESS
Expand All @@ -861,9 +868,9 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FSGNJ_S)) = {
function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FSGNJN_S)) = {
let rs1_val_S = F_or_X_S(rs1);
let rs2_val_S = F_or_X_S(rs2);
let (s1, e1, m1) = fsplit_S (rs1_val_S);
let (s2, e2, m2) = fsplit_S (rs2_val_S);
let rd_val_S = fmake_S (0b1 ^ s2, e1, m1);
let (s1, e1, m1) = fstruct_S (rs1_val_S);
let (s2, e2, m2) = fstruct_S (rs2_val_S);
let rd_val_S = fstruct_S ((0b1 ^ s2, e1, m1));

F_or_X_S(rd) = rd_val_S;
RETIRE_SUCCESS
Expand All @@ -872,9 +879,9 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FSGNJN_S)) = {
function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FSGNJX_S)) = {
let rs1_val_S = F_or_X_S(rs1);
let rs2_val_S = F_or_X_S(rs2);
let (s1, e1, m1) = fsplit_S (rs1_val_S);
let (s2, e2, m2) = fsplit_S (rs2_val_S);
let rd_val_S = fmake_S (s1 ^ s2, e1, m1);
let (s1, e1, m1) = fstruct_S (rs1_val_S);
let (s2, e2, m2) = fstruct_S (rs2_val_S);
let rd_val_S = fstruct_S ((s1 ^ s2, e1, m1));

F_or_X_S(rd) = rd_val_S;
RETIRE_SUCCESS
Expand Down
Loading
Loading