Formal verification and system functions

SystemVerilog
, , ,
1

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.

2

In reply to DefaultName:

There is no need for the $bittoshortreal function or any of the bit-to or to to-bits system function in SystemVerilog. They were hacks to get around the favt that Verilog only supported packed integral arrays through ports.

Efficiency of particular tools is off-topic for this forum.

You may want to read: https://dvcon-proceedings.org/wp-content/uploads/formal-verification-of-floating-point-hardware-with-assertion-based-vip.pdf