Add idWithModelDf test for Axi4 Write Address channel

Author: hiddemoll

clash-protocols/tests/Tests/Protocols/Axi4.hs

@@ -23,6 +23,7 @@ import Test.Tasty.TH (testGroupGenerator)
 
 -- clash-protocols (me!)
 import Protocols
+import Protocols.Axi4.Common
 import Protocols.Axi4.ReadAddress
 import Protocols.Axi4.ReadData
 import Protocols.Axi4.Stream
@@ -31,6 +32,7 @@ import Protocols.Axi4.WriteData
 import Protocols.Axi4.WriteResponse
 import Protocols.DfConv qualified as DfConv
 import Protocols.Hedgehog
+import Protocols.Internal
 
 -- tests
 import Tests.Protocols.Df qualified as DfTest
@@ -48,6 +50,71 @@ type ConfAR =
   'Axi4ReadAddressConfig 'True 'True 2 2 'True 'True 'True 'True 'True 'True
 type ConfR = 'Axi4ReadDataConfig 'True 2
 
+prop_axi4_convert_write_address_id :: Property
+prop_axi4_convert_write_address_id =
+  DfTest.idWithModelDf
+    defExpectOptions
+    (DfTest.genData genInfo)
+    id
+    ( C.withClockResetEnable @C.System C.clockGen C.resetGen C.enableGen $
+        DfConv.dfConvTestBench
+          Proxy
+          Proxy
+          (repeat True)
+          (repeat Nothing)
+          ckt
+    )
+ where
+  ckt ::
+    (C.HiddenClockResetEnable dom) =>
+    Circuit
+      (Axi4WriteAddress dom ConfAW Int)
+      (Axi4WriteAddress dom ConfAW Int)
+  ckt = DfConv.convert Proxy Proxy
+
+  genInfo =
+    (,,)
+      <$> genWriteAddrInfo
+      <*> genBurstLen
+      <*> genBurst
+  genWriteAddrInfo =
+    Axi4WriteAddressInfo
+      <$> Gen.enumBounded
+      <*> Gen.enumBounded
+      <*> (toKeepType <$> Gen.enumBounded)
+      <*> ( toKeepType
+              <$> ( pure Bs1
+                      C.<|> pure Bs2
+                      C.<|> pure Bs4
+                      C.<|> pure Bs8
+                      C.<|> pure Bs16
+                      C.<|> pure Bs32
+                      C.<|> pure Bs64
+                      C.<|> pure Bs128
+                  )
+          )
+      <*> (toKeepType <$> (pure NonExclusiveAccess C.<|> pure ExclusiveAccess))
+      <*> ( toKeepType
+              <$> ( (,,,)
+                      <$> (pure NonBufferable C.<|> pure Bufferable)
+                      <*> (pure NonModifiable C.<|> pure Modifiable)
+                      <*> (pure OtherNoLookupCache C.<|> pure OtherLookupCache)
+                      <*> (pure NoLookupCache C.<|> pure LookupCache)
+                  )
+          )
+      <*> ( toKeepType
+              <$> ( (,,)
+                      <$> (pure Privileged C.<|> pure NotPrivileged)
+                      <*> (pure Secure C.<|> pure NonSecure)
+                      <*> (pure Instruction C.<|> pure Data)
+                  )
+          )
+      <*> (toKeepType <$> Gen.enumBounded)
+      <*> DfTest.genSmallInt
+
+  genBurstLen = pure (toKeepType 0)
+  genBurst = toKeepType <$> (pure BmFixed C.<|> pure BmIncr C.<|> pure BmWrap)
+
 -- also test out the DfConv instance for Axi4Stream
 
 prop_axi4_stream_fifo_id :: Property