Fix Refs #696: bluespec special constFp

copilot-bluespec/CHANGELOG

@@ -1,3 +1,6 @@
+2025-12-19
+        * Fix constFP function in Expr.hs to correctly translate special Double values (#696)
+
 2025-11-07
         * Version bump (4.6). (#679)
         * Flip direction of interface inputs and outputs in Bluespec. (#677)

copilot-bluespec/copilot-bluespec.cabal

@@ -42,6 +42,8 @@ library
   build-depends           : base              >= 4.9    && < 5
                           , directory         >= 1.3    && < 1.4
                           , filepath          >= 1.4    && < 1.6
+                          , fp-ieee           >= 0.1.0  && < 0.2
+                          , ieee754           >= 0.8.0  && < 0.9
                           , pretty            >= 1.1.2  && < 1.2
 
                           , copilot-core      >= 4.6 && < 4.7

copilot-bluespec/examples/special_doubles/Makefile

@@ -0,0 +1,18 @@
+
+run: mkTop.exe
+	./mkTop.exe -m 4
+
+mkTop.exe: mkTop
+	bsc -sim -e mkTop -o mkTop.exe bs_fp.c
+
+BluespecFP.bsv bs_fp.c Doubles.bs DoublesTypes.bs:
+	runhaskell special_doubles.hs
+
+mkTop: BluespecFP.bsv bs_fp.c SpecialDoubles.bs SpecialDoublesTypes.bs
+	bsc -sim -g mkTop -u Top.bs
+
+verilog: mkTop
+	bsc -verilog -g mkDoubless -u SpecialDoubles.bs
+
+clean:
+	rm -rf *.ba *.bo BluespecFP.bsv *.c SpecialDoublesTypes.bs SpecialDoubles.bs *.h *.o *.cxx *.exe *.so *.v obj_dir/

copilot-bluespec/examples/special_doubles/Top.bs

@@ -0,0 +1,21 @@
+package Top where
+
+import SpecialDoubles
+import SpecialDoublesTypes
+
+mkTop :: Module Empty
+mkTop =
+       module
+               doublesMod <- mkSpecialDoubles
+
+               rules
+                       "first": when doublesMod.nan_0_guard ==> do
+                                let nan_bits  = pack doublesMod.nan_0_arg0
+                                    inf_bits  = pack doublesMod.inf_1_arg0
+                                    zero_bits = pack doublesMod.zeros_2_arg0
+                                    othr_bits = pack doublesMod.others_3_arg0
+                                $display "NaN value --- sign: %b exponent: %b silent: %b payload: %b" nan_bits[63:63] nan_bits[62:52] nan_bits[51:51] nan_bits[50:0]
+                                $display "inf value --- sign: %b exponent: %b mantissa: %b" inf_bits[63:63] inf_bits[62:52] inf_bits[51:0]
+                                $display "zero value -- sign: %b exponent: %b mantissa: %b" zero_bits[63:63] zero_bits[62:52] zero_bits[51:0]
+                                $display "other value - sign: %b exponent: %b mantissa: %b" othr_bits[63:63] othr_bits[62:52] othr_bits[51:0]
+                                $display ""

copilot-bluespec/examples/special_doubles/special_doubles.hs

@@ -0,0 +1,35 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+module Main (main) where
+
+import qualified Copilot.Compile.Bluespec as Bluespec
+import Language.Copilot
+import Numeric.Floating.IEEE.NaN
+
+nans :: Stream Double
+nans = [setPayload 0, setPayloadSignaling 2] ++ nans
+
+infinities :: Stream Double
+infinities = [inf, -inf] ++ infinities
+  where
+    inf :: Double
+    inf = read "Infinity"
+
+zeroes :: Stream Double
+zeroes = [0, -0] ++ zeroes
+
+others :: Stream Double
+others = [1.0, 2.0, 3.0] ++ others
+
+spec :: Spec
+spec = do
+  --trigger "rtf" true [arg nans, arg infinities, arg zeroes, arg others]
+  trigger "nan" true [arg nans]
+  trigger "inf" true [arg infinities]
+  trigger "zeros" true [arg zeroes]
+  trigger "others" true [arg others]
+
+main :: IO ()
+main = do
+  interpret 3 spec
+  spec' <- reify spec
+  Bluespec.compile "SpecialDoubles" spec'

copilot-bluespec/src/Copilot/Compile/Bluespec/Expr.hs

@@ -17,6 +17,8 @@ import Data.Foldable (foldl')
 import Data.String (IsString (..))
 import qualified Language.Bluespec.Classic.AST as BS
 import qualified Language.Bluespec.Classic.AST.Builtin.Ids as BS
+import Numeric.Floating.IEEE.NaN (isSignaling, setPayloadSignaling, setPayload, getPayload)
+import GHC.Float (double2Float, castFloatToWord32, castDoubleToWord64)
 
 -- Internal imports: Copilot
 import Copilot.Core
@@ -608,17 +610,44 @@ constInt ty i
                     (BS.CVar $ BS.idNegateAt BS.NoPos)
                     [cLit $ BS.LInt $ BS.ilDec $ negate i]
 
+-- Because NaNs are specially placed as bit-representations by `constfp` and `constfp` requires Doubles as inputs,
+--  we need to convert NaN doubles safely into NaN floats. GHC Double2Float does not preserve signal nor payload 
+--  internals of NaNs so in this case we need a special conversion.
+uncastDoubleNaNToFloat :: Double -> Float
+uncastDoubleNaNToFloat nan = if (isSignaling nan) 
+              then (setPayloadSignaling payload) 
+              else (setPayload payload)
+              where 
+                payload = double2Float $ getPayload nan
+
 -- | Translate a Copilot floating-point literal into a Bluespec expression.
 constFP :: Type ty -> Double -> BS.CExpr
 constFP ty d
+    -- Bluespec internally represents all IEEE floating-point values as structs so 
+    -- special symbols have to be called for constructing special values. see
+    --- https://github.com/B-Lang-org/bsc/blob/main/src/Libraries/Base3-Math/FloatingPoint.bsv#L441
+    | isInfinite d = BS.CApply 
+                      (BS.CVar $ BS.mkId BS.NoPos "infinity") 
+                      [if d < 0 then BS.CCon BS.idTrue [] else BS.CCon BS.idFalse []]
+    | isNaN d      = BS.CApply 
+                      (BS.CVar $ BS.mkId BS.NoPos $ 
+                        fromString $ (
+                        case ty of 
+                          Float  -> "unpack (" ++ show (castFloatToWord32 $ uncastDoubleNaNToFloat d) ++ " :: Bit 32 {-nan val-})"
+                          Double -> "unpack (" ++ show (castDoubleToWord64 d) ++ " :: Bit 64 {-nan val-})"
+                          _ -> impossible "constFP" "copilot-bluespec"
+                        )) []
+    | d == 0       = BS.CApply 
+                      (BS.CVar $ BS.mkId BS.NoPos "zero") 
+                      [if isNegativeZero d then BS.CCon BS.idTrue [] else BS.CCon BS.idFalse []]
+    | d > 0        = withTypeAnnotation ty $ cLit $ BS.LReal d
     -- Bluespec intentionally does not support negative literal syntax (e.g.,
     -- -42.5), so we must create negative floating-point literals using the
     -- `negate` function.
-    | d >= 0    = withTypeAnnotation ty $ cLit $ BS.LReal d
-    | otherwise = withTypeAnnotation ty $
-                  BS.CApply
-                    (BS.CVar $ BS.idNegateAt BS.NoPos)
-                    [cLit $ BS.LReal $ negate d]
+    | otherwise    = withTypeAnnotation ty $
+                     BS.CApply
+                       (BS.CVar $ BS.idNegateAt BS.NoPos)
+                       [cLit $ BS.LReal $ negate d]
 
 -- | Create a Bluespec expression consisting of a literal.
 cLit :: BS.Literal -> BS.CExpr