diff --git a/clash-protocols.cabal b/clash-protocols.cabal
index 243964c7..be2bb8f1 100644
--- a/clash-protocols.cabal
+++ b/clash-protocols.cabal
@@ -135,6 +135,8 @@ library
       -- To be removed; we need 'Test.Tasty.Hedgehog.Extra' to fix upstream issues
     , tasty >= 1.2 && < 1.5
     , tasty-hedgehog >= 1.2
+    , tasty-th
+    , strict-tuple
 
   exposed-modules:
     Protocols
@@ -146,6 +148,7 @@ library
     Protocols.Axi4.WriteAddress
     Protocols.Axi4.WriteData
     Protocols.Axi4.WriteResponse
+    Protocols.Axi4.Lite.Axi4Lite
 
     Protocols.Df
     Protocols.DfLike
@@ -154,6 +157,7 @@ library
     Protocols.Internal
     Protocols.Plugin
 
+
     -- 'testProperty' is broken upstream, it reports wrong test names
     -- TODO: test / upstream ^
     Test.Tasty.Hedgehog.Extra
diff --git a/src/Protocols.hs b/src/Protocols.hs
index 427e6a47..672f46b3 100644
--- a/src/Protocols.hs
+++ b/src/Protocols.hs
@@ -31,15 +31,22 @@ module Protocols
 
     -- * Simulation
   , Simulate
-     ( SimulateType
-     , ExpectType
+     ( SimulateFwdType
+     , SimulateBwdType
      , SimulateChannels
-     , toSimulateType
-     , fromSimulateType
-     , driveC
-     , sampleC
+     , sigToSimFwd
+     , sigToSimBwd
+     , simToSigFwd
+     , simToSigBwd
      , stallC
      )
+  , Drivable
+    ( ExpectType
+    , toSimulateType
+    , fromSimulateType
+    , driveC
+    , sampleC
+    )
   , SimulationConfig(..)
   , StallAck(..)
   , simulateC
diff --git a/src/Protocols/Axi4/Common.hs b/src/Protocols/Axi4/Common.hs
index bb450a61..abd5d854 100644
--- a/src/Protocols/Axi4/Common.hs
+++ b/src/Protocols/Axi4/Common.hs
@@ -16,7 +16,9 @@ import qualified Clash.Prelude as C
 import Clash.Prelude (type (^), type (-), type (*))
 
 -- strict-tuple
-import Data.Tuple.Strict (T3, T4)
+import Data.Tuple.Strict (T4)
+
+import Control.DeepSeq
 
 -- | Simple wrapper to achieve "named arguments" when instantiating an AXI protocol
 data IdWidth = IdWidth Nat
@@ -70,10 +72,10 @@ data SKeepStrobe (strobeType :: KeepStrobe) where
   SNoStrobe :: SKeepStrobe 'NoStrobe
 
 -- | Extracts Nat from 'IdWidth', 'AddrWidth', and 'LengthWidth'
-type family Width (a :: k) :: Nat where
-  Width ('IdWidth n) = n
-  Width ('AddrWidth n) = n
-  Width ('LengthWidth n) = n
+type family Width (a :: k) :: Nat --where
+type instance Width ('IdWidth n) = n
+type instance Width ('AddrWidth n) = n
+type instance Width ('LengthWidth n) = n
 
 -- | Enables or disables 'BurstMode'
 type family BurstType (keepBurst :: KeepBurst) where
@@ -102,7 +104,7 @@ type family LockType (keepLockType :: KeepLock) where
 
 -- | Enables or disables 'Privileged', 'Secure', and 'InstructionOrData'
 type family PermissionsType (keepPermissions :: KeepPermissions) where
-  PermissionsType 'KeepPermissions = T3 Privileged Secure InstructionOrData
+  PermissionsType 'KeepPermissions = (Privileged, Secure, InstructionOrData)
   PermissionsType 'NoPermissions = ()
 
 -- | Enables or disables 'Qos'
@@ -245,6 +247,19 @@ data Resp
   | RDecodeError
   deriving (Show, C.ShowX, Generic, C.NFDataX)
 
+-- | Status of a read or write transaction on AXI4 Lite.
+data RespLite
+  -- | Normal access success. Indicates that a normal access has been
+  -- successful.
+  = RLOkay
+  -- | Slave error. Used when the access has reached the slave successfully, but
+  -- the slave wishes to return an error condition to the originating master.
+  | RLSlaveError
+  -- | Decode error. Generated, typically by an interconnect component, to
+  -- indicate that there is no slave at the transaction address.
+  | RLDecodeError
+  deriving (Show, C.ShowX, Generic, C.NFDataX)
+
 -- | Whether a resource is accessed with exclusive access or not
 data AtomicAccess
   = NonExclusiveAccess
@@ -260,12 +275,14 @@ data Modifiable
 data Secure
   = Secure
   | NonSecure
+  deriving (Show, Generic, C.NFDataX, NFData, C.ShowX, Eq)
 
 -- | An AXI master might support more than one level of operating privilege,
 -- and extend this concept of privilege to memory access.
 data Privileged
   = NotPrivileged
   | Privileged
+  deriving (Show, Generic, C.NFDataX, NFData, C.ShowX, Eq)
 
 -- | Whether the transaction is an instruction access or a data access. The AXI
 -- protocol defines this indication as a hint. It is not accurate in all cases,
@@ -276,3 +293,4 @@ data Privileged
 data InstructionOrData
   = Data
   | Instruction
+  deriving (Show, Generic, C.NFDataX, NFData, C.ShowX, Eq)
diff --git a/src/Protocols/Axi4/Lite/Axi4Lite.hs b/src/Protocols/Axi4/Lite/Axi4Lite.hs
new file mode 100644
index 00000000..36a24225
--- /dev/null
+++ b/src/Protocols/Axi4/Lite/Axi4Lite.hs
@@ -0,0 +1,412 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE RecordWildCards #-}
+{-|
+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.
+-}
+
+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.
+data BusWidth = Width32 | Width64 deriving (Show, Eq, Generic, NFDataX)
+
+type instance Width 'Width32 = 32
+type instance Width 'Width64 = 64
+
+-- | AXI4 Lite defines a strobe signal to signify which bytes of the input
+-- signal should be committed to memory. The strobe signal is encoded in
+-- the 'Maybe' data type. Strobing is mandatory in AXI4 Lite.
+type family WriteBusWidthType (bw :: BusWidth) where
+  WriteBusWidthType 'Width32 = C.Vec 4 (Maybe (C.BitVector 8))
+  WriteBusWidthType 'Width64 = C.Vec 8 (Maybe (C.BitVector 8))
+
+-- | Type family mapping the two available bus widths to vectors of bytes.
+type family ReadBusWidthType (bw :: BusWidth) where
+  ReadBusWidthType 'Width32 = C.Vec 4 (C.BitVector 8)
+  ReadBusWidthType 'Width64 = C.Vec 8 (C.BitVector 8)
+
+---------------------------
+--- Write address types ---
+---------------------------
+
+
+-- | The xvalid signals in AXI4 Lite are encoded in the datatype by having two
+-- options, e.g. M2S_NoWriteAddress and M2S_WriteAddress. The rest of the channels
+-- are fields in the record. Table B1.1 defines which signals AXI4 Lite uses.
+data M2S_WriteAddress
+  (aw :: AddrWidth)
+  = M2S_NoWriteAddress
+  | M2S_WriteAddress {
+    -- | Address to be written to
+    _awaddr :: !(C.BitVector (Width aw)),
+
+    -- | Protection permissions, in AXI4 Lite these are always enabled.
+    _awprot :: PermissionsType 'KeepPermissions
+  } deriving (Generic, NFData)
+
+deriving instance (C.KnownNat (Width aw))
+  => Show (M2S_WriteAddress aw)
+
+deriving instance (C.KnownNat (Width aw))
+  => ShowX (M2S_WriteAddress aw)
+
+deriving instance (C.KnownNat (Width aw))
+  => Eq (M2S_WriteAddress aw)
+
+deriving instance (C.KnownNat (Width aw))
+  => NFDataX (M2S_WriteAddress aw)
+
+-- | Ready signal for the write address channel.
+data S2M_WriteAddress
+  = S2M_WriteAddress {
+    _awready :: Bool
+  } deriving (Show, Generic, NFDataX)
+
+
+------------------------
+--- Write data types ---
+------------------------
+
+-- | Data type for the write data channel.
+data M2S_WriteData
+  (bw :: BusWidth)
+  = M2S_NoWriteData
+  | M2S_WriteData {
+    -- | Write data
+    _wdata :: !(WriteBusWidthType bw)
+  } deriving (Generic)
+
+deriving instance
+  (C.KnownNat (Width bw)
+  , Show (WriteBusWidthType bw))
+  => Show (M2S_WriteData bw)
+
+deriving instance (NFDataX (WriteBusWidthType bw)) => NFDataX (M2S_WriteData bw)
+
+-- | Ready signal for the write data channel.
+data S2M_WriteData
+  = S2M_WriteData {
+    _wready :: Bool
+  } deriving (Show, Generic, NFDataX)
+
+----------------------------
+--- Write response types ---
+----------------------------
+
+-- | Data type for the write response channel. Notice that here the ready signal
+-- goes from master to slave instead of the other way around.
+data M2S_WriteResponse
+  = M2S_WriteResponse {
+    _bready :: Bool
+  } deriving (Show, Generic, NFDataX)
+
+-- | Data type for the write response channel from slave to master. On this channel
+-- the response as defined in A3.4.4 is sent.
+data S2M_WriteResponse
+  = S2M_NoWriteResponse
+  | S2M_WriteResponse {
+    _bresp :: RespLite
+  } deriving (Show, Generic, NFDataX)
+
+
+--------------------------
+--- Read address types ---
+--------------------------
+
+-- | Data type for the read address channel.
+data M2S_ReadAddress
+  (aw :: AddrWidth)
+  = M2S_NoReadAddress
+  | M2S_ReadAddress {
+    _araddr :: !(C.BitVector (Width aw)),
+    _arprot :: PermissionsType 'KeepPermissions
+  } deriving (Generic)
+
+deriving instance (KnownNat (Width aw)) => NFDataX (M2S_ReadAddress aw)
+
+deriving instance
+  (C.KnownNat (Width aw))
+  => Show (M2S_ReadAddress aw)
+
+-- | Ready signal for the read address channel.
+data S2M_ReadAddress
+  = S2M_ReadAddress {
+    _arready :: Bool
+  } deriving (Show, Generic, NFDataX)
+
+
+-----------------------
+--- Read data types ---
+-----------------------
+
+-- | Acknowledges data from the slave component.
+data M2S_ReadData
+  = M2S_ReadData {
+    _rready :: Bool
+  } deriving (Generic, NFDataX, Show)
+
+
+-- | Data type for the data sent over the read data channel from the slave to the master.
+data S2M_ReadData
+  (bw :: BusWidth)
+  = S2M_NoReadData
+  | S2M_ReadData {
+    _rdata :: ReadBusWidthType bw,
+    _rresp :: RespLite
+  } deriving (Generic)
+
+deriving instance (Show (ReadBusWidthType bw)) => Show (S2M_ReadData bw)
+deriving instance (NFDataX (ReadBusWidthType bw)) => NFDataX (S2M_ReadData bw)
+
+
+-- | Product type of the types of the five different channels in the direction of master to slave.
+data M2S_Axi4Lite
+  (aw :: AddrWidth)
+  (bw :: BusWidth)
+  = M2S_Axi4Lite {
+    m2s_wa :: M2S_WriteAddress aw,
+    m2s_wd :: M2S_WriteData bw,
+    m2s_wr :: M2S_WriteResponse,
+    m2s_ra :: M2S_ReadAddress aw,
+    m2s_rd :: M2S_ReadData
+  }
+  deriving (Generic)
+
+deriving instance
+  (NFDataX (ReadBusWidthType bw), NFDataX (WriteBusWidthType bw), KnownNat (Width aw))
+  => NFDataX (M2S_Axi4Lite aw bw)
+
+deriving instance
+  ( Show (ReadBusWidthType bw)
+  , Show (WriteBusWidthType bw)
+  , KnownNat (Width aw)
+  , KnownNat (Width bw))
+  => Show (M2S_Axi4Lite aw bw)
+
+-- | Product type of the types of the five different channels in the direction of slave to master.
+data S2M_Axi4Lite
+  (aw :: AddrWidth)
+  (bw :: BusWidth)
+  = S2M_Axi4Lite {
+    s2m_wa :: S2M_WriteAddress,
+    s2m_wd :: S2M_WriteData,
+    s2m_wr :: S2M_WriteResponse,
+    s2m_ra :: S2M_ReadAddress,
+    s2m_rd :: S2M_ReadData bw
+  }
+  deriving (Generic)
+
+deriving instance (NFDataX (ReadBusWidthType bw)) => NFDataX (S2M_Axi4Lite aw bw)
+
+deriving instance
+  ( Show (ReadBusWidthType bw)
+  , Show (WriteBusWidthType bw)
+  , KnownNat (Width aw)
+  , KnownNat (Width bw))
+  => Show (S2M_Axi4Lite aw bw)
+
+-- | Type for the full AXI4 Lite protocol.
+data Axi4Lite
+  (dom :: C.Domain)
+  (aw :: AddrWidth)
+  (bw :: BusWidth)
+
+-- | Protocol instance for Axi4Lite. The protocol instance is a one signal of all the channels
+-- in the AXI4 Lite protocol. Each channel type contains the data that is communicated over that channel.
+instance Protocol (Axi4Lite dom aw bw) where
+  type Fwd (Axi4Lite dom aw bw) = C.Signal dom (M2S_Axi4Lite aw bw)
+  type Bwd (Axi4Lite dom aw bw) = C.Signal dom (S2M_Axi4Lite aw bw)
+
+
+instance (C.KnownDomain dom, NFDataX (S2M_Axi4Lite aw bw)) => Simulate (Axi4Lite dom aw bw) where
+  type SimulateFwdType (Axi4Lite dom aw bw) = [M2S_Axi4Lite aw bw]
+  type SimulateBwdType (Axi4Lite dom aw bw) = [S2M_Axi4Lite aw bw]
+  type SimulateChannels (Axi4Lite dom aw bw) = 5
+
+  simToSigFwd _ = C.fromList_lazy
+  simToSigBwd _ = C.fromList_lazy
+  sigToSimFwd _ = C.sample_lazy
+  sigToSimBwd _ = C.sample_lazy
+
+  stallC conf stallAckVector = Circuit go
+    where
+      -- A pattern match failed as the linting needs all patterns to be caught, even though we know
+      -- due to the type of SimulateChannels that this vector always has length five, this way
+      -- of deconstructing the vector gives no such pattern matching errors...
+      (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]
+
+      -- Very similar to the go function found in the stallC implementation of DfLike.
+      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)
+
+      -- stalling from slave to master is the same as the other way around, just with the forward and
+      -- backward channels switched.
+      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
+
+      -- TODO: A similar function also exists in another stallC implementation, perhaps better to generalize?
+      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
diff --git a/src/Protocols/Axi4/ReadAddress.hs b/src/Protocols/Axi4/ReadAddress.hs
index 5d4113b5..b89db223 100644
--- a/src/Protocols/Axi4/ReadAddress.hs
+++ b/src/Protocols/Axi4/ReadAddress.hs
@@ -86,19 +86,19 @@ instance DfLike dom (Axi4ReadAddress dom kb ksz lw iw aw kr kbl kl kc kp kq) use
 instance (C.KnownDomain dom, C.NFDataX userType, C.ShowX userType, Show userType) =>
   Simulate (Axi4ReadAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) where
 
-  type SimulateType (Axi4ReadAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) =
+  type SimulateFwdType (Axi4ReadAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) =
     [M2S_ReadAddress kb ksz lw iw aw kr kbl kl kc kp kq userType]
 
-  type ExpectType (Axi4ReadAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) =
-    [M2S_ReadAddress kb ksz lw iw aw kr kbl kl kc kp kq userType]
+  type SimulateBwdType (Axi4ReadAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) =
+    [S2M_ReadAddress]
 
   type SimulateChannels (Axi4ReadAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) = 1
 
-  toSimulateType _ = id
-  fromSimulateType _ = id
+  simToSigFwd Proxy = C.fromList_lazy
+  simToSigBwd Proxy = C.fromList_lazy
+  sigToSimFwd Proxy = C.sample_lazy
+  sigToSimBwd Proxy = C.sample_lazy
 
-  driveC = DfLike.drive Proxy
-  sampleC = DfLike.sample Proxy
   stallC conf (C.head -> (stallAck, stalls)) =
     DfLike.stall Proxy conf stallAck stalls
 
diff --git a/src/Protocols/Axi4/ReadData.hs b/src/Protocols/Axi4/ReadData.hs
index 0fe6ba1f..e543fa97 100644
--- a/src/Protocols/Axi4/ReadData.hs
+++ b/src/Protocols/Axi4/ReadData.hs
@@ -107,19 +107,19 @@ instance DfLike dom (Axi4ReadData dom kr iw userType) dataType where
 instance (C.KnownDomain dom, C.NFDataX dataType, C.ShowX dataType, Show dataType) =>
   Simulate (Axi4ReadData dom kr iw userType dataType) where
 
-  type SimulateType (Axi4ReadData dom kr iw userType dataType) =
+  type SimulateFwdType (Axi4ReadData dom kr iw userType dataType) =
     [S2M_ReadData kr iw userType dataType]
 
-  type ExpectType (Axi4ReadData dom kr iw userType dataType) =
-    [S2M_ReadData kr iw userType dataType]
+  type SimulateBwdType (Axi4ReadData dom kr iw userType dataType) =
+    [M2S_ReadData]
 
   type SimulateChannels (Axi4ReadData dom kr iw userType dataType) = 1
 
-  toSimulateType _ = id
-  fromSimulateType _ = id
+  simToSigFwd Proxy = C.fromList_lazy
+  simToSigBwd Proxy = C.fromList_lazy
+  sigToSimFwd Proxy = C.sample_lazy
+  sigToSimBwd Proxy = C.sample_lazy
 
-  driveC = DfLike.drive Proxy
-  sampleC = DfLike.sample Proxy
   stallC conf (C.head -> (stallAck, stalls)) =
     DfLike.stall Proxy conf stallAck stalls
 
diff --git a/src/Protocols/Axi4/WriteAddress.hs b/src/Protocols/Axi4/WriteAddress.hs
index 1d27d658..94034424 100644
--- a/src/Protocols/Axi4/WriteAddress.hs
+++ b/src/Protocols/Axi4/WriteAddress.hs
@@ -86,19 +86,19 @@ instance DfLike dom (Axi4WriteAddress dom kb ksz lw iw aw kr kbl kl kc kp kq) us
 instance (C.KnownDomain dom, C.NFDataX userType, C.ShowX userType, Show userType) =>
   Simulate (Axi4WriteAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) where
 
-  type SimulateType (Axi4WriteAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) =
+  type SimulateFwdType (Axi4WriteAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) =
     [M2S_WriteAddress kb ksz lw iw aw kr kbl kl kc kp kq userType]
 
-  type ExpectType (Axi4WriteAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) =
-    [M2S_WriteAddress kb ksz lw iw aw kr kbl kl kc kp kq userType]
+  type SimulateBwdType (Axi4WriteAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) =
+    [S2M_WriteAddress]
 
   type SimulateChannels (Axi4WriteAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) = 1
 
-  toSimulateType _ = id
-  fromSimulateType _ = id
+  simToSigFwd Proxy = C.fromList_lazy
+  simToSigBwd Proxy = C.fromList_lazy
+  sigToSimFwd Proxy = C.sample_lazy
+  sigToSimBwd Proxy = C.sample_lazy
 
-  driveC = DfLike.drive Proxy
-  sampleC = DfLike.sample Proxy
   stallC conf (C.head -> (stallAck, stalls)) =
     DfLike.stall Proxy conf stallAck stalls
 
diff --git a/src/Protocols/Axi4/WriteData.hs b/src/Protocols/Axi4/WriteData.hs
index e8679eba..35a3d84d 100644
--- a/src/Protocols/Axi4/WriteData.hs
+++ b/src/Protocols/Axi4/WriteData.hs
@@ -80,19 +80,19 @@ instance DfLike dom (Axi4WriteData dom ks dataType) userType where
 instance (C.KnownDomain dom, C.NFDataX userType, C.ShowX userType, Show userType) =>
   Simulate (Axi4WriteData dom ks nBytes userType) where
 
-  type SimulateType (Axi4WriteData dom ks nBytes userType) =
+  type SimulateFwdType (Axi4WriteData dom ks nBytes userType) =
     [M2S_WriteData ks nBytes userType]
 
-  type ExpectType (Axi4WriteData dom ks nBytes userType) =
-    [M2S_WriteData ks nBytes userType]
+  type SimulateBwdType (Axi4WriteData dom ks nBytes userType) =
+    [S2M_WriteData]
 
   type SimulateChannels (Axi4WriteData dom ks nBytes userType) = 1
 
-  toSimulateType _ = id
-  fromSimulateType _ = id
+  simToSigFwd Proxy = C.fromList_lazy
+  simToSigBwd Proxy = C.fromList_lazy
+  sigToSimFwd Proxy = C.sample_lazy
+  sigToSimBwd Proxy = C.sample_lazy
 
-  driveC = DfLike.drive Proxy
-  sampleC = DfLike.sample Proxy
   stallC conf (C.head -> (stallAck, stalls)) =
     DfLike.stall Proxy conf stallAck stalls
 
diff --git a/src/Protocols/Axi4/WriteResponse.hs b/src/Protocols/Axi4/WriteResponse.hs
index 14adc734..563d57c4 100644
--- a/src/Protocols/Axi4/WriteResponse.hs
+++ b/src/Protocols/Axi4/WriteResponse.hs
@@ -77,19 +77,19 @@ instance DfLike dom (Axi4WriteResponse dom kr iw) userType where
 instance (C.KnownDomain dom, C.NFDataX userType, C.ShowX userType, Show userType) =>
   Simulate (Axi4WriteResponse dom kr iw userType) where
 
-  type SimulateType (Axi4WriteResponse dom kr iw userType) =
+  type SimulateFwdType (Axi4WriteResponse dom kr iw userType) =
     [S2M_WriteResponse kr iw userType]
 
-  type ExpectType (Axi4WriteResponse dom kr iw userType) =
-    [S2M_WriteResponse kr iw userType]
+  type SimulateBwdType (Axi4WriteResponse dom kr iw userType) =
+    [M2S_WriteResponse]
 
   type SimulateChannels (Axi4WriteResponse dom kr iw userType) = 1
 
-  toSimulateType _ = id
-  fromSimulateType _ = id
+  simToSigFwd Proxy = C.fromList_lazy
+  simToSigBwd Proxy = C.fromList_lazy
+  sigToSimFwd Proxy = C.sample_lazy
+  sigToSimBwd Proxy = C.sample_lazy
 
-  driveC = DfLike.drive Proxy
-  sampleC = DfLike.sample Proxy
   stallC conf (C.head -> (stallAck, stalls)) =
     DfLike.stall Proxy conf stallAck stalls
 
diff --git a/src/Protocols/Df.hs b/src/Protocols/Df.hs
index 5bb053a5..dde8f6f2 100644
--- a/src/Protocols/Df.hs
+++ b/src/Protocols/Df.hs
@@ -81,6 +81,7 @@ import           Protocols.Internal
 import           Protocols.DfLike (DfLike)
 import qualified Protocols.DfLike as DfLike
 
+
 -- $setup
 -- >>> import Protocols
 -- >>> import Clash.Prelude (Vec(..))
@@ -101,6 +102,7 @@ instance Protocol (Df dom a) where
   -- | Backward part of simple dataflow: @Signal dom Bool@
   type Bwd (Df dom a) = Signal dom Ack
 
+
 instance Backpressure (Df dom a) where
   boolsToBwd _ = C.fromList_lazy . coerce
 
@@ -135,17 +137,28 @@ dataToMaybe :: Data a -> Maybe a
 dataToMaybe NoData = Nothing
 dataToMaybe (Data a) = Just a
 
+
 instance (C.KnownDomain dom, C.NFDataX a, C.ShowX a, Show a) => Simulate (Df dom a) where
-  type SimulateType (Df dom a) = [Data a]
-  type ExpectType (Df dom a) = [a]
+  type SimulateFwdType (Df dom a) = [Data a]
+  type SimulateBwdType (Df dom a) = [Ack]
   type SimulateChannels (Df dom a) = 1
 
+  simToSigFwd _ = C.fromList_lazy
+  simToSigBwd _ = C.fromList_lazy
+  sigToSimFwd _ = C.sample_lazy
+  sigToSimBwd _ = C.sample_lazy
+
+  stallC conf (C.head -> (stallAck, stalls)) = stall conf stallAck stalls
+
+instance (C.KnownDomain dom, C.NFDataX a, C.ShowX a, Show a) => Drivable (Df dom a) where
+  type ExpectType (Df dom a) = [a]
+
   toSimulateType Proxy = P.map Data
   fromSimulateType Proxy = Maybe.mapMaybe dataToMaybe
 
   driveC = drive
   sampleC = sample
-  stallC conf (C.head -> (stallAck, stalls)) = stall conf stallAck stalls
+
 
 instance DfLike dom (Df dom) a where
   type Data (Df dom) a = Data a
@@ -429,6 +442,7 @@ registerBwd = DfLike.registerBwd Proxy
 
 --------------------------------- SIMULATE -------------------------------------
 
+
 -- | Emit values given in list. Emits no data while reset is asserted. Not
 -- synthesizable.
 drive ::
diff --git a/src/Protocols/DfLike.hs b/src/Protocols/DfLike.hs
index 1dc98aed..766cd510 100644
--- a/src/Protocols/DfLike.hs
+++ b/src/Protocols/DfLike.hs
@@ -595,7 +595,7 @@ fanin ::
   ) =>
   (a -> a -> a) ->
   Circuit (C.Vec n (df x)) (df x)
-fanin f = bundleVec Proxy Proxy |> map Proxy Proxy (C.fold @(n-1) f)
+fanin f = bundleVec Proxy Proxy |> map Proxy Proxy (C.fold  @(n-1) f)
 {-# INLINE fanin #-}
 
 -- | Merge data of multiple streams using Monoid's '<>'.
@@ -673,7 +673,7 @@ unbundleVec dfX dfY =
 
           -- Store new acks, send ack if all "clients" have acked
           acked1 = C.zipWith (||) acked (C.map (ackToBool dfY) acks)
-          ack = C.fold @(n-1) (&&) acked1
+          ack = C.fold  @(n-1) (&&) acked1
         in
           ( if ack then initState else acked1
           , (boolToAck dfX ack, dats1) )
@@ -776,7 +776,7 @@ roundrobinCollect dfA Parallel =
     acks = Maybe.fromMaybe nacks ((\i -> C.replace i ack nacks) <$> iM)
     dat1 = Maybe.fromMaybe (noData dfA) dat0
     (iM, dat0) = Data.List.NonEmpty.unzip dats1
-    dats1 = C.fold @(n-1) (<|>) (C.zipWith goDat C.indicesI dats0)
+    dats1 = C.fold  @(n-1) (<|>) (C.zipWith goDat C.indicesI dats0)
 
     goDat i dat
       | hasPayload dfA dat = Just (i, dat)
@@ -883,7 +883,9 @@ stall ::
   Proxy (df a) ->
   SimulationConfig ->
   -- | Acknowledgement to send when LHS does not send data. Stall will act
-  -- transparently when reset is asserted.
+  -- transparently when reset is asserted. A correct circuit would nack during reset,
+  -- however since "stall" is used to debug other components it acts transparently as
+  -- otherwise it may occlude the behavior of the components under test.
   StallAck ->
   -- Number of cycles to stall for every valid Df packet
   [Int] ->
diff --git a/src/Protocols/Hedgehog/Internal.hs b/src/Protocols/Hedgehog/Internal.hs
index ff3e0497..486bcfb5 100644
--- a/src/Protocols/Hedgehog/Internal.hs
+++ b/src/Protocols/Hedgehog/Internal.hs
@@ -67,8 +67,8 @@ instance (NFData a, C.NFDataX a, C.ShowX a, C.Show a, Eq a) => TestType a
 
 -- | Provides a way of comparing expected data with data produced by a
 -- protocol component.
-class ( Simulate a
-      , TestType (SimulateType a)
+class ( Drivable a
+      , TestType (SimulateFwdType a)
       , TestType (ExpectType a)
 
       -- Foldable requirement on Vec :(
@@ -91,13 +91,13 @@ class ( Simulate a
     -- | Number of valid data cycles expected on each channel
     C.Vec (SimulateChannels a) Int ->
     -- | Raw sampled data
-    SimulateType a ->
+    SimulateFwdType a ->
     -- | Depending on "ExpectOptions", fails the test if:
     --
     --   * Circuit produced less data than expected
     --   * Circuit produced more data than expected
     --
-    -- If it does not fail, /SimulateType a/ will contain exactly the number
+    -- If it does not fail, /SimulateFwdType a/ will contain exactly the number
     -- of expected data packets.
     --
     -- TODO:
@@ -174,7 +174,7 @@ instance
     Proxy (C.Vec n a) ->
     ExpectOptions ->
     C.Vec (n * SimulateChannels a) Int ->
-    C.Vec n (SimulateType a) ->
+    C.Vec n (SimulateFwdType a) ->
     m (C.Vec n (ExpectType a))
   expectN Proxy opts nExpecteds sampled = do
     -- TODO: This creates some pretty terrible error messages, as one
@@ -199,7 +199,7 @@ instance
     Proxy (a, b) ->
     ExpectOptions ->
     C.Vec (SimulateChannels a + SimulateChannels b) Int ->
-    (SimulateType a, SimulateType b) ->
+    (SimulateFwdType a, SimulateFwdType b) ->
     m (ExpectType a, ExpectType b)
   expectN Proxy opts nExpecteds (sampledA, sampledB) = do
     -- TODO: This creates some pretty terrible error messages, as one
diff --git a/src/Protocols/Internal.hs b/src/Protocols/Internal.hs
index 07c4d2e1..febd2070 100644
--- a/src/Protocols/Internal.hs
+++ b/src/Protocols/Internal.hs
@@ -6,6 +6,7 @@ Internal module to prevent hs-boot files (breaks Haddock)
 {-# LANGUAGE NamedFieldPuns #-}
 {-# LANGUAGE TypeFamilyDependencies #-}
 {-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
 
 module Protocols.Internal where
 
@@ -143,7 +144,8 @@ newtype Circuit a b =
 
 -- | Protocol-agnostic acknowledgement
 newtype Ack = Ack Bool
-  deriving (Generic, C.NFDataX)
+  deriving (Generic, C.NFDataX, Show)
+
 
 -- | Acknowledge. Used in circuit-notation plugin to drive ignore components.
 instance Default Ack where
@@ -161,7 +163,7 @@ instance Default a => Default (CSignal dom a) where
 class Protocol a where
   -- | Sender to receiver type family. See 'Circuit' for an explanation on the
   -- existence of 'Fwd'.
-  type Fwd (a :: Type) = (r :: Type) | r -> a
+  type Fwd (a :: Type)
 
   -- | Receiver to sender type family. See 'Circuit' for an explanation on the
   -- existence of 'Bwd'.
@@ -365,20 +367,12 @@ data StallAck
   | StallCycle
   deriving (Eq, Bounded, Enum, Show)
 
--- | Class that defines how to /drive/, /sample/, and /stall/ a "Circuit" of
- -- some shape.
-class (C.KnownNat (SimulateChannels a), Backpressure a) => Simulate a where
-  -- Type a /Circuit/ driver needs or sampler yields. For example:
-  --
-  -- >>> :kind! (forall dom a. SimulateType (Df dom a))
-  -- ...
-  -- = [Data a]
-  --
-  -- This means sampling a @Circuit () (Df dom a)@ with 'sampleC' yields
-  -- @[Data a]@.
-  type SimulateType a :: Type
 
-  -- | Similar to 'SimulateType', but without backpressure information. For
+-- | Class that defines how to /drive/, /sample/, and /stall/ a "Circuit" of
+-- 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 'SimulateFwdType', but without backpressure information. For
   -- example:
   --
   -- >>> :kind! (forall dom a. ExpectType (Df dom a))
@@ -390,28 +384,23 @@ class (C.KnownNat (SimulateChannels a), Backpressure a) => Simulate a where
   -- in "Protocols.Hedgehog" and 'simulateCS'.
   type ExpectType a :: Type
 
-  -- | The number of simulation channel this channel has after flattening it.
-  -- For example, @(Df dom a, Df dom a)@ has 2, while
-  -- @Vec 4 (Df dom a, Df dom a)@ has 8.
-  type SimulateChannels a :: C.Nat
-
   -- | 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 ->
     -- | Expect type: input for a protocol /without/ stall information
     ExpectType a ->
     -- | Expect type: input for a protocol /with/ stall information
-    SimulateType a
+    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 ->
     -- | Expect type: input for a protocol /with/ stall information
-    SimulateType a ->
+    SimulateFwdType a ->
     -- | Expect type: input for a protocol /without/ stall information
     ExpectType a
 
@@ -419,7 +408,7 @@ class (C.KnownNat (SimulateChannels a), Backpressure a) => Simulate a where
   -- to simulate a circuit. Related: 'simulateC'.
   driveC ::
     SimulationConfig ->
-    SimulateType a ->
+    SimulateFwdType a ->
     Circuit () a
 
   -- | Sample a circuit that is trivially drivable. Use 'driveC'  to create
@@ -427,7 +416,42 @@ class (C.KnownNat (SimulateChannels a), Backpressure a) => Simulate a where
   sampleC ::
     SimulationConfig ->
     Circuit () a ->
-    SimulateType a
+    SimulateFwdType a
+
+
+-- | Defines functions necessary for implementation of the 'simulateCircuit' function. This
+-- kind of simulation requires a lists for both the forward and the backward direction.
+--
+-- This class requires the definition of the types that the test supplies and returns. Its
+-- functions are converters from these /simulation types/ to types on the 'Signal' level.
+-- The 'simulateCircuit' function can thus receive the necessary simulation types, convert
+-- them to types on the 'Signal' level, pass those signals to the circuit, and convert the
+-- result of the circuit back to the simulation types giving the final result.
+class (C.KnownNat (SimulateChannels a), Protocol a) => Simulate a where
+  -- | The type that a test must provide to the 'simulateCircuit' function in the forward direction.
+  -- Usually this is some sort of list.
+  type SimulateFwdType a :: Type
+
+  -- | The type that a test must provide to the 'simulateCircuit' function in the backward direction.
+  -- Usually this is some sort of list
+  type SimulateBwdType a :: Type
+
+  -- | The number of simulation channels this channel has after flattening it.
+  -- For example, @(Df dom a, Df dom a)@ has 2, while
+  -- @Vec 4 (Df dom a, Df dom a)@ has 8.
+  type SimulateChannels a :: C.Nat
+
+  -- | Convert the forward simulation type to the 'Fwd' of @a@.
+  simToSigFwd :: Proxy a -> SimulateFwdType a -> Fwd a
+
+  -- | Convert the backward simulation type to the 'Bwd' of @a@.
+  simToSigBwd :: Proxy a -> SimulateBwdType a -> Bwd a
+
+  -- | Convert a signal of type @Bwd a@ to the backward simulation type.
+  sigToSimFwd :: Proxy a -> Fwd a -> SimulateFwdType a
+
+  -- | Convert a signal of type @Fwd a@ to the forward simulation type.
+  sigToSimBwd :: Proxy a -> Bwd a -> SimulateBwdType a
 
   -- | Create a /stalling/ circuit. For each simulation channel (see
   -- 'SimulateChannels') a tuple determines how the component stalls:
@@ -445,23 +469,55 @@ class (C.KnownNat (SimulateChannels a), Backpressure a) => Simulate a where
     C.Vec (SimulateChannels a) (StallAck, [Int]) ->
     Circuit a a
 
+
 instance Simulate () where
-  type SimulateType () = ()
-  type ExpectType () = ()
+  type SimulateFwdType () = ()
+  type SimulateBwdType () = ()
   type SimulateChannels () = 0
 
+  simToSigFwd _ = id
+  simToSigBwd _ = id
+  sigToSimFwd _ = id
+  sigToSimBwd _ = id
+
+  stallC _ _ = idC
+
+instance Drivable () where
+  type ExpectType () = ()
+
   toSimulateType Proxy () = ()
   fromSimulateType Proxy () = ()
 
   driveC _ _ = idC
   sampleC _  _ = ()
-  stallC _ _ = idC
+
 
 instance (Simulate a, Simulate b) => Simulate (a, b) where
-  type SimulateType (a, b) = (SimulateType a, SimulateType b)
-  type ExpectType (a, b) = (ExpectType a, ExpectType b)
+  type SimulateFwdType (a, b) = (SimulateFwdType a, SimulateFwdType b)
+  type SimulateBwdType (a, b) = (SimulateBwdType a, SimulateBwdType b)
   type SimulateChannels (a, b) = SimulateChannels a + SimulateChannels b
 
+  simToSigFwd Proxy (fwdsA, fwdsB) = (simToSigFwd (Proxy @a) fwdsA, simToSigFwd (Proxy @b) fwdsB)
+  simToSigBwd Proxy (bwdsA, bwdsB) = (simToSigBwd (Proxy @a) bwdsA, simToSigBwd (Proxy @b) bwdsB)
+  sigToSimFwd Proxy (fwdSigA, fwdSigB) = (sigToSimFwd (Proxy @a) fwdSigA, sigToSimFwd (Proxy @b) fwdSigB)
+  sigToSimBwd Proxy (bwdSigA, bwdSigB) = (sigToSimBwd (Proxy @a) bwdSigA, sigToSimBwd (Proxy @b) bwdSigB)
+
+  stallC conf stalls =
+    let
+      (stallsL, stallsR) = C.splitAtI @(SimulateChannels a) @(SimulateChannels b) stalls
+      Circuit stalledL = stallC @a conf stallsL
+      Circuit stalledR = stallC @b conf stallsR
+    in
+      Circuit $ \((fwdL0, fwdR0), (bwdL0, bwdR0)) ->
+        let
+          (fwdL1, bwdL1) = stalledL (fwdL0, bwdL0)
+          (fwdR1, bwdR1) = stalledR (fwdR0, bwdR0)
+        in
+          ((fwdL1, fwdR1), (bwdL1, bwdR1))
+
+instance (Drivable a, Drivable b) => Drivable (a, b) where
+  type ExpectType (a, b) = (ExpectType a, ExpectType b)
+
   toSimulateType Proxy (t1, t2) =
     ( toSimulateType (Proxy @a) t1
     , toSimulateType (Proxy @b) t2 )
@@ -471,7 +527,7 @@ instance (Simulate a, Simulate b) => Simulate (a, b) where
     , fromSimulateType (Proxy @b) t2 )
 
   driveC conf (fwd1, fwd2) =
-    let (Circuit f1, Circuit f2) = (driveC conf fwd1, driveC conf fwd2) in
+    let (Circuit f1, Circuit f2) = (driveC @a conf fwd1, driveC @b conf fwd2) in
     Circuit (\(_, ~(bwd1, bwd2)) -> ((), (snd (f1 ((), bwd1)), snd (f2 ((), bwd2)))))
 
   sampleC conf (Circuit f) =
@@ -479,36 +535,39 @@ instance (Simulate a, Simulate b) => Simulate (a, b) where
       bools = replicate (resetCycles conf) False <> repeat True
       (_, (fwd1, fwd2)) = f ((), (boolsToBwd (Proxy @a) bools, boolsToBwd (Proxy @b) bools))
     in
-      ( sampleC conf (Circuit $ \_ -> ((), fwd1))
-      , sampleC conf (Circuit $ \_ -> ((), fwd2)) )
+      ( sampleC @a conf (Circuit $ \_ -> ((), fwd1))
+      , sampleC @b conf (Circuit $ \_ -> ((), fwd2)) )
 
-  stallC conf stalls =
-    let
-      (stallsL, stallsR) = C.splitAtI @(SimulateChannels a) @(SimulateChannels b) stalls
-      Circuit stalledL = stallC @a conf stallsL
-      Circuit stalledR = stallC @b conf stallsR
-    in
-      Circuit $ \((fwdL0, fwdR0), (bwdL0, bwdR0)) ->
-        let
-          (fwdL1, bwdL1) = stalledL (fwdL0, bwdL0)
-          (fwdR1, bwdR1) = stalledR (fwdR0, bwdR0)
-        in
-          ((fwdL1, fwdR1), (bwdL1, bwdR1))
 
 -- TODO TemplateHaskell?
 -- instance SimulateType (a, b, c)
 -- instance SimulateType (a, b, c, d)
 
-instance (C.KnownNat n, Simulate a) => Simulate (C.Vec n a) where
-  type SimulateType (C.Vec n a) = C.Vec n (SimulateType a)
-  type ExpectType (C.Vec n a) = C.Vec n (ExpectType a)
+instance (CE.KnownNat n, Simulate a) => Simulate (C.Vec n a) where
+  type SimulateFwdType (C.Vec n a) = C.Vec n (SimulateFwdType a)
+  type SimulateBwdType (C.Vec n a) = C.Vec n (SimulateBwdType a)
   type SimulateChannels (C.Vec n a) = n * SimulateChannels a
 
+  simToSigFwd Proxy = C.map (simToSigFwd (Proxy @a))
+  simToSigBwd Proxy = C.map (simToSigBwd (Proxy @a))
+  sigToSimFwd Proxy = C.map (sigToSimFwd (Proxy @a))
+  sigToSimBwd Proxy = C.map (sigToSimBwd (Proxy @a))
+
+  stallC conf stalls0 =
+    let
+      stalls1 = C.unconcatI @n @(SimulateChannels a) stalls0
+      stalled = C.map (toSignals . stallC @a conf) stalls1
+    in
+      Circuit $ \(fwds, bwds) -> C.unzip (C.zipWith ($) stalled (C.zip fwds bwds))
+
+instance (C.KnownNat n, Drivable a) => Drivable (C.Vec n a) where
+  type ExpectType (C.Vec n a) = C.Vec n (ExpectType a)
+
   toSimulateType Proxy = C.map (toSimulateType (Proxy @a))
   fromSimulateType Proxy = C.map (fromSimulateType (Proxy @a))
 
   driveC conf fwds =
-    let circuits = C.map (($ ()) . curry . toSignals . driveC conf) fwds in
+    let circuits = C.map (($ ()) . curry . (toSignals @_ @a) . driveC conf) fwds in
     Circuit (\(_, bwds) -> ((), C.map snd (C.zipWith ($) circuits bwds)))
 
   sampleC conf (Circuit f) =
@@ -516,22 +575,26 @@ instance (C.KnownNat n, Simulate a) => Simulate (C.Vec n a) where
       bools = replicate (resetCycles conf) False <> repeat True
       (_, fwds) = f ((), (C.repeat (boolsToBwd (Proxy @a) bools)))
     in
-      C.map (\fwd -> sampleC conf (Circuit $ \_ -> ((), fwd))) fwds
+      C.map (\fwd -> sampleC @a conf (Circuit $ \_ -> ((), fwd))) fwds
 
-  stallC conf stalls0 =
-    let
-      stalls1 = C.unconcatI @n @(SimulateChannels a) stalls0
-      stalled = C.map (toSignals . stallC @a conf) stalls1
-    in
-      Circuit $ \(fwds, bwds) -> C.unzip (C.zipWith ($) stalled (C.zip fwds bwds))
+
+instance (C.KnownDomain dom) => Simulate (CSignal dom a) where
+  type SimulateFwdType (CSignal dom a) = [a]
+  type SimulateBwdType (CSignal dom a) = ()
+  type SimulateChannels (CSignal dom a) = 1
+
+  simToSigFwd Proxy list = CSignal (C.fromList_lazy list)
+  simToSigBwd Proxy () = def
+  sigToSimFwd Proxy (CSignal sig) = C.sample_lazy sig
+  sigToSimBwd Proxy _ = ()
+
+  stallC _ _ = idC
 
 instance Default (CSignal dom (Const () a)) where
   def = CSignal (pure (Const ()))
 
-instance (C.NFDataX a, C.ShowX a, Show a) => Simulate (CSignal dom a) where
-  type SimulateType (CSignal dom a) = [a]
+instance (C.NFDataX a, C.ShowX a, Show a, C.KnownDomain dom) => Drivable (CSignal dom a) where
   type ExpectType (CSignal dom a) = [a]
-  type SimulateChannels (CSignal dom a) = 1
 
   toSimulateType Proxy = id
   fromSimulateType Proxy = id
@@ -545,15 +608,14 @@ instance (C.NFDataX a, C.ShowX a, Show a) => Simulate (CSignal dom a) where
     let sampled = CE.sample_lazy ((\(CSignal s) -> s) (snd (f ((), def)))) in
     if ignoreReset then drop resetCycles sampled else sampled
 
-  stallC _ _ = idC
 
 -- | Simulate a circuit. Includes samples while reset is asserted.
 -- 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]
 --
@@ -563,16 +625,16 @@ instance (C.NFDataX a, C.ShowX a, Show a) => Simulate (CSignal dom a) where
 -- stalls nor introduce backpressure. If you want to to this use 'Df.stall'.
 simulateC ::
   forall a b.
-  (Simulate a, Simulate b) =>
+  (Drivable a, Drivable b) =>
   -- | Circuit to simulate
   Circuit a b ->
   -- | Simulation configuration. Note that some options only apply to 'sampleC'
   -- and some only to 'driveC'.
   SimulationConfig ->
   -- | Circuit input
-  SimulateType a ->
+  SimulateFwdType a ->
   -- | Circuit output
-  SimulateType b
+  SimulateFwdType b
 simulateC c conf as =
   sampleC conf (driveC conf as |> c)
 
@@ -587,7 +649,7 @@ simulateC c conf as =
 -- [1,3]
 simulateCS ::
   forall a b.
-  (Simulate a, Simulate b) =>
+  (Drivable a, Drivable b) =>
   -- | Circuit to simulate
   Circuit a b ->
   -- | Circuit input
@@ -602,7 +664,7 @@ simulateCS c =
 -- | Like 'simulateCS', but takes a circuit expecting a clock, reset, and enable.
 simulateCSE ::
   forall dom a b.
-  (Simulate a, Simulate b, C.KnownDomain dom) =>
+  (Drivable a, Drivable b, C.KnownDomain dom) =>
   -- | Circuit to simulate
   (C.Clock dom -> C.Reset dom -> C.Enable dom -> Circuit a b) ->
   -- | Circuit input
@@ -617,6 +679,21 @@ simulateCSE c = simulateCS (c clk rst ena)
 
   resetGen n = C.unsafeFromHighPolarity (C.fromList (replicate n True <> repeat False))
 
+-- | Applies conversion functions defined in the 'Simulate' instance of @a@ and @b@ to
+-- the given simulation types, and applies the results to the internal function of the
+-- given 'Circuit'. The resulting internal types are converted to the simulation types.
+-- TODO: implement SimulationConfig
+simulateCircuit :: forall a b . (Simulate a, Simulate b) =>
+  SimulateFwdType a -> SimulateBwdType b ->
+  Circuit a b ->
+  (SimulateBwdType a, SimulateFwdType b)
+simulateCircuit fwds bwds circ =
+    (sigToSimBwd (Proxy @a) bwdSig, sigToSimFwd (Proxy @b) fwdSig)
+    where
+      (bwdSig, fwdSig) = toSignals circ $
+        (simToSigFwd (Proxy @a) fwds, simToSigBwd (Proxy @b) bwds)
+
+
 -- | Picked up by "Protocols.Plugin" to process protocol DSL. See
 -- "Protocols.Plugin" for more information.
 circuit :: Any
@@ -628,3 +705,4 @@ circuit =
 (-<) :: Any
 (-<) =
   error "(-<) called: did you forget to enable \"Protocols.Plugin\"?"
+