clash-prelude-0.10.4: CAES Language for Synchronous Hardware - Prelude library

Copyright (C) 2013-2015, University of Twente BSD2 (see the file LICENSE) Christiaan Baaij Trustworthy Haskell2010 UndecidableInstancesMonoLocalBindsTemplateHaskellScopedTypeVariablesTypeFamiliesConstraintKindsDataKindsStandaloneDerivingFlexibleContextsMultiParamTypeClassesKindSignaturesGeneralizedNewtypeDerivingTypeOperatorsExplicitNamespacesExplicitForAll

CLaSH.Sized.Fixed

Description

Fixed point numbers

• The `Num` operators for the given types saturate on overflow, and use truncation as the rounding method.
• `Fixed` has an instance for `Fractional` meaning you use fractional literals `(3.75 :: SFixed 4 18)`.
• Both integer literals and fractional literals are clipped to `minBound` and `maxBound`.
• There is no `Floating` instance for `Fixed`, but you can use `\$\$(fLit d)` to create `Fixed` point literal from `Double` constant at compile-time.
• Use Constraint synonyms when writing type signatures for polymorphic functions that use `Fixed` point numbers.

BEWARE: rounding by truncation introduces a sign bias!

• Truncation for positive numbers effectively results in: round towards zero.
• Truncation for negative numbers effectively results in: round towards -infinity.

Synopsis

# `SFixed`: `Signed``Fixed` point numbers

Signed `Fixed`-point number, with `int` integer bits (including sign-bit) and `frac` fractional bits.

• The range `SFixed` `int` `frac` numbers is: [-(2^(`int` -1)) .. 2^(`int`-1) - 2^-`frac` ]
• The resolution of `SFixed` `int` `frac` numbers is: 2^`frac`
• The `Num` operators for this type saturate on overflow, and use truncation as the rounding method.
````>>> ````maxBound :: SFixed 3 4
```3.9375
`>>> ````minBound :: SFixed 3 4
```-4.0
`>>> ````1 + 2 :: SFixed 3 4
```3.0
`>>> ````2 + 3 :: SFixed 3 4
```3.9375
`>>> ````(-2) + (-3) :: SFixed 3 4
```-4.0
`>>> ````1.375 * (-0.8125) :: SFixed 3 4
```-1.125
`>>> ````(1.375 :: SFixed 3 4) `times` (-0.8125 :: SFixed 3 4) :: SFixed 6 8
```-1.1171875
`>>> ````(2 :: SFixed 3 4) `plus` (3 :: SFixed 3 4) :: SFixed 4 4
```5.0
`>>> ````(-2 :: SFixed 3 4) `plus` (-3 :: SFixed 3 4) :: SFixed 4 4
```-5.0
```

Arguments

 :: SNat frac Position of the virtual `point` -> Signed (int + frac) The `Signed` integer -> SFixed int frac

Treat a `Signed` integer as a `Signed` `Fixed`-`point` integer

````>>> ````sf d4 (-22 :: Signed 7)
```-1.375
```

unSF :: SFixed int frac -> Signed (int + frac) Source

See the underlying representation of a Signed Fixed-point integer

# `UFixed`: `Unsigned``Fixed` point numbers

Unsigned `Fixed`-point number, with `int` integer bits and `frac` fractional bits

• The range `UFixed` `int` `frac` numbers is: [0 .. 2^`int` - 2^-`frac` ]
• The resolution of `UFixed` `int` `frac` numbers is: 2^`frac`
• The `Num` operators for this type saturate on overflow, and use truncation as the rounding method.
````>>> ````maxBound :: UFixed 3 4
```7.9375
`>>> ````minBound :: UFixed 3 4
```0.0
`>>> ````1 + 2 :: UFixed 3 4
```3.0
`>>> ````2 + 6 :: UFixed 3 4
```7.9375
`>>> ````1 - 3 :: UFixed 3 4
```0.0
`>>> ````1.375 * 0.8125 :: UFixed 3 4
```1.0625
`>>> ````(1.375 :: UFixed 3 4) `times` (0.8125 :: UFixed 3 4) :: UFixed 6 8
```1.1171875
`>>> ````(2 :: UFixed 3 4) `plus` (6 :: UFixed 3 4) :: UFixed 4 4
```8.0
```

However, `minus` does not saturate to `minBound` on underflow:

````>>> ````(1 :: UFixed 3 4) `minus` (3 :: UFixed 3 4) :: UFixed 4 4
```14.0
```

Arguments

 :: SNat frac Position of the virtual `point` -> Unsigned (int + frac) The `Unsigned` integer -> UFixed int frac

Treat an `Unsigned` integer as a `Unsigned` `Fixed`-`point` number

````>>> ````uf d4 (92 :: Unsigned 7)
```5.75
```

unUF :: UFixed int frac -> Unsigned (int + frac) Source

See the underlying representation of an Unsigned Fixed-point integer

# Division

divide :: DivideC rep int1 frac1 int2 frac2 => Fixed rep int1 frac1 -> Fixed rep int2 frac2 -> Fixed rep ((int1 + frac2) + 1) (int2 + frac1) Source

Fixed point division

When used in a polymorphic setting, use the following Constraint synonyms for less verbose type signatures:

• `DivideC rep int1 frac1 int2 frac2` for: `Fixed rep int1 frac1 -> Fixed rep int2 frac2 -> Fixed rep (int1 + frac2 + 1) (int2 + frac1)`
• `DivideSC rep int1 frac1 int2 frac2` for: `SFixed int1 frac1 -> SFixed int2 frac2 -> SFixed (int1 + frac2 + 1) (int2 + frac1)`
• `DivideUC rep int1 frac1 int2 frac2` for: `UFixed int1 frac1 -> UFixed int2 frac2 -> UFixed (int1 + frac2 + 1) (int2 + frac1)`

# Compile-time `Double` conversion

fLit :: forall rep int frac size. (size ~ (int + frac), KnownNat frac, Bounded (rep size), Integral (rep size)) => Double -> Q (TExp (Fixed rep int frac)) Source

Convert, at compile-time, a `Double` constant to a `Fixed`-point literal. The conversion saturates on overflow, and uses truncation as its rounding method.

So when you type:

```n = \$\$(`fLit` pi) :: `SFixed` 4 4
```

The compiler sees:

```n = `Fixed` (fromInteger 50) :: `SFixed` 4 4
```

Upon evaluation you see that the value is rounded / truncated in accordance to the fixed point representation:

````>>> ````n
```3.125
```

Further examples:

````>>> ````sin 0.5 :: Double
```0.479425538604203
`>>> ````\$\$(fLit (sin 0.5)) :: SFixed 1 8
```0.4765625
`>>> ````atan 0.2 :: Double
```0.19739555984988078
`>>> ````\$\$(fLit (atan 0.2)) :: SFixed 1 8
```0.1953125
`>>> ````\$\$(fLit (atan 0.2)) :: SFixed 1 20
```0.19739532470703125
```

# Run-time `Double` conversion (not synthesisable)

fLitR :: forall rep int frac size. (size ~ (int + frac), KnownNat frac, Bounded (rep size), Integral (rep size)) => Double -> Fixed rep int frac Source

Convert, at run-time, a `Double` to a `Fixed`-point.

NB: this functions is not synthesisable

# Creating data-files

An example usage of this function is for example to convert a data file containing `Double`s to a data file with ASCI-encoded binary numbers to be used by a synthesisable function like `asyncRomFile`. For example, given a file `Data.txt` containing:

```1.2 2.0 3.0 4.0
-1.0 -2.0 -3.5 -4.0
```

which we want to put in a ROM, interpreting them as `8.8` signed fixed point numbers. What we do is that we first create a conversion utility, `createRomFile`, which uses `fLitR`:

`createRomFile.hs`:

```module Main where

import CLaSH.Prelude
import System.Environment
import qualified Data.List as L

createRomFile :: KnownNat n => (Double -> BitVector n)
-> FilePath -> FilePath -> IO ()
createRomFile convert fileR fileW = do
f <- readFile fileR
let ds :: [Double]
ds = L.concat . (L.map . L.map) read . L.map words \$ lines f
bvs = L.map (filter (/= '_') . show . convert) ds
writeFile fileW (unlines bvs)

toSFixed8_8 :: Double -> SFixed 8 8
toSFixed8_8 = `fLitR`

main :: IO ()
main = do
[fileR,fileW] <- getArgs
createRomFile (`pack` . toSFixed8_8) fileR fileW
```

We then compile this to an executable:

```\$ clash --make createRomFile.hs
```

We can then use this utility to convert our `Data.txt` file which contains `Double`s to a `Data.bin` file which will containing the desired ASCI-encoded binary data:

```\$ ./createRomFile "Data.txt" "Data.bin"
```

Which results in a `Data.bin` file containing:

```0000000100110011
0000001000000000
0000001100000000
0000010000000000
1111111100000000
1111111000000000
1111110010000000
1111110000000000
```

We can then use this `Data.bin` file in for our ROM:

```romF :: Unsigned 3 -> Unsigned 3 -> SFixed 8 8
romF rowAddr colAddr = `unpack`
\$ `asyncRomFile` d8 "Data.bin" ((rowAddr * 4) + colAddr)
```

And see that it works as expected:

```>>> romF 1 2
-3.5
>>> romF 0 0
1.19921875
```

## Using Template Haskell

For those of us who like to live on the edge, another option is to convert our `Data.txt` at compile-time using Template Haskell. For this we first create a module `CreateRomFileTH.hs`:

```module CreateRomFileTH (romDataFromFile) where

import CLaSH.Prelude
import qualified Data.List        as L
import Language.Haskell.TH        (ExpQ, litE, stringL)
import Language.Haskell.TH.Syntax (qRunIO)

createRomFile :: KnownNat n => (Double -> BitVector n)
-> FilePath -> FilePath -> IO ()
createRomFile convert fileR fileW = do
f <- readFile fileR
let ds :: [Double]
ds = L.concat . (L.map . L.map) read . L.map words \$ lines f
bvs = L.map (filter (/= '_') . show . convert) ds
writeFile fileW (unlines bvs)

romDataFromFile :: KnownNat n => (Double -> BitVector n) -> String -> ExpQ
romDataFromFile convert fileR = do
let fileW = fileR L.++ ".bin"
bvF <- qRunIO (createRomFile convert fileR fileW)
litE (stringL fileW)
```

Instead of first converting `Data.txt` to `Data.bin`, we will now use the `romDataFromFile` function to convert `Data.txt` to a new file in the proper format at compile-time of our new `romF'` function:

```import CLaSH.Prelude
import CreateRomFileTH

toSFixed8_8 :: Double -> SFixed 8 8
toSFixed8_8 = `fLitR`

romF' :: Unsigned 3 -> Unsigned 3 -> SFixed 8 8
romF' rowAddr colAddr = unpack \$
asyncRomFile d8
\$(romDataFromFile (pack . toSFixed8_8) "Data.txt") -- Template Haskell splice
((rowAddr * 4) + colAddr)
```

And see that it works just like the `romF` function from earlier:

```>>> romF' 1 2
-3.5
>>> romF' 0 0
1.19921875
```

# `Fixed` point wrapper

newtype Fixed rep int frac Source

`Fixed`-point number

Where:

• `rep` is the underlying representation
• `int` is the number of bits used to represent the integer part
• `frac` is the number of bits used to represent the fractional part

The `Num` operators for this type saturate to `maxBound` on overflow and `minBound` on underflow, and use truncation as the rounding method.

Constructors

 Fixed FieldsunFixed :: rep (int + frac)

Instances

 Bounded (rep ((+) int frac)) => Bounded (Fixed rep int frac) Source Enum (rep ((+) int frac)) => Enum (Fixed rep int frac) Source Eq (rep ((+) int frac)) => Eq (Fixed rep int frac) Source FracFixedC rep int frac => Fractional (Fixed rep int frac) Source The operators of this instance saturate on overflow, and use truncation as the rounding method.When used in a polymorphic setting, use the following Constraint synonyms for less verbose type signatures:`FracFixedC frac rep size` for: `Fixed frac rep size``FracSFixedC int frac` for: `SFixed int frac``FracUFixedC int frac` for: `UFixed int frac` NumFixedC rep int frac => Num (Fixed rep int frac) Source The operators of this instance saturate on overflow, and use truncation as the rounding method.When used in a polymorphic setting, use the following Constraint synonyms for less verbose type signatures:`NumFixedC frac rep size` for: `Fixed frac rep size``NumSFixedC int frac` for: `SFixed int frac``NumUFixedC int frac` for: `UFixed int frac` Ord (rep ((+) int frac)) => Ord (Fixed rep int frac) Source ((~) Nat size ((+) int frac), KnownNat frac, Integral (rep size)) => Show (Fixed rep int frac) Source Arbitrary (rep ((+) int frac)) => Arbitrary (Fixed rep int frac) Source CoArbitrary (rep ((+) int frac)) => CoArbitrary (Fixed rep int frac) Source Bits (rep ((+) int frac)) => Bits (Fixed rep int frac) Source FiniteBits (rep ((+) int frac)) => FiniteBits (Fixed rep int frac) Source Default (rep ((+) int frac)) => Default (Fixed rep int frac) Source (Lift (rep ((+) int frac)), KnownNat frac, KnownNat int, Typeable (Nat -> *) rep) => Lift (Fixed rep int frac) Source NumFixedC rep int frac => SaturatingNum (Fixed rep int frac) Source BitPack (rep ((+) int frac)) => BitPack (Fixed rep int frac) Source Bundle (Fixed rep int frac) Source ENumFixedC rep int1 frac1 int2 frac2 => ExtendingNum (Fixed rep int1 frac1) (Fixed rep int2 frac2) Source When used in a polymorphic setting, use the following Constraint synonyms for less verbose type signatures:`ENumFixedC rep frac1 frac2 size1 size2` for: `Fixed``ENumSFixedC int1 frac1 int2 frac2` for: `SFixed``ENumUFixedC int1 frac1 int2 frac2` for: `UFixed` type Unbundled' clk (Fixed rep int frac) = Signal' clk (Fixed rep int frac) type BitSize (Fixed rep int frac) = BitSize (rep ((+) int frac)) Source type AResult (Fixed rep int1 frac1) (Fixed rep int2 frac2) = Fixed rep ((+) 1 (Max int1 int2)) (Max frac1 frac2) Source type MResult (Fixed rep int1 frac1) (Fixed rep int2 frac2) = Fixed rep ((+) int1 int2) ((+) frac1 frac2) Source

resizeF :: (ResizeFC rep int1 frac1 int2 frac2, Bounded (rep (int2 + frac2))) => Fixed rep int1 frac1 -> Fixed rep int2 frac2 Source

Saturating resize operation, truncates for rounding

````>>> ````0.8125 :: SFixed 3 4
```0.8125
`>>> ````resizeF (0.8125 :: SFixed 3 4) :: SFixed 2 3
```0.75
`>>> ````3.4 :: SFixed 3 4
```3.375
`>>> ````resizeF (3.4 :: SFixed 3 4) :: SFixed 2 3
```1.875
`>>> ````maxBound :: SFixed 2 3
```1.875
```

When used in a polymorphic setting, use the following Constraint synonyms for less verbose type signatures:

• `ResizeFC rep int1 frac1 int2 frac2` for: `Fixed rep int1 frac1 -> Fixed rep int2 frac2`
• `ResizeSFC int1 frac1 int2 frac2` for: `SFixed int1 frac1 -> SFixed int2 frac2`
• `ResizeUFC rep int1 frac1 int2 frac2` for: `UFixed int1 frac1 -> UFixed int2 frac2`

fracShift :: KnownNat frac => Fixed rep int frac -> Int Source

Get the position of the virtual `point` of a `Fixed`-`point` number

# Constraint synonyms

Writing polymorphic functions over fixed point numbers can be a potentially verbose due to the many class constraints induced by the functions and operators of this module.

Writing a simple multiply-and-accumulate function can already give rise to many lines of constraints:

```mac :: ( `KnownNat` frac
, `KnownNat` (frac + frac)
, `KnownNat` (int + frac)
, `KnownNat` (1 + (int + frac))
, `KnownNat` ((int + frac) + (int + frac))
, ((int + int) + (frac + frac)) ~ ((int + frac) + (int + frac))
)
=> `SFixed` int frac
-> `SFixed` int frac
-> `SFixed` int frac
-> `SFixed` int frac
mac s x y = s + (x * y)
```

But with constraint synonyms, you can write the type signature like this:

```mac1 :: `NumSFixedC` int frac
=> `SFixed` int frac
-> `SFixed` int frac
-> `SFixed` int frac
-> `SFixed` int frac
mac1 s x y = s + (x * y)
```

Where `NumSFixedC` refers to the `Constraints` needed by the operators of the `Num` class for the `SFixed` datatype.

Although the number of constraints for the `mac` function defined earlier might be considered small, here is an "this way lies madness" example where you really want to use constraint kinds:

```mac2 :: ( `KnownNat` frac1
, `KnownNat` frac2
, `KnownNat` frac3
, `KnownNat` (Max frac1 frac2)
, `KnownNat` (int1 + frac1)
, `KnownNat` (int2 + frac2)
, `KnownNat` (int3 + frac3)
, `KnownNat` (frac1 + frac2)
, `KnownNat` (Max (frac1 + frac2) frac3)
, `KnownNat` (((int1 + int2) + (frac1 + frac2)) + (int3 + frac3))
, `KnownNat` ((int1 + int2) + (frac1 + frac2))
, `KnownNat` (1 + Max (int1 + frac1) (int2 + frac2))
, `KnownNat` (1 + Max (int1 + int2) int3 + Max (frac1 + frac2) frac3)
, `KnownNat` ((1 + Max int1 int2) + Max frac1 frac2)
, `KnownNat` ((1 + Max ((int1 + int2) + (frac1 + frac2)) (int3 + frac3)))
, ((int1 + frac1) + (int2 + frac2)) ~ ((int1 + int2) + (frac1 + frac2))
, (((int1 + int2) + int3) + ((frac1 + frac2) + frac3)) ~ (((int1 + int2) + (frac1 + frac2)) + (int3 + frac3))
)
=> `SFixed` int1 frac1
-> `SFixed` int2 frac2
-> `SFixed` int3 frac3
-> `SFixed` (1 + Max (int1 + int2) int3) (Max (frac1 + frac2) frac3)
mac2 x y s = (x `times` y) `plus` s
```

Which, with the proper constraint kinds can be reduced to:

```mac3 :: ( `ENumSFixedC` int1 frac1 int2 frac2
, `ENumSFixedC` (int1 + int2) (frac1 + frac2) int3 frac3
)
=> `SFixed` int1 frac1
-> `SFixed` int2 frac2
-> `SFixed` int3 frac3
-> `SFixed` (1 + Max (int1 + int2) int3) (Max (frac1 + frac2) frac3)
mac3 x y s = (x `times` y) `plus` s
```

## Constraint synonyms for `SFixed`

type NumSFixedC int frac = (KnownNat frac, KnownNat (frac + frac), KnownNat (int + frac), KnownNat (1 + (int + frac)), KnownNat ((int + frac) + (int + frac)), ((int + int) + (frac + frac)) ~ ((int + frac) + (int + frac))) Source

Constraint for the `Num` instance of `SFixed`

type ENumSFixedC int1 frac1 int2 frac2 = (KnownNat frac1, KnownNat frac2, KnownNat (Max frac1 frac2), KnownNat (int1 + frac1), KnownNat (int2 + frac2), KnownNat ((int1 + int2) + (frac1 + frac2)), KnownNat (1 + Max (int1 + frac1) (int2 + frac2)), KnownNat ((1 + Max int1 int2) + Max frac1 frac2), ((int1 + frac1) + (int2 + frac2)) ~ ((int1 + int2) + (frac1 + frac2))) Source

Constraint for the `ExtendingNum` instance of `SFixed`

type FracSFixedC int frac = (NumSFixedC int frac, KnownNat int, KnownNat (((int + frac) + 1) + (int + frac))) Source

Constraint for the `Fractional` instance of `SFixed`

type ResizeSFC int1 frac1 int2 frac2 = (KnownNat frac1, KnownNat frac2, KnownNat (int1 + frac1), KnownNat (int2 + frac2)) Source

Constraint for the `resizeF` function, specialized for `SFixed`

type DivideSC int1 frac1 int2 frac2 = (KnownNat int2, KnownNat frac2, KnownNat (int1 + frac1), KnownNat (int2 + frac2), KnownNat (((int1 + frac2) + 1) + (int2 + frac1))) Source

Constraint for the `divide` function, specialized for `SFixed`

## Constraint synonyms for `UFixed`

type NumUFixedC int frac = NumSFixedC int frac Source

Constraint for the `Num` instance of `UFixed`

type ENumUFixedC int1 frac1 int2 frac2 = ENumSFixedC int1 frac1 int2 frac2 Source

Constraint for the `ExtendingNum` instance of `UFixed`

type FracUFixedC int frac = FracSFixedC int frac Source

Constraint for the `Fractional` instance of `UFixed`

type ResizeUFC int1 frac1 int2 frac2 = ResizeSFC int1 frac1 int2 frac2 Source

Constraint for the `resizeF` function, specialized for `UFixed`

type DivideUC int1 frac1 int2 frac2 = DivideSC int1 frac1 int2 frac2 Source

Constraint for the `divide` function, specialized for `UFixed`

## Constraint synonyms for `Fixed` wrapper

type NumFixedC rep int frac = (SaturatingNum (rep (int + frac)), ExtendingNum (rep (int + frac)) (rep (int + frac)), ResizeFC rep (int + int) (frac + frac) int frac, MResult (rep (int + frac)) (rep (int + frac)) ~ rep ((int + int) + (frac + frac))) Source

Constraint for the `Num` instance of `Fixed`

type ENumFixedC rep int1 frac1 int2 frac2 = (ResizeFC rep int1 frac1 (1 + Max int1 int2) (Max frac1 frac2), ResizeFC rep int2 frac2 (1 + Max int1 int2) (Max frac1 frac2), Bounded (rep ((1 + Max int1 int2) + Max frac1 frac2)), Num (rep ((1 + Max int1 int2) + Max frac1 frac2)), ExtendingNum (rep (int1 + frac1)) (rep (int2 + frac2)), MResult (rep (int1 + frac1)) (rep (int2 + frac2)) ~ rep ((int1 + int2) + (frac1 + frac2))) Source

Constraint for the `ExtendingNum` instance of `Fixed`

type FracFixedC rep int frac = (NumFixedC rep int frac, DivideC rep int frac int frac, Integral (rep (int + frac))) Source

Constraint for the `Fractional` instance of `Fixed`

type ResizeFC rep int1 frac1 int2 frac2 = (Resize rep, Ord (rep (int1 + frac1)), Num (rep (int1 + frac1)), Bits (rep (int1 + frac1)), Bits (rep (int2 + frac2)), KnownNat frac1, KnownNat frac2, KnownNat (int1 + frac1), KnownNat (int2 + frac2)) Source

Constraint for the `resizeF` function

type DivideC rep int1 frac1 int2 frac2 = (Resize rep, Integral (rep (((int1 + frac2) + 1) + (int2 + frac1))), Bits (rep (((int1 + frac2) + 1) + (int2 + frac1))), KnownNat int2, KnownNat frac2, KnownNat (int1 + frac1), KnownNat (int2 + frac2), KnownNat (((int1 + frac2) + 1) + (int2 + frac1))) Source

Constraint for the `divide` function

# Proxy

asRepProxy :: Fixed rep int frac -> Proxy rep Source

`Fixed` as a `Proxy` for it's representation type `rep`

asIntProxy :: Fixed rep int frac -> Proxy int Source

`Fixed` as a `Proxy` for the number of integer bits `int`