1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
|
open import Pervasives
open import Pervasives_extra
open import Sail2_instr_kinds
open import Sail2_values
open import Sail2_operators_mwords
open import Sail2_prompt_monad
open import Sail2_prompt
type bitvector 'a = mword 'a
(* stub functions emulating the C softfloat interface *)
val softfloat_f32_add : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
let softfloat_f32_add _ _ _ = ()
val softfloat_f32_sub : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
let softfloat_f32_sub _ _ _ = ()
val softfloat_f32_mul : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
let softfloat_f32_mul _ _ _ = ()
val softfloat_f32_div : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
let softfloat_f32_div _ _ _ = ()
val softfloat_f64_add : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
let softfloat_f64_add _ _ _ = ()
val softfloat_f64_sub : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
let softfloat_f64_sub _ _ _ = ()
val softfloat_f64_mul : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
let softfloat_f64_mul _ _ _ = ()
val softfloat_f64_div : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
let softfloat_f64_div _ _ _ = ()
val softfloat_f32_muladd : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> bitvector 's -> unit
let softfloat_f32_muladd _ _ _ _ = ()
val softfloat_f64_muladd : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> bitvector 's -> unit
let softfloat_f64_muladd _ _ _ _ = ()
val softfloat_f32_sqrt : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
let softfloat_f32_sqrt _ _ = ()
val softfloat_f64_sqrt : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
let softfloat_f64_sqrt _ _ = ()
val softfloat_f32_to_i32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
let softfloat_f32_to_i32 _ _ = ()
val softfloat_f32_to_ui32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
let softfloat_f32_to_ui32 _ _ = ()
val softfloat_i32_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
let softfloat_i32_to_f32 _ _ = ()
val softfloat_ui32_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
let softfloat_ui32_to_f32 _ _ = ()
val softfloat_f32_to_i64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
let softfloat_f32_to_i64 _ _ = ()
val softfloat_f32_to_ui64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
let softfloat_f32_to_ui64 _ _ = ()
val softfloat_i64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
let softfloat_i64_to_f32 _ _ = ()
val softfloat_ui64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
let softfloat_ui64_to_f32 _ _ = ()
val softfloat_f64_to_i32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
let softfloat_f64_to_i32 _ _ = ()
val softfloat_f64_to_ui32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
let softfloat_f64_to_ui32 _ _ = ()
val softfloat_i32_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
let softfloat_i32_to_f64 _ _ = ()
val softfloat_ui32_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
let softfloat_ui32_to_f64 _ _ = ()
val softfloat_f64_to_i64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
let softfloat_f64_to_i64 _ _ = ()
val softfloat_f64_to_ui64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
let softfloat_f64_to_ui64 _ _ = ()
val softfloat_i64_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
let softfloat_i64_to_f64 _ _ = ()
val softfloat_ui64_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
let softfloat_ui64_to_f64 _ _ = ()
val softfloat_f32_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
let softfloat_f32_to_f64 _ _ = ()
val softfloat_f64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
let softfloat_f64_to_f32 _ _ = ()
val softfloat_f32_lt : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
let softfloat_f32_lt _ _ = ()
val softfloat_f32_le : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
let softfloat_f32_le _ _ = ()
val softfloat_f32_eq : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
let softfloat_f32_eq _ _ = ()
val softfloat_f64_lt : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
let softfloat_f64_lt _ _ = ()
val softfloat_f64_le : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
let softfloat_f64_le _ _ = ()
val softfloat_f64_eq : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
let softfloat_f64_eq _ _ = ()
|
