Strange evaluation-time error when comparing two FloatingPoint values

[RyanGlScott]

I've been attempting to debug an evaluation-time error that I observe when compiling a program that uses the FloatingPoint package. First, let's start with a program that does work:

package Top where

import FloatingPoint

mkTop :: Module Empty
mkTop =
  module
    let x :: Double
        x = 0.0

        y :: Double
        y = 0.0
    rules
      "step": when True ==>
        $display (fshow (x < y))

This will print False on each cycle, as expected. Now, let's make the program slightly more interesting by storing the values of x and y in registers:

package Top where

import FloatingPoint

mkTop :: Module Empty
mkTop =
  module
    x :: Reg Double <- mkReg 0.0
    y :: Reg Double <- mkReg 0.0
    rules
      "step": when True ==>
        $display (fshow (x < y))

I would expect this program to be equivalent. Surprisingly, bsc-2024.01 fails to compile this program:

$ ~/Software/bsc-2024.01/bin/bsc -sim -g mkTop -u Top.bs
checking package dependencies
compiling Top.bs
code generation for mkTop starts
Error: "FloatingPoint.bsv", line 948, column 86: (S0015)
  Bluespec evaluation-time error: Unordered comparison of type
  `FloatingPoint'.
  During elaboration of the body of rule `step' at "Top.bs", line 11, column
  6.
  During elaboration of `mkTop' at "Top.bs", line 5, column 0.

The error message arises from here:

bsc/src/Libraries/Base3-Math/FloatingPoint.bsv

Lines 945 to 953 in 9a97f9d

	function Ordering compare( FloatingPoint#(e,m) x, FloatingPoint#(e,m) y );
	let c = compareFP(x, y);
	case (c)
	UO: return error("Unordered comparison of type " + quote("FloatingPoint") + ".");
	EQ: return EQ;
	LT: return LT;
	GT: return GT;
	endcase
	endfunction

I am very unclear as to how compareFP is returning UO, however. If I'm reading the implementation of compareFP correctly, then compareFP can only return UO when one of the arguments is NaN, and that isn't happening in my program. What is going on here?

[quark17]

They are not equivalent because, in one, the inputs are constants that are known (statically) at compile time and, in the other, the inputs come from registers who values are only known (dynamically) at runtime of the hardware. The reset value of 0.0 to the registers does not matter; BSC must assume that the registers could contain any possible values, including NaN values. (In theory, maybe BSC could perform "model checking" to detect what states can be reached, but BSC does not currently do that.) When the input is statically known, BSC can pick the right case-arm and only evaluate that. However, when the input is not known at compile time, BSC must generate the hardware for all possible case-arms, to handle all possible situations if they arise at runtime. If one of the case-arms is an error, then compilation results in an error.

We can see this with a simpler example:

(* synthesize *)
module mkTest();

  Reg#(Bit#(2)) rgA <- mkRegU;
  Reg#(Bool)    rgB <- mkRegU;

  rule rl;
    case (rgA)
      0 : rgB <= True;
      1 : rgB <= False;
      2 : error("Invalid rgA");
      3 : rgB <= True;
    endcase
  endrule

endmodule

BSC has to produce hardware for all possible case-arms, so it has to evaluate all arms, and one of the arms is an error, so you get an evaluation-time error.

In your example, instead of using the operator <, you should probably just call compareFP directly. I notice that the result type (Disorder) does not derive FShow, so you can't just fshow the result as you were doing with the < operator -- maybe that's something we can fix in the FloatingPoint library. (You can locally define an FShow instance as a workaround, if you want.) Another approach would to define your own function that calls compareFP and handles the UO result however you would like.

It's also possible that you could add a guard like !isNaN(x) && !isNaN(y) and maybe that would cause BSC to recognize that the case-arm is not reachable and to avoid evaluating it. However, I can't guarantee that BSC is always able to do that, so it's possible that BSC might evaluate the error call still. I think the best option is to call functions that don't use error but instead return a datatype that encodes the error condition (like Maybe, or Disorder in this case) and then handle the error result at the caller.

[RyanGlScott]

Thanks! That explanation makes sense.

A follow-up question: I am a bit surprised that < (and similar operators) aren't defined such that x < y returns False if x or y is a NaN value, as this is the convention I am used to when dealing with languages such as C and Haskell. Is there a particular reason why Bluespec's < instead errors if x or y is a NaN?

[rsnikhil]

Haskell returns False for this? I'm surprised.

I'd have expected that an error is the more reasonable result when comparing NaNs?

[RyanGlScott]

Haskell returns False for this?

Yes:

$ cabal repl -b ieee754
λ> import Numeric.IEEE
λ> nan < (0.0 :: Double)
False
λ> (0.0 :: Double) < nan
False

The rationale is explained in this comment. (tl;dr It's for IEEE 754 compliance.)

I'd have expected that an error is the more reasonable result when comparing NaNs?

Possibly, but one thing that I didn't appreciate until after reading @quark17's answer above is that if I call f x, where the value of x is derived from a register, then if f calls error on any code path, then bsc will fail to compile it. That is a show-stopper for my use case.

In this particular instance, this means that I will need to redefine <, <=, >, and >= to avoid calling error, and since C and Haskell already return False when one of the arguments is a NaN, I think I will stick to that convention. Still, it would be nice if the FloatingPoint package offered versions of these operators that didn't call error, as that would mean I could use those directly (and not have to work around the issue on my end).