B19 Coverage Issues

[sww0000]

@coreyqh There are a few bugs I found with the B19.svh:

1. Issues w/ cross

        B19_F128__norm_x_subnorm:    cross FP_compare_ops, F128_operand_a_sign, F128_operand_b_sign, F128_a_norm, F128_b_subnorm,
                                          /* a.EXP > b.EXP*/       F128_frac_compare,   F128_result_fmt;

        B19_F128__subnorm_x_norm:    cross FP_compare_ops, F128_operand_a_sign, F128_operand_b_sign, F128_a_norm, F128_b_subnorm,
                                          /* a.EXP < b.EXP*/       F128_frac_compare,   F128_result_fmt;

        B19_F128__subnorm_x_subnorm: cross FP_compare_ops, F128_operand_a_sign, F128_operand_b_sign, F128_a_norm, F128_b_subnorm,
                                          F128_exp_compare,         F128_frac_compare,   F128_result_fmt;

• subnorm x norm is crossing a_norm and b_subnorm
• same w/ subnorm x subnorm

2. GTE, LTE errors with subnormal x zero / zero x subnorm for F128

        B19_F128__subnorm_x_zero:       cross FP_compare_ops, F128_operand_a_sign, F128_operand_b_sign, F128_a_subnorm, F128_b_zero,
                                          /* a.EXP < b.EXP*/       F128_frac_LT,        F128_result_fmt;

        B19_F128__zero_x_subnorm:       cross FP_compare_ops, F128_operand_a_sign, F128_operand_b_sign, F128_a_zero, F128_b_subnorm,
                                          /* a.EXP > b.EXP*/       F128_frac_GT,       F128_result_fmt;

• for subnorm x zero: since sub_norm exp < zero_exp, then sub_norm_fraction can only be GTE to zero_fraction, but we have F128_frac_LT.
• inverse of above for zero x subnorm.

Changing the two above gets the coverage to ~82% (I have done the changes to B19.svh locally, let me know if I could just commit what I have currently or it would be better for you to make the adjustments @coreyqh)

@coreyqh A few more issues that I am looking into:

1. For some reason, with any subnormal x (zero / normal), the bin <*,neg,*,*,*,eq,*> is consistently missed. Unsure if it is a coverage problem or a testgen problem.
2. Please look over coverage scenarios for subnormal x subnormal, with the following bins missed:

#             bin <*,*,*,*,*,lt,gt,*>                         0          1         20    ZERO                 
#             bin <*,*,*,*,*,gt,eq,*>                         0          1         20    ZERO                 
#             bin <*,*,*,*,*,lt,eq,*>                         0          1         20    ZERO                 
#             bin <*,*,*,*,*,gt,lt,*>                         0          1         20    ZERO                 
#             bin <*,pos,neg,*,*,*,eq,*>                      0          1         15    ZERO                 
#             bin <*,neg,pos,*,*,*,eq,*>                      0          1         15    ZERO  

I believe the first 4 bins are impossible conditions for subnorm x subnorm, and the last two could be a testgen error or coverage.

[sww0000]

@coreyqh Can you look at:

1. subnorm x subnorm frac compare crosses. I don't think you can use (format)_frac_compare to cover the conditions for subnorm x subnorm (check the adoc for table). This should get the coverage to 100%

• Issue 1 from the previous comment didn't get fixed, and I adjusted it & committed (please check it out for reference + double check if they are correct and if the adoc is interpreting this model correctly).
• Your zero x subnormal and subnormal x zero has the GT and LT in reverse (it should also be GTE and LTE because in our definition, if the subnormal has a frac of 1000...000, everything after the effective 1 is all zeros, which we consider to have the same frac as a normal where its frac is all zeros). I also changed it for the commit.

The current coverage after adjusting the cross vectors according to the two points above is at ~87.16%, I believe we just need to get the subnorm x subnorm frac comparison problem taken care of and that should get the model to 100%

[coreyqh]

@sww0000 #105 fixes the majority of the issues here. I am not quite sure what the problem is with subnorm X subnorm exponent compare. Could you elaborate or provide a specific example that does not line up with expectations?

[sww0000]

#             bin <*,*,*,*,*,lt,gt,*>                         0          1         20    ZERO                 
#             bin <*,*,*,*,*,gt,eq,*>                         0          1         20    ZERO                 
#             bin <*,*,*,*,*,lt,eq,*>                         0          1         20    ZERO                 
#             bin <*,*,*,*,*,gt,lt,*>                         0          1         20    ZERO                 
#             bin <*,pos,neg,*,*,*,eq,*>                      0          1         15    ZERO                 
#             bin <*,neg,pos,*,*,*,eq,*>                      0          1         15    ZERO  

These are the bins that are not hit for any of the subnorm x subnorm, and according to the documentation in section 3.4 - Case 4, the following combinations for exponent compare and frac compare should be ignored as they are impossible to reach:

1. exponent gt, frac eq
2. exponent gt, frac lt
3. exponent lt, frac eq
4. exponent lt, frac gt

Unclear why the pos, neg, eq bins are not getting hit. But ignoring the bins above should get the coverage to at least 95%+

[coreyqh]

What if we had 0.0001100... and 0.01100....

If these were normalized with infinite range, then they would be
1.1 * 2 ^ (MIN_EXP - 4)
and
1.1 * 2 ^ (MIN_EXP - 3)

These have the same fraction (.10000...) but different exponents. To me, it seems like points 1 and 3 could be disproven by this. Let me know if I am missing something.

the same way, we could have 0.00101... and 0.000110... for point 2 and 4

[sww0000]

ohhhh I see! I will get that changed and pr in a bit