Skip to content

Commit df7ae02

Browse files
jordancarlinjordancarlin
committed
Add f128 support for Lem
1 parent 69e47da commit df7ae02

File tree

2 files changed

+103
-25
lines changed

2 files changed

+103
-25
lines changed

‎handwritten_support/riscv_extras_fdext.lem‎

Lines changed: 80 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -89,6 +89,9 @@ let softfloat_f32_round_to_int _ _ _ = ()
8989
val softfloat_f64_round_to_int : bitvector -> bitvector -> bool -> unit
9090
let softfloat_f64_round_to_int _ _ _ = ()
9191

92+
val softfloat_f128_round_to_int : bitvector -> bitvector -> bool -> unit
93+
let softfloat_f128_round_to_int _ _ _ = ()
94+
9295
val softfloat_f16_add : bitvector -> bitvector -> bitvector -> unit
9396
let softfloat_f16_add _ _ _ = ()
9497

@@ -125,6 +128,18 @@ let softfloat_f64_mul _ _ _ = ()
125128
val softfloat_f64_div : bitvector -> bitvector -> bitvector -> unit
126129
let softfloat_f64_div _ _ _ = ()
127130

131+
val softfloat_f128_add : bitvector -> bitvector -> bitvector -> unit
132+
let softfloat_f128_add _ _ _ = ()
133+
134+
val softfloat_f128_sub : bitvector -> bitvector -> bitvector -> unit
135+
let softfloat_f128_sub _ _ _ = ()
136+
137+
val softfloat_f128_mul : bitvector -> bitvector -> bitvector -> unit
138+
let softfloat_f128_mul _ _ _ = ()
139+
140+
val softfloat_f128_div : bitvector -> bitvector -> bitvector -> unit
141+
let softfloat_f128_div _ _ _ = ()
142+
128143

129144
val softfloat_f16_muladd : bitvector -> bitvector -> bitvector -> bitvector -> unit
130145
let softfloat_f16_muladd _ _ _ _ = ()
@@ -135,6 +150,9 @@ let softfloat_f32_muladd _ _ _ _ = ()
135150
val softfloat_f64_muladd : bitvector -> bitvector -> bitvector -> bitvector -> unit
136151
let softfloat_f64_muladd _ _ _ _ = ()
137152

153+
val softfloat_f128_muladd : bitvector -> bitvector -> bitvector -> bitvector -> unit
154+
let softfloat_f128_muladd _ _ _ _ = ()
155+
138156

139157
val softfloat_f16_sqrt : bitvector -> bitvector -> unit
140158
let softfloat_f16_sqrt _ _ = ()
@@ -145,6 +163,9 @@ let softfloat_f32_sqrt _ _ = ()
145163
val softfloat_f64_sqrt : bitvector -> bitvector -> unit
146164
let softfloat_f64_sqrt _ _ = ()
147165

166+
val softfloat_f128_sqrt : bitvector -> bitvector -> unit
167+
let softfloat_f128_sqrt _ _ = ()
168+
148169

149170
val softfloat_f16_to_i32: bitvector -> bitvector -> unit
150171
let softfloat_f16_to_i32 _ _ = ()
@@ -220,25 +241,67 @@ let softfloat_i64_to_f64 _ _ = ()
220241
val softfloat_ui64_to_f64: bitvector -> bitvector -> unit
221242
let softfloat_ui64_to_f64 _ _ = ()
222243

244+
val softfloat_f128_to_i32: bitvector -> bitvector -> unit
245+
let softfloat_f128_to_i32 _ _ = ()
246+
247+
val softfloat_f128_to_ui32: bitvector -> bitvector -> unit
248+
let softfloat_f128_to_ui32 _ _ = ()
249+
250+
val softfloat_i32_to_f128: bitvector -> bitvector -> unit
251+
let softfloat_i32_to_f128 _ _ = ()
252+
253+
val softfloat_ui32_to_f128: bitvector -> bitvector -> unit
254+
let softfloat_ui32_to_f128 _ _ = ()
255+
256+
val softfloat_f128_to_i64: bitvector -> bitvector -> unit
257+
let softfloat_f128_to_i64 _ _ = ()
258+
259+
val softfloat_f128_to_ui64: bitvector -> bitvector -> unit
260+
let softfloat_f128_to_ui64 _ _ = ()
261+
262+
val softfloat_i64_to_f128: bitvector -> bitvector -> unit
263+
let softfloat_i64_to_f128 _ _ = ()
264+
265+
val softfloat_ui64_to_f128: bitvector -> bitvector -> unit
266+
let softfloat_ui64_to_f128 _ _ = ()
267+
223268

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

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

230-
val softfloat_f32_to_f64: bitvector -> bitvector -> unit
231-
let softfloat_f32_to_f64 _ _ = ()
275+
val softfloat_f16_to_f128: bitvector -> bitvector -> unit
276+
let softfloat_f16_to_f128 _ _ = ()
232277

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

281+
val softfloat_f32_to_f64: bitvector -> bitvector -> unit
282+
let softfloat_f32_to_f64 _ _ = ()
283+
284+
val softfloat_f32_to_f128: bitvector -> bitvector -> unit
285+
let softfloat_f32_to_f128 _ _ = ()
286+
236287
val softfloat_f64_to_f16: bitvector -> bitvector -> unit
237288
let softfloat_f64_to_f16 _ _ = ()
238289

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

293+
val softfloat_f64_to_f128: bitvector -> bitvector -> unit
294+
let softfloat_f64_to_f128 _ _ = ()
295+
296+
val softfloat_f128_to_f16: bitvector -> bitvector -> unit
297+
let softfloat_f128_to_f16 _ _ = ()
298+
299+
val softfloat_f128_to_f32: bitvector -> bitvector -> unit
300+
let softfloat_f128_to_f32 _ _ = ()
301+
302+
val softfloat_f128_to_f64: bitvector -> bitvector -> unit
303+
let softfloat_f128_to_f64 _ _ = ()
304+
242305

243306
val softfloat_f16_lt : bitvector -> bitvector -> unit
244307
let softfloat_f16_lt _ _ = ()
@@ -284,3 +347,18 @@ let softfloat_f64_le_quiet _ _ = ()
284347

285348
val softfloat_f64_eq : bitvector -> bitvector -> unit
286349
let softfloat_f64_eq _ _ = ()
350+
351+
val softfloat_f128_lt : bitvector -> bitvector -> unit
352+
let softfloat_f128_lt _ _ = ()
353+
354+
val softfloat_f128_lt_quiet : bitvector -> bitvector -> unit
355+
let softfloat_f128_lt_quiet _ _ = ()
356+
357+
val softfloat_f128_le : bitvector -> bitvector -> unit
358+
let softfloat_f128_le _ _ = ()
359+
360+
val softfloat_f128_le_quiet : bitvector -> bitvector -> unit
361+
let softfloat_f128_le_quiet _ _ = ()
362+
363+
val softfloat_f128_eq : bitvector -> bitvector -> unit
364+
let softfloat_f128_eq _ _ = ()

‎model/riscv_softfloat_interface.sail‎

Lines changed: 23 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -133,28 +133,28 @@ function riscv_f64Div (rm, v1, v2) = {
133133
}
134134

135135

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

0 commit comments

Comments
 (0)