Previously, we would translate the Copilot expression x < y to the Bluespec expression x < y. While this is a nice and direct translation, it unfortunately does not work when x or y is derived from a register value. (See https://github.com/Copilot-Language/copilot-bluespec/issues/15 for the full story.) There existed similar problems for (<=), (>), and (>=).
We now translate x < y to compareFP x y == LT, where compareFP is an auxiliary function defined in Bluespec's FloatingPoint package. This results in the generated Bluespec code being able to compile, and more importantly, the generated code will have the same semantics as Bluespec when one of the arguments is a NaN value.
Previously, we would translate the Copilot expression
x < yto the Bluespec expressionx < y. While this is a nice and direct translation, it unfortunately does not work whenxoryis derived from a register value. (See https://github.com/Copilot-Language/copilot-bluespec/issues/15 for the full story.) There existed similar problems for(<=),(>), and(>=).We now translate
x < ytocompareFP x y == LT, wherecompareFPis an auxiliary function defined in Bluespec'sFloatingPointpackage. This results in the generated Bluespec code being able to compile, and more importantly, the generated code will have the same semantics as Bluespec when one of the arguments is a NaN value.Fixes #15.