Add Simulate instance for AXI4Lite

Author: PietPtr

src/Protocols/Axi4/Lite/Axi4Lite.hs

@@ -1,10 +1,7 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE UndecidableInstances #-}
-<<<<<<< HEAD
 {-# LANGUAGE RecordWildCards #-}
-=======
->>>>>>> cc790e6... Add AXI4 Lite types
 {-|
 Defines datatypes for all five channels of the AXI4 Lite protocol. For more
 information on AXI4 Lite, see chapter B of the AMBA AXI specification.
@@ -15,15 +12,17 @@ module Protocols.Axi4.Lite.Axi4Lite where
 import Protocols
 import Protocols.Axi4.Common
 import Clash.Prelude as C
+import Clash.Signal.Internal
+import Data.List ((\\))
 
 import Control.DeepSeq
 
+import qualified Data.Bifunctor as B
+
+
+
 -- | AXI4 Lite busses are always either 32 bit or 64 bit.
-<<<<<<< HEAD
 data BusWidth = Width32 | Width64 deriving (Show, Eq, Generic, NFDataX)
-=======
-data BusWidth = Width32 | Width64 deriving (Show, Eq)
->>>>>>> cc790e6... Add AXI4 Lite types
 
 type instance Width 'Width32 = 32
 type instance Width 'Width64 = 64
@@ -40,10 +39,6 @@ type family ReadBusWidthType (bw :: BusWidth) where
   ReadBusWidthType 'Width32 = C.Vec 4 (C.BitVector 8)
   ReadBusWidthType 'Width64 = C.Vec 8 (C.BitVector 8)
 
-<<<<<<< HEAD
-=======
-
->>>>>>> cc790e6... Add AXI4 Lite types
 ---------------------------
 --- Write address types ---
 ---------------------------
@@ -162,12 +157,10 @@ data S2M_ReadAddress
 -- to fullfil the injectivity requirement of 'Fwd' in 'Protocol', even though it only
 -- contains a ready signal of type 'Bool'.
 data M2S_ReadData
-  (bw :: BusWidth)
   = M2S_ReadData {
     _rready :: Bool
-  } deriving (Generic, NFDataX)
+  } deriving (Generic, NFDataX, Show)
 
-deriving instance (Show (ReadBusWidthType bw)) => Show (M2S_ReadData bw)
 
 -- | Data type for the data sent over the read data channel from the slave to the master.
 data S2M_ReadData
@@ -191,7 +184,7 @@ data M2S_Axi4Lite
     m2s_wd :: M2S_WriteData bw,
     m2s_wr :: M2S_WriteResponse,
     m2s_ra :: M2S_ReadAddress aw,
-    m2s_rd :: M2S_ReadData bw
+    m2s_rd :: M2S_ReadData
   }
   deriving (Generic)
 
@@ -252,6 +245,164 @@ instance (C.KnownDomain dom, NFDataX (S2M_Axi4Lite aw bw)) => Simulate (Axi4Lite
   sigToSimFwd _ = C.sample_lazy
   sigToSimBwd _ = C.sample_lazy
 
-  stallC SimulationConfig{..} (waStalls:>wdStalls:>wrStalls:>raStalls:>rdStalls:>Nil) = Circuit go
+  stallC conf stallAckVector = Circuit go
     where
-      go (fwd, bwd) = (bwd, fwd)
+      (waStalls:>wdStalls:>wrStalls:>raStalls:>rdStalls:>Nil) = stallAckVector
+      SimulationConfig{..} = conf
+      go :: (Signal dom (M2S_Axi4Lite aw bw),
+             Signal dom (S2M_Axi4Lite aw bw)) ->
+            (Signal dom (S2M_Axi4Lite aw bw),
+             Signal dom (M2S_Axi4Lite aw bw))
+      go (fwd, bwd) = (bwd', fwd')
+        where
+          bwd' = S2M_Axi4Lite <$> waBwdOut <*> wdBwdOut <*> wrBwdOut <*> raBwdOut <*> rdBwdOut
+          fwd' = M2S_Axi4Lite <$> waFwdOut <*> wdFwdOut <*> wrFwdOut <*> raFwdOut <*> rdFwdOut
+
+          (waFwd, wdFwd, wrFwd, raFwd, rdFwd) = dissectM2S fwd
+          (waBwd, wdBwd, wrBwd, raBwd, rdBwd) = dissectS2M bwd
+
+          (waStallAck, waStallNs) = waStalls
+          (waBwdOut, waFwdOut) = stallM2S (stallAcks waStallAck) waStallNs resetCycles waFwd waBwd
+
+          (wdStallAck, wdStallNs) = wdStalls
+          (wdBwdOut, wdFwdOut) = stallM2S (stallAcks wdStallAck) wdStallNs resetCycles wdFwd wdBwd
+
+          (wrStallAck, wrStallNs) = wrStalls
+          (wrBwdOut, wrFwdOut) = stallS2M (stallAcks wrStallAck) wrStallNs resetCycles wrFwd wrBwd
+
+          (raStallAck, raStallNs) = raStalls
+          (raBwdOut, raFwdOut) = stallM2S (stallAcks raStallAck) raStallNs resetCycles raFwd raBwd
+
+          (rdStallAck, rdStallNs) = rdStalls
+          (rdBwdOut, rdFwdOut) = stallS2M (stallAcks rdStallAck) rdStallNs resetCycles rdFwd rdBwd
+
+      dissectM2S (m :- m2s) =
+        ( m2s_wa m :- waSig
+        , m2s_wd m :- wdSig
+        , m2s_wr m :- wrSig
+        , m2s_ra m :- raSig
+        , m2s_rd m :- rdSig )
+        where
+          (waSig, wdSig, wrSig, raSig, rdSig) = dissectM2S m2s
+
+      dissectS2M (s :- s2m) =
+        ( s2m_wa s :- waSig
+        , s2m_wd s :- wdSig
+        , s2m_wr s :- wrSig
+        , s2m_ra s :- raSig
+        , s2m_rd s :- rdSig )
+        where
+          (waSig, wdSig, wrSig, raSig, rdSig) = dissectS2M s2m
+
+
+      stallAcks stallAck = cycle saList
+        where
+          saList | stallAck == StallCycle = [minBound..maxBound] \\ [StallCycle]
+                 | otherwise = [stallAck]
+
+
+      stallM2S :: (Source src, Destination dst) =>
+        [StallAck] -> [Int] -> Int ->
+        Signal dom src -> Signal dom dst ->
+        (Signal dom dst, Signal dom src)
+      stallM2S [] _ _ _ _ = error "finite stallAck list"
+      stallM2S sas stalls resetN (f :- fwd) (b :- bwd) | resetN > 0 =
+        B.bimap (b :-) (f :-) (stallM2S sas stalls (resetN - 1) fwd bwd)
+      stallM2S (sa:sas) [] _ (f :- fwd) ~(b :- bwd) =
+        B.bimap (toStallAck (maybePayload f) (isReady b) sa :-) (f :-) (stallM2S sas [] 0 fwd bwd)
+      stallM2S (sa:sas) stalls _ ((maybePayload -> Nothing) :- fwd) ~(b :- bwd) =
+        B.bimap (b' :-) (noData :-) (stallM2S sas stalls 0 fwd bwd)
+          where b' = toStallAck (Nothing :: Maybe (M2S_WriteAddress aw)) (isReady b) sa
+      stallM2S (_:sas) (stall:stalls) _ (f0 :- fwd) ~(b0 :- bwd) =
+        let
+          (f1, b1, stalls') = case compare 0 stall of
+            LT -> (noData, ready False, (stall - 1):stalls)
+            EQ -> (f0, b0, if isReady b0 then stalls else stall:stalls)
+            GT -> error ("Unexpected negative stall: " <> show stall)
+        in
+          B.bimap (b1 :-) (f1 :-) (stallM2S sas stalls' 0 fwd bwd)
+
+      stallS2M :: (Destination dst, Source src) =>
+        [StallAck] -> [Int] -> Int ->
+        Signal dom dst -> Signal dom src ->
+        (Signal dom src, Signal dom dst)
+      stallS2M sas stalls resetN fwd bwd = (src, dst)
+        where (dst, src) = stallM2S sas stalls resetN bwd fwd
+
+      toStallAck :: (Source src, Destination dst) => Maybe src -> Bool -> StallAck -> dst
+      toStallAck (Just _) ack = const (ready ack)
+      toStallAck Nothing ack = \case
+        StallWithNack -> ready False
+        StallWithAck -> ready True
+        StallWithErrorX -> C.errorX "No defined ack"
+        StallTransparently -> ready ack
+        StallCycle -> ready False -- shouldn't happen..
+
+-- | Every data-carrying direction in a channel in AXI4 has a @<Channel>@ and @No<Channel>@
+-- constructor. In some functions (like "stallC") it is useful to write functions that
+-- use this fact such that these can be applied to every channel of AXI4. This typeclass
+-- provides functions to convert a value in a channel to @Maybe@, where the @No<Channel>@ is
+-- converted to @Nothing@, and any other value to @Just value@.
+--
+-- This class is called @Source@ because a source of useful data is the sender of the type
+-- for which this class is relevant.
+class Source src where
+  -- | Converts a channel type to a @Maybe@
+  maybePayload :: src -> Maybe src
+  -- | The value of type "src" that is mapped to @Nothing@ by "maybePayload"
+  noData :: src
+
+-- | Typeclass to convert Booleans to channel-specific acknowledgement types.
+class Destination dst where
+  ready :: Bool -> dst
+  isReady :: dst -> Bool
+
+instance Source (M2S_WriteAddress aw) where
+  maybePayload M2S_NoWriteAddress = Nothing
+  maybePayload m2s_wa = Just m2s_wa
+
+  noData = M2S_NoWriteAddress
+
+instance Destination S2M_WriteAddress where
+  ready b = S2M_WriteAddress b
+  isReady (S2M_WriteAddress b) = b
+
+instance Source (M2S_WriteData bw) where
+  maybePayload M2S_NoWriteData = Nothing
+  maybePayload m2s_wd = Just m2s_wd
+
+  noData = M2S_NoWriteData
+
+instance Destination S2M_WriteData where
+  ready b = S2M_WriteData b
+  isReady (S2M_WriteData b) = b
+
+instance Source (S2M_WriteResponse) where
+  maybePayload S2M_NoWriteResponse = Nothing
+  maybePayload s2m_wr = Just s2m_wr
+
+  noData = S2M_NoWriteResponse
+
+instance Destination (M2S_WriteResponse) where
+  ready b = M2S_WriteResponse b
+  isReady (M2S_WriteResponse b) = b
+
+instance Source (M2S_ReadAddress aw) where
+  maybePayload M2S_NoReadAddress = Nothing
+  maybePayload m2s_ra = Just m2s_ra
+
+  noData = M2S_NoReadAddress
+
+instance Destination S2M_ReadAddress where
+  ready b = S2M_ReadAddress b
+  isReady (S2M_ReadAddress b) = b
+
+instance Source (S2M_ReadData bw) where
+  maybePayload S2M_NoReadData = Nothing
+  maybePayload s2m_rd = Just s2m_rd
+
+  noData = S2M_NoReadData
+
+instance Destination M2S_ReadData where
+  ready b = M2S_ReadData b
+  isReady (M2S_ReadData b) = b

src/Protocols/Df.hs

@@ -75,17 +75,12 @@ import qualified Prelude as P
 import           Clash.Prelude (type (<=))
 import           Clash.Signal.Internal (Signal)
 import qualified Clash.Prelude as C
-import qualified Clash.Explicit.Prelude as CE
 
 -- me
 import           Protocols.Internal
 import           Protocols.DfLike (DfLike)
 import qualified Protocols.DfLike as DfLike
 
-<<<<<<< HEAD
-=======
-import Debug.Trace
->>>>>>> cc790e6... Add AXI4 Lite types
 
 -- $setup
 -- >>> import Protocols
@@ -165,52 +160,6 @@ instance (C.KnownDomain dom, C.NFDataX a, C.ShowX a, Show a) => Drivable (Df dom
   sampleC = sample
 
 
-  simulateRight SimulationConfig{..} acks circ =
-    P.take timeoutAfter $
-    CE.sample_lazy $
-    P.snd $
-    toSignals circ ((), resetAndAcks)
-    where
-      resetAndAcks = C.fromList $ (P.map Ack (replicate resetCycles False) <> acks)
-
-  simulateLeft SimulationConfig{..} fwds circ = CE.sample_lazy ackSig
-    where
-      (ackSig, ()) = toSignals circ (dataSig, ())
-      dataSig = C.fromList_lazy (ackedData resetCycles fwds (C.sample ackSig))
-
-      ackedData resetN _ (_:acks) | resetN > 0 =
-        NoData : ackedData (resetN - 1) fwds acks
-      ackedData _ _ [] = C.errorX "Empty acks list."
-      ackedData _ [] (_:acks) = NoData : ackedData 0 [] acks
-      ackedData _ (dat:datas) (ack:acks) = case ack of
-        Ack True -> dat : ackedData 0 (datas) acks
-        Ack False -> dat : ackedData 0 (dat:datas) acks
-
-
-
-  simulateManager SimulationConfig{..} acks circ =
-    P.take timeoutAfter $
-    CE.sample_lazy $
-    P.snd $
-    toSignals circ ((), resetAndAcks)
-    where
-      resetAndAcks = C.fromList $ (P.map Ack (replicate resetCycles False) <> acks)
-
-  -- TODO: apply simulation config
-  simulateSubordinate SimulationConfig{..} fwds circ = CE.sample_lazy ackSig
-    where
-      (ackSig, ()) = toSignals circ (dataSig, ())
-      dataSig = C.fromList_lazy (ackedData resetCycles fwds (C.sample ackSig))
-
-      ackedData resetN _ (_:acks) | resetN > 0 =
-        NoData : ackedData (resetN - 1) fwds acks
-      ackedData _ [] (_:acks) = NoData : ackedData 0 [] acks
-      ackedData _ (dat:datas) (ack:acks) = case ack of
-        Ack True -> dat : ackedData 0 (datas) acks
-        Ack False -> dat : ackedData 0 (dat:datas) acks
-
-
-
 instance DfLike dom (Df dom) a where
   type Data (Df dom) a = Data a
   type Payload a = a

src/Protocols/Internal.hs

@@ -372,7 +372,7 @@ data StallAck
 -- some shape. The "Backpressure" instance requires that the /backward/ type of the
 -- circuit can be generated from a list of Booleans.
 class (C.KnownNat (SimulateChannels a), Backpressure a, Simulate a) => Drivable a where
-  -- | Similar to 'SimulateType', but without backpressure information. For
+  -- | Similar to 'SimulateFwdType', but without backpressure information. For
   -- example:
   --
   -- >>> :kind! (forall dom a. ExpectType (Df dom a))
@@ -385,7 +385,7 @@ class (C.KnownNat (SimulateChannels a), Backpressure a, Simulate a) => Drivable
   type ExpectType a :: Type
 
   -- | Convert a /ExpectType a/, a type representing data without backpressure,
-  -- into a type that does, /SimulateType a/.
+  -- into a type that does, /SimulateFwdType a/.
   toSimulateType ::
     -- | Type witness
     Proxy a ->
@@ -395,7 +395,7 @@ class (C.KnownNat (SimulateChannels a), Backpressure a, Simulate a) => Drivable
     SimulateFwdType a
 
   -- | Convert a /ExpectType a/, a type representing data without backpressure,
-  -- into a type that does, /SimulateType a/.
+  -- into a type that does, /SimulateFwdType a/.
   fromSimulateType ::
     -- | Type witness
     Proxy a ->
@@ -493,13 +493,6 @@ instance Drivable () where
   sampleC _  _ = ()
 
 
-  simulateRight _ _ _ = ()
-  simulateLeft _ _ _ = ()
-
-  simulateManager _ _ _ = ()
-  simulateSubordinate _ _ _ = ()
-
-
 instance (Simulate a, Simulate b) => Simulate (a, b) where
   type SimulateFwdType (a, b) = (SimulateFwdType a, SimulateFwdType b)
   type SimulateBwdType (a, b) = (SimulateBwdType a, SimulateBwdType b)
@@ -621,9 +614,9 @@ instance (C.NFDataX a, C.ShowX a, Show a, C.KnownDomain dom) => Drivable (CSigna
 -- Not synthesizable.
 --
 -- To figure out what input you need to supply, either solve the type
--- "SimulateType" manually, or let the repl do the work for you! Example:
+-- "SimulateFwdType" manually, or let the repl do the work for you! Example:
 --
--- >>> :kind! (forall dom a. SimulateType (Df dom a))
+-- >>> :kind! (forall dom a. SimulateFwdType (Df dom a))
 -- ...
 -- = [Protocols.Df.Data a]
 --
@@ -687,6 +680,7 @@ simulateCSE c = simulateCS (c clk rst ena)
 
   resetGen n = C.unsafeFromHighPolarity (C.fromList (replicate n True <> repeat False))
 
+-- TODO: implement SimulationConfig
 simulateCircuit :: forall a b . (Simulate a, Simulate b) =>
   SimulateFwdType a -> SimulateBwdType b ->
   Circuit a b ->