kansas-lava-cores-0.1.2: Hardware/KansasLava/FIFO.hs
{-# LANGUAGE TypeFamilies, ExistentialQuantification, FlexibleInstances, UndecidableInstances, FlexibleContexts,
ScopedTypeVariables, MultiParamTypeClasses, FunctionalDependencies,ParallelListComp,
RankNTypes, TypeOperators #-}
module Hardware.KansasLava.FIFO where
import Control.Concurrent
import Control.Monad
import Data.Maybe as Maybe
import Data.Sized.Arith as Arith
import Data.Sized.Ix as X
import Data.Word
import Data.Sized.Unsigned
import Language.KansasLava
import System.IO
------------------------------------------------------------------------------
-- | Make a sequence obey the given reset signal, returning given value on a reset.
resetable :: forall a c. (Clock c, Rep a) => Signal c Bool -> a -> Signal c a -> Signal c a
resetable rst val x = mux rst (x,pureS val)
fifoFE :: forall c a counter ix sig .
(Size counter
, Size ix
, counter ~ ADD ix X1
, Rep a
, Rep counter
, Rep ix
, Num counter
, Num ix
, Clock c
, sig ~ Signal c
)
=> Witness ix
-- ^ depth of FIFO
-> Signal c Bool
-- ^ hard reset option
-> Patch (sig (Enabled a)) (sig (Enabled (ix,a)) :> sig Bool)
(sig Ack) (sig Ready :> sig counter)
-- ^ input, and Seq trigger of how much to decrement the counter,
-- ^ backedge for input, internal counter, and write request for memory.
fifoFE w rst = ackToReadyBridge $$ fifoFE' w rst where
fifoFE' Witness rst ~(inp,mem_ready :> dec_by) = (toReady inp_ready, wr :> inp_done0)
where
inp_try0 :: Signal c Bool
inp_try0 = inp_ready `and2` isEnabled inp -- `and2` fromReady mem_ready
wr :: Signal c (Enabled (ix,a))
wr = packEnabled (inp_try0)
(pack (wr_addr,enabledVal inp))
inp_done0 :: Signal c Bool
inp_done0 = isEnabled wr `and2` fromReady mem_ready
wr_addr :: Signal c ix
wr_addr = resetable rst 0
$ register 0
$ mux inp_done0 (wr_addr,loopingIncS wr_addr)
in_counter0 :: Signal c counter
in_counter0 = resetable rst 0
$ in_counter1
+ (unsigned) inp_done0
- dec_by
in_counter1 :: Signal c counter
in_counter1 = register 0 in_counter0
-- TODO: make this happen on the clock edge
inp_ready :: Signal c Bool
inp_ready = (in_counter1 .<. fromIntegral (size (error "witness" :: ix)))
`and2`
(bitNot rst)
`and2`
(fromReady mem_ready)
fifoBE :: forall a c counter ix sig .
(Size counter
, Size ix
, counter ~ ADD ix X1
, Rep a
, Rep counter
, Rep ix
, Num counter
, Num ix
, Clock c
, sig ~ Signal c
)
=> Witness ix
-> Signal c Bool -- ^ reset
-- -> (Signal comb Bool -> Signal comb counter -> Signal comb counter)
-- -> Seq (counter -> counter)
-> Patch (sig (Enabled a) :> sig counter) (sig (Enabled a))
(sig (Enabled ix) :> sig Bool) (sig Ack)
{-
-> (Signal c counter,Signal c (Enabled a))
-- inc from FE
-- input from Memory read
-> Signal c Ack
-> ((Signal c ix, Signal c Bool, Signal c counter), Signal c (Enabled a))
-}
-- address for Memory read
-- dec to FE
-- internal counter, and
-- output for HandShaken
fifoBE Witness rst (mem_rd :> inc_by, out_ready) =
let
rd_addr0 :: Signal c ix
rd_addr0 = resetable rst 0
$ mux out_done0 (rd_addr1,loopingIncS rd_addr1)
rd_addr1 = register 0
$ rd_addr0
-- technically, ack should never happen if isEnabled out is not set
out_done0 :: Signal c Bool
out_done0 = fromAck out_ready `and2` (isEnabled out)
out :: Signal c (Enabled a)
out = packEnabled ((out_counter1 .>. 0) `and2` bitNot rst `and2` isEnabled mem_rd) (enabledVal mem_rd)
out_counter0 :: Signal c counter
out_counter0 = resetable rst 0
$ out_counter1
+ inc_by
- (unsigned) out_done0
out_counter1 = register 0 out_counter0
in
(enabledS rd_addr0 :> out_done0, out)
-- This remains 'ready', because it is a reasonable use of ready.
-- TODO: Consider
fifoMem :: forall a c1 c2 counter ix sig1 sig2 .
(Size counter
, Size ix
, counter ~ ADD ix X1
, Rep a
, Rep counter
, Rep ix
, Num counter
, Num ix
, Clock c1
, Clock c2
, sig1 ~ Signal c1
, sig2 ~ Signal c2
, c1 ~ c2
)
=> Witness ix
-> Patch (sig1 (Enabled (ix,a)) :> sig1 Bool) (sig2 (Enabled a) :> sig2 counter)
(sig1 Ready :> sig1 counter) (sig2 (Enabled ix) :> sig2 Bool)
fifoMem Witness ~(~(wr_in :> wr_in_done),~(rd_addr :> sent)) = (toReady high :> dec_fe,mem_val :> inc_be)
where
-- This is the memory.
mem_val = packEnabled (register False (isEnabled rd_addr))
$ syncRead (writeMemory wr_in)
(enabledVal rd_addr)
-- Saying Here is some space to write to.
dec_fe = (unsigned) sent
-- This needs a two-cycle delay, to provide time for the memory read
inc_be = (unsigned) $ register False $ register False $ wr_in_done
fifoCounter :: forall counter . (Num counter, Rep counter) => Seq Bool -> Seq Bool -> Seq Bool -> Seq counter
fifoCounter rst inc dec = counter1
where
counter0 :: Seq counter
counter0 = resetable rst 0
$ counter1
+ (unsigned) inc
- (unsigned) dec
counter1 = register 0 counter0
fifoCounter' :: forall counter . (Num counter, Rep counter) => Seq Bool -> Seq counter -> Seq counter -> Seq counter
fifoCounter' rst inc dec = counter1
where
counter0 :: Seq counter
counter0 = resetable rst 0
$ counter1
+ inc -- mux2 inc (1,0)
- dec -- mux2 dec (1,0)
counter1 = register 0 counter0
fifo :: forall a c counter ix .
(Size counter
, Size ix
, counter ~ ADD ix X1
, Rep a
, Rep counter
, Rep ix
, Num counter
, Num ix
, Clock c
)
=> Witness ix
-> Signal c Bool
-> Patch (Signal c (Enabled a)) (Signal c (Enabled a))
(Signal c Ack) (Signal c Ack)
fifo w_ix rst = fifo_patch
where
fifo_patch = fifoFE w_ix rst $$ fifoMem w_ix $$ fifoBE w_ix rst
{-
fifo w_ix rst (inp,out_ready) =
let
wr :: Signal c (Maybe (ix, a))
inp_ready :: Signal c Ready
(inp_ready, counter_fe, wr) = fifoFE w_ix rst (inp,dec_by)
inp_done2 :: Signal c Bool
inp_done2 = resetable rst low $ register False $ resetable rst low $ register False $ resetable rst low $ isEnabled wr
mem :: Signal c ix -> Signal c (Enabled a)
mem = enabledS . pipeToMemory wr
(rd_addr0 :> out_done0,counter_be,out) = fifoBE w_ix rst (mem rd_addr0 :> inc_by, out_ready)
dec_by = (unsigned) out_done0
inc_by = (unsigned) inp_done2
in
(inp_ready, counter_fe, out)
-}
{-
fifoZ :: forall a c counter ix .
(Size counter
, Size ix
, counter ~ ADD ix X1
, Rep a
, Rep counter
, Rep ix
, Num counter
, Num ix
, Clock c
)
=> Witness ix
-> Signal c Bool
-> I (Signal c (Enabled a)) (Signal c Ack)
-> O (Signal c Ready) (Signal c (Enabled a),Signal c counter)
fifoZ w_ix rst (inp,out_ready) =
let
wr :: Signal c (Maybe (ix, a))
inp_ready :: Signal c Ready
(inp_ready, counter, wr) = fifoFE w_ix rst (inp,dec_by)
inp_done2 :: Signal c Bool
inp_done2 = resetable rst low $ register False $ resetable rst low $ register False $ resetable rst low $ isEnabled wr
mem :: Signal c ix -> Signal c (Enabled a)
mem = enabledS . pipeToMemory wr
((rd_addr0,out_done0,_),out) = fifoBE w_ix rst (inc_by,mem rd_addr0) out_ready
dec_by = liftS1 (\ b -> mux2 b (1,0)) out_done0
inc_by = liftS1 (\ b -> mux2 b (1,0)) inp_done2
in
(inp_ready, (out,counter))
-}
{-
fifoToMatrix :: forall a counter counter2 ix iy iz c .
(Size counter
, Size ix
, Size counter2, Rep counter2, Num counter2
, counter ~ ADD ix X1
, counter2 ~ ADD iy X1
, Rep a
, Rep counter
, Rep ix
, Num counter
, Num ix
, Size iy
, Rep iy, StdLogic ix, StdLogic iy, StdLogic a,
WIDTH ix ~ ADD (WIDTH iz) (WIDTH iy),
StdLogic counter, StdLogic counter2,
StdLogic iz, Size iz, Rep iz, Num iy
, WIDTH counter ~ ADD (WIDTH iz) (WIDTH counter2)
, Num iz
, Clock c
)
=> Witness ix
-> Witness iy
-> Signal c Bool
-> HandShaken c (Signal c (Enabled a))
-> HandShaken c (Signal c (Enabled (M.Matrix iz a)))
fifoToMatrix w_ix@Witness w_iy@Witness rst hs = HandShaken $ \ out_ready ->
let
wr :: Signal c (Maybe (ix, a))
wr = fifoFE w_ix rst (hs,dec_by)
inp_done2 :: Signal c Bool
inp_done2 = resetable rst low
$ register False
$ resetable rst low
$ register False
$ resetable rst low
$ isEnabled wr
mem :: Signal c (Enabled (M.Matrix iz a))
mem = enabledS
$ pack
$ fmap (\ f -> f rd_addr0)
$ fmap pipeToMemory
$ splitWrite
$ mapEnabled (mapPacked $ \ (a,d) -> (unappendS a,d))
$ wr
((rd_addr0,out_done0),out) = fifoBE w_iy rst (inc_by,mem) <~~ out_ready
dec_by = mulBy (Witness :: Witness iz) out_done0
inc_by = divBy (Witness :: Witness iz) rst inp_done2
in
out
-- Move into a Commute module?
-- classical find the implementation problem.
splitWrite :: forall a a1 a2 d c . (Rep a1, Rep a2, Rep d, Size a1) => Signal c (Pipe (a1,a2) d) -> M.Matrix a1 (Signal c (Pipe a2 d))
splitWrite inp = M.forAll $ \ i -> let (g,v) = unpackEnabled inp
(a,d) = unpack v
(a1,a2) = unpack a
in packEnabled (g .&&. (a1 .==. pureS i))
(pack (a2,d))
-}
mulBy :: forall x sz c . (Clock c, Size sz, Num sz, Num x, Rep x) => Witness sz -> Signal c Bool -> Signal c x
mulBy Witness trig = mux trig (pureS 0,pureS $ fromIntegral $ size (error "witness" :: sz))
divBy :: forall x sz c . (Clock c, Size sz, Num sz, Rep sz, Num x, Rep x) => Witness sz -> Signal c Bool -> Signal c Bool -> Signal c x
divBy Witness rst trig = mux issue (0,1)
where
issue = trig .&&. (counter1 .==. (pureS $ fromIntegral (size (error "witness" :: sz) - 1)))
counter0 :: Signal c sz
counter0 = cASE [ (rst,0)
, (trig,counter1 + 1)
] counter1
counter1 :: Signal c sz
counter1 = register 0
$ mux issue (counter0,0)