blob: 24356a8ad1e2ced3b846d3faa13769cbee45d221 (
plain)
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
|
// =======================================================================================
// This Sail RISC-V architecture model, comprising all files and
// directories except where otherwise noted is subject the BSD
// two-clause license in the LICENSE file.
//
// SPDX-License-Identifier: BSD-2-Clause
// =======================================================================================
// Convert the floating point class to the RISC-V one-hot encoding.
mapping float_class_onehot_bits : float_class <-> bits(10) = {
float_class_negative_inf <-> 0b0000000001,
float_class_negative_normal <-> 0b0000000010,
float_class_negative_subnormal <-> 0b0000000100,
float_class_negative_zero <-> 0b0000001000,
float_class_positive_zero <-> 0b0000010000,
float_class_positive_subnormal <-> 0b0000100000,
float_class_positive_normal <-> 0b0001000000,
float_class_positive_inf <-> 0b0010000000,
float_class_snan <-> 0b0100000000,
float_class_qnan <-> 0b1000000000,
}
// Prove that the float is in one broad class.
$[property]
function float_in_one_broad_class(f : bits(16)) -> bool =
bool_int(float_is_snan(f)) +
bool_int(float_is_qnan(f)) +
bool_int(float_is_zero(f)) +
bool_int(float_is_subnormal(f)) +
bool_int(float_is_normal(f)) +
bool_int(float_is_inf(f)) == 1
// Prove that all floats must be positive or negative.
// This includes NaNs.
$[property]
function float_pos_neg_or_nan(f : bits(16)) -> bool =
float_is_positive(f) != float_is_negative(f)
// Another overall class proof. A bit redundant but can't hurt.
$[property]
function float_in_one_class(f : bits(16)) -> bool =
bool_int(float_is_negative(f) & float_is_inf(f)) +
bool_int(float_is_negative(f) & float_is_normal(f)) +
bool_int(float_is_negative(f) & float_is_subnormal(f)) +
bool_int(float_is_negative(f) & float_is_zero(f)) +
bool_int(float_is_positive(f) & float_is_zero(f)) +
bool_int(float_is_positive(f) & float_is_subnormal(f)) +
bool_int(float_is_positive(f) & float_is_normal(f)) +
bool_int(float_is_positive(f) & float_is_inf(f)) +
bool_int(float_is_snan(f)) +
bool_int(float_is_qnan(f)) == 1
|
