diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,11 @@
# Changelog for [`clash-prelude` package](http://hackage.haskell.org/package/clash-prelude)
+## 0.10.1 *October 16th 2015*
+* New features:
+ * The `f` in `dfold p f`, now has an `SNat l` instead of a `Proxy l` as its first argument.
+ * Add `bv2v` and `v2bv` functions that convert between `Vec n Bit` and `BitVector n`.
+ * Add `smap`: apply a function to every element of a vector and the element's position (as an 'SNat' value) in the vector.
+
## 0.10 *October 3rd 2015*
* New features:
* The Vec constructor `:>` is now an explicitly bidirectional pattern synonym (the actual constructor has been renamed to Cons).
diff --git a/clash-prelude.cabal b/clash-prelude.cabal
--- a/clash-prelude.cabal
+++ b/clash-prelude.cabal
@@ -1,5 +1,5 @@
Name: clash-prelude
-Version: 0.10
+Version: 0.10.1
Synopsis: CAES Language for Synchronous Hardware - Prelude library
Description:
CλaSH (pronounced ‘clash’) is a functional hardware description language that
@@ -103,8 +103,9 @@
CLaSH.Prelude.Testbench
CLaSH.Promoted.Nat
- CLaSH.Promoted.Nat.TH
CLaSH.Promoted.Nat.Literals
+ CLaSH.Promoted.Nat.TH
+ CLaSH.Promoted.Nat.Unsafe
CLaSH.Promoted.Ord
CLaSH.Promoted.Symbol
@@ -157,6 +158,7 @@
ghc-typelits-natnormalise >= 0.3,
lens >= 4.9,
QuickCheck >= 2.7 && <2.9,
+ reflection >= 0.2,
singletons >= 1.0 && <3.0,
template-haskell >= 2.9.0.0
diff --git a/doc/csSort.svg b/doc/csSort.svg
--- a/doc/csSort.svg
+++ b/doc/csSort.svg
@@ -1,3 +1,3 @@
-
+
diff --git a/src/CLaSH/Promoted/Nat.hs b/src/CLaSH/Promoted/Nat.hs
--- a/src/CLaSH/Promoted/Nat.hs
+++ b/src/CLaSH/Promoted/Nat.hs
@@ -21,9 +21,11 @@
)
where
-import Data.Proxy
-import GHC.TypeLits
-import Unsafe.Coerce
+import Data.Proxy (Proxy (..))
+import Data.Reflection (reifyNat)
+import GHC.TypeLits (KnownNat, Nat, type (+), type (-), type (*), type (^),
+ natVal)
+import Unsafe.Coerce (unsafeCoerce)
-- | Singleton value for a type-level natural number 'n'
--
@@ -91,17 +93,21 @@
powUNat x (USucc y) = multUNat x (powUNat x y)
-- | Add two singleton natural numbers
-addSNat :: KnownNat (a + b) => SNat a -> SNat b -> SNat (a+b)
-addSNat _ _ = snat
+addSNat :: SNat a -> SNat b -> SNat (a+b)
+addSNat x y = reifyNat (snatToInteger x + snatToInteger y) (unsafeCoerce . SNat)
+{-# NOINLINE addSNat #-}
-- | Subtract two singleton natural numbers
-subSNat :: KnownNat (a - b) => SNat a -> SNat b -> SNat (a-b)
-subSNat _ _ = snat
+subSNat :: SNat a -> SNat b -> SNat (a-b)
+subSNat x y = reifyNat (snatToInteger x - snatToInteger y) (unsafeCoerce . SNat)
+{-# NOINLINE subSNat #-}
-- | Multiply two singleton natural numbers
-mulSNat :: KnownNat (a * b) => SNat a -> SNat b -> SNat (a*b)
-mulSNat _ _ = snat
+mulSNat :: SNat a -> SNat b -> SNat (a*b)
+mulSNat x y = reifyNat (snatToInteger x * snatToInteger y) (unsafeCoerce . SNat)
+{-# NOINLINE mulSNat #-}
-- | Power of two singleton natural numbers
-powSNat :: KnownNat (a ^ b) => SNat a -> SNat b -> SNat (a^b)
-powSNat _ _ = snat
+powSNat :: SNat a -> SNat b -> SNat (a^b)
+powSNat x y = reifyNat (snatToInteger x ^ snatToInteger y) (unsafeCoerce . SNat)
+{-# NOINLINE powSNat #-}
diff --git a/src/CLaSH/Promoted/Nat/Unsafe.hs b/src/CLaSH/Promoted/Nat/Unsafe.hs
new file mode 100644
--- /dev/null
+++ b/src/CLaSH/Promoted/Nat/Unsafe.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE Unsafe #-}
+
+{-|
+Copyright : (C) 2015, University of Twente
+License : BSD2 (see the file LICENSE)
+Maintainer : Christiaan Baaij
+-}
+module CLaSH.Promoted.Nat.Unsafe
+ (unsafeSNat)
+where
+
+import Data.Reflection (reifyNat)
+import Unsafe.Coerce (unsafeCoerce)
+
+import CLaSH.Promoted.Nat (SNat (..))
+
+-- | I hope you know what you're doing
+unsafeSNat :: Integer -> SNat k
+unsafeSNat i = reifyNat i (unsafeCoerce . SNat)
+{-# NOINLINE unsafeSNat #-}
diff --git a/src/CLaSH/Sized/Vector.hs b/src/CLaSH/Sized/Vector.hs
--- a/src/CLaSH/Sized/Vector.hs
+++ b/src/CLaSH/Sized/Vector.hs
@@ -63,7 +63,7 @@
, rotateLeft, rotateRight, rotateLeftS, rotateRightS
-- * Element-wise operations
-- ** Mapping
- , map, imap
+ , map, imap, smap
-- ** Zipping
, zipWith, zipWith3
, zip, zip3
@@ -83,12 +83,11 @@
, windows1d, windows2d
-- * Conversions
, toList
+ , bv2v
+ , v2bv
-- * Misc
- , lazyV, asNatProxy
+ , lazyV, VCons, asNatProxy
-- * Primitives
- -- ** 'Eq' instance
- , eq#
- , neq#
-- ** 'Traversable' instance
, traverse#
-- ** 'BitPack' instance
@@ -103,7 +102,7 @@
import Data.Proxy (Proxy (..))
import Data.Singletons.Prelude (TyFun,Apply,type ($))
import GHC.TypeLits (CmpNat, KnownNat, Nat, type (+), type (*),
- natVal)
+ type (-), natVal)
import GHC.Base (Int(I#),Int#,isTrue#)
import GHC.Prim ((==#),(<#),(-#))
import Language.Haskell.TH (ExpQ)
@@ -118,8 +117,11 @@
import Test.QuickCheck (Arbitrary (..), CoArbitrary (..))
import Unsafe.Coerce (unsafeCoerce)
-import CLaSH.Promoted.Nat (SNat (..), UNat (..), snat, withSNat, toUNat)
-import CLaSH.Sized.Internal.BitVector (BitVector, (++#), split#)
+import CLaSH.Promoted.Nat (SNat (..), UNat (..), snat, snatToInteger,
+ subSNat, withSNat, toUNat)
+import CLaSH.Promoted.Nat.Literals (d1)
+import CLaSH.Promoted.Nat.Unsafe (unsafeSNat)
+import CLaSH.Sized.Internal.BitVector (Bit, BitVector, (++#), split#)
import CLaSH.Sized.Index (Index)
import CLaSH.Class.BitPack (BitPack (..))
@@ -161,9 +163,9 @@
-- >>> data Append (m :: Nat) (a :: *) (f :: TyFun Nat *) :: *
-- >>> type instance Apply (Append m a) l = Vec (l + m) a
-- >>> let append' xs ys = dfold (Proxy :: Proxy (Append m a)) (const (:>)) ys xs
--- >>> let cs a b = if a > b then (a,b) else (b,a)
--- >>> let csRow y xs = let (y',xs') = mapAccumL cs y xs in xs' :< y'
--- >>> let csSort = vfold csRow
+-- >>> let compareSwap a b = if a > b then (a,b) else (b,a)
+-- >>> let insert y xs = let (y',xs') = mapAccumL compareSwap y xs in xs' :< y'
+-- >>> let insertionSort = vfold insert
infixr 5 `Cons`
-- | Fixed size vectors.
@@ -192,7 +194,7 @@
-- >>> f (3:>4:>5:>6:>7:>Nil)
-- 7
--
--- Also in conjunctions with ':<':
+-- Also in conjunctions with (':<'):
--
-- >>> let g (a :> b :> (_ :< y :< x)) = a + b + x + y
-- >>> :t g
@@ -215,16 +217,17 @@
punc (x `Cons` xs) = show x P.++ "," P.++ punc xs
instance Eq a => Eq (Vec n a) where
- (==) = eq#
- (/=) = neq#
-
-{-# NOINLINE eq# #-}
-eq# :: Eq a => Vec n a -> Vec n a -> Bool
-eq# v1 v2 = foldr (&&) True (zipWith (==) v1 v2)
-
-{-# NOINLINE neq# #-}
-neq# :: Eq a => Vec n a -> Vec n a -> Bool
-neq# v1 v2 = not (eq# v1 v2)
+ (==) Nil _ = True
+ (==) v1 v2 = fold (&&) (unsafeCoerce (zipWith (==) v1 v2))
+ -- FIXME: the `unsafeCoerce` is a hack because the CLaSH compiler cannot deal
+ -- with the existential length of the 'xs' in "Cons x xs".
+ --
+ -- Ideally we would write:
+ --
+ -- (==) Nil _ = True
+ -- (==) v1@(Cons _ _) v2 = fold (&&) (zipWith (==) v1 v2)
+ --
+ -- But the CLaSH compiler currently fails on that definition.
instance Ord a => Ord (Vec n a) where
compare x y = foldr f EQ $ zipWith compare x y
@@ -394,7 +397,7 @@
-- >>> f (3:>4:>5:>6:>7:>Nil)
-- 13
--
--- Also in conjunctions with ':>':
+-- Also in conjunctions with (':>'):
--
-- >>> let g (a :> b :> (_ :< y :< x)) = a + b + x + y
-- >>> :t g
@@ -1496,11 +1499,17 @@
-- <2,3,4,1>
--
-- __NB:__ use `rotateLeft` if you want to rotate left by a /dynamic/ amount.
-rotateLeftS :: Vec (d + n) a
+rotateLeftS :: KnownNat n
+ => Vec n a
-> SNat d
- -> Vec (n + d) a
-rotateLeftS xs d = let (l,r) = splitAt d xs in r ++ l
-{-# INLINE rotateLeftS #-}
+ -> Vec n a
+rotateLeftS xs d = go (snatToInteger d `mod` natVal (asNatProxy xs)) xs
+ where
+ go :: Integer -> Vec k a -> Vec k a
+ go _ Nil = Nil
+ go 0 ys = ys
+ go n (y `Cons` ys) = go (n-1) (ys :< y)
+{-# NOINLINE rotateLeftS #-}
-- | /Statically/ rotate a 'Vec'tor to the right:
--
@@ -1509,12 +1518,16 @@
-- <4,1,2,3>
--
-- __NB:__ use `rotateRight` if you want to rotate right by a /dynamic/ amount.
-rotateRightS :: forall n d a . (KnownNat n)
- => Vec (n + d) a
+rotateRightS :: KnownNat n
+ => Vec n a
-> SNat d
- -> Vec (d + n) a
-rotateRightS xs _ = let (l,r) = splitAtI xs :: (Vec n a, Vec d a) in r ++ l
-{-# INLINE rotateRightS #-}
+ -> Vec n a
+rotateRightS xs d = go (snatToInteger d `mod` natVal (asNatProxy xs)) xs
+ where
+ go _ Nil = Nil
+ go 0 ys = ys
+ go n ys@(Cons _ _) = go (n-1) (last ys :> init ys)
+{-# NOINLINE rotateRightS #-}
-- | Convert a vector to a list.
--
@@ -1665,23 +1678,34 @@
-- We now see that @append'@ has the appropriate type:
--
-- >>> :t append'
--- append' :: Vec k a -> Vec m a -> Vec (k + m) a
+-- append' :: KnownNat k => Vec k a -> Vec m a -> Vec (k + m) a
--
-- And that it works:
--
-- >>> append' (1 :> 2 :> Nil) (3 :> 4 :> Nil)
-- <1,2,3,4>
-dfold :: Proxy (p :: TyFun Nat * -> *) -- ^ The /motive/
- -> (forall l . Proxy l -> a -> (p $ l) -> (p $ (l + 1))) -- ^ Function to fold
+dfold :: forall p k a . KnownNat k
+ => Proxy (p :: TyFun Nat * -> *) -- ^ The /motive/
+ -> (forall l . SNat l -> a -> (p $ l) -> (p $ (l + 1))) -- ^ Function to fold
-> (p $ 0) -- ^ Initial element
-> Vec k a -- ^ Vector to fold over
-> (p $ k)
-dfold _ _ z Nil = z
-dfold p f z (x `Cons` (xs :: Vec l a)) = f (Proxy :: Proxy l) x (dfold p f z xs)
+dfold _ f z xs = go (natVal (asNatProxy xs) - 1) xs
+ where
+ go :: Integer -> Vec n a -> (p $ n)
+ go _ Nil = z
+ go i (y `Cons` (ys :: Vec z a)) = f (unsafeSNat i :: SNat z) y (go (i-1) ys)
{-# NOINLINE dfold #-}
-data V (a :: *) (f :: TyFun Nat *) :: *
-type instance Apply (V a) l = Vec l a
+-- | To be used as the motive /p/ for 'dfold', when the /f/ in \"'dfold' @p f@\"
+-- is a variation on (':>'), e.g.:
+--
+-- @
+-- map' :: KnownNat k => (a -> b) -> Vec n a -> Vec n b
+-- map' f = 'dfold' (Proxy :: Proxy ('VCons' a)) (\_ x xs -> f x :> xs)
+-- @
+data VCons (a :: *) (f :: TyFun Nat *) :: *
+type instance Apply (VCons a) l = Vec l a
-- | Specialised version of 'dfold' that builds a triangular computational
-- structure.
@@ -1689,25 +1713,43 @@
-- Example:
--
-- @
--- cs a b = if a > b then (a,b) else (b,a)
--- csRow y xs = let (y',xs') = 'mapAccumL' cs y xs in xs' ':<' y'
--- csSort = 'vfold' csRow
+-- compareSwap a b = if a > b then (a,b) else (b,a)
+-- insert y xs = let (y',xs') = 'mapAccumL' compareSwap y xs in xs' ':<' y'
+-- insertionSort = 'vfold' insert
-- @
--
-- Builds a triangular structure of compare and swaps to sort a row.
--
--- >>> csSort (7 :> 3 :> 9 :> 1 :> Nil)
+-- >>> insertionSort (7 :> 3 :> 9 :> 1 :> Nil)
-- <1,3,7,9>
--
--- The circuit layout of @csSort@, build using 'vfold', is:
+-- The circuit layout of @insertionSort@, build using 'vfold', is:
--
-- <>
-vfold :: (forall l . a -> Vec l b -> Vec (l + 1) b)
+vfold :: KnownNat k
+ => (forall l . a -> Vec l b -> Vec (l + 1) b)
-> Vec k a
-> Vec k b
-vfold f xs = dfold (Proxy :: Proxy (V a)) (const f) Nil xs
+vfold f xs = dfold (Proxy :: Proxy (VCons a)) (const f) Nil xs
{-# INLINE vfold #-}
+-- | Apply a function to every element of a vector and the element's position
+-- (as an 'SNat' value) in the vector.
+--
+-- >>> let rotateMatrix = smap (flip rotateRightS)
+-- >>> let xss = (1:>2:>3:>Nil):>(1:>2:>3:>Nil):>(1:>2:>3:>Nil):>Nil
+-- >>> xss
+-- <<1,2,3>,<1,2,3>,<1,2,3>>
+-- >>> rotateMatrix xss
+-- <<1,2,3>,<3,1,2>,<2,3,1>>
+smap :: KnownNat k => (forall l . SNat (k-1-l) -> a -> b) -> Vec k a -> Vec k b
+smap f xs = dfold (Proxy :: Proxy (VCons a))
+ (\sn x xs' -> f (xsL `subSNat` d1 `subSNat` sn) x :> xs')
+ Nil xs
+ where
+ xsL = lengthS xs
+{-# INLINE smap #-}
+
instance (KnownNat n, KnownNat (BitSize a), BitPack a) => BitPack (Vec n a) where
type BitSize (Vec n a) = n * (BitSize a)
pack = concatBitVector# . map pack
@@ -1737,6 +1779,26 @@
ucBV (USucc n) bv = let (bv',x :: BitVector m) = split# bv
in ucBV n bv' :< x
{-# INLINE ucBV #-}
+
+-- | Convert a 'BitVector' to a 'Vec' of 'Bit's.
+--
+-- >>> let x = 6 :: BitVector 8
+-- >>> x
+-- 0000_0110
+-- >>> bv2v x
+-- <0,0,0,0,0,1,1,0>
+bv2v :: KnownNat n => BitVector n -> Vec n Bit
+bv2v = unpack
+
+-- | Convert a 'Vec' of 'Bit's to a 'BitVector'.
+--
+-- >>> let x = (0:>0:>0:>1:>0:>0:>1:>0:>Nil) :: Vec 8 Bit
+-- >>> x
+-- <0,0,0,1,0,0,1,0>
+-- >>> v2bv x
+-- 0001_0010
+v2bv :: KnownNat n => Vec n Bit -> BitVector n
+v2bv = pack
instance Lift a => Lift (Vec n a) where
lift Nil = [| Nil |]
diff --git a/src/CLaSH/Tutorial.hs b/src/CLaSH/Tutorial.hs
--- a/src/CLaSH/Tutorial.hs
+++ b/src/CLaSH/Tutorial.hs
@@ -113,29 +113,51 @@
-- >>> let topEntity = mac :: Signal (Signed 9, Signed 9) -> Signal (Signed 9)
-- >>> let testInput = stimuliGenerator $(v [(1,1) :: (Signed 9,Signed 9),(2,2),(3,3),(4,4)])
-- >>> let expectedOutput = outputVerifier $(v [0 :: Signed 9,1,5,14])
+-- >>> :{
+-- let fibR :: Unsigned 64 -> Unsigned 64
+-- fibR 0 = 0
+-- fibR 1 = 1
+-- fibR n = fibR (n-1) + fibR (n-2)
+-- :}
+--
+-- >>> :{
+-- let fibS :: Signal (Unsigned 64)
+-- fibS = r
+-- where r = register 0 r + register 0 (register 1 r)
+-- :}
{- $introduction
CλaSH (pronounced ‘clash’) is a functional hardware description language that
borrows both its syntax and semantics from the functional programming language
-Haskell. The merits of using a functional language to describe hardware comes
-from the fact that combinational circuits can be directly modeled as
-mathematical functions and that functional languages lend themselves very well
-at describing and (de-)composing mathematical functions. The CλaSH compiler
-transforms these high-level descriptions to low-level synthesizable VHDL,
-Verilog, or SystemVerilog.
+Haskell. It provides a familiar structural design approach to both combination
+and synchronous sequential circuits. The CλaSH compiler transforms these
+high-level descriptions to low-level synthesizable VHDL, Verilog, or
+SystemVerilog.
+Features of CλaSH:
+
+ * Strongly typed (like VHDL), yet with a very high degree of type inference,
+ enabling both safe and fast prototying using concise descriptions (like
+ Verilog).
+ * Interactive REPL: load your designs in an interpreter and easily test all
+ your component without needing to setup a test bench.
+ * Compile your designs for fast simulation.
+ * Higher-order functions, in combination with type inference, result in
+ designs that are fully parametric by default.
+ * Synchronous sequential circuit design based on streams of values, called
+ @Signal@s, lead to natural descriptions of feedback loops.
+ * Multiple clock domains, with type safe clock domain crossing.
+ * Template language for introducing new VHDL/(System)Verilog primitives.
+
Although we say that CλaSH borrows the semantics of Haskell, that statement
should be taken with a grain of salt. What we mean to say is that the CλaSH
compiler views a circuit description as /structural/ description. This means,
in an academic handwavy way, that every function denotes a component and every
function application denotes an instantiation of said component. Now, this has
-consequences on how we view /recursive/ functions: structurally, a recursive
-function would denote an /infinitely/ deep / structured component, something
-that cannot be turned into an actual circuit (See also <#unsupported Unsupported Haskell features>).
-Of course there are variants of recursion that could be completely unfolded at
-compile-time with a finite amount of steps and hence could be converted to a
-realisable circuit. Sadly, this last feature is missing in the current version
-of the compiler.
+consequences on how we view /recursively/ defined functions: structurally, a
+recursively defined function would denote an /infinitely/ deep / structured
+component, something that cannot be turned into an actual circuit
+(See also <#unsupported Unsupported Haskell features>).
On the other hand, Haskell's by-default non-strict evaluation works very well
for the simulation of the feedback loops, which are ubiquitous in digital
@@ -148,6 +170,9 @@
s = 'register' 0 (s + 1)
@
+The above definition, which uses value-recursion, /can/ be synthesized to a
+circuit by the CλaSH compiler.
+
Over time, you will get a better feeling for the consequences of taking a
/structural/ view on circuit descriptions. What is always important to
remember is that every applied functions results in an instantiated component,
@@ -665,10 +690,10 @@
topEntity = fir (0 ':>' 1 ':>' 2 ':>' 3 ':>' 'Nil')
@
-Here we can see that, although the CλaSH compiler does not support recursion,
-many of the regular patterns that we often encounter in circuit design are
-already captured by the higher-order functions that are present for the 'Vec'tor
-type.
+Here we can see that, although the CλaSH compiler handles recursive function
+definitions poorly, many of the regular patterns that we often encounter in
+circuit design are already captured by the higher-order functions that are
+present for the 'Vec'tor type.
-}
{- $composition_sequential
@@ -1666,33 +1691,120 @@
{- $unsupported #unsupported#
Here is a list of Haskell features which the CλaSH compiler cannot synthesize
-to VHDL/Verilog/SystemVerilog (for now):
+to VHDL/(System)Verilog (for now):
-* __Recursive functions__
+* __Recursively defined functions__
- Although it seems rather bad that a compiler for a
- functional language does not support recursion, this bug/feature of the
- CλaSH compiler is amortized by the builtin knowledge of all the functions
- listed in "CLaSH.Sized.Vector". And as you saw in this tutorial, the
- higher-order functions of "CLaSH.Sized.Vector" can cope with many of the
- recursive design patterns found in circuit design.
+ At first hand, it seems rather bad that a compiler for a functional language
+ cannot synthesize recursively defined functions to circuits. However, when
+ viewing your functions as a /structural/ specification of a circuit, this
+ /feature/ of the CλaSH compiler makes sense. Also, only certain types of
+ recursion are considered non-synthesisable; recursively defined values are
+ for example synthesisable: they are (often) synthesized to feedback loops.
- Also note that although recursive functions are not supported, recursively
- (tying-the-knot) defined values are supported (as long as these values do
- not have a function type). An example that uses recursively defined values
- is the following function that performs one iteration of bubble sort:
+ Let us distinguish between three variants of recursion:
- @
- sortV xs = 'map' fst sorted :< (snd ('last' sorted))
- where
- lefts = 'head' xs :> 'map' snd ('init' sorted)
- rights = 'tail' xs
- sorted = 'zipWith' compareSwapL lefts rights
- @
+ * __Dynamic data-dependent recursion__
- Where we can clearly see that 'lefts' and 'sorted' are defined in terms of
- each other.
+ As demonstrated in this definition of a function that calculates the
+ n'th Fibbonacci number:
+ @
+ fibR 0 = 0
+ fibR 1 = 1
+ fibR n = fibR (n-1) + fibR (n-2)
+ @
+
+ To get the first 10 numbers, we do the following:
+
+ >>> import qualified Data.List as L
+ >>> L.map fibR [0..9]
+ [0,1,1,2,3,5,8,13,21,34]
+
+ The @fibR@ function is not synthesizable by the CλaSH compiler, because,
+ when we take a /structural/ view, @fibR@ describes an infinitely deep
+ structure.
+
+ In principal, descriptions like the above could be synthesized to a
+ circuit, but it would have to be a /sequential/ circuit. Where the most
+ general synthesis would then require a stack. Such a synthesis approach
+ is also known as /behavioural/ synthesis, something which the CλaSH
+ compiler simply does not do. One reason that CλaSH does not do this is
+ because it does not fit the paradigm that only functions working on
+ values of type 'Signal' result in sequential circuits, and all other
+ (non higher-order) functions result in combinational circuits. This
+ paradigm gives the designer the most straightforward mapping from the
+ original Haskell description to generated circuit, and thus the greatest
+ control over the eventual size of the circuit and longest propagation
+ delay.
+
+ * __Value-recursion__
+
+ As demonstrated in this definition of a function that calculates the
+ n'th Fibbonaci number on the n'th clock cycle:
+
+ @
+ fibS = r
+ where r = 'register' 0 r + 'register' 0 ('register' 1 r)
+ @
+
+ To get the first 10 numbers, we do the following:
+
+ >>> sampleN 10 fibS
+ [0,1,1,2,3,5,8,13,21,34]
+
+ Unlike the @fibR@ function, the above @fibS@ function /is/ synthesisable
+ by the CλaSH compiler. Where the recursively defined (non-function)
+ value /r/ is synthesized to a feedback loop containing three registers
+ and one adder.
+
+ Note that not all recursively defined values result in a feedback loop.
+ An example that uses recursively defined values which does not result
+ in a feedback loop is the following function that performs one iteration
+ of bubble sort:
+
+ @
+ sortV xs = 'map' fst sorted :< (snd ('last' sorted))
+ where
+ lefts = 'head' xs :> 'map' snd ('init' sorted)
+ rights = 'tail' xs
+ sorted = 'zipWith' compareSwapL lefts rights
+ @
+
+ Where we can clearly see that 'lefts' and 'sorted' are defined in terms
+ of each other. Also the above @sortV@ function /is/ synthesisable.
+
+ * __Static/Structure-dependent recursion__
+
+ Static, or, structure-dependent recursion is a rather /vague/ concept.
+ What we mean by this concept are recursive definitions where a user can
+ sensibly imagine that the recursive definition can be completely
+ unfolded (all recursion is eliminated) at compile-time in a finite
+ amount of time.
+
+ Such definitions would e.g. be:
+
+ @
+ mapV :: (a -> b) -> Vec n a -> Vec n b
+ mapV _ Nil = Nil
+ mapV f (Cons x xs) = Cons (f x) (mapV f xs)
+
+ topEntity :: Vec 4 Int -> Vec 4 Int
+ topEntity = mapV (+1)
+ @
+
+ Where one can imagine that a compiler can unroll the definition of
+ @mapV@ four times, knowing that the @topEntity@ function applies @mapV@
+ to a 'Vec' of length 4. Sadly, the compile-time evaluation mechanisms in
+ the CλaSH compiler are very poor, and a user-defined function such as
+ the @mapV@ function defined above, is /currently/ not synthesisable.
+ We /do/ plan to add support for this in the future. In the mean time,
+ this poor support for user-defined recursive functions is amortized by
+ the fact that the CλaSH compiler has built-in support for the
+ higher-order functions defined in "CLaSH.Sized.Vector". Most regular
+ design patterns often encountered in circuit design are captured by the
+ higher-order functions in "CLaSH.Sized.Vector".
+
* __Recursive datatypes__
The CλaSH compiler needs to be able to determine a bit-size for any value
@@ -1723,7 +1835,6 @@
1. In order to achieve reasonable operating frequencies, arithmetic
circuits for floating point data types must be pipelined.
-
2. Haskell's primitive arithmetic operators on floating point data types,
such as 'plusFloat#'
@@ -1748,7 +1859,7 @@
'Char', 'Array', etc. cannot to translated to hardware.
The translations of 'Int', 'Int#', and 'Integer' are also incorrect: they
- are translated to the VHDL @integer@ type, the Verilog @signed [31:0], or
+ are translated to the VHDL @integer@ type, the Verilog @signed [31:0]@, or
the SystemVerilog @signed logic [31:0]@ type, which can only represent
32-bit integer values. Use these types with due diligence.
@@ -1774,7 +1885,7 @@
embedded language approach is already clearly visible: synthesis of recursive
descriptions does not come for \"free\". This will be implemented in CλaSH in
due time, but that doesn't help the circuit designer right now. As already
-mentioned earlier, the lack of support for recursive functions is amortized by
+mentioned earlier, the poor support for recursive functions is amortized by
the built-in support for the higher-order in "CLaSH.Sized.Vector".
The big upside of CλaSH and its static analysis approach is that CλaSH can