diff --git a/clash-protocols.cabal b/clash-protocols.cabal
index 352e6534..0335f59f 100644
--- a/clash-protocols.cabal
+++ b/clash-protocols.cabal
@@ -134,9 +134,14 @@ library
       -- To be removed; we need 'Test.Tasty.Hedgehog.Extra' to fix upstream issues
     , tasty >= 1.2 && < 1.5
     , tasty-hedgehog
+    , strict-tuple
 
   exposed-modules:
     Protocols
+
+    Protocols.Axi4.Common
+    Protocols.Axi4.Lite.Axi4Lite
+
     Protocols.Df
     Protocols.DfLike
     Protocols.Hedgehog
@@ -144,6 +149,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/Axi4/Common.hs b/src/Protocols/Axi4/Common.hs
new file mode 100644
index 00000000..3e9f43da
--- /dev/null
+++ b/src/Protocols/Axi4/Common.hs
@@ -0,0 +1,294 @@
+{-|
+Types and utilities shared between AXI4, AXI4-Lite, and AXI3.
+-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Protocols.Axi4.Common where
+
+-- base
+import Data.Kind (Type)
+import GHC.Generics (Generic)
+import GHC.TypeNats (Nat)
+
+-- clash-prelude
+import qualified Clash.Prelude as C
+import Clash.Prelude (type (^), type (-), type (*))
+
+-- strict-tuple
+import Data.Tuple.Strict (T4)
+
+-- | Simple wrapper to achieve "named arguments" when instantiating an AXI protocol
+data IdWidth = IdWidth Nat deriving (Show, Eq)
+
+-- | Simple wrapper to achieve "named arguments" when instantiating an AXI protocol
+data AddrWidth = AddrWidth Nat deriving (Show, Eq)
+
+-- | Simple wrapper to achieve "named arguments" when instantiating an AXI protocol
+data LengthWidth = LengthWidth Nat deriving (Show, Eq)
+
+-- | Simple wrapper to achieve "named arguments" when instantiating an AXI protocol
+data UserType = UserType Type KeepStrobe
+
+-- | Keep or remove Burst, see 'BurstMode'
+data KeepBurst = KeepBurst | NoBurst deriving (Show, Eq)
+
+-- | Keep or remove Burst Length, see 'BurstSize'
+data KeepBurstLength = KeepBurstLength | NoBurstLength deriving (Show, Eq)
+
+-- | Keep or remove cache field, see 'Cache'
+data KeepCache = KeepCache | NoCache deriving (Show, Eq)
+
+-- | Keep or remove last field
+data KeepLast = KeepLast | NoLast deriving (Show, Eq)
+
+-- | Keep or remove lock, see 'AtomicAccess'
+data KeepLock = KeepLock | NoLock deriving (Show, Eq)
+
+-- | Keep or remove permissions, see 'Privileged', 'Secure', and
+-- 'InstructionOrData'.
+data KeepPermissions = KeepPermissions | NoPermissions deriving (Show, Eq)
+
+-- | Keep or remove quality of service field. See 'Qos'.
+data KeepQos = KeepQos | NoQos deriving (Show, Eq)
+
+-- | Keep or remove region field
+data KeepRegion = KeepRegion | NoRegion deriving (Show, Eq)
+
+-- | Keep or remove response field. See 'Resp'.
+data KeepResponse = KeepResponse | NoResponse deriving (Show, Eq)
+
+-- | Keep or remove burst size field. See 'BurstSize'.
+data KeepSize = KeepSize | NoSize deriving (Show, Eq)
+
+-- | Keep or remove strobe field. See 'Strobe'
+data KeepStrobe = KeepStrobe | NoStrobe deriving (Show, Eq)
+
+-- | Type used to introduce strobe information on the term level
+data SKeepStrobe (strobeType :: KeepStrobe) where
+  SKeepStrobe :: SKeepStrobe 'KeepStrobe
+  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
+
+-- | Enables or disables 'BurstMode'
+type family BurstType (keepBurst :: KeepBurst) where
+  BurstType 'KeepBurst = BurstMode
+  BurstType 'NoBurst = ()
+
+-- | Enables or disables burst length
+type family BurstLengthType (keepBurstLength :: KeepBurstLength) where
+  BurstLengthType 'KeepBurstLength = C.Index (2^8)
+  BurstLengthType 'NoBurstLength = ()
+
+-- | Enables or disables 'Cache'
+type family CacheType (keepCache :: KeepCache) where
+  CacheType 'KeepCache = Cache
+  CacheType 'NoCache = ()
+
+-- | Enables or disables a boolean indicating whether a transaction is done
+type family LastType (keepLast :: KeepLast) where
+  LastType 'KeepLast = Bool
+  LastType 'NoLast = ()
+
+-- | Enables or disables 'AtomicAccess'
+type family LockType (keepLockType :: KeepLock) where
+  LockType 'KeepLock = AtomicAccess
+  LockType 'NoLock = ()
+
+-- | Enables or disables 'Privileged', 'Secure', and 'InstructionOrData'
+type family PermissionsType (keepPermissions :: KeepPermissions) where
+  PermissionsType 'KeepPermissions = (Privileged, Secure, InstructionOrData)
+  PermissionsType 'NoPermissions = ()
+
+-- | Enables or disables 'Qos'
+type family QosType (keepQos :: KeepQos) where
+  QosType 'KeepQos = Qos
+  QosType 'NoQos = ()
+
+-- | Enables or disables region type
+type family RegionType (keepRegion :: KeepRegion) where
+  RegionType 'KeepRegion = C.BitVector 4
+  RegionType 'NoRegion = ()
+
+-- | Enables or disables 'Resp'
+type family ResponseType (keepResponse :: KeepResponse) where
+  ResponseType 'KeepResponse = Resp
+  ResponseType 'NoResponse = ()
+
+-- | Enables or disables 'BurstSize'
+type family SizeType (keepSize :: KeepSize) where
+  SizeType 'KeepSize = BurstSize
+  SizeType 'NoSize = ()
+
+-- | Enable or disable 'Strobe'
+type family StrobeType (byteSize :: Nat) (keepStrobe :: KeepStrobe) where
+  StrobeType byteSize 'KeepStrobe = Strobe byteSize
+  StrobeType byteSize 'NoStrobe = ()
+
+-- | Enable or disable 'Strobe'
+type family StrictStrobeType (byteSize :: Nat) (keepStrobe :: KeepStrobe) where
+  StrictStrobeType byteSize 'KeepStrobe = C.Vec byteSize (Maybe (C.BitVector 8))
+  StrictStrobeType byteSize 'NoStrobe = C.BitVector (byteSize * 8)
+
+-- | Indicates valid bytes on data field.
+type Strobe (byteSize :: Nat) = C.BitVector byteSize
+
+-- | The protocol does not specify the exact use of the QoS identifier. This
+-- specification recommends that AxQOS is used as a priority indicator for the
+-- associated write or read transaction. A higher value indicates a higher
+-- priority transaction.
+--
+-- A default value of 0 indicates that the interface is not participating in any
+-- QoS scheme.
+type Qos = C.Index ((2^4) - 1)
+
+-- | The burst type and the size information, determine how the address for
+-- each transfer within the burst is calculated.
+data BurstMode
+  -- | In a fixed burst, the address is the same for every transfer in the
+  -- burst. This burst type is used for repeated accesses to the same location
+  -- such as when loading or emptying a FIFO
+  = BmFixed
+  -- | Incrementing. In an incrementing burst, the address for each transfer in
+  -- the burst is an increment of the address for the previous transfer. The
+  -- increment value depends on the size of the transfer. For example, the
+  -- address for each transfer in a burst with a size of four bytes is the
+  -- previous address plus four. This burst type is used for accesses to normal
+  -- sequential memory.
+  | BmIncr
+  -- | A wrapping burst is similar to an incrementing burst, except that the
+  -- address wraps around to a lower address if an upper address limit is
+  -- reached. The following restrictions apply to wrapping bursts:
+  --
+  --   * the start address must be aligned to the size of each transfer
+  --   * the length of the burst must be 2, 4, 8, or 16 transfers.
+  --
+  -- The behavior of a wrapping burst is:
+  --
+  --   * The lowest address used by the burst is aligned to the total size of
+  --     the data to be transferred, that is, to ((size of each transfer in the
+  --     burst) × (number of transfers in the burst)). This address is defined
+  --     as the _wrap boundary_.
+  --
+  --   * After each transfer, the address increments in the same way as for an
+  --     INCR burst. However, if this incremented address is ((wrap boundary) +
+  --     (total size of data to be transferred)) then the address wraps round to
+  --     the wrap boundary.
+  --
+  --   * The first transfer in the burst can use an address that is higher than
+  --     the wrap boundary, subject to the restrictions that apply to wrapping
+  --     bursts. This means that the address wraps for any WRAP burst for which
+  --     the first address is higher than the wrap boundary.
+  --
+  -- This burst type is used for cache line accesses.
+  --
+  | BmWrap
+  deriving (Show, C.ShowX, Generic, C.NFDataX, Eq)
+
+-- | The maximum number of bytes to transfer in each data transfer, or beat,
+-- in a burst.
+data BurstSize
+  = Bs1
+  | Bs2
+  | Bs4
+  | Bs8
+  | Bs16
+  | Bs32
+  | Bs64
+  | Bs128
+  deriving (Show, C.ShowX, Generic, C.NFDataX)
+
+-- | Convert burst size to a numeric value
+burstSizeToNum :: Num a => BurstSize -> a
+burstSizeToNum = \case
+  Bs1 -> 1
+  Bs2 -> 2
+  Bs4 -> 4
+  Bs8 -> 8
+  Bs16 -> 16
+  Bs32 -> 32
+  Bs64 -> 64
+  Bs128 -> 128
+
+-- | Whether a transaction is bufferable
+data Bufferable = NonBufferable | Bufferable
+
+-- | When set to "LookupCache", it is recommended that this transaction is
+-- allocated in the cache for performance reasons.
+data Allocate = NoLookupCache | LookupCache
+
+-- | When set to "OtherLookupCache", it is recommended that this transaction is
+-- allocated in the cache for performance reasons.
+data OtherAllocate = OtherNoLookupCache | OtherLookupCache
+
+-- | See Table A4-3 AWCACHE bit allocations
+type Cache = T4 Bufferable Modifiable OtherAllocate Allocate
+
+-- | Status of the write transaction.
+data Resp
+  -- | Normal access success. Indicates that a normal access has been
+  -- successful. Can also indicate an exclusive access has failed.
+  = ROkay
+  -- | Exclusive access okay. Indicates that either the read or write portion
+  -- of an exclusive access has been successful.
+  | RExclusiveOkay
+  -- | Slave error. Used when the access has reached the slave successfully, but
+  -- the slave wishes to return an error condition to the originating master.
+  | RSlaveError
+  -- | Decode error. Generated, typically by an interconnect component, to
+  -- indicate that there is no slave at the transaction address.
+  | 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
+  | ExclusiveAccess
+
+-- | Whether transaction can be modified
+data Modifiable
+  = Modifiable
+  | NonModifiable
+
+-- | An AXI master might support Secure and Non-secure operating states, and
+-- extend this concept of security to memory access.
+data Secure
+  = Secure
+  | NonSecure
+  deriving (Show, Generic, C.NFDataX)
+
+-- | 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)
+
+-- | 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,
+-- for example, where a transaction contains a mix of instruction and data
+-- items. This specification recommends that a master sets it to "Data", to
+-- indicate a data access unless the access is specifically known to be an
+-- instruction access.
+data InstructionOrData
+  = Data
+  | Instruction
+  deriving (Show, Generic, C.NFDataX)
diff --git a/src/Protocols/Axi4/Lite/Axi4Lite.hs b/src/Protocols/Axi4/Lite/Axi4Lite.hs
new file mode 100644
index 00000000..3af4e99e
--- /dev/null
+++ b/src/Protocols/Axi4/Lite/Axi4Lite.hs
@@ -0,0 +1,226 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-|
+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
+
+
+-- | AXI4 Lite busses are always either 32 bit or 64 bit.
+data BusWidth = Width32 | Width64 deriving (Show, Eq)
+
+-- | 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, NFDataX)
+
+deriving instance (C.KnownNat (Width aw))
+  => Show (M2S_WriteAddress aw)
+
+-- | Ready signal for the write address channel.
+data S2M_WriteAddress
+  = S2M_WriteAddress {
+    _awready :: Bool
+  } deriving (Show, Generic, NFDataX)
+
+-- | Protocol type for the write address channel.
+data Axi4LiteWA
+  (dom :: C.Domain)
+  (aw :: AddrWidth)
+
+-- | Protocol instance for the write address channel.
+instance Protocol (Axi4LiteWA dom aw) where
+  type Fwd (Axi4LiteWA dom aw) = C.Signal dom (M2S_WriteAddress aw)
+  type Bwd (Axi4LiteWA dom aw) = C.Signal dom (S2M_WriteAddress)
+
+------------------------
+--- 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)
+
+-- | Protocol type for the write data channel
+data Axi4LiteWD
+  (dom :: C.Domain)
+  (bw :: BusWidth)
+
+-- | Protocol instance for the write data channel.
+instance Protocol (Axi4LiteWD dom bw) where
+  type Fwd (Axi4LiteWD dom bw) = C.Signal dom (M2S_WriteData bw)
+  type Bwd (Axi4LiteWD dom bw) = C.Signal dom (S2M_WriteData)
+
+----------------------------
+--- 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)
+
+-- | Protocol type for the write response channel.
+data Axi4LiteWR
+  (dom :: C.Domain)
+
+-- | Protocol instance for the write response channel.
+instance Protocol (Axi4LiteWR dom) where
+  type Fwd (Axi4LiteWR dom) = C.Signal dom (M2S_WriteResponse)
+  type Bwd (Axi4LiteWR dom) = C.Signal dom (S2M_WriteResponse)
+
+--------------------------
+--- 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, NFDataX)
+
+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)
+
+-- | Protocol type for the read address channel.
+data Axi4LiteRA
+  (dom :: C.Domain)
+  (aw :: AddrWidth)
+
+-- | Protocol instance for the read address channel.
+instance Protocol (Axi4LiteRA dom aw) where
+  type Fwd (Axi4LiteRA dom aw) = C.Signal dom (M2S_ReadAddress aw)
+  type Bwd (Axi4LiteRA dom aw) = C.Signal dom (S2M_ReadAddress)
+
+-----------------------
+--- Read data types ---
+-----------------------
+
+-- | Acknowledges data from the slave component. This data type needs the 'bw' type
+-- 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 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
+  (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)
+
+-- | Protocol type for the read data channel.
+data Axi4LiteRD
+  (dom :: C.Domain)
+  (bw :: BusWidth)
+
+-- | Protocol instance for the read data channel. Notice that in this protocol
+-- data flows over the backward channel, but due to type injectivity the forward
+-- channel needs to contain the 'bw' type as well.
+instance Protocol (Axi4LiteRD dom bw) where
+  type Fwd (Axi4LiteRD dom bw) = C.Signal dom (M2S_ReadData bw)
+  type Bwd (Axi4LiteRD dom bw) = C.Signal dom (S2M_ReadData bw)
+
+
+-- | Protocols for writing to an AXI4 Lite component.
+type Axi4LiteWrite
+  (dom :: C.Domain)
+  (aw :: AddrWidth)
+  (bw :: BusWidth)
+  = (Axi4LiteWA dom aw, Axi4LiteWD dom bw, Axi4LiteWR dom)
+
+-- | Protocols for reading from an AXI4 Lite component.
+type Axi4LiteRead
+  (dom :: C.Domain)
+  (aw :: AddrWidth)
+  (bw :: BusWidth)
+  = (Axi4LiteRA dom aw, Axi4LiteRD dom bw)
+
+-- | Full AXI4 Lite protocol with both read and write channel sets.
+type Axi4Lite
+  (dom :: C.Domain)
+  (aw :: AddrWidth)
+  (bw :: BusWidth)
+  = (Axi4LiteWrite dom aw bw, Axi4LiteRead dom aw bw)