7132a28426c578334a53832eff4b6d1583a93830
[ieee754fpu.git] / fp16mul_test.smt2
1 ; SPDX-License-Identifier: LGPL-2.1-or-later
2
3 ; Test to see if using smt-lib2's floating-point support for checking fpu hw
4 ; is feasible by implementing fp multiplication with bit-vectors and seeing if
5 ; the smt checkers work. The idea is we can run this test before putting in
6 ; all the effort to add support in yosys and nmigen for smtlib2 reals and
7 ; floating-point numbers.
8
9 ; run with: z3 -smt2 fp16mul_test.smt2
10 (set-logic ALL)
11
12 ; create some handy type aliases
13 (define-sort bv1 () (_ BitVec 1))
14 (define-sort bv2 () (_ BitVec 2))
15 (define-sort bv4 () (_ BitVec 4))
16 (define-sort bv5 () (_ BitVec 5))
17 (define-sort bv8 () (_ BitVec 8))
18 (define-sort bv10 () (_ BitVec 10))
19 (define-sort bv11 () (_ BitVec 11))
20 (define-sort bv16 () (_ BitVec 16))
21 (define-sort bv22 () (_ BitVec 22))
22 (define-sort bv32 () (_ BitVec 32))
23
24 ; type for signed f16 exponents
25 (define-sort f16_sexp_t () bv8)
26 ; signed less-than comparison
27 (define-fun f16_sexp_lt ((a f16_sexp_t) (b f16_sexp_t)) Bool
28 (bvult (bvxor #x80 a) (bvxor #x80 b))
29 )
30 ; subtraction
31 (define-fun f16_sexp_sub ((a f16_sexp_t) (b f16_sexp_t)) f16_sexp_t
32 (bvadd a (bvneg b))
33 )
34 ; conversion
35 (define-fun f16_sexp_to_bv5 ((v f16_sexp_t)) bv5 ((_ extract 4 0) v))
36 (define-fun bv5_to_f16_sexp ((v bv5)) f16_sexp_t (concat #b000 v))
37 (define-fun f16_sexp_to_bv22 ((v f16_sexp_t)) bv22 (concat #b00000000000000 v))
38 (define-fun bv22_to_f16_sexp ((v bv22)) f16_sexp_t ((_ extract 7 0) v))
39 (define-fun bv11_to_bv22 ((v bv11)) bv22 (concat #b00000000000 v))
40 (define-fun bv22_to_bv11 ((v bv22)) bv11 ((_ extract 10 0) v))
41 (define-fun bv22_to_bv32 ((v bv22)) bv32 (concat #b0000000000 v))
42 (define-fun bv32_to_bv22 ((v bv32)) bv22 ((_ extract 21 0) v))
43 (define-fun bv16_to_bv32 ((v bv16)) bv32 (concat #x0000 v))
44 (define-fun bv32_to_bv16 ((v bv32)) bv16 ((_ extract 15 0) v))
45 (define-fun bv8_to_bv16 ((v bv8)) bv16 (concat #x00 v))
46 (define-fun bv16_to_bv8 ((v bv16)) bv8 ((_ extract 7 0) v))
47 (define-fun bv4_to_bv8 ((v bv4)) bv8 (concat #x0 v))
48 (define-fun bv8_to_bv4 ((v bv8)) bv4 ((_ extract 3 0) v))
49 (define-fun bv2_to_bv4 ((v bv2)) bv4 (concat #b00 v))
50 (define-fun bv4_to_bv2 ((v bv4)) bv2 ((_ extract 1 0) v))
51 (define-fun bv1_to_bv2 ((v bv1)) bv2 (concat #b0 v))
52 (define-fun bv2_to_bv1 ((v bv2)) bv1 ((_ extract 0 0) v))
53 ; count-leading-zeros
54 (define-fun bv1_clz ((v bv1)) bv1
55 (bvxor #b1 v)
56 )
57 (define-fun bv2_clz ((v bv2)) bv2
58 (let
59 ((shift (ite (bvult #b01 v) #b00 #b01)))
60 (bvadd shift (bv1_to_bv2 (bv1_clz ((_ extract 1 1) (bvshl v shift)))))
61 )
62 )
63 (define-fun bv4_clz ((v bv4)) bv4
64 (let
65 ((shift (ite (bvult #x3 v) #x0 #x2)))
66 (bvadd shift (bv2_to_bv4 (bv2_clz ((_ extract 3 2) (bvshl v shift)))))
67 )
68 )
69 (define-fun bv8_clz ((v bv8)) bv8
70 (let
71 ((shift (ite (bvult #x0F v) #x00 #x04)))
72 (bvadd shift (bv4_to_bv8 (bv4_clz ((_ extract 7 4) (bvshl v shift)))))
73 )
74 )
75 (define-fun bv16_clz ((v bv16)) bv16
76 (let
77 ((shift (ite (bvult #x00FF v) #x0000 #x0008)))
78 (bvadd shift (bv8_to_bv16 (bv8_clz
79 ((_ extract 15 8) (bvshl v shift)))))
80 )
81 )
82 (define-fun bv32_clz ((v bv32)) bv32
83 (let
84 ((shift (ite (bvult #x0000FFFF v) #x00000000 #x00000010)))
85 (bvadd shift (bv16_to_bv32 (bv16_clz
86 ((_ extract 31 16) (bvshl v shift)))))
87 )
88 )
89 (define-fun bv22_clz ((v bv22)) bv22
90 (bv32_to_bv22 (bv32_clz (concat v #b0000000000)))
91 )
92 ; shift right merging shifted out bits into the result's lsb
93 (define-fun bv22_lshr_merging ((v bv22) (shift bv22)) bv22
94 ; did we shift out only zeros?
95 (ite (= v (bvshl (bvlshr v shift) shift))
96 ; yes. no adjustment needed
97 (bvlshr v shift)
98 ; no. set lsb
99 (bvor (bvlshr v shift) #b0000000000000000000001)
100 )
101 )
102
103 ; field extraction functions
104 (define-fun f16_sign_field ((v bv16)) bv1 ((_ extract 15 15) v))
105 (define-fun f16_exponent_field ((v bv16)) bv5 ((_ extract 14 10) v))
106 (define-fun f16_mantissa_field ((v bv16)) bv10 ((_ extract 9 0) v))
107 (define-fun f16_mantissa_field_msb ((v bv16)) bv1 ((_ extract 9 9) v))
108 ; construction from fields
109 (define-fun f16_from_fields ((sign_field bv1)
110 (exponent_field bv5)
111 (mantissa_field bv10)) bv16
112 (concat sign_field exponent_field mantissa_field)
113 )
114 ; handy constants
115 (define-fun f16_infinity ((sign_field bv1)) bv16
116 (f16_from_fields sign_field #b11111 #b0000000000)
117 )
118 (define-fun f16_zero ((sign_field bv1)) bv16
119 (f16_from_fields sign_field #b00000 #b0000000000)
120 )
121 ; conversion to quiet NaN
122 (define-fun f16_into_qnan ((v bv16)) bv16
123 (f16_from_fields
124 (f16_sign_field v)
125 #b11111
126 (bvor #b1000000000 (f16_mantissa_field v))
127 )
128 )
129 ; conversion
130 (define-fun f16_to_fp ((v bv16)) Float16 ((_ to_fp 5 11) v))
131 ; classification
132 (define-fun f16_is_nan ((v bv16)) Bool (fp.isNaN (f16_to_fp v)))
133 (define-fun f16_is_infinite ((v bv16)) Bool (fp.isInfinite (f16_to_fp v)))
134 (define-fun f16_is_normal ((v bv16)) Bool (fp.isNormal (f16_to_fp v)))
135 (define-fun f16_is_subnormal ((v bv16)) Bool (fp.isSubnormal (f16_to_fp v)))
136 (define-fun f16_is_zero ((v bv16)) Bool (fp.isZero (f16_to_fp v)))
137 (define-fun f16_is_qnan ((v bv16)) Bool
138 (and (f16_is_nan v) (= (f16_mantissa_field_msb v) #b1))
139 )
140 ; get mantissa value -- only correct for finite values
141 (define-fun f16_mantissa_value ((v bv16)) bv11
142 (ite (f16_is_subnormal v)
143 (concat #b0 (f16_mantissa_field v))
144 (concat #b1 (f16_mantissa_field v))
145 )
146 )
147 ; f16 field values
148 (define-const f16_exponent_bias f16_sexp_t #x0F)
149 (define-const f16_max_exponent f16_sexp_t #x10)
150 (define-const f16_subnormal_exponent f16_sexp_t #xF2) ; -14
151 (define-fun f16_exponent_value ((v bv16)) f16_sexp_t
152 (ite (= (f16_exponent_field v) #b00000)
153 f16_subnormal_exponent
154 (f16_sexp_sub
155 (bv5_to_f16_sexp (f16_exponent_field v))
156 f16_exponent_bias
157 )
158 )
159 )
160 ; f16 mul
161 (define-fun f16_round_product_final_step_rne ((sign bv1)
162 (product bv22)
163 (exponent f16_sexp_t)
164 (exponent_field bv5)) bv16
165 ; if the exponent doesn't overflow
166 (ite (f16_sexp_lt exponent f16_max_exponent)
167 ; if we rounded a subnormal up to a normal
168 (ite (and (= exponent_field #b00000) (not (bvult product #b1000000000000000000000)))
169 (f16_from_fields
170 sign
171 #b00001
172 ((_ extract 20 11) product)
173 )
174 (f16_from_fields
175 sign
176 exponent_field
177 ((_ extract 20 11) product)
178 )
179 )
180 (f16_infinity sign)
181 )
182 )
183 (define-fun f16_round_product_rne ((sign bv1)
184 (product bv22)
185 (exponent f16_sexp_t)
186 (exponent_field bv5)) bv16
187 (let
188 (
189 (half_way (= (bv22_to_bv11 product) #b10000000000))
190 (is_even (= ((_ extract 11 11) product) #b0))
191 (rounded_up (bvadd product (bv11_to_bv22 #b10000000000)))
192 )
193 (let
194 (
195 (round_up_overflows (bvult rounded_up product))
196 (do_round_up
197 (ite half_way
198 (not is_even)
199 (bvult #b10000000000 (bv22_to_bv11 product))
200 )
201 )
202 )
203 (ite do_round_up
204 (ite round_up_overflows
205 (f16_round_product_final_step_rne
206 sign
207 (bvor
208 (bvlshr rounded_up #b0000000000000000000001)
209 #b1000000000000000000000
210 )
211 (bvadd exponent #x01)
212 (bvadd exponent_field #b00001)
213 )
214 (f16_round_product_final_step_rne
215 sign rounded_up exponent exponent_field)
216 )
217 (f16_round_product_final_step_rne
218 sign product exponent exponent_field)
219 )
220 )
221 )
222 )
223 (define-fun f16_mul_nonzero_finite_rne ((a bv16) (b bv16)) bv16
224 (let
225 (
226 (product (bvmul (bv11_to_bv22 (f16_mantissa_value a))
227 (bv11_to_bv22 (f16_mantissa_value b))))
228 (sign (bvxor (f16_sign_field a) (f16_sign_field b)))
229 (exponent (bvadd (f16_exponent_value a) (f16_exponent_value b)))
230 )
231 ; normalize product
232 (let
233 (
234 (norm_product (bvshl product (bv22_clz product)))
235 (norm_exponent
236 (bvadd
237 exponent
238
239 ; compensation for product changing from having two
240 ; integer-part bits to one by normalization
241 #x01
242
243 (bvneg (bv22_to_f16_sexp (bv22_clz product)))
244 )
245 )
246 )
247 (let
248 (
249 ; amount to shift norm_product right to de-normalize again
250 ; for subnormals
251 (subnormal_shift
252 (f16_sexp_sub f16_subnormal_exponent norm_exponent)
253 )
254 )
255 ; if subnormal_shift would not cause the mantissa to overflow
256 (ite (f16_sexp_lt #x00 subnormal_shift)
257 ; subnormals:
258 (f16_round_product_rne
259 sign
260 (bv22_lshr_merging
261 norm_product
262 (f16_sexp_to_bv22 subnormal_shift)
263 )
264 f16_subnormal_exponent
265 #b00000
266 )
267 ; normals:
268 (f16_round_product_rne
269 sign
270 norm_product
271 norm_exponent
272 (f16_sexp_to_bv5 (bvadd norm_exponent
273 f16_exponent_bias))
274 )
275 )
276 )
277 )
278 )
279 )
280
281 (define-fun f16_mul_rne ((a bv16) (b bv16)) bv16
282 (ite (f16_is_nan a)
283 (f16_into_qnan a)
284 (ite (f16_is_nan b)
285 (f16_into_qnan b)
286 (ite
287 (or
288 (and (f16_is_zero a) (f16_is_infinite b))
289 (and (f16_is_infinite a) (f16_is_zero b))
290 )
291 #x7E00
292 (ite (or (f16_is_infinite a) (f16_is_infinite b))
293 (f16_infinity (bvxor (f16_sign_field a) (f16_sign_field b)))
294 (ite (or (f16_is_zero a) (f16_is_zero b))
295 (f16_zero (bvxor (f16_sign_field a) (f16_sign_field b)))
296 (f16_mul_nonzero_finite_rne a b)
297 )
298 )
299 )
300 )
301 )
302 )
303
304 ; input values in ieee754 f16 format as bit-vectors
305 (declare-const a bv16)
306 (declare-const b bv16)
307 ; product for debugging
308 (declare-const p bv16)
309 (assert (= (f16_to_fp p) (fp.mul RNE (f16_to_fp a) (f16_to_fp b))))
310 ; intermediate values from f16_mul_nonzero_finite_rne for debugging
311 (define-const product bv22 (bvmul (bv11_to_bv22 (f16_mantissa_value a))
312 (bv11_to_bv22 (f16_mantissa_value b))))
313 (define-const sign bv1 (bvxor (f16_sign_field a) (f16_sign_field b)))
314 (define-const exponent f16_sexp_t (bvadd (f16_exponent_value a) (f16_exponent_value b)))
315 (define-const norm_product bv22 (bvshl product (bv22_clz product)))
316 (define-const norm_exponent f16_sexp_t
317 (bvadd
318 exponent
319
320 ; compensation for product changing from having two
321 ; integer-part bits to one by normalization
322 #x01
323
324 (bvneg (bv22_to_f16_sexp (bv22_clz product)))
325 )
326 )
327 (define-const subnormal_shift f16_sexp_t
328 (f16_sexp_sub f16_subnormal_exponent norm_exponent)
329 )
330 ; intermediate values from f16_round_product_rne when the result is subnormal:
331 (define-const product_subnormal bv22
332 (bv22_lshr_merging
333 norm_product
334 (f16_sexp_to_bv22 subnormal_shift)
335 )
336 )
337 (define-const half_way_subnormal Bool
338 (= (bv22_to_bv11 product_subnormal) #b10000000000))
339 (define-const is_even_subnormal Bool
340 (= ((_ extract 11 11) product_subnormal) #b0))
341 (define-const rounded_up_subnormal bv22
342 (bvadd product_subnormal (bv11_to_bv22 #b10000000000)))
343 (define-const round_up_overflows_subnormal Bool
344 (bvult rounded_up_subnormal product_subnormal))
345 (define-const do_round_up_subnormal Bool
346 (ite half_way_subnormal
347 (not is_even_subnormal)
348 (bvult #b10000000000 (bv22_to_bv11 product_subnormal))
349 )
350 )
351 ; intermediate values from f16_round_product_rne when the result is normal:
352 (define-const exponent_field_normal bv5
353 (f16_sexp_to_bv5 (bvadd norm_exponent f16_exponent_bias))
354 )
355 (define-const half_way_normal Bool (= (bv22_to_bv11 norm_product) #b10000000000))
356 (define-const is_even_normal Bool (= ((_ extract 11 11) norm_product) #b0))
357 (define-const rounded_up_normal bv22
358 (bvadd norm_product (bv11_to_bv22 #b10000000000))
359 )
360 (define-const round_up_overflows_normal Bool (bvult rounded_up_normal norm_product))
361 (define-const do_round_up_normal Bool
362 (ite half_way_normal
363 (not is_even_normal)
364 (bvult #b10000000000 (bv22_to_bv11 norm_product))
365 )
366 )
367
368
369
370 ; now look for a case where f16_mul_rne is broke:
371 (assert (not (=
372 (f16_to_fp (f16_mul_rne a b))
373 (fp.mul RNE (f16_to_fp a) (f16_to_fp b))
374 )))
375 ; should return unsat, meaning there aren't any broken cases
376 (echo "should return unsat:")
377 (check-sat)
378 (echo "dumping values in case it returned sat:")
379 (get-value (
380 a
381 b
382 p
383 (f16_to_fp a)
384 (f16_to_fp b)
385 (fp.mul RNE (f16_to_fp a) (f16_to_fp b))
386 (f16_to_fp (f16_mul_rne a b))
387 (f16_mul_nonzero_finite_rne a b)
388 (f16_mantissa_field a)
389 (f16_mantissa_value a)
390 (f16_mantissa_field b)
391 (f16_mantissa_value b)
392 product
393 sign
394 exponent
395 (bv22_clz product)
396 norm_product
397 norm_exponent
398 subnormal_shift
399 product_subnormal
400 half_way_subnormal
401 is_even_subnormal
402 rounded_up_subnormal
403 round_up_overflows_subnormal
404 do_round_up_subnormal
405 exponent_field_normal
406 half_way_normal
407 is_even_normal
408 rounded_up_normal
409 round_up_overflows_normal
410 do_round_up_normal
411 ))