$ runghc Bug.hs
$ bsc -sim -g mkTop -u Top.bs
checking package dependencies
compiling Top.bs
Warning: "Top.bs", line 11, column 4: (T0054)
Field not defined: `e'
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 explicit condition of rule `trig' at "Bug.bs",
line 18, column 8.
During elaboration of `mkTop' at "Top.bs", line 15, column 0.
The same problem arises if you use (<=), (>), or (>=) instead of (<).
The culprit is this part of the generated Bug.bs file:
Here, we are using Bluespec's (<) function to compare the value of ifc.e._read, a Double value that comes from a register. This is bad, as Bluespec's (<) function is partial and will error on NaN values, resulting in the evaulation-time error seen above. See https://github.com/B-Lang-org/bsc/discussions/711 for more information on why this happens.
The solution is to not translate the Copilot expression x < y to the Bluespec expression x < y. Instead, we should translate it to something like compareFP x y == LT (where compareFP is defined here). Unlike (<) and friends, compareFP is total and will not error if one of the inputs is a NaN value.
(Spun off from a discussion in https://github.com/Copilot-Language/copilot-bluespec/issues/14#issuecomment-2220273226.)
This Copilot specification:
Will result in Bluespec code that fails to compile against this
Top.bs
file:The same problem arises if you use
(<=)
,(>)
, or(>=)
instead of(<)
.The culprit is this part of the generated
Bug.bs
file:Here, we are using Bluespec's
(<)
function to compare the value ofifc.e._read
, aDouble
value that comes from a register. This is bad, as Bluespec's(<)
function is partial and will error on NaN values, resulting in the evaulation-time error seen above. See https://github.com/B-Lang-org/bsc/discussions/711 for more information on why this happens.The solution is to not translate the Copilot expression
x < y
to the Bluespec expressionx < y
. Instead, we should translate it to something likecompareFP x y == LT
(wherecompareFP
is defined here). Unlike(<)
and friends,compareFP
is total and will not error if one of the inputs is a NaN value.