Suppose I need to verify the floating point adder. Can I write such a assertion and will the format tool be able to carry out verification in a reasonable time? Is such an approach viable?

```
input ival,
input [31:0] in_a,
input [31:0] in_b,
output oval,
output [31:0] result
...
some rtl code
...
property check_sum;
shortreal sum;
(ival, sum = $bitstoshortreal(in_a) + $bitstoshortreal(in_b)) |=> oval & (result == $shortrealtobits(sum));
endproperty
sva_check_sum: assert property (check_sum);
```

Or in this case, the effectiveness of the tool will not be better than going through all the values in the simulation?

The `$bitstoshortreal`

function works with constant expressions, but for example, suppose I managed to get around this limitation.

Thank you.