Skip to content

Commit

Permalink
Add f128 support for Lem
Browse files Browse the repository at this point in the history
  • Loading branch information
@jordancarlin
jordancarlin committed Apr 19, 2024
1 parent a6f2091 commit e52a2b0
Show file tree
Hide file tree
Showing 2 changed files with 103 additions and 25 deletions.
82 changes: 80 additions & 2 deletions handwritten_support/riscv_extras_fdext.lem
View file
Original file line number Diff line number Diff line change
Expand Up @@ -89,6 +89,9 @@ let softfloat_f32_round_to_int _ _ _ = ()
val softfloat_f64_round_to_int : bitvector -> bitvector -> bool -> unit
let softfloat_f64_round_to_int _ _ _ = ()

val softfloat_f128_round_to_int : bitvector -> bitvector -> bool -> unit
let softfloat_f128_round_to_int _ _ _ = ()

val softfloat_f16_add : bitvector -> bitvector -> bitvector -> unit
let softfloat_f16_add _ _ _ = ()

Expand Down Expand Up @@ -125,6 +128,18 @@ let softfloat_f64_mul _ _ _ = ()
val softfloat_f64_div : bitvector -> bitvector -> bitvector -> unit
let softfloat_f64_div _ _ _ = ()

val softfloat_f128_add : bitvector -> bitvector -> bitvector -> unit
let softfloat_f128_add _ _ _ = ()

val softfloat_f128_sub : bitvector -> bitvector -> bitvector -> unit
let softfloat_f128_sub _ _ _ = ()

val softfloat_f128_mul : bitvector -> bitvector -> bitvector -> unit
let softfloat_f128_mul _ _ _ = ()

val softfloat_f128_div : bitvector -> bitvector -> bitvector -> unit
let softfloat_f128_div _ _ _ = ()


val softfloat_f16_muladd : bitvector -> bitvector -> bitvector -> bitvector -> unit
let softfloat_f16_muladd _ _ _ _ = ()
Expand All @@ -135,6 +150,9 @@ let softfloat_f32_muladd _ _ _ _ = ()
val softfloat_f64_muladd : bitvector -> bitvector -> bitvector -> bitvector -> unit
let softfloat_f64_muladd _ _ _ _ = ()

val softfloat_f128_muladd : bitvector -> bitvector -> bitvector -> bitvector -> unit
let softfloat_f128_muladd _ _ _ _ = ()


val softfloat_f16_sqrt : bitvector -> bitvector -> unit
let softfloat_f16_sqrt _ _ = ()
Expand All @@ -145,6 +163,9 @@ let softfloat_f32_sqrt _ _ = ()
val softfloat_f64_sqrt : bitvector -> bitvector -> unit
let softfloat_f64_sqrt _ _ = ()

val softfloat_f128_sqrt : bitvector -> bitvector -> unit
let softfloat_f128_sqrt _ _ = ()


val softfloat_f16_to_i32: bitvector -> bitvector -> unit
let softfloat_f16_to_i32 _ _ = ()
Expand Down Expand Up @@ -220,25 +241,67 @@ let softfloat_i64_to_f64 _ _ = ()
val softfloat_ui64_to_f64: bitvector -> bitvector -> unit
let softfloat_ui64_to_f64 _ _ = ()

val softfloat_f128_to_i32: bitvector -> bitvector -> unit
let softfloat_f128_to_i32 _ _ = ()

val softfloat_f128_to_ui32: bitvector -> bitvector -> unit
let softfloat_f128_to_ui32 _ _ = ()

val softfloat_i32_to_f128: bitvector -> bitvector -> unit
let softfloat_i32_to_f128 _ _ = ()

val softfloat_ui32_to_f128: bitvector -> bitvector -> unit
let softfloat_ui32_to_f128 _ _ = ()

val softfloat_f128_to_i64: bitvector -> bitvector -> unit
let softfloat_f128_to_i64 _ _ = ()

val softfloat_f128_to_ui64: bitvector -> bitvector -> unit
let softfloat_f128_to_ui64 _ _ = ()

val softfloat_i64_to_f128: bitvector -> bitvector -> unit
let softfloat_i64_to_f128 _ _ = ()

val softfloat_ui64_to_f128: bitvector -> bitvector -> unit
let softfloat_ui64_to_f128 _ _ = ()


val softfloat_f16_to_f32: bitvector -> bitvector -> unit
let softfloat_f16_to_f32 _ _ = ()

val softfloat_f16_to_f64: bitvector -> bitvector -> unit
let softfloat_f16_to_f64 _ _ = ()

val softfloat_f32_to_f64: bitvector -> bitvector -> unit
let softfloat_f32_to_f64 _ _ = ()
val softfloat_f16_to_f128: bitvector -> bitvector -> unit
let softfloat_f16_to_f128 _ _ = ()

val softfloat_f32_to_f16: bitvector -> bitvector -> unit
let softfloat_f32_to_f16 _ _ = ()

val softfloat_f32_to_f64: bitvector -> bitvector -> unit
let softfloat_f32_to_f64 _ _ = ()

val softfloat_f32_to_f128: bitvector -> bitvector -> unit
let softfloat_f32_to_f128 _ _ = ()

val softfloat_f64_to_f16: bitvector -> bitvector -> unit
let softfloat_f64_to_f16 _ _ = ()

val softfloat_f64_to_f32: bitvector -> bitvector -> unit
let softfloat_f64_to_f32 _ _ = ()

val softfloat_f64_to_f128: bitvector -> bitvector -> unit
let softfloat_f64_to_f128 _ _ = ()

val softfloat_f128_to_f16: bitvector -> bitvector -> unit
let softfloat_f128_to_f16 _ _ = ()

val softfloat_f128_to_f32: bitvector -> bitvector -> unit
let softfloat_f128_to_f32 _ _ = ()

val softfloat_f128_to_f64: bitvector -> bitvector -> unit
let softfloat_f128_to_f64 _ _ = ()


val softfloat_f16_lt : bitvector -> bitvector -> unit
let softfloat_f16_lt _ _ = ()
Expand Down Expand Up @@ -284,3 +347,18 @@ let softfloat_f64_le_quiet _ _ = ()

val softfloat_f64_eq : bitvector -> bitvector -> unit
let softfloat_f64_eq _ _ = ()

val softfloat_f128_lt : bitvector -> bitvector -> unit
let softfloat_f128_lt _ _ = ()

val softfloat_f128_lt_quiet : bitvector -> bitvector -> unit
let softfloat_f128_lt_quiet _ _ = ()

val softfloat_f128_le : bitvector -> bitvector -> unit
let softfloat_f128_le _ _ = ()

val softfloat_f128_le_quiet : bitvector -> bitvector -> unit
let softfloat_f128_le_quiet _ _ = ()

val softfloat_f128_eq : bitvector -> bitvector -> unit
let softfloat_f128_eq _ _ = ()
46 changes: 23 additions & 23 deletions model/riscv_softfloat_interface.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -133,28 +133,28 @@ function riscv_f64Div (rm, v1, v2) = {
}


val extern_f128Add = {c: "softfloat_f128add", ocaml: "Softfloat.f128_add"} : (bits_rm, bits_Q, bits_Q) -> unit
val extern_f128Add = {c: "softfloat_f128add", ocaml: "Softfloat.f128_add", lem: "softfloat_f128_add"} : (bits_rm, bits_Q, bits_Q) -> unit
val riscv_f128Add : (bits_rm, bits_Q, bits_Q) -> (bits_fflags, bits_Q)
function riscv_f128Add (rm, v1, v2) = {
extern_f128Add(rm, v1, v2);
(float_fflags[4 .. 0], float_result[127..0])
}

val extern_f128Sub = {c: "softfloat_f128sub", ocaml: "Softfloat.f128_sub"} : (bits_rm, bits_Q, bits_Q) -> unit
val extern_f128Sub = {c: "softfloat_f128sub", ocaml: "Softfloat.f128_sub", lem: "softfloat_f128_sub"} : (bits_rm, bits_Q, bits_Q) -> unit
val riscv_f128Sub : (bits_rm, bits_Q, bits_Q) -> (bits_fflags, bits_Q)
function riscv_f128Sub (rm, v1, v2) = {
extern_f128Sub(rm, v1, v2);
(float_fflags[4 .. 0], float_result[127..0])
}

val extern_f128Mul = {c: "softfloat_f128mul", ocaml: "Softfloat.f128_mul"} : (bits_rm, bits_Q, bits_Q) -> unit
val extern_f128Mul = {c: "softfloat_f128mul", ocaml: "Softfloat.f128_mul", lem: "softfloat_f128_mul"} : (bits_rm, bits_Q, bits_Q) -> unit
val riscv_f128Mul : (bits_rm, bits_Q, bits_Q) -> (bits_fflags, bits_Q)
function riscv_f128Mul (rm, v1, v2) = {
extern_f128Mul(rm, v1, v2);
(float_fflags[4 .. 0], float_result[127..0])
}

val extern_f128Div = {c: "softfloat_f128div", ocaml: "Softfloat.f128_div"} : (bits_rm, bits_Q, bits_Q) -> unit
val extern_f128Div = {c: "softfloat_f128div", ocaml: "Softfloat.f128_div", lem: "softfloat_f128_div"} : (bits_rm, bits_Q, bits_Q) -> unit
val riscv_f128Div : (bits_rm, bits_Q, bits_Q) -> (bits_fflags, bits_Q)
function riscv_f128Div (rm, v1, v2) = {
extern_f128Div(rm, v1, v2);
Expand Down Expand Up @@ -184,7 +184,7 @@ function riscv_f64MulAdd (rm, v1, v2, v3) = {
(float_fflags[4 .. 0], float_result[63..0])
}

val extern_f128MulAdd = {c: "softfloat_f128muladd", ocaml: "Softfloat.f128_muladd"} : (bits_rm, bits_Q, bits_Q, bits_Q) -> unit
val extern_f128MulAdd = {c: "softfloat_f128muladd", ocaml: "Softfloat.f128_muladd", lem: "softfloat_f128_muladd"} : (bits_rm, bits_Q, bits_Q, bits_Q) -> unit
val riscv_f128MulAdd : (bits_rm, bits_Q, bits_Q, bits_Q) -> (bits_fflags, bits_Q)
function riscv_f128MulAdd (rm, v1, v2, v3) = {
extern_f128MulAdd(rm, v1, v2, v3);
Expand Down Expand Up @@ -216,7 +216,7 @@ function riscv_f64Sqrt (rm, v) = {
(float_fflags[4 .. 0], float_result[63..0])
}

val extern_f128Sqrt = {c: "softfloat_f128sqrt", ocaml: "Softfloat.f128_sqrt"} : (bits_rm, bits_Q) -> unit
val extern_f128Sqrt = {c: "softfloat_f128sqrt", ocaml: "Softfloat.f128_sqrt", lem: "softfloat_f128_sqrt"} : (bits_rm, bits_Q) -> unit
val riscv_f128Sqrt : (bits_rm, bits_Q) -> (bits_fflags, bits_Q)
function riscv_f128Sqrt (rm, v) = {
extern_f128Sqrt(rm, v);
Expand Down Expand Up @@ -394,56 +394,56 @@ function riscv_ui64ToF64 (rm, v) = {
(float_fflags[4 .. 0], float_result[63..0])
}

val extern_f128ToI32 = {c: "softfloat_f128toi32", ocaml: "Softfloat.f128_to_i32"} : (bits_rm, bits_Q) -> unit
val extern_f128ToI32 = {c: "softfloat_f128toi32", ocaml: "Softfloat.f128_to_i32", lem: "softfloat_f128_to_i32"} : (bits_rm, bits_Q) -> unit
val riscv_f128ToI32 : (bits_rm, bits_Q) -> (bits_fflags, bits_W)
function riscv_f128ToI32 (rm, v) = {
extern_f128ToI32(rm, v);
(float_fflags[4 .. 0], float_result[31..0])
}

val extern_f128ToUi32 = {c: "softfloat_f128toui32", ocaml: "Softfloat.f128_to_ui32"} : (bits_rm, bits_Q) -> unit
val extern_f128ToUi32 = {c: "softfloat_f128toui32", ocaml: "Softfloat.f128_to_ui32", lem: "softfloat_f128_to_ui32"} : (bits_rm, bits_Q) -> unit
val riscv_f128ToUi32 : (bits_rm, bits_Q) -> (bits_fflags, bits_W)
function riscv_f128ToUi32 (rm, v) = {
extern_f128ToUi32(rm, v);
(float_fflags[4 .. 0], float_result[31..0])
}

val extern_i32ToF128 = {c: "softfloat_i32tof128", ocaml: "Softfloat.i32_to_f128"} : (bits_rm, bits_W) -> unit
val extern_i32ToF128 = {c: "softfloat_i32tof128", ocaml: "Softfloat.i32_to_f128", lem: "softfloat_i32_to_f128"} : (bits_rm, bits_W) -> unit
val riscv_i32ToF128 : (bits_rm, bits_W) -> (bits_fflags, bits_Q)
function riscv_i32ToF128 (rm, v) = {
extern_i32ToF128(rm, v);
(float_fflags[4 .. 0], float_result[127..0])
}

val extern_ui32ToF128 = {c: "softfloat_ui32tof128", ocaml: "Softfloat.ui32_to_f128"} : (bits_rm, bits_W) -> unit
val extern_ui32ToF128 = {c: "softfloat_ui32tof128", ocaml: "Softfloat.ui32_to_f128", lem: "softfloat_ui32_to_f128"} : (bits_rm, bits_W) -> unit
val riscv_ui32ToF128 : (bits_rm, bits_W) -> (bits_fflags, bits_Q)
function riscv_ui32ToF128 (rm, v) = {
extern_ui32ToF128(rm, v);
(float_fflags[4 .. 0], float_result[127..0])
}

val extern_f128ToI64 = {c: "softfloat_f128toi64", ocaml: "Softfloat.f128_to_i64"} : (bits_rm, bits_Q) -> unit
val extern_f128ToI64 = {c: "softfloat_f128toi64", ocaml: "Softfloat.f128_to_i64", lem: "softfloat_f128_to_i64"} : (bits_rm, bits_Q) -> unit
val riscv_f128ToI64 : (bits_rm, bits_Q) -> (bits_fflags, bits_L)
function riscv_f128ToI64 (rm, v) = {
extern_f128ToI64(rm, v);
(float_fflags[4 .. 0], float_result[63..0])
}

val extern_f128ToUi64 = {c: "softfloat_f128toui64", ocaml: "Softfloat.f128_to_ui64"} : (bits_rm, bits_Q) -> unit
val extern_f128ToUi64 = {c: "softfloat_f128toui64", ocaml: "Softfloat.f128_to_ui64", lem: "softfloat_f128_to_ui64"} : (bits_rm, bits_Q) -> unit
val riscv_f128ToUi64 : (bits_rm, bits_Q) -> (bits_fflags, bits_LU)
function riscv_f128ToUi64 (rm, v) = {
extern_f128ToUi64(rm, v);
(float_fflags[4 .. 0], float_result[63..0])
}

val extern_i64ToF128 = {c: "softfloat_i64tof128", ocaml: "Softfloat.i64_to_f128"} : (bits_rm, bits_L) -> unit
val extern_i64ToF128 = {c: "softfloat_i64tof128", ocaml: "Softfloat.i64_to_f128", lem: "softfloat_i64_to_f128"} : (bits_rm, bits_L) -> unit
val riscv_i64ToF128 : (bits_rm, bits_L) -> (bits_fflags, bits_Q)
function riscv_i64ToF128 (rm, v) = {
extern_i64ToF128(rm, v);
(float_fflags[4 .. 0], float_result[127..0])
}

val extern_ui64ToF128 = {c: "softfloat_ui64tof128", ocaml: "Softfloat.ui64_to_f128"} : (bits_rm, bits_LU) -> unit
val extern_ui64ToF128 = {c: "softfloat_ui64tof128", ocaml: "Softfloat.ui64_to_f128", lem: "softfloat_ui64_to_f128"} : (bits_rm, bits_LU) -> unit
val riscv_ui64ToF128 : (bits_rm, bits_LU) -> (bits_fflags, bits_Q)
function riscv_ui64ToF128 (rm, v) = {
extern_ui64ToF128(rm, v);
Expand All @@ -464,7 +464,7 @@ function riscv_f16ToF64 (rm, v) = {
(float_fflags[4 .. 0], float_result[63..0])
}

val extern_f16ToF128 = {c: "softfloat_f16tof128", ocaml: "Softfloat.f16_to_f128"} : (bits_rm, bits_H) -> unit
val extern_f16ToF128 = {c: "softfloat_f16tof128", ocaml: "Softfloat.f16_to_f128", lem: "softfloat_f16_to_f128"} : (bits_rm, bits_H) -> unit
val riscv_f16ToF128 : (bits_rm, bits_H) -> (bits_fflags, bits_Q)
function riscv_f16ToF128 (rm, v) = {
extern_f16ToF128(rm, v);
Expand All @@ -485,7 +485,7 @@ function riscv_f32ToF64 (rm, v) = {
(float_fflags[4 .. 0], float_result[63..0])
}

val extern_f32ToF128 = {c: "softfloat_f32tof128", ocaml: "Softfloat.f32_to_f128"} : (bits_rm, bits_S) -> unit
val extern_f32ToF128 = {c: "softfloat_f32tof128", ocaml: "Softfloat.f32_to_f128", lem: "softfloat_f32_to_f128"} : (bits_rm, bits_S) -> unit
val riscv_f32ToF128 : (bits_rm, bits_S) -> (bits_fflags, bits_Q)
function riscv_f32ToF128 (rm, v) = {
extern_f32ToF128(rm, v);
Expand All @@ -506,28 +506,28 @@ function riscv_f64ToF32 (rm, v) = {
(float_fflags[4 .. 0], float_result[31 .. 0])
}

val extern_f64ToF128 = {c: "softfloat_f64tof128", ocaml: "Softfloat.f64_to_f128"} : (bits_rm, bits_D) -> unit
val extern_f64ToF128 = {c: "softfloat_f64tof128", ocaml: "Softfloat.f64_to_f128", lem: "softfloat_f64_to_f128"} : (bits_rm, bits_D) -> unit
val riscv_f64ToF128 : (bits_rm, bits_D) -> (bits_fflags, bits_Q)
function riscv_f64ToF128 (rm, v) = {
extern_f64ToF128(rm, v);
(float_fflags[4 .. 0], float_result[127..0])
}

val extern_f128ToF16 = {c: "softfloat_f128tof16", ocaml: "Softfloat.f128_to_f16"} : (bits_rm, bits_Q) -> unit
val extern_f128ToF16 = {c: "softfloat_f128tof16", ocaml: "Softfloat.f128_to_f16", lem: "softfloat_f128_to_f16"} : (bits_rm, bits_Q) -> unit
val riscv_f128ToF16 : (bits_rm, bits_Q) -> (bits_fflags, bits_H)
function riscv_f128ToF16 (rm, v) = {
extern_f128ToF16(rm, v);
(float_fflags[4 .. 0], float_result[15..0])
}

val extern_f128ToF32 = {c: "softfloat_f128tof32", ocaml: "Softfloat.f128_to_f32"} : (bits_rm, bits_Q) -> unit
val extern_f128ToF32 = {c: "softfloat_f128tof32", ocaml: "Softfloat.f128_to_f32", lem: "softfloat_f128_to_f32"} : (bits_rm, bits_Q) -> unit
val riscv_f128ToF32 : (bits_rm, bits_Q) -> (bits_fflags, bits_S)
function riscv_f128ToF32 (rm, v) = {
extern_f128ToF32(rm, v);
(float_fflags[4 .. 0], float_result[31..0])
}

val extern_f128ToF64 = {c: "softfloat_f128tof64", ocaml: "Softfloat.f128_to_f64"} : (bits_rm, bits_Q) -> unit
val extern_f128ToF64 = {c: "softfloat_f128tof64", ocaml: "Softfloat.f128_to_f64", lem: "softfloat_f128_to_f64"} : (bits_rm, bits_Q) -> unit
val riscv_f128ToF64 : (bits_rm, bits_Q) -> (bits_fflags, bits_D)
function riscv_f128ToF64 (rm, v) = {
extern_f128ToF64(rm, v);
Expand Down Expand Up @@ -642,7 +642,7 @@ function riscv_f64Eq (v1, v2) = {
(float_fflags[4 .. 0], bit_to_bool(float_result[0]))
}

val extern_f128Lt = {c: "softfloat_f128lt", ocaml: "Softfloat.f128_lt"} : (bits_Q, bits_Q) -> unit
val extern_f128Lt = {c: "softfloat_f128lt", ocaml: "Softfloat.f128_lt", lem: "softfloat_f128_lt"} : (bits_Q, bits_Q) -> unit
val riscv_f128Lt : (bits_Q, bits_Q) -> (bits_fflags, bool)
function riscv_f128Lt (v1, v2) = {
extern_f128Lt(v1, v2);
Expand All @@ -656,7 +656,7 @@ function riscv_f128Lt_quiet (v1, v2) = {
(float_fflags[4 .. 0], bit_to_bool(float_result[0]))
}

val extern_f128Le = {c: "softfloat_f128le", ocaml: "Softfloat.f128_le"} : (bits_Q, bits_Q) -> unit
val extern_f128Le = {c: "softfloat_f128le", ocaml: "Softfloat.f128_le", lem: "softfloat_f128_le"} : (bits_Q, bits_Q) -> unit
val riscv_f128Le : (bits_Q, bits_Q) -> (bits_fflags, bool)
function riscv_f128Le (v1, v2) = {
extern_f128Le(v1, v2);
Expand All @@ -670,7 +670,7 @@ function riscv_f128Le_quiet (v1, v2) = {
(float_fflags[4 .. 0], bit_to_bool(float_result[0]))
}

val extern_f128Eq = {c: "softfloat_f128eq", ocaml: "Softfloat.f128_eq"} : (bits_Q, bits_Q) -> unit
val extern_f128Eq = {c: "softfloat_f128eq", ocaml: "Softfloat.f128_eq", lem: "softfloat_f128_eq"} : (bits_Q, bits_Q) -> unit
val riscv_f128Eq : (bits_Q, bits_Q) -> (bits_fflags, bool)
function riscv_f128Eq (v1, v2) = {
extern_f128Eq(v1, v2);
Expand Down

0 comments on commit e52a2b0

Please sign in to comment.