-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathDefinitions.v
286 lines (227 loc) · 9.22 KB
/
Definitions.v
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
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
Require Import Kami.AllNotations.
Section Definitions.
Variable expWidthMinus2 sigWidthMinus2: nat.
Local Notation expWidthMinus1 := (expWidthMinus2 + 1).
Local Notation expWidth := (expWidthMinus1 + 1).
Local Notation sigWidthMinus1 := (sigWidthMinus2 + 1).
Local Notation sigWidth := (sigWidthMinus1 + 1).
Definition FN :=
STRUCT_TYPE {
"sign" :: Bool;
"exp" :: Bit expWidth;
"frac" :: Bit sigWidthMinus1
}.
Definition RawFloat :=
STRUCT_TYPE {
"isNaN" :: Bool;
"isInf" :: Bool;
"isZero" :: Bool;
"sign" :: Bool;
"sExp" :: Bit (expWidth + 1);
"sig" :: Bit sigWidthMinus1
}.
Definition RecFN :=
STRUCT_TYPE {
"sign" :: Bool;
"isZeroNaNInf0" :: Bit 1;
"isZeroNaNInf1" :: Bit 1;
"isZeroNaNInf2" :: Bit 1;
"exp" :: Bit expWidthMinus2;
"fract" :: Bit sigWidthMinus1
}.
Definition NF :=
STRUCT_TYPE {
"isNaN" :: Bool;
"isInf" :: Bool;
"isZero" :: Bool;
"sign" :: Bool;
"sExp" :: Bit (expWidth + 1);
"sig" :: Bit sigWidthMinus1
}.
Definition ExceptionFlags :=
STRUCT_TYPE {
"invalid" :: Bool;
"infinite" :: Bool;
"overflow" :: Bool;
"underflow" :: Bool;
"inexact" :: Bool
}.
Definition OpOutput :=
STRUCT_TYPE {
"out" :: NF;
"exceptionFlags" :: ExceptionFlags
}.
Section Ty.
Open Scope kami_expr.
Variable ty: Kind -> Type.
Section FromFN.
Variable fn: FN @# ty.
Definition sign := fn @% "sign".
Let expIn := fn @% "exp".
Let fractIn := fn @% "frac".
Definition infOrNaN := expIn == $$ (wones expWidth).
Definition isZeroExpIn := expIn == $ 0.
Definition isZeroFractIn := fractIn == $ 0.
Definition isNaN := infOrNaN && ! isZeroFractIn.
Definition normDist :=
IF fractIn == $0
then $sigWidthMinus2
else countLeadingZeros (expWidth + 1) fractIn.
Definition subnormFract := fractIn << (normDist + $ 1).
Definition normalizedExp: Bit (expWidth + 1) @# ty :=
(IF isZeroExpIn
then $ 2 - $ (2 ^ expWidthMinus1) - (normDist + $ 1)
else ZeroExtend 1 expIn - $ (2 ^ expWidthMinus1 - 1)).
Definition normalizedFrac: Bit sigWidthMinus1 @# ty := IF isZeroExpIn then subnormFract else fractIn.
Definition isZero := isZeroExpIn && isZeroFractIn.
Definition getNF_from_FN: NF @# ty :=
STRUCT {
"isNaN" ::= isNaN;
"isInf" ::= infOrNaN && isZeroFractIn;
"isZero" ::= isZero;
"sign" ::= sign;
"sExp" ::= normalizedExp;
"sig" ::= normalizedFrac
}.
Definition fracMsb := UniBit (TruncMsb _ 1) fractIn.
Definition isSNaN := isNaN && fracMsb == $$ WO~0.
Definition adjustedExp: Bit (expWidth + 1) @# ty :=
(IF isZeroExpIn
then ~ normDist
else ZeroExtend 1 expIn) + ZeroExtend 1 ({<$$ WO~1, IF isZeroExpIn then $ 2 else $ 1 >}).
Definition isSpecialMsb := UniBit (TruncMsb expWidth 1) adjustedExp == $ 1.
Definition isSpecialLsb := ConstExtract expWidthMinus1 1 1 adjustedExp == $ 1.
Definition isSpecial := isSpecialMsb && isSpecialLsb.
Definition getRawFloat_from_FN: RawFloat @# ty :=
STRUCT {
"isNaN" ::= isSpecial && !isZeroFractIn;
"isInf" ::= isSpecial && isZeroFractIn;
"isZero" ::= isZero;
"sign" ::= sign;
"sExp" ::= adjustedExp;
"sig" ::= IF isZeroExpIn then subnormFract else fractIn
}.
End FromFN.
Section getRecFN_from_RawFloat.
Variable rawFloat: RawFloat @# ty.
Let sExp := rawFloat @% "sExp".
Definition sExp_expWidth := UniBit (TruncMsb _ 1) sExp.
Definition sExp_expWidthMinus1 := UniBit (TruncMsb _ 1)
(UniBit (TruncLsb _ 1) sExp).
Definition sExp_expWidthMinus2 := UniBit (TruncMsb _ 1)
(UniBit (TruncLsb _ 1)
(UniBit (TruncLsb _ 1) sExp)).
Definition getRecFN_from_RawFloat: RecFN @# ty :=
STRUCT {
"sign" ::= rawFloat @% "sign";
"isZeroNaNInf0" ::= (IF rawFloat @% "isZero" then $$ WO~0 else
sExp_expWidth);
"isZeroNaNInf1" ::= (IF rawFloat @% "isZero" then $$ WO~0 else
sExp_expWidthMinus1);
"isZeroNaNInf2" ::= ((IF rawFloat @% "isZero" then $$ WO~0 else
sExp_expWidthMinus2) .| (IF rawFloat @% "isNaN" then
$$ WO~1 else $$ WO~0));
"exp" ::= UniBit (TruncLsb _ 1)
(UniBit (TruncLsb _ 1)
(UniBit (TruncLsb _ 1) sExp));
"fract" ::= rawFloat @% "sig"
}.
End getRecFN_from_RawFloat.
Section getRawFloat_from_RecFN.
Variable recFN: RecFN @# ty.
Let exp := recFN @% "exp".
Definition isZeroNaNInf0 := recFN @% "isZeroNaNInf0".
Definition isZeroNaNInf1 := recFN @% "isZeroNaNInf1".
Definition isZeroNaNInf2 := recFN @% "isZeroNaNInf2".
Definition isZeroRecFN := isZeroNaNInf0 == $0 && isZeroNaNInf1 == $0 && isZeroNaNInf2 == $0.
Definition isNaN_or_Inf := isZeroNaNInf0 == $1 && isZeroNaNInf1 == $1.
Definition get_exp_from_RecFN: Bit (expWidth + 1) @# ty :=
{< isZeroNaNInf0, isZeroNaNInf1, isZeroNaNInf2, exp >}.
Definition getRawFloat_from_RecFN: RawFloat @# ty :=
STRUCT {
"isNaN" ::= isNaN_or_Inf && isZeroNaNInf2 == $ 1;
"isInf" ::= isNaN_or_Inf && isZeroNaNInf2 == $ 0;
"isZero" ::= isZeroRecFN;
"sign" ::= recFN @% "sign";
"sExp" ::= get_exp_from_RecFN;
"sig" ::= recFN @% "fract"
}.
End getRawFloat_from_RecFN.
Section getFN_from_NF.
Variable nf: NF @# ty.
Let exp := nf @% "sExp".
Let frac := nf @% "sig".
Let isZeroNF := nf @% "isZero".
Let isNaNNF := nf @% "isNaN".
Let isInfNF := nf @% "isInf".
Definition isSubnormalExp := exp <s ($ 2 - $(2 ^ expWidthMinus1)).
Definition subnormDist := $1 - $(2 ^ expWidthMinus1) - exp.
Definition truncFrac : Expr ty (SyntaxKind (Bit (sigWidthMinus2))).
refine (UniBit (TruncMsb 1 sigWidthMinus2)
(castBits _ frac)).
rewrite Nat.add_comm; reflexivity.
Defined.
Definition subnormFrac := {< $$(WO~1), truncFrac >} >> subnormDist.
Definition nonSpecializedFrac := IF isSubnormalExp then subnormFrac else frac.
Definition nonSpecializedExp: Bit expWidth @# ty :=
IF isSubnormalExp
then $0
else UniBit (TruncLsb _ 1) (exp + $(2 ^ expWidthMinus1 - 1)).
Definition specializedExp :=
(IF isZeroNF
then $0
else IF (isNaNNF || isInfNF)
then $$(wones expWidth)
else nonSpecializedExp).
Definition specializedFrac :=
(IF (isZeroNF || isInfNF)
then $0
else (IF isNaNNF
then (IF frac == $0
then {< $$ WO~1, $ 0 >}
else frac) (* {< $$ WO~1, $ 0 >} *)
else nonSpecializedFrac)).
Definition getFN_from_NF: FN @# ty :=
STRUCT {
"sign" ::= nf @% "sign" (* && !(nf @% "isNaN") *);
"exp" ::= specializedExp;
"frac" ::= specializedFrac
}.
End getFN_from_NF.
Section getRawFloat_from_NF.
Variable nf: NF @# ty.
Definition getRawFloat_from_NF: RawFloat @# ty :=
STRUCT {
"isNaN" ::= (nf @% "isNaN");
"isInf" ::= (nf @% "isInf");
"isZero" ::= (nf @% "isZero");
"sign" ::= (nf @% "sign");
"sExp" ::= (nf @% "sExp" - $(2 ^ expWidth));
"sig" ::= (nf @% "sig")
}.
End getRawFloat_from_NF.
Section getNF_from_RawFloat.
Variable rf: RawFloat @# ty.
Definition getNF_from_RawFloat: NF @# ty :=
STRUCT {
"isNaN" ::= (rf @% "isNaN");
"isInf" ::= (rf @% "isInf");
"isZero" ::= (rf @% "isZero");
"sign" ::= (rf @% "sign");
"sExp" ::= (rf @% "sExp" + $(2 ^ expWidth));
"sig" ::= (rf @% "sig")
}.
End getNF_from_RawFloat.
Definition getRecFN_from_FN fn := getRecFN_from_RawFloat (getRawFloat_from_FN fn).
Definition getFN_from_RawFloat rf := getFN_from_NF (getNF_from_RawFloat rf).
Definition getNF_from_RecFN rfn := getNF_from_RawFloat (getRawFloat_from_RecFN rfn).
Definition getFN_from_RecFN rfn := getFN_from_NF (getNF_from_RecFN rfn).
Definition getRecFN_from_NF nf := getRecFN_from_FN (getFN_from_NF nf).
End Ty.
End Definitions.
Notation round_near_even := (natToWord 3 0).
Notation round_minMag := (natToWord 3 1).
Notation round_min := (natToWord 3 2).
Notation round_max := (natToWord 3 3).
Notation round_near_maxMag := (natToWord 3 4).
Notation round_odd := (natToWord 3 6).