From a73282a1b904b3a0704e1b0193e3b30ae124d271 Mon Sep 17 00:00:00 2001 From: t-wallet Date: Mon, 2 Sep 2024 17:48:42 +0200 Subject: [PATCH] Signicantly overhaul the Ethernet tests Mostly includes improvements in packet generation, and reuse of models and generators. Aside from that, most test files have also been formatted with fourmolu. --- clash-cores.cabal | 1 + nix/sources.json | 6 +- src/Clash/Cores/Ethernet/Arp/ArpManager.hs | 9 +- src/Clash/Cores/Ethernet/Arp/ArpTypes.hs | 40 ++ .../Cores/Ethernet/Examples/FullUdpStack.hs | 2 +- test/Test/Cores/Ethernet.hs | 8 +- test/Test/Cores/Ethernet/Arp/ArpManager.hs | 424 ++++++++---------- test/Test/Cores/Ethernet/Base.hs | 56 +++ test/Test/Cores/Ethernet/IP/EthernetStream.hs | 171 ++++--- test/Test/Cores/Ethernet/IP/IPPacketizers.hs | 275 +++++------- .../Cores/Ethernet/IP/InternetChecksum.hs | 30 ++ test/Test/Cores/Ethernet/Icmp.hs | 230 ++++------ .../Cores/Ethernet/Mac/FrameCheckSequence.hs | 294 ++++++------ .../Ethernet/Mac/InterpacketGapInserter.hs | 88 ++-- .../Cores/Ethernet/Mac/PaddingInserter.hs | 132 +++--- 15 files changed, 847 insertions(+), 919 deletions(-) create mode 100644 test/Test/Cores/Ethernet/Base.hs diff --git a/clash-cores.cabal b/clash-cores.cabal index 7449449..a100fd1 100644 --- a/clash-cores.cabal +++ b/clash-cores.cabal @@ -224,6 +224,7 @@ test-suite unittests Test.Cores.Crc Test.Cores.Ethernet Test.Cores.Ethernet.Arp.ArpManager + Test.Cores.Ethernet.Base Test.Cores.Ethernet.Icmp Test.Cores.Ethernet.IP.EthernetStream Test.Cores.Ethernet.IP.InternetChecksum diff --git a/nix/sources.json b/nix/sources.json index 37f2cb6..64e6874 100644 --- a/nix/sources.json +++ b/nix/sources.json @@ -18,10 +18,10 @@ "homepage": null, "owner": "clash-lang", "repo": "clash-protocols", - "rev": "3c88c305668b08671e7ea7fbc1f88633388d85d2", - "sha256": "167is7j8x55sqdwwln1ysv4m2b94lh46ks9v699rrqb2li6ybhj4", + "rev": "a38eadc74b33cc1e15cf5f56c1b4c7c92c2e61a4", + "sha256": "0b219y7nxaxcr3xrk6dq5qj5hl9ggaxqpysk8rwmjh9nmkvzxifa", "type": "tarball", - "url": "https://github.com/clash-lang/clash-protocols/archive/3c88c305668b08671e7ea7fbc1f88633388d85d2.tar.gz", + "url": "https://github.com/clash-lang/clash-protocols/archive/a38eadc74b33cc1e15cf5f56c1b4c7c92c2e61a4.tar.gz", "url_template": "https://github.com///archive/.tar.gz" }, "doctest-parallel": { diff --git a/src/Clash/Cores/Ethernet/Arp/ArpManager.hs b/src/Clash/Cores/Ethernet/Arp/ArpManager.hs index a7ea627..f0af8e1 100644 --- a/src/Clash/Cores/Ethernet/Arp/ArpManager.hs +++ b/src/Clash/Cores/Ethernet/Arp/ArpManager.hs @@ -168,19 +168,12 @@ arpReceiverC myIP = circuit $ \ethStream -> do -- before `depacketizetoDfC` should work, as depacketizeToDfC already -- implements dropping of arpDf <- depacketizeToDfC const -< ethStream - arpDf' <- Df.filterS (validArp <$> myIP) -< arpDf + arpDf' <- Df.filterS (isValidArp <$> myIP) -< arpDf (arpRequests, arpEntries) <- partitionS (isRequest <$> myIP) -< arpDf' lites <- Df.map (\p -> ArpLite (_sha p) (_spa p) False) -< arpRequests entries <- Df.map (\p -> ArpEntry (_sha p) (_spa p)) -< arpEntries idC -< (entries, lites) where - validArp ip ArpPacket{..} = - _htype == 1 - && _ptype == 0x0800 - && _hlen == 6 - && _plen == 4 - &&(_oper == 1 && (_tpa == ip || _tpa == _spa) || _oper == 2) - isRequest ip ArpPacket{..} = _oper == 1 && _tpa == ip -- TODO upstream to clash-protocols diff --git a/src/Clash/Cores/Ethernet/Arp/ArpTypes.hs b/src/Clash/Cores/Ethernet/Arp/ArpTypes.hs index 09f5c49..e6514c5 100644 --- a/src/Clash/Cores/Ethernet/Arp/ArpTypes.hs +++ b/src/Clash/Cores/Ethernet/Arp/ArpTypes.hs @@ -1,3 +1,5 @@ +{-# LANGUAGE RecordWildCards #-} + {-| Module : Clash.Cores.Ethernet.Arp.ArpTypes Description : Provides various data types, aliases, constructors and constants for the Address Resolution Protocol. This module only provides the most common use case of ARP, which is mapping IPv4 addresses to MAC addresses. @@ -95,3 +97,41 @@ newArpPacket myMac myIP targetMac targetIP isRequest _tha = targetMac, _tpa = targetIP } + + +-- | Construct a link-layer `EthernetHeader` from an ARP packet. +arpToEthernetHeader :: ArpPacket -> EthernetHeader +arpToEthernetHeader ArpPacket{..} = + EthernetHeader + { _macDst = _tha + , _macSrc = _sha + , _etherType = arpEtherType + } + +-- | Construct a link-layer `EthernetHeader` from a reduced ARP packet. +arpLiteToEthernetHeader :: + -- | Our MAC address + MacAddress -> + ArpLite -> + EthernetHeader +arpLiteToEthernetHeader ourMac ArpLite{..} = + EthernetHeader + { _macDst = _targetMac + , _macSrc = ourMac + , _etherType = arpEtherType + } + +-- | Whether we should accept an incoming ARP packet or not. +isValidArp :: + -- | Our IPv4 address + IPv4Address -> + -- | Incoming ARP packet + ArpPacket -> + Bool +isValidArp ourIPv4 ArpPacket{..} = + _htype == 1 && + _ptype == 0x0800 && + _hlen == 6 && + _plen == 4 && + -- If TPA == SPA, the ARP packet is gratuitous. + (_oper == 1 && (_tpa == ourIPv4 || _tpa == _spa) || _oper == 2) diff --git a/src/Clash/Cores/Ethernet/Examples/FullUdpStack.hs b/src/Clash/Cores/Ethernet/Examples/FullUdpStack.hs index eb6b316..a85cfe8 100644 --- a/src/Clash/Cores/Ethernet/Examples/FullUdpStack.hs +++ b/src/Clash/Cores/Ethernet/Examples/FullUdpStack.hs @@ -307,7 +307,7 @@ arpIcmpUdpStackC macAddressS ipS udpCkt = circuit $ \ethIn -> do where icmpUdpStack = circuit $ \ipIn -> do [icmpIn, udpIn] <- packetDispatcherC (routeBy _ipv4lProtocol $ 0x0001 :> 0x0011 :> Nil) -< ipIn - icmpOut <- icmpEchoResponderC @dom @dataWidth (fst <$> ipS) -< icmpIn + icmpOut <- icmpEchoResponderC (fst <$> ipS) -< icmpIn udpInParsed <- udpDepacketizerC -< udpIn udpOutParsed <- udpPacketizerC (fst <$> ipS) <| udpCkt -< udpInParsed packetArbiterC RoundRobin -< [icmpOut, udpOutParsed] diff --git a/test/Test/Cores/Ethernet.hs b/test/Test/Cores/Ethernet.hs index d24ebef..f51bbe9 100644 --- a/test/Test/Cores/Ethernet.hs +++ b/test/Test/Cores/Ethernet.hs @@ -4,10 +4,10 @@ module Test.Cores.Ethernet ( import Test.Tasty import qualified Test.Cores.Ethernet.Arp.ArpManager ---import qualified Test.Cores.Ethernet.Icmp +import qualified Test.Cores.Ethernet.Icmp import qualified Test.Cores.Ethernet.IP.EthernetStream import qualified Test.Cores.Ethernet.IP.InternetChecksum ---import qualified Test.Cores.Ethernet.IP.IPPacketizers +import qualified Test.Cores.Ethernet.IP.IPPacketizers import qualified Test.Cores.Ethernet.Mac.FrameCheckSequence import qualified Test.Cores.Ethernet.Mac.InterpacketGapInserter import qualified Test.Cores.Ethernet.Mac.PaddingInserter @@ -17,10 +17,10 @@ tests = testGroup "Ethernet" [ Test.Cores.Ethernet.Arp.ArpManager.tests - --, Test.Cores.Ethernet.Icmp.tests + , Test.Cores.Ethernet.Icmp.tests , Test.Cores.Ethernet.IP.EthernetStream.tests , Test.Cores.Ethernet.IP.InternetChecksum.tests - --, Test.Cores.Ethernet.IP.IPPacketizers.tests + , Test.Cores.Ethernet.IP.IPPacketizers.tests , Test.Cores.Ethernet.Mac.FrameCheckSequence.tests , Test.Cores.Ethernet.Mac.InterpacketGapInserter.tests , Test.Cores.Ethernet.Mac.PaddingInserter.tests diff --git a/test/Test/Cores/Ethernet/Arp/ArpManager.hs b/test/Test/Cores/Ethernet/Arp/ArpManager.hs index 95504ef..e9cf5b4 100644 --- a/test/Test/Cores/Ethernet/Arp/ArpManager.hs +++ b/test/Test/Cores/Ethernet/Arp/ArpManager.hs @@ -1,4 +1,3 @@ -{-# language FlexibleContexts #-} {-# language NumericUnderscores #-} {-# language RecordWildCards #-} {-# LANGUAGE TupleSections #-} @@ -6,283 +5,246 @@ module Test.Cores.Ethernet.Arp.ArpManager where --- base -import qualified Data.List as L -import Prelude +import Clash.Cores.Ethernet.Arp.ArpManager +import Clash.Cores.Ethernet.Arp.ArpTypes +import Clash.Cores.Ethernet.IP.IPv4Types +import Clash.Cores.Ethernet.Mac.EthernetTypes + +import Clash.Prelude --- clash-prelude -import Clash.Prelude hiding ( repeat ) -import Clash.Prelude as C +import qualified Data.List as L --- hedgehog import Hedgehog import qualified Hedgehog.Gen as Gen import qualified Hedgehog.Range as Range --- tasty -import Test.Tasty -import Test.Tasty.Hedgehog ( HedgehogTestLimit(HedgehogTestLimit) ) -import Test.Tasty.Hedgehog.Extra ( testProperty ) -import Test.Tasty.TH ( testGroupGenerator ) - --- clash-protocols import Protocols import qualified Protocols.Df as Df -import Protocols.PacketStream import Protocols.Hedgehog - --- ethernet -import Clash.Cores.Ethernet.Arp.ArpManager -import Clash.Cores.Ethernet.Arp.ArpTypes -import Clash.Cores.Ethernet.IP.IPv4Types -import Clash.Cores.Ethernet.Mac.EthernetTypes - --- tests +import Protocols.PacketStream import Protocols.PacketStream.Hedgehog -import Clash.Hedgehog.Sized.Vector (genVec) +import Test.Cores.Ethernet.Base (genEthernetHeader, genIPv4Addr, genMacAddr) -createDomain vSystem - { vName="TestDom10Hz" - , vPeriod=100_000_000_000 - , vActiveEdge=Rising - , vResetKind=Asynchronous - , vInitBehavior=Unknown - , vResetPolarity=ActiveHigh - } +import Test.Tasty +import Test.Tasty.Hedgehog (HedgehogTestLimit (HedgehogTestLimit)) +import Test.Tasty.Hedgehog.Extra (testProperty) +import Test.Tasty.TH (testGroupGenerator) + +createDomain + vSystem + { vName = "TestDom10Hz" + , vPeriod = 100_000_000_000 + , vActiveEdge = Rising + , vResetKind = Asynchronous + , vInitBehavior = Unknown + , vResetPolarity = ActiveHigh + } ip1, ip2 :: IPv4Address -ip1 = IPv4Address $ 0xDE :> 0xAD :> 0xBE :> 0xEF :> Nil -ip2 = IPv4Address $ 0xDE :> 0xAD :> 0xBE :> 0xEE :> Nil +ip1 = IPv4Address (0xDE :> 0xAD :> 0xBE :> 0xEF :> Nil) +ip2 = IPv4Address (0xDE :> 0xAD :> 0xBE :> 0xEE :> Nil) -mac1, mac2 :: MacAddress -mac1 = MacAddress (C.repeat 0x01) -mac2 = MacAddress (C.repeat 0x02) - --- | Test proper outgoing requests, relaying and timeouts of the ARP manager. --- Manual test, because circuits containing ArpLookup cannot be automatically tested. -prop_arp_manager :: Property -prop_arp_manager = property $ - do L.zip expectedBwdOut expectedFwdOut === sampleN 32 (bundle (bwdOut, bundle fwdOut)) - where - fwdIn :: [Maybe IPv4Address] - fwdIn = [ Nothing - , Nothing - , Just ip1 - , Just ip1 - , Nothing - , Just ip1 - , Just ip1 - , Just ip1 - , Just ip1 - ] L.++ L.repeat (Just ip2) - - bwdIn :: [(Maybe ArpResponse, Ack)] - bwdIn = L.map (, Ack True) $ - [ Nothing - , Nothing - , Nothing - , Just (ArpEntryFound mac1) - , Nothing - , Nothing - , Just ArpEntryNotFound - , Nothing - , Just (ArpEntryFound mac1) - , Nothing - , Just ArpEntryNotFound] - L.++ L.replicate 20 Nothing - L.++ [Just ArpEntryNotFound] - - bwdOut :: Signal TestDom10Hz (Maybe ArpResponse) - fwdOut :: (Signal TestDom10Hz (Maybe IPv4Address), Signal TestDom10Hz (Df.Data ArpLite)) - (bwdOut, fwdOut) = toSignals ckt inp - where - -- We wait 1-2 seconds for ARP replies - ckt = exposeClockResetEnable (arpManagerC @TestDom10Hz d2) clockGen resetGen enableGen - inp = (unbundle $ fromList fwdIn, unbundle $ fromList bwdIn) - - expectedBwdOut :: [Maybe ArpResponse] - expectedBwdOut - = [ Nothing - , Nothing - , Nothing - , Just (ArpEntryFound mac1) -- Relaying to client circuit from ARP table - , Nothing - , Nothing - , Nothing - , Nothing - , Just (ArpEntryFound mac1)] -- Relaying to client circuit from ARP reply - L.++ L.replicate 22 Nothing - L.++ - [Just ArpEntryNotFound] -- We were waiting for an ARP reply, but we timed out. - - expectedFwdOut :: [(Maybe IPv4Address, Df.Data ArpLite)] - expectedFwdOut - = [ (Nothing, Df.NoData) - , (Nothing, Df.NoData) - , (Just ip1, Df.NoData) -- Relay IP lookup to ARP table - , (Just ip1, Df.NoData) - , (Nothing, Df.NoData) - , (Just ip1, Df.NoData) - , (Just ip1, Df.Data (ArpLite broadcastMac ip1 True)) -- We received ArpEntryNotFound from the ARP table, so send request - , (Just ip1, Df.NoData) - , (Just ip1, Df.NoData) -- Received ArpEntryFound - , (Just ip2, Df.NoData) - , (Just ip2, Df.Data (ArpLite broadcastMac ip2 True))] -- We received ArpEntryNotFound from the ARP table, so send request - L.++ L.replicate 21 (Just ip2, Df.NoData) -- We were waiting for an ARP reply, but we timed out. +mac1 :: MacAddress +mac1 = MacAddress (repeat 0x01) ourMac :: MacAddress -ourMac = MacAddress (0xDE C.:> 0xAD C.:> 0xBE C.:> 0xEF C.:> 0x01 C.:> 0x02 C.:> C.Nil) +ourMac = MacAddress (0xDE :> 0xAD :> 0xBE :> 0xEF :> 0x01 :> 0x02 :> Nil) -ourIP :: IPv4Address -ourIP = IPv4Address (0x33 C.:> 0x44 C.:> 0x55 C.:> 0x66 C.:> C.Nil) +ourIPv4 :: IPv4Address +ourIPv4 = IPv4Address (0x33 :> 0x44 :> 0x55 :> 0x66 :> Nil) genArpLite :: Gen ArpLite -genArpLite = ArpLite <$> - (MacAddress <$> genVec Gen.enumBounded) <*> - (IPv4Address <$> genVec Gen.enumBounded) <*> - Gen.enumBounded - -arpTransmitterPropertyGenerator - :: forall (dataWidth :: C.Nat) - . 1 C.<= dataWidth - => C.SNat dataWidth - -> Property -arpTransmitterPropertyGenerator C.SNat = +genArpLite = + ArpLite + <$> genMacAddr + <*> genIPv4Addr + <*> Gen.enumBounded + +{- | Test proper outgoing requests, relaying and timeouts of the ARP manager. + Manual test, because circuits containing ArpLookup cannot be automatically tested. +-} +prop_arp_manager :: Property +prop_arp_manager = property $ + do L.zip expectedBwdOut expectedFwdOut === sampleN 32 (bundle (bwdOut, bundle fwdOut)) + where + fwdIn :: [Maybe IPv4Address] + fwdIn = + [ Nothing + , Nothing + , Just ip1 + , Just ip1 + , Nothing + , Just ip1 + , Just ip1 + , Just ip1 + , Just ip1 + ] + L.++ L.repeat (Just ip2) + + bwdIn :: [(Maybe ArpResponse, Ack)] + bwdIn = + L.map (,Ack True) $ + [ Nothing + , Nothing + , Nothing + , Just (ArpEntryFound mac1) + , Nothing + , Nothing + , Just ArpEntryNotFound + , Nothing + , Just (ArpEntryFound mac1) + , Nothing + , Just ArpEntryNotFound + ] + L.++ L.replicate 20 Nothing + L.++ [Just ArpEntryNotFound] + + bwdOut :: Signal TestDom10Hz (Maybe ArpResponse) + fwdOut :: (Signal TestDom10Hz (Maybe IPv4Address), Signal TestDom10Hz (Df.Data ArpLite)) + (bwdOut, fwdOut) = toSignals ckt inp + where + -- We wait 1-2 seconds for ARP replies + ckt = exposeClockResetEnable (arpManagerC @TestDom10Hz d2) clockGen resetGen enableGen + inp = (unbundle $ fromList fwdIn, unbundle $ fromList bwdIn) + + expectedBwdOut :: [Maybe ArpResponse] + expectedBwdOut = + [ Nothing + , Nothing + , Nothing + , Just (ArpEntryFound mac1) -- Relaying to client circuit from ARP table + , Nothing + , Nothing + , Nothing + , Nothing + , Just (ArpEntryFound mac1) -- Relaying to client circuit from ARP reply + ] + L.++ L.replicate 22 Nothing + L.++ [Just ArpEntryNotFound] -- We were waiting for an ARP reply, but we timed out. + expectedFwdOut :: [(Maybe IPv4Address, Df.Data ArpLite)] + expectedFwdOut = + [ (Nothing, Df.NoData) + , (Nothing, Df.NoData) + , (Just ip1, Df.NoData) -- Relay IP lookup to ARP table + , (Just ip1, Df.NoData) + , (Nothing, Df.NoData) + , (Just ip1, Df.NoData) + , (Just ip1, Df.Data (ArpLite broadcastMac ip1 True)) -- We received ArpEntryNotFound from the ARP table, so send request + , (Just ip1, Df.NoData) + , (Just ip1, Df.NoData) -- Received ArpEntryFound + , (Just ip2, Df.NoData) + , (Just ip2, Df.Data (ArpLite broadcastMac ip2 True)) -- We received ArpEntryNotFound from the ARP table, so send request + ] + L.++ L.replicate 21 (Just ip2, Df.NoData) -- We were waiting for an ARP reply, but we timed out. + +arpTransmitterPropertyGenerator :: + forall (dataWidth :: Nat). + (1 <= dataWidth) => + SNat dataWidth -> + Property +arpTransmitterPropertyGenerator SNat = propWithModelSingleDomain - @C.System - defExpectOptions{eoSampleMax = 2000} + @System + defExpectOptions{eoSampleMax = 1000} (Gen.list (Range.linear 1 10) genArpLite) - (C.exposeClockResetEnable model) - (C.exposeClockResetEnable @C.System (arpTransmitterC (pure ourMac) (pure ourIP))) + (exposeClockResetEnable model) + (exposeClockResetEnable @System (arpTransmitterC (pure ourMac) (pure ourIPv4))) (===) - where - model :: [ArpLite] -> [PacketStreamM2S dataWidth EthernetHeader] - model = packetizeFromDfModel toEthernetHdr toArpPkt - - toEthernetHdr arpLite = EthernetHeader { - _macDst = _targetMac arpLite, - _macSrc = ourMac, - _etherType = arpEtherType - } - - toArpPkt arpLite = newArpPacket ourMac ourIP (_targetMac arpLite) (_targetIPv4 arpLite) (_isRequest arpLite) + where + model :: [ArpLite] -> [PacketStreamM2S dataWidth EthernetHeader] + model = packetizeFromDfModel (arpLiteToEthernetHeader ourMac) toArpPkt + + toArpPkt arpLite = + newArpPacket + ourMac + ourIPv4 + (_targetMac arpLite) + (_targetIPv4 arpLite) + (_isRequest arpLite) + +arpReceiverPropertyGenerator :: + forall (dataWidth :: Nat). + (1 <= dataWidth) => + SNat dataWidth -> + Property +arpReceiverPropertyGenerator SNat = + idWithModelSingleDomain + @System + defExpectOptions{eoStopAfterEmpty = 1000} + (genPackets (Range.linear 1 5) Abort genPkt) + (exposeClockResetEnable model) + (exposeClockResetEnable @System (arpReceiverC $ pure ourIPv4)) + where + genArpPacket isGratuitous = do + spa <- genIPv4Addr + newArpPacket + <$> genMacAddr + <*> Gen.constant spa + <*> Gen.constant ourMac + <*> Gen.constant (if isGratuitous then spa else ourIPv4) + <*> Gen.bool + + genPkt am = + Gen.choice + [ -- Random packet + genValidPacket genEthernetHeader (Range.linear 0 20) am + , -- Valid ARP reply/request + do + arpPkt <- genArpPacket False + pure (packetizeFromDfModel arpToEthernetHeader id [arpPkt]) + , -- Valid gratuitous ARP reply/request + do + arpPkt <- genArpPacket True + pure (packetizeFromDfModel arpToEthernetHeader id [arpPkt]) + ] + + model :: [PacketStreamM2S dataWidth EthernetHeader] -> ([ArpEntry], [ArpLite]) + model ethStr = (entries, lites) + where + arpDf = L.filter (isValidArp ourIPv4) (depacketizeToDfModel const ethStr) + (arpRequests, arpEntries) = L.partition (isRequest ourIPv4) arpDf + + isRequest ip ArpPacket{..} = _oper == 1 && _tpa == ip + + entries = (\p -> ArpEntry (_sha p) (_spa p)) <$> arpEntries + lites = (\p -> ArpLite (_sha p) (_spa p) False) <$> arpRequests -- | headerBytes mod dataWidth ~ 0 prop_arp_transmitter_d1 :: Property -prop_arp_transmitter_d1 = arpTransmitterPropertyGenerator C.d1 +prop_arp_transmitter_d1 = arpTransmitterPropertyGenerator d1 -- | dataWidth < headerBytes prop_arp_transmitter_d15 :: Property -prop_arp_transmitter_d15 = arpTransmitterPropertyGenerator C.d11 +prop_arp_transmitter_d15 = arpTransmitterPropertyGenerator d11 -- | dataWidth ~ headerBytes prop_arp_transmitter_d28 :: Property -prop_arp_transmitter_d28 = arpTransmitterPropertyGenerator C.d28 +prop_arp_transmitter_d28 = arpTransmitterPropertyGenerator d28 -- | dataWidth > headerBytes prop_arp_transmitter_d29 :: Property -prop_arp_transmitter_d29 = arpTransmitterPropertyGenerator C.d29 - --- | generates 1/4 well-formed ARP requests intended for us, --- 1/4 well-formed ARP requests intended for us but aborted, --- 1/2 non-ARP request packet streams (with varying length and content). --- All generated streams consist of full packets (i.e. end with a fragment with _last == True). -genPackets :: forall - (dataWidth :: C.Nat) - . C.KnownNat dataWidth - => 1 C.<= dataWidth - => Gen [PacketStreamM2S dataWidth EthernetHeader] -genPackets = do - arpPkt <- genArpPacket - abort <- Gen.bool - pickRandomPacket <- Gen.bool - if pickRandomPacket - then - C.fmap fullPackets (Gen.list (Range.linear 1 100) genPackets') - else - let stream = packetizeFromDfModel toEthernetHdr C.id [arpPkt] :: [PacketStreamM2S dataWidth EthernetHeader] - in C.pure C.$ L.init stream L.++ [(L.last stream){_abort = abort}] - - where - genArpPacket = - newArpPacket C.<$> - (MacAddress C.<$> genVec Gen.enumBounded) C.<*> - (IPv4Address C.<$> genVec Gen.enumBounded) C.<*> - Gen.constant ourMac C.<*> - Gen.constant ourIP C.<*> - Gen.bool - - genPackets' = - PacketStreamM2S C.<$> - genVec Gen.enumBounded C.<*> - Gen.maybe Gen.enumBounded C.<*> - genEthernetHdr C.<*> - Gen.enumBounded - - genEthernetHdr :: Gen EthernetHeader - genEthernetHdr = - EthernetHeader C.<$> - Gen.constant ourMac C.<*> - (MacAddress C.<$> genVec Gen.enumBounded) C.<*> - Gen.constant arpEtherType - - toEthernetHdr ArpPacket{..} = EthernetHeader { - _macDst = _tha, - _macSrc = _sha, - _etherType = arpEtherType - } - -arpReceiverPropertyGenerator - :: forall (dataWidth :: C.Nat) - . 1 C.<= dataWidth - => C.SNat dataWidth - -> Property -arpReceiverPropertyGenerator C.SNat = - propWithModelSingleDomain - @C.System - defExpectOptions - genPackets - (C.exposeClockResetEnable model) - (C.exposeClockResetEnable @C.System C.$ arpReceiverC C.$ C.pure ourIP) - (===) - where - model :: [PacketStreamM2S dataWidth EthernetHeader] -> ([ArpEntry],[ArpLite]) - model ethStr = (entries, lites) - where - arpDf = L.filter (validArp ourIP) (depacketizeToDfModel C.const ethStr) - (arpRequests, arpEntries) = L.partition (isRequest ourIP) arpDf - - validArp ip ArpPacket{..} = - _htype C.== 1 - C.&& _ptype C.== 0x0800 - C.&& _hlen C.== 6 - C.&& _plen C.== 4 - C.&&(_oper C.== 1 C.&& (_tpa C.== ip C.|| _tpa C.== _spa) C.|| _oper C.== 2) - - isRequest ip ArpPacket{..} = _oper C.== 1 C.&& _tpa C.== ip - - entries = (\p -> ArpEntry (_sha p) (_spa p)) C.<$> arpEntries - lites = (\p -> ArpLite (_sha p) (_spa p) C.False) C.<$> arpRequests +prop_arp_transmitter_d29 = arpTransmitterPropertyGenerator d29 -- | headerBytes mod dataWidth ~ 0 prop_arp_receiver_d1 :: Property -prop_arp_receiver_d1 = arpReceiverPropertyGenerator C.d1 +prop_arp_receiver_d1 = arpReceiverPropertyGenerator d1 -- | dataWidth < headerBytes prop_arp_receiver_d11 :: Property -prop_arp_receiver_d11 = arpReceiverPropertyGenerator C.d11 +prop_arp_receiver_d11 = arpReceiverPropertyGenerator d11 -- | dataWidth ~ headerBytes prop_arp_receiver_d28 :: Property -prop_arp_receiver_d28 = arpReceiverPropertyGenerator C.d28 +prop_arp_receiver_d28 = arpReceiverPropertyGenerator d28 -- | dataWidth > headerBytes prop_arp_receiver_d29 :: Property -prop_arp_receiver_d29 = arpReceiverPropertyGenerator C.d29 +prop_arp_receiver_d29 = arpReceiverPropertyGenerator d29 tests :: TestTree tests = - localOption (mkTimeout 10_000_000 {- 10 seconds -}) - $ localOption (HedgehogTestLimit (Just 500)) - $(testGroupGenerator) + localOption (mkTimeout 20_000_000 {- 20 seconds -}) $ + localOption + (HedgehogTestLimit (Just 500)) + $(testGroupGenerator) diff --git a/test/Test/Cores/Ethernet/Base.hs b/test/Test/Cores/Ethernet/Base.hs new file mode 100644 index 0000000..524800e --- /dev/null +++ b/test/Test/Cores/Ethernet/Base.hs @@ -0,0 +1,56 @@ +module Test.Cores.Ethernet.Base ( + genMacAddr, + genEthernetHeader, + genIPv4Addr, + genIPv4Header, + genIPv4HeaderLite, +) where + +import Clash.Cores.Ethernet.Mac.EthernetTypes +import Clash.Cores.Ethernet.IP.IPv4Types + +import Clash.Hedgehog.Sized.Vector (genVec) +import Clash.Prelude + +import Hedgehog (Gen) +import qualified Hedgehog.Gen as Gen + +genMacAddr :: Gen MacAddress +genMacAddr = MacAddress <$> genVec Gen.enumBounded + +genEthernetHeader :: Gen EthernetHeader +genEthernetHeader = EthernetHeader + <$> genMacAddr + <*> genMacAddr + <*> Gen.enumBounded + +genIPv4Addr :: Gen IPv4Address +genIPv4Addr = IPv4Address <$> genVec Gen.enumBounded + +genIPv4Header :: Gen IPv4Header +genIPv4Header = + IPv4Header + <$> Gen.constant 4 -- Version + <*> Gen.constant 5 -- IHL + <*> Gen.enumBounded -- DSCP + <*> Gen.enumBounded -- ECN + <*> Gen.enumBounded -- Total length + <*> Gen.enumBounded -- Identification + <*> Gen.enumBounded -- Reserved flag + <*> Gen.enumBounded -- DF flag + <*> Gen.enumBounded -- MF flag + <*> Gen.enumBounded -- Fragment offset + <*> Gen.enumBounded -- TTL + <*> Gen.enumBounded -- Protocol + <*> Gen.constant 0 -- Checksum + <*> genIPv4Addr -- Source IPv4 + <*> genIPv4Addr -- Destination IPv4 + + +genIPv4HeaderLite :: IPv4Address -> Gen IPv4HeaderLite +genIPv4HeaderLite ourIPv4 = + IPv4HeaderLite + <$> genIPv4Addr -- Source IPv4 + <*> Gen.constant ourIPv4 -- Destination IPv4 + <*> Gen.enumBounded -- Protocol + <*> Gen.enumBounded -- Payload length diff --git a/test/Test/Cores/Ethernet/IP/EthernetStream.hs b/test/Test/Cores/Ethernet/IP/EthernetStream.hs index 9087e24..b4c8897 100644 --- a/test/Test/Cores/Ethernet/IP/EthernetStream.hs +++ b/test/Test/Cores/Ethernet/IP/EthernetStream.hs @@ -1,65 +1,63 @@ -{-# language FlexibleContexts #-} -{-# language NumericUnderscores #-} -{-# language RecordWildCards #-} +{-# LANGUAGE NumericUnderscores #-} {-# OPTIONS_GHC -fplugin Protocols.Plugin #-} -module Test.Cores.Ethernet.IP.EthernetStream where +module Test.Cores.Ethernet.IP.EthernetStream ( + tests, +) where + +import Clash.Cores.Ethernet.Arp.ArpTypes +import Clash.Cores.Ethernet.IP.EthernetStream +import Clash.Cores.Ethernet.IP.IPv4Types +import Clash.Cores.Ethernet.Mac.EthernetTypes import Clash.Prelude --- hedgehog -import Hedgehog +import Hedgehog (Property) import qualified Hedgehog.Range as Range --- tasty -import Test.Tasty -import Test.Tasty.Hedgehog ( HedgehogTestLimit(HedgehogTestLimit) ) -import Test.Tasty.Hedgehog.Extra ( testProperty ) -import Test.Tasty.TH ( testGroupGenerator ) - --- clash-protocols import Protocols -import Protocols.PacketStream import Protocols.Hedgehog +import Protocols.PacketStream +import Protocols.PacketStream.Hedgehog --- IP -import Clash.Cores.Ethernet.IP.EthernetStream -import Clash.Cores.Ethernet.IP.IPv4Types - --- MAC -import Clash.Cores.Ethernet.Mac.EthernetTypes +import Test.Cores.Ethernet.Base (genIPv4Addr) --- ARP -import Clash.Cores.Ethernet.Arp.ArpTypes -import Protocols.PacketStream.Hedgehog +import Test.Tasty +import Test.Tasty.Hedgehog (HedgehogTestLimit (HedgehogTestLimit)) +import Test.Tasty.Hedgehog.Extra (testProperty) +import Test.Tasty.TH (testGroupGenerator) myMac :: MacAddress -myMac = MacAddress (6 :> 6:> 6:> 6:> 6:> 6:> Nil) +myMac = MacAddress (6 :> 6 :> 6 :> 6 :> 6 :> 6 :> Nil) someMac :: MacAddress -someMac = MacAddress (7 :> 7:> 0:> 7 :> 7:> 6:> Nil) - --- | drive the bwd of the arp lookup constantly with --- a given response. -arpConstC - :: forall (dom :: Domain) - . HiddenClockResetEnable dom - => KnownDomain dom - => ArpResponse - -> Circuit (ArpLookup dom) () +someMac = MacAddress (7 :> 7 :> 0 :> 7 :> 7 :> 6 :> Nil) + +{- | drive the bwd of the arp lookup constantly with +a given response. +-} +arpConstC :: + forall (dom :: Domain). + (HiddenClockResetEnable dom) => + (KnownDomain dom) => + ArpResponse -> + Circuit (ArpLookup dom) () arpConstC response = fromSignals ckt - where - ckt (_,_) = (pure $ Just response, ()) - --- | toEthernetStream, but with the arp lookup given --- by arpConstC -testCircuit - :: forall (dom :: Domain) (dataWidth :: Nat) - . HiddenClockResetEnable dom - => KnownDomain dom - => KnownNat dataWidth - => ArpResponse - -> Circuit (PacketStream dom dataWidth IPv4Address) (PacketStream dom dataWidth EthernetHeader) + where + ckt (_, _) = (pure $ Just response, ()) + +{- | toEthernetStream, but with the arp lookup given +by arpConstC +-} +testCircuit :: + forall (dom :: Domain) (dataWidth :: Nat). + (HiddenClockResetEnable dom) => + (KnownDomain dom) => + (KnownNat dataWidth) => + ArpResponse -> + Circuit + (PacketStream dom dataWidth IPv4Address) + (PacketStream dom dataWidth EthernetHeader) testCircuit response = circuit $ \packet -> do (packetOut, lookup) <- toEthernetStreamC $ pure myMac -< packet () <- arpConstC response -< lookup @@ -68,60 +66,61 @@ testCircuit response = circuit $ \packet -> do -- model of testCircuit: inserts the given macadress when the -- arp response is an ArpEntryFound mac, -- drops the entire packet if the arp response is ArpEntryNotFound. -model - :: ArpResponse - -> [PacketStreamM2S dataWidth IPv4Address] - -> [PacketStreamM2S dataWidth EthernetHeader] +model :: + ArpResponse -> + [PacketStreamM2S dataWidth IPv4Address] -> + [PacketStreamM2S dataWidth EthernetHeader] model response = case response of ArpEntryNotFound -> const [] ArpEntryFound ma -> fmap (hdr <$) - where - hdr = EthernetHeader ma myMac 0x0800 - -ethernetStreamTest - :: forall (dataWidth :: Nat) - . 1 <= dataWidth - => KnownNat dataWidth - => 1 <= dataWidth - => SNat dataWidth - -> ArpResponse - -> Property + where + hdr = EthernetHeader ma myMac 0x0800 + +ethernetStreamTest :: + forall (dataWidth :: Nat). + (1 <= dataWidth) => + SNat dataWidth -> + ArpResponse -> + Property ethernetStreamTest SNat arpResponse = - propWithModelSingleDomain + idWithModelSingleDomain @System defExpectOptions - (genValidPackets (Range.linear 1 10) (Range.linear 0 10) Abort) + (genPackets (Range.linear 1 10) Abort (genValidPacket genIPv4Addr (Range.linear 0 10))) (exposeClockResetEnable (model arpResponse)) - (exposeClockResetEnable @System ckt) - (===) - where - ckt :: forall (dom :: Domain) - . HiddenClockResetEnable dom - => Circuit (PacketStream dom dataWidth IPv4Address) (PacketStream dom dataWidth EthernetHeader) - ckt = testCircuit arpResponse - --- | We test whether the circuit succesfully inserts the given macadress when the --- arp lookup service constantly gives an ArpEntryFound mac, --- and whether the circuit succesfully drops the entire packet if the arp lookup --- service constantly gives an ArpEntryNotFound. -prop_ethernetstreamer_d1_noresp, prop_ethernetstreamer_d21_noresp, prop_ethernetstreamer_d28_noresp :: Property -prop_ethernetstreamer_d1_resp, prop_ethernetstreamer_d21_resp, prop_ethernetstreamer_d28_resp :: Property + (exposeClockResetEnable (testCircuit @_ @dataWidth arpResponse)) + +{- +We test whether the circuit succesfully inserts the given MAC address when +the ARP lookup service constantly gives an @ArpEntryFound@, and whether the +circuit succesfully drops the entire packet if the ARP lookup service +constantly gives an @ArpEntryNotFound@. +-} -- dataWidth ~ 1 -prop_ethernetstreamer_d1_noresp = ethernetStreamTest d1 ArpEntryNotFound -prop_ethernetstreamer_d1_resp = ethernetStreamTest d21 (ArpEntryFound someMac) +prop_ethernetstream_d1_noresp :: Property +prop_ethernetstream_d1_noresp = ethernetStreamTest d1 ArpEntryNotFound + +prop_ethernetstream_d1_resp :: Property +prop_ethernetstream_d1_resp = ethernetStreamTest d21 (ArpEntryFound someMac) -- dataWidth large -prop_ethernetstreamer_d21_resp = ethernetStreamTest d21 (ArpEntryFound someMac) -prop_ethernetstreamer_d21_noresp = ethernetStreamTest d21 ArpEntryNotFound +prop_ethernetstream_d21_resp :: Property +prop_ethernetstream_d21_resp = ethernetStreamTest d21 (ArpEntryFound someMac) + +prop_ethernetstream_d21_noresp :: Property +prop_ethernetstream_d21_noresp = ethernetStreamTest d21 ArpEntryNotFound -- dataWidth extra large -prop_ethernetstreamer_d28_resp = ethernetStreamTest d28 (ArpEntryFound someMac) -prop_ethernetstreamer_d28_noresp = ethernetStreamTest d28 ArpEntryNotFound +prop_ethernetstream_d28_resp :: Property +prop_ethernetstream_d28_resp = ethernetStreamTest d28 (ArpEntryFound someMac) +prop_ethernetstream_d28_noresp :: Property +prop_ethernetstream_d28_noresp = ethernetStreamTest d28 ArpEntryNotFound tests :: TestTree tests = - localOption (mkTimeout 12_000_000 {- 12 seconds -}) - $ localOption (HedgehogTestLimit (Just 1_000)) - $(testGroupGenerator) + localOption (mkTimeout 20_000_000 {- 20 seconds -}) $ + localOption + (HedgehogTestLimit (Just 1_000)) + $(testGroupGenerator) diff --git a/test/Test/Cores/Ethernet/IP/IPPacketizers.hs b/test/Test/Cores/Ethernet/IP/IPPacketizers.hs index aeb63a4..f2c5071 100644 --- a/test/Test/Cores/Ethernet/IP/IPPacketizers.hs +++ b/test/Test/Cores/Ethernet/IP/IPPacketizers.hs @@ -1,187 +1,128 @@ -{-# language FlexibleContexts #-} -{-# language NumericUnderscores #-} -{-# language RecordWildCards #-} +{-# LANGUAGE NumericUnderscores #-} -module Test.Cores.Ethernet.IP.IPPacketizers where +module Test.Cores.Ethernet.IP.IPPacketizers ( + tests, +) where --- base -import Control.Monad -import Prelude +import Clash.Cores.Ethernet.IP.IPPacketizers +import Clash.Cores.Ethernet.IP.IPv4Types + +import Clash.Prelude --- clash -import qualified Clash.Prelude as C -import qualified Clash.Sized.Vector as C +import qualified Data.List as L --- hedgehog -import Hedgehog +import Hedgehog (Property) import qualified Hedgehog.Gen as Gen import qualified Hedgehog.Range as Range --- tasty -import Test.Tasty -import Test.Tasty.Hedgehog ( HedgehogTestLimit(HedgehogTestLimit) ) -import Test.Tasty.Hedgehog.Extra ( testProperty ) -import Test.Tasty.TH ( testGroupGenerator ) - --- clash-protocols -import Protocols.PacketStream import Protocols.Hedgehog - --- ethernet -import Clash.Cores.Ethernet.IP.IPPacketizers ( ipDepacketizerC, ipPacketizerC ) -import Clash.Cores.Ethernet.IP.IPv4Types -import Clash.Cores.Ethernet.Mac.EthernetTypes - --- tests -import Test.Cores.Ethernet.IP.InternetChecksum ( pureInternetChecksum ) +import Protocols.PacketStream import Protocols.PacketStream.Hedgehog +import Test.Cores.Ethernet.Base +import Test.Cores.Ethernet.IP.InternetChecksum (pureInternetChecksum) -genVec :: (C.KnownNat n, 1 C.<= n) => Gen a -> Gen (C.Vec n a) -genVec gen = sequence (C.repeat gen) - -genPackets :: 1 C.<= n => C.KnownNat n => Gen a -> Gen (PacketStreamM2S n a) -genPackets genMeta = - PacketStreamM2S <$> - genVec Gen.enumBounded <*> - Gen.maybe Gen.enumBounded <*> - genMeta <*> - Gen.enumBounded - --- | Tests the IP packetizer for arbitrary packets -testSetChecksumC - :: forall (dataWidth :: C.Nat) - . ( C.KnownNat dataWidth - , 1 C.<= dataWidth - , 20 `C.Mod` dataWidth C.<= dataWidth - ) - => C.SNat dataWidth - -> Property -testSetChecksumC _ = idWithModelSingleDomain - @C.System defExpectOptions - gen - (C.exposeClockResetEnable $ packetizerModel _ipv4Destination id . model) - (C.exposeClockResetEnable (ipPacketizerC @C.System @dataWidth)) - where - fragments = fmap fullPackets (Gen.list (Range.linear 1 100) (genPackets (pure ()))) - - gen = do - packets <- chunkByPacket <$> fragments - headers <- replicateM (length packets) genIPv4Header - return $ concat $ zipWith (\ps h -> (h <$) <$> ps) packets headers - - geb :: forall x . (Enum x, Bounded x) => Gen x - geb = Gen.enumBounded - genIpAddr = IPv4Address <$> genVec geb - genIPv4Header = IPv4Header - <$> pure 4 <*> pure 5 <*> geb <*> geb --version, ihl, dscp, ecn - <*> geb <*> geb <*> geb <*> geb <*> geb --length, identification, flags - <*> geb <*> geb <*> geb <*> pure 0 --fragment-offset, protocol, ttl, checksum - <*> genIpAddr <*> genIpAddr --source, destination - - model ps = withChecksum - where - checksums = pureInternetChecksum @(C.Vec 10) . C.bitCoerce . _meta <$> ps - withChecksum = zipWith (\c p -> p {_meta = (_meta p) {_ipv4Checksum = c}}) checksums ps - --- Odd data widths -prop_ip_set_checksum_d8 :: Property -prop_ip_set_checksum_d8 = testSetChecksumC C.d8 - --- | Tests the IP depacketizer for arbitrary packets -testIPDepacketizer - :: forall (dataWidth :: C.Nat) - . ( C.KnownNat dataWidth - , 1 C.<= dataWidth - , 20 `C.Mod` dataWidth C.<= dataWidth - ) - => C.SNat dataWidth - -> Property -testIPDepacketizer _ = idWithModelSingleDomain - @C.System defExpectOptions - gen - (C.exposeClockResetEnable model) - (C.exposeClockResetEnable (ipDepacketizerC @C.System @dataWidth)) - where - gen = Gen.choice [genGarbage, genValidHeaders] - - genGarbage = genValidPackets (Range.linear 1 10) (Range.linear 0 10) Abort - geb :: forall x . (Enum x, Bounded x) => Gen x - geb = Gen.enumBounded - genIpAddr = IPv4Address <$> genVec geb - genIPv4Header = IPv4Header <$> pure 4 <*> pure 5 <*> geb <*> geb <*> geb <*> geb <*> geb <*> geb <*> geb <*> geb <*> geb <*> geb <*> pure 0 <*> genIpAddr <*> genIpAddr - genValidHeaderPacket = do - ethernetHeader :: EthernetHeader <- C.unpack <$> Gen.enumBounded - rawHeader <- genIPv4Header - let checksum = pureInternetChecksum (C.bitCoerce rawHeader :: C.Vec 10 (C.BitVector 16)) - header = rawHeader {_ipv4Checksum = checksum} - headerBytes = C.toList (C.bitCoerce header :: C.Vec 20 (C.BitVector 8)) - dataBytes :: [C.BitVector 8] <- Gen.list (Range.linear 0 (5 * C.natToNum @dataWidth)) geb - let dataFragments = chopBy (C.natToNum @dataWidth) (headerBytes ++ dataBytes) - fragments = (\x -> PacketStreamM2S x Nothing ethernetHeader False) <$> (C.unsafeFromList @dataWidth <$> (++ repeat 0xAA) <$> dataFragments) - fragments' = init fragments ++ [(last fragments) {_last = Just (fromIntegral (length (last dataFragments) - 1))}] - aborts <- sequence (Gen.bool <$ fragments) - let fragments'' = zipWith (\p abort -> p {_abort = abort}) fragments' aborts - return fragments'' - - genValidHeaders = concat <$> Gen.list (Range.linear 1 50) genValidHeaderPacket - - model fragments = concat $ zipWith setAbort packets aborts - where - setAbort packet abort = (\f -> f {_abort = _abort f || abort}) <$> packet - validateHeader hdr = - pureInternetChecksum (C.bitCoerce hdr :: C.Vec 10 (C.BitVector 16)) /= 0 || - _ipv4Ihl hdr /= 5 || - _ipv4Version hdr /= 4 || - _ipv4FlagReserved hdr || - _ipv4FlagMF hdr - packets = chunkByPacket $ depacketizerModel const fragments - aborts = validateHeader . _meta . head <$> packets - - --- Odd data widths +import Test.Tasty +import Test.Tasty.Hedgehog (HedgehogTestLimit (HedgehogTestLimit)) +import Test.Tasty.Hedgehog.Extra (testProperty) +import Test.Tasty.TH (testGroupGenerator) + +testIPPacketizer :: + forall (dataWidth :: Nat). + (1 <= dataWidth) => + SNat dataWidth -> + Property +testIPPacketizer SNat = + idWithModelSingleDomain + @System + defExpectOptions{eoSampleMax = 400, eoStopAfterEmpty = 400} + (genPackets (Range.linear 1 4) Abort (genValidPacket genIPv4Header (Range.linear 0 30))) + (exposeClockResetEnable (packetizerModel _ipv4Destination id . setChecksums)) + (exposeClockResetEnable (ipPacketizerC @_ @dataWidth)) + where + setChecksums ps = L.concatMap setChecksum (chunkByPacket ps) + setChecksum xs = L.map (\x -> x{_meta = (_meta x){_ipv4Checksum = checksum}}) xs + where + checksum = (pureInternetChecksum @(Vec 10) . bitCoerce . _meta) (L.head xs) + +testIPDepacketizer :: + forall (dataWidth :: Nat). + (1 <= dataWidth) => + SNat dataWidth -> + Property +testIPDepacketizer SNat = + idWithModelSingleDomain + @System + defExpectOptions{eoStopAfterEmpty = 400} + (genPackets (Range.linear 1 10) Abort genPkt) + (exposeClockResetEnable model) + (exposeClockResetEnable (ipDepacketizerC @_ @dataWidth)) + where + validPkt = genValidPacket genEthernetHeader (Range.linear 0 10) + genPkt am = + Gen.choice + [ -- Random packet: extremely high chance to get aborted. + validPkt am + , -- Packet with valid header: should not get aborted. + do + hdr <- genIPv4Header + packetizerModel + id + (const hdr{_ipv4Checksum = pureInternetChecksum (bitCoerce hdr :: Vec 10 (BitVector 16))}) + <$> validPkt am + , -- Packet with valid header apart from (most likely) the checksum. + do + hdr <- genIPv4Header + packetizerModel id (const hdr{_ipv4Checksum = 0xABCD}) <$> validPkt am + ] + + model fragments = L.concat $ L.zipWith setAbort packets aborts + where + setAbort packet abort = (\f -> f{_abort = _abort f || abort}) <$> packet + validateHeader hdr = + pureInternetChecksum (bitCoerce hdr :: Vec 10 (BitVector 16)) /= 0 + || _ipv4Ihl hdr /= 5 + || _ipv4Version hdr /= 4 + || _ipv4FlagReserved hdr + || _ipv4FlagMF hdr + packets = chunkByPacket $ depacketizerModel const fragments + aborts = validateHeader . _meta . L.head <$> packets + +-- | 20 % dataWidth ~ 0 +prop_ip_ip_packetizer_d1 :: Property +prop_ip_ip_packetizer_d1 = testIPPacketizer d1 + +-- | dataWidth < 20 +prop_ip_ip_packetizer_d7 :: Property +prop_ip_ip_packetizer_d7 = testIPPacketizer d7 + +-- | dataWidth ~ 20 +prop_ip_ip_packetizer_d20 :: Property +prop_ip_ip_packetizer_d20 = testIPPacketizer d20 + +-- | dataWidth > 20 +prop_ip_ip_packetizer_d23 :: Property +prop_ip_ip_packetizer_d23 = testIPPacketizer d23 + +-- | 20 % dataWidth ~ 0 prop_ip_depacketizer_d1 :: Property -prop_ip_depacketizer_d1 = testIPDepacketizer C.d1 - -prop_ip_depacketizer_d3 :: Property -prop_ip_depacketizer_d3 = testIPDepacketizer C.d3 - -prop_ip_depacketizer_d5 :: Property -prop_ip_depacketizer_d5 = testIPDepacketizer C.d5 +prop_ip_depacketizer_d1 = testIPDepacketizer d1 +-- | dataWidth < 20 prop_ip_depacketizer_d7 :: Property -prop_ip_depacketizer_d7 = testIPDepacketizer C.d7 - -prop_ip_depacketizer_d19 :: Property -prop_ip_depacketizer_d19 = testIPDepacketizer C.d19 - -prop_ip_depacketizer_d21 :: Property -prop_ip_depacketizer_d21 = testIPDepacketizer C.d21 - -prop_ip_depacketizer_d23 :: Property -prop_ip_depacketizer_d23 = testIPDepacketizer C.d23 - --- Even data widths -prop_ip_depacketizer_d2 :: Property -prop_ip_depacketizer_d2 = testIPDepacketizer C.d2 - -prop_ip_depacketizer_d4 :: Property -prop_ip_depacketizer_d4 = testIPDepacketizer C.d4 - -prop_ip_depacketizer_d6 :: Property -prop_ip_depacketizer_d6 = testIPDepacketizer C.d6 - -prop_ip_depacketizer_d18 :: Property -prop_ip_depacketizer_d18 = testIPDepacketizer C.d18 +prop_ip_depacketizer_d7 = testIPDepacketizer d7 +-- | dataWidth ~ 20 prop_ip_depacketizer_d20 :: Property -prop_ip_depacketizer_d20 = testIPDepacketizer C.d20 +prop_ip_depacketizer_d20 = testIPDepacketizer d20 -prop_ip_depacketizer_d28 :: Property -prop_ip_depacketizer_d28 = testIPDepacketizer C.d28 +-- | dataWidth > 20 +prop_ip_depacketizer_d23 :: Property +prop_ip_depacketizer_d23 = testIPDepacketizer d23 tests :: TestTree tests = - localOption (mkTimeout 20_000_000 {- 20 seconds -}) - $ localOption (HedgehogTestLimit (Just 1_000)) - $(testGroupGenerator) + localOption (mkTimeout 20_000_000 {- 20 seconds -}) $ + localOption + (HedgehogTestLimit (Just 1_000)) + $(testGroupGenerator) diff --git a/test/Test/Cores/Ethernet/IP/InternetChecksum.hs b/test/Test/Cores/Ethernet/IP/InternetChecksum.hs index 90ed983..43296c9 100644 --- a/test/Test/Cores/Ethernet/IP/InternetChecksum.hs +++ b/test/Test/Cores/Ethernet/IP/InternetChecksum.hs @@ -28,6 +28,11 @@ import Test.Tasty.TH ( testGroupGenerator ) -- ethernet import Clash.Cores.Ethernet.IP.InternetChecksum +import Protocols.PacketStream +import Protocols.PacketStream.Hedgehog + +import qualified Clash.Sized.Vector as Vec + uncurryS :: (Signal dom a -> Signal dom b -> Signal dom c) @@ -88,6 +93,31 @@ pureInternetChecksum = complement . fromInteger . L.foldr (pureOnesComplementAdd pureOnesComplementAdd :: Integral a => a -> a -> a pureOnesComplementAdd a b = (a + b) `mod` 65_536 + (a + b) `div` 65_536 +alignTo :: Int -> a -> [a] -> [a] +alignTo n a xs = xs L.++ L.replicate (n - mod (L.length xs) n) a + +{- | +Like 'pureInternetChecksum', but over a packet stream. +Assumes that there is only one packet in the input stream. +-} +calculateChecksum :: + forall dataWidth meta. + (KnownNat dataWidth) => + (1 <= dataWidth) => + [PacketStreamM2S dataWidth meta] -> + BitVector 16 +calculateChecksum fragments = checksum + where + dataToList PacketStreamM2S{..} = L.take validData $ Vec.toList _data + where + validData = 1 + fromIntegral (fromMaybe maxBound _last) + checksum = + pureInternetChecksum $ + fmap (pack . Vec.unsafeFromList @2) $ + chopBy 2 $ + alignTo 2 0x00 $ + L.concatMap dataToList fragments + -- Tests the one's complement sum prop_onescomplementadd :: Property prop_onescomplementadd = property $ do diff --git a/test/Test/Cores/Ethernet/Icmp.hs b/test/Test/Cores/Ethernet/Icmp.hs index 7bdabc5..ebeba0c 100644 --- a/test/Test/Cores/Ethernet/Icmp.hs +++ b/test/Test/Cores/Ethernet/Icmp.hs @@ -1,176 +1,102 @@ -{-# language FlexibleContexts #-} -{-# language NumericUnderscores #-} -{-# language RecordWildCards #-} +{-# LANGUAGE NumericUnderscores #-} +{-# LANGUAGE RecordWildCards #-} -module Test.Cores.Ethernet.Icmp where +module Test.Cores.Ethernet.Icmp ( + tests, +) where --- base -import Data.Bifunctor ( bimap, second ) -import Data.Maybe ( fromMaybe ) -import Prelude +import Clash.Cores.Ethernet.IP.IPv4Types +import Clash.Cores.Ethernet.Icmp --- clash-prelude -import qualified Clash.Prelude as C -import qualified Clash.Sized.Vector as V +import Clash.Prelude --- hedgehog -import Hedgehog -import qualified Hedgehog.Gen as Gen -import qualified Hedgehog.Range as Range +import qualified Data.Bifunctor as B +import qualified Data.List as L --- tasty -import Test.Tasty -import Test.Tasty.Hedgehog ( HedgehogTestLimit(HedgehogTestLimit) ) -import Test.Tasty.Hedgehog.Extra ( testProperty ) -import Test.Tasty.TH ( testGroupGenerator ) +import Hedgehog (Property) +import qualified Hedgehog.Range as Range --- clash-protocols -import Protocols.PacketStream import Protocols.Hedgehog - --- ethernet -import Clash.Cores.Ethernet.Icmp -import Clash.Cores.Ethernet.IP.IPv4Types - --- tests -import Test.Cores.Ethernet.IP.InternetChecksum ( pureInternetChecksum ) +import Protocols.PacketStream (PacketStreamM2S(_meta)) import Protocols.PacketStream.Hedgehog -genViaBits :: C.BitPack a => Gen a -genViaBits = C.unpack <$> Gen.enumBounded - -genIpAddr :: Gen IPv4Address -genIpAddr = IPv4Address <$> C.sequence (C.repeat @4 Gen.enumBounded) - -genIPv4HeaderLite :: Gen IPv4HeaderLite -genIPv4HeaderLite = IPv4HeaderLite <$> genIpAddr <*> genIpAddr <*> Gen.enumBounded <*> pure 0 - -packetize - :: 1 C.<= dataWidth - => C.KnownNat dataWidth - => [PacketStreamM2S dataWidth (IPv4HeaderLite, IcmpHeaderLite)] - -> [PacketStreamM2S dataWidth IPv4HeaderLite] -packetize = packetizerModel fst (fromIcmpLite . snd) - -depacketize - :: 1 C.<= dataWidth - => C.KnownNat dataWidth - => [PacketStreamM2S dataWidth IPv4HeaderLite] - -> [PacketStreamM2S dataWidth (IPv4HeaderLite, IcmpHeaderLite)] -depacketize inFragments = outFragments - where - goodHeader hdr = _type hdr == 8 && _code hdr == 0 - outFragments = fmap (fmap (second toIcmpLite)) - $ filter (goodHeader . snd . _meta) - $ depacketizerModel (\icmpHdr ipHdr -> (ipHdr, icmpHdr)) inFragments - -alignTo :: Int -> a -> [a] -> [a] -alignTo n a xs = xs ++ replicate (n - mod (length xs) n) a - -updateLast :: (a -> a) -> [a] -> [a] -updateLast _ [] = [] -updateLast f xs = init xs ++ [f $ last xs] - --- This generates a packet with a valid ICMP header prepended including --- a correct checksum -genValidIcmpRequestPacket - :: forall dataWidth - . 1 C.<= dataWidth - => C.KnownNat dataWidth - => Gen [PacketStreamM2S dataWidth IPv4HeaderLite] -genValidIcmpRequestPacket = do - let saneHeader chkSum hdr = hdr { _type = 8, _code = 0, _checksum = chkSum } - rawHeader <- fmap (saneHeader 0) $ genViaBits @IcmpHeader - let rawHeaderWords = V.toList (C.bitCoerce rawHeader :: C.Vec 2 (C.BitVector 16)) - payloadWords <- Gen.list (Range.linear 1 50) (Gen.enumBounded :: Gen (C.BitVector 16)) - - let checksum = pureInternetChecksum $ rawHeaderWords ++ payloadWords - let validHeader = saneHeader checksum rawHeader - let headerBytes = V.toList (C.bitCoerce validHeader :: C.Vec 4 (C.BitVector 8)) - let dataBytes = payloadWords >>= \w -> V.toList (C.bitCoerce w :: C.Vec 2 (C.BitVector 8)) - - ipv4Hdr <- genViaBits @IPv4HeaderLite - let toFragments vs = PacketStreamM2S vs Nothing ipv4Hdr <$> Gen.enumBounded - let dataWidth = C.natToNum @dataWidth - let totalBytes = headerBytes ++ dataBytes - let lastIdxRaw = mod (length totalBytes) dataWidth - let lastIdx = if lastIdxRaw == 0 - then C.natToNum @dataWidth - 1 - else lastIdxRaw - fmap (updateLast (\pkt -> pkt { _last = Just $ fromIntegral lastIdx })) - $ mapM toFragments - $ fmap (V.unsafeFromList @dataWidth) - $ chopBy dataWidth - $ alignTo dataWidth 0x00 totalBytes - --- This function assumes all fragments belong to a single packet -calcChecksum - :: forall dataWidth meta - . 1 C.<= dataWidth - => C.KnownNat dataWidth - => [PacketStreamM2S dataWidth meta] - -> C.BitVector 16 -calcChecksum fragments = checksum - where - dataToList PacketStreamM2S{..} = take validData $ V.toList _data - where - validData = 1 + fromIntegral (fromMaybe maxBound _last) - checksum = pureInternetChecksum - $ fmap (C.pack . V.unsafeFromList @2) - $ chopBy 2 - $ alignTo 2 0x00 - $ concatMap dataToList fragments - -icmpResponderPropertyGenerator - :: forall dataWidth - . 1 C.<= dataWidth - => C.SNat dataWidth - -> Property -icmpResponderPropertyGenerator C.SNat = +import Test.Cores.Ethernet.Base (genIPv4HeaderLite) +import Test.Cores.Ethernet.IP.InternetChecksum (calculateChecksum) + +import Test.Tasty +import Test.Tasty.Hedgehog (HedgehogTestLimit (HedgehogTestLimit)) +import Test.Tasty.Hedgehog.Extra (testProperty) +import Test.Tasty.TH (testGroupGenerator) + +ourIPv4 :: IPv4Address +ourIPv4 = IPv4Address (repeat @4 0x3) + +icmpResponderPropertyGenerator :: + forall dataWidth. + (1 <= dataWidth) => + SNat dataWidth -> + Property +icmpResponderPropertyGenerator SNat = idWithModelSingleDomain - @C.System + @System defExpectOptions - (concat <$> Gen.list (Range.linear 1 10) genValidIcmpRequestPacket) - (C.exposeClockResetEnable (concatMap model . chunkByPacket)) - (C.exposeClockResetEnable (icmpEchoResponderC $ pure ourIpAddr)) + (genPackets (Range.linear 1 5) Abort genValidIcmpRequestPacket) + (exposeClockResetEnable (L.concatMap model . chunkByPacket)) + (exposeClockResetEnable (icmpEchoResponderC $ pure ourIPv4)) where - ourIpAddr = IPv4Address (C.repeat @4 0x3) - - model :: [PacketStreamM2S dataWidth IPv4HeaderLite] -> [PacketStreamM2S dataWidth IPv4HeaderLite] + genValidIcmpRequestPacket am = do + dat <- genValidPacket (genIPv4HeaderLite ourIPv4) (Range.linear 0 10) am + let checksum = calculateChecksum (packetizerModel id (const (IcmpHeader 8 0 0)) dat) + pure $ packetizerModel id (const $ IcmpHeader 8 0 checksum) dat + + model :: + [PacketStreamM2S dataWidth IPv4HeaderLite] -> + [PacketStreamM2S dataWidth IPv4HeaderLite] model fragments = res - where - res = packetize $ fmap (bimap swapIps (updateIcmp newChecksum)) <$> depacketize fragments - newFragments0 = packetize $ fmap (bimap swapIps (updateIcmp 0)) <$> depacketize fragments - newChecksum = calcChecksum newFragments0 - swapIps ip@IPv4HeaderLite{..} = ip{_ipv4lSource = ourIpAddr, _ipv4lDestination = _ipv4lSource} - updateIcmp chk icmp = icmp {_checksumL = chk} + where + filtered = + L.map (fmap (B.second toIcmpLite)) $ + L.filter ((\hdr -> _code hdr == 0 && _type hdr == 8) . snd . _meta) $ + depacketizerModel (\icmpHdr ipHdr -> (ipHdr, icmpHdr)) fragments + + withIcmpHeader = + packetizerModel fst (fromIcmpLite . snd) $ fmap (B.bimap swapIPs (updateChecksum 0)) + <$> filtered + + res = + packetizerModel fst (fromIcmpLite . snd) $ + L.map (fmap (B.bimap swapIPs (updateChecksum newChecksum))) filtered + + -- To prevent the tests from failing, we set the checksum to 0x0000 if + -- it is 0xFFFF. This is a limitation of manually adjusting the checksum, + -- but the case will almost never happen in practice. See the comments in + -- Clash.Cores.Ethernet.Icmp for more information. + newChecksum = + let c = calculateChecksum withIcmpHeader + in if c == 0xFFFF then 0x0000 else c + + swapIPs ipHdr = + ipHdr + { _ipv4lSource = ourIPv4 + , _ipv4lDestination = _ipv4lSource ipHdr + } + updateChecksum chk icmpHdr = icmpHdr{_checksumL = chk} prop_icmp_responder_d1 :: Property -prop_icmp_responder_d1 = icmpResponderPropertyGenerator C.d1 - -prop_icmp_responder_d2 :: Property -prop_icmp_responder_d2 = icmpResponderPropertyGenerator C.d2 +prop_icmp_responder_d1 = icmpResponderPropertyGenerator d1 prop_icmp_responder_d3 :: Property -prop_icmp_responder_d3 = icmpResponderPropertyGenerator C.d3 +prop_icmp_responder_d3 = icmpResponderPropertyGenerator d3 prop_icmp_responder_d4 :: Property -prop_icmp_responder_d4 = icmpResponderPropertyGenerator C.d4 - -prop_icmp_responder_d5 :: Property -prop_icmp_responder_d5 = icmpResponderPropertyGenerator C.d5 - -prop_icmp_responder_d6 :: Property -prop_icmp_responder_d6 = icmpResponderPropertyGenerator C.d6 +prop_icmp_responder_d4 = icmpResponderPropertyGenerator d4 prop_icmp_responder_d7 :: Property -prop_icmp_responder_d7 = icmpResponderPropertyGenerator C.d7 - -prop_icmp_responder_d8 :: Property -prop_icmp_responder_d8 = icmpResponderPropertyGenerator C.d8 +prop_icmp_responder_d7 = icmpResponderPropertyGenerator d7 tests :: TestTree tests = - localOption (mkTimeout 12_000_000 {- 12 seconds -}) - $ localOption (HedgehogTestLimit (Just 1_000)) - $(testGroupGenerator) + localOption (mkTimeout 20_000_000 {- 20 seconds -}) $ + localOption + (HedgehogTestLimit (Just 1_000)) + $(testGroupGenerator) diff --git a/test/Test/Cores/Ethernet/Mac/FrameCheckSequence.hs b/test/Test/Cores/Ethernet/Mac/FrameCheckSequence.hs index 4d35081..3d7593d 100644 --- a/test/Test/Cores/Ethernet/Mac/FrameCheckSequence.hs +++ b/test/Test/Cores/Ethernet/Mac/FrameCheckSequence.hs @@ -1,177 +1,155 @@ +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE NumericUnderscores #-} {-# OPTIONS_GHC -Wno-orphans #-} -{-# language FlexibleContexts #-} -{-# language MultiParamTypeClasses #-} -{-# language NumericUnderscores #-} -{-# language RecordWildCards #-} -{-# language ScopedTypeVariables #-} -{-# language TemplateHaskell #-} -module Test.Cores.Ethernet.Mac.FrameCheckSequence where +module Test.Cores.Ethernet.Mac.FrameCheckSequence ( + tests, +) where --- base -import Control.Monad -import qualified Data.List as L -import Prelude - --- clash import Clash.Cores.Crc import Clash.Cores.Crc.Catalog -import qualified Clash.Prelude as C +import Clash.Cores.Ethernet.Mac.FrameCheckSequence + +import Clash.Prelude + +import qualified Data.List as L --- hedgehog -import Hedgehog +import Hedgehog (Property) import qualified Hedgehog.Gen as Gen import qualified Hedgehog.Range as Range --- tasty -import Test.Tasty -import Test.Tasty.Hedgehog ( HedgehogTestLimit(HedgehogTestLimit) ) -import Test.Tasty.Hedgehog.Extra ( testProperty ) -import Test.Tasty.TH ( testGroupGenerator ) +import Protocols.Hedgehog --- clash-protocols -import Protocols import Protocols.PacketStream import Protocols.PacketStream.Hedgehog -import Protocols.Hedgehog - --- ethernet -import Clash.Cores.Ethernet.Mac.FrameCheckSequence - -$(deriveHardwareCrc Crc32_ethernet C.d8 C.d1) -$(deriveHardwareCrc Crc32_ethernet C.d8 C.d2) -$(deriveHardwareCrc Crc32_ethernet C.d8 C.d4) -$(deriveHardwareCrc Crc32_ethernet C.d8 C.d8) - -genVec :: (C.KnownNat n, 1 C.<= n) => Gen a -> Gen (C.Vec n a) -genVec gen = sequence (C.repeat gen) - -modelInsert - :: C.KnownNat dataWidth - => 1 C.<= dataWidth - => [PacketStreamM2S dataWidth ()] -> [PacketStreamM2S dataWidth ()] -modelInsert fragments = insertCrc =<< chunkByPacket fragments - -packetToCrcInp - :: C.KnownNat dataWidth - => 1 C.<= dataWidth - => [PacketStreamM2S dataWidth ()] -> [C.BitVector 8] -packetToCrcInp packet = C.head . _data <$> (chopPacket =<< packet) - -insertCrc - :: forall (dataWidth :: C.Nat) - . C.KnownNat dataWidth - => 1 C.<= dataWidth - => [PacketStreamM2S dataWidth ()] -> [PacketStreamM2S dataWidth ()] -insertCrc = upConvert . go . downConvert - where - go :: [PacketStreamM2S 1 ()] -> [PacketStreamM2S 1 ()] - go pkt = pkt'' - where - crcInp = C.head . _data <$> pkt - softwareCrc = mkSoftwareCrc Crc32_ethernet C.d8 - crc = digest $ L.foldl' feed softwareCrc crcInp - crc' = C.singleton . C.v2bv <$> (C.toList . C.reverse . C.unconcat C.d8 . C.bv2v $ crc) - lastfmnt = L.last pkt - pkt' = init pkt L.++ [lastfmnt {_last = Nothing}] L.++ fmap (\dat -> lastfmnt {_data = dat, _last = Nothing}) crc' - pkt'' = init pkt' ++ [(last pkt'){_last = Just 0}] - --- | Test the fcsinserter -fcsinserterTest - :: forall n - . (1 C.<= n, HardwareCrc Crc32_ethernet 8 n) - => C.SNat n -> Property -fcsinserterTest C.SNat = +import Test.Tasty +import Test.Tasty.Hedgehog (HedgehogTestLimit (HedgehogTestLimit)) +import Test.Tasty.Hedgehog.Extra (testProperty) +import Test.Tasty.TH (testGroupGenerator) + +$(deriveHardwareCrc Crc32_ethernet d8 d1) +$(deriveHardwareCrc Crc32_ethernet d8 d2) +$(deriveHardwareCrc Crc32_ethernet d8 d4) +$(deriveHardwareCrc Crc32_ethernet d8 d8) + +packetToCrcInp :: + (KnownNat dataWidth) => + (1 <= dataWidth) => + [PacketStreamM2S dataWidth ()] -> + [BitVector 8] +packetToCrcInp packet = head . _data <$> (chopPacket =<< packet) + +insertCrc :: + forall (dataWidth :: Nat). + (KnownNat dataWidth) => + (1 <= dataWidth) => + [PacketStreamM2S dataWidth ()] -> + [PacketStreamM2S dataWidth ()] +insertCrc = upConvert . go . downConvert + where + go :: [PacketStreamM2S 1 ()] -> [PacketStreamM2S 1 ()] + go pkt = pkt'' + where + crcInp = head . _data <$> pkt + softwareCrc = mkSoftwareCrc Crc32_ethernet d8 + crc = digest $ L.foldl' feed softwareCrc crcInp + crc' = singleton . v2bv <$> (toList . reverse . unconcat d8 . bv2v $ crc) + lastfmnt = L.last pkt + pkt' = + L.init pkt + L.++ [lastfmnt{_last = Nothing}] + L.++ fmap (\dat -> lastfmnt{_data = dat, _last = Nothing}) crc' + pkt'' = L.init pkt' L.++ [(L.last pkt'){_last = Just 0}] + + +validateCrc :: + forall (dataWidth :: Nat). + (KnownNat dataWidth) => + (1 <= dataWidth) => + [PacketStreamM2S dataWidth ()] -> + [PacketStreamM2S dataWidth ()] +validateCrc packet = L.init packet L.++ [lastPacketSetAbort] + where + lastFragment = L.last packet + softwareCrc = mkSoftwareCrc Crc32_ethernet d8 + crcBytes = digest $ L.foldl' feed softwareCrc $ packetToCrcInp packet + valid = complement crcBytes == residue Crc32_ethernet + + lastPacketSetAbort = + lastFragment + { _abort = not valid || _abort lastFragment + } + +-- | Test the FCS inserter +fcsinserterTest :: + forall dataWidth. + (1 <= dataWidth) => + (HardwareCrc Crc32_ethernet 8 dataWidth) => + SNat dataWidth -> + Property +fcsinserterTest SNat = idWithModelSingleDomain - @C.System + @System defExpectOptions - (genValidPackets (Range.linear 1 4) (Range.linear 0 30) Abort) - (C.exposeClockResetEnable modelInsert) - (C.exposeClockResetEnable (fcsInserterC @C.System @n)) - -prop_fcsinserter_d1, prop_fcsinserter_d2, prop_fcsinserter_d4, prop_fcsinserter_d8 :: Property -prop_fcsinserter_d1 = fcsinserterTest C.d1 -prop_fcsinserter_d2 = fcsinserterTest C.d2 -prop_fcsinserter_d4 = fcsinserterTest C.d4 -prop_fcsinserter_d8 = fcsinserterTest C.d8 - -modelValidate - :: C.KnownNat dataWidth - => 1 C.<= dataWidth - => [PacketStreamM2S dataWidth ()] -> [PacketStreamM2S dataWidth ()] -modelValidate fragments = validateCrc =<< chunkByPacket fragments - -validateCrc - :: forall (dataWidth :: C.Nat) - . C.KnownNat dataWidth - => 1 C.<= dataWidth - => [PacketStreamM2S dataWidth ()] -> [PacketStreamM2S dataWidth ()] -validateCrc packet = L.init packet ++ [lastPacketSetAbort] - where - lastFragment = last packet - softwareCrc = mkSoftwareCrc Crc32_ethernet C.d8 - crcBytes = digest $ L.foldl' feed softwareCrc $ packetToCrcInp packet - valid = C.complement crcBytes == residue Crc32_ethernet - - lastPacketSetAbort = lastFragment { - _abort = not valid || _abort lastFragment - } - --- | Test the fcsvalidator -fcsvalidatorTest - :: forall n - . (1 C.<= n, HardwareCrc Crc32_ethernet 8 n) - => C.SNat n -> Property -fcsvalidatorTest C.SNat = - propWithModelSingleDomain - @C.System + (genPackets (Range.linear 1 4) Abort (genValidPacket (pure ()) (Range.linear 0 20))) + (exposeClockResetEnable modelInsert) + (exposeClockResetEnable (fcsInserterC @_ @dataWidth)) + where + modelInsert packets = L.concatMap insertCrc (chunkByPacket packets) + +-- | Test the FCS validator +fcsvalidatorTest :: + forall dataWidth. + (1 <= dataWidth) => + (HardwareCrc Crc32_ethernet 8 dataWidth) => + SNat dataWidth -> + Property +fcsvalidatorTest SNat = + idWithModelSingleDomain + @System defExpectOptions - inpPackets'' -- Input packets - (C.exposeClockResetEnable modelValidate) -- Desired behaviour of FcsInserter - (C.exposeClockResetEnable ckt) -- Implementation of FcsInserter - (===) -- Property to test - where - ckt - :: forall (dom :: C.Domain) (dataWidth :: C.Nat) - . C.KnownDomain dom - => 1 C.<= dataWidth - => C.HiddenClockResetEnable dom - => HardwareCrc Crc32_ethernet 8 dataWidth - => Circuit - (PacketStream dom dataWidth ()) - (PacketStream dom dataWidth ()) - ckt = fcsValidatorC - - -- This generates the packets - inpPackets'' = join <$> genPackets' - - genPackets' = do - fragments <- insertCrc . fullPackets <$> Gen.list (Range.linear 1 100) genPackets - let packets = chunkByPacket fragments - forM packets $ \packet -> do - poison <- Gen.enumBounded :: Gen Bool - let lastfmnt = last packet - return $ - if poison - then init packet L.++ [lastfmnt {_last = Nothing}] L.++ [lastfmnt] - else packet - - genPackets = - PacketStreamM2S <$> - genVec @n Gen.enumBounded <*> - Gen.maybe Gen.enumBounded <*> - Gen.enumBounded <*> - Gen.enumBounded - -prop_fcsvalidator_d1, prop_fcsvalidator_d2, prop_fcsvalidator_d4, prop_fcsvalidator_d8 :: Property -prop_fcsvalidator_d1 = fcsvalidatorTest C.d1 -prop_fcsvalidator_d2 = fcsvalidatorTest C.d2 -prop_fcsvalidator_d4 = fcsvalidatorTest C.d4 -prop_fcsvalidator_d8 = fcsvalidatorTest C.d8 + (genPackets (Range.linear 1 4) Abort genPkt) + (exposeClockResetEnable modelValidate) + (exposeClockResetEnable (fcsValidatorC @_ @dataWidth)) + where + genPkt am = + Gen.choice + [ -- Random packet + genValidPacket (pure ()) (Range.linear 0 20) am + , -- Packet with valid CRC + insertCrc <$> genValidPacket (pure ()) (Range.linear 0 20) am + ] + + modelValidate packets = validateCrc =<< chunkByPacket packets + +prop_fcsinserter_d1 :: Property +prop_fcsinserter_d1 = fcsinserterTest d1 + +prop_fcsinserter_d2 :: Property +prop_fcsinserter_d2 = fcsinserterTest d2 + +prop_fcsinserter_d4 :: Property +prop_fcsinserter_d4 = fcsinserterTest d4 + +prop_fcsinserter_d8 :: Property +prop_fcsinserter_d8 = fcsinserterTest d8 + +prop_fcsvalidator_d1 :: Property +prop_fcsvalidator_d1 = fcsvalidatorTest d1 + +prop_fcsvalidator_d2 :: Property +prop_fcsvalidator_d2 = fcsvalidatorTest d2 + +prop_fcsvalidator_d4 :: Property +prop_fcsvalidator_d4 = fcsvalidatorTest d4 + +prop_fcsvalidator_d8 :: Property +prop_fcsvalidator_d8 = fcsvalidatorTest d8 tests :: TestTree tests = - localOption (mkTimeout 12_000_000 {- 12 seconds -}) - $ localOption (HedgehogTestLimit (Just 1_000)) - $(testGroupGenerator) + localOption (mkTimeout 20_000_000 {- 20 seconds -}) $ + localOption + (HedgehogTestLimit (Just 1_000)) + $(testGroupGenerator) diff --git a/test/Test/Cores/Ethernet/Mac/InterpacketGapInserter.hs b/test/Test/Cores/Ethernet/Mac/InterpacketGapInserter.hs index 269cc5e..dd5f1bb 100644 --- a/test/Test/Cores/Ethernet/Mac/InterpacketGapInserter.hs +++ b/test/Test/Cores/Ethernet/Mac/InterpacketGapInserter.hs @@ -1,57 +1,44 @@ -{-# language FlexibleContexts #-} -{-# language NumericUnderscores #-} -{-# language RecordWildCards #-} +{-# LANGUAGE NumericUnderscores #-} -module Test.Cores.Ethernet.Mac.InterpacketGapInserter where +module Test.Cores.Ethernet.Mac.InterpacketGapInserter ( + tests, +) where -import qualified Data.List as L -import Prelude +import Clash.Cores.Ethernet.Mac.InterpacketGapInserter -import Clash.Prelude hiding ( repeat ) -import qualified Clash.Prelude as C +import Clash.Prelude + +import qualified Data.List as L import Hedgehog -import qualified Hedgehog.Gen as Gen import qualified Hedgehog.Range as Range -import Test.Tasty -import Test.Tasty.Hedgehog ( HedgehogTestLimit(HedgehogTestLimit) ) -import Test.Tasty.Hedgehog.Extra ( testProperty ) -import Test.Tasty.TH ( testGroupGenerator ) - import Protocols -import Protocols.PacketStream import Protocols.Hedgehog +import Protocols.PacketStream +import Protocols.PacketStream.Hedgehog -import Clash.Cores.Ethernet.Mac.InterpacketGapInserter - - -genVec :: (KnownNat n, 1 <= n) => Gen a -> Gen (Vec n a) -genVec gen = sequence (C.repeat gen) - --- | If we do not consider the timing information of the component, --- all it should do is forward its inputs. Hence, this id test. +import Test.Tasty +import Test.Tasty.Hedgehog (HedgehogTestLimit (HedgehogTestLimit)) +import Test.Tasty.Hedgehog.Extra (testProperty) +import Test.Tasty.TH (testGroupGenerator) + +{- | +If we do not consider the timing information of this component, +all it should do is forward its inputs. Hence, this id test. +-} prop_interpacket_gap_inserter_id :: Property prop_interpacket_gap_inserter_id = - propWithModelSingleDomain - @C.System + idWithModelSingleDomain + @System defExpectOptions - (Gen.list (Range.linear 0 100) genPackets) + (genPackets (Range.linear 1 10) Abort (genValidPacket (pure ()) (Range.linear 0 20))) (exposeClockResetEnable id) - (exposeClockResetEnable @System (interpacketGapInserterC d12)) - (===) - where - -- This is used to generate - genPackets = - PacketStreamM2S <$> - genVec Gen.enumBounded <*> - Gen.maybe Gen.enumBounded <*> - Gen.enumBounded <*> - Gen.enumBounded + (exposeClockResetEnable (interpacketGapInserterC d12)) fwdIn :: [Maybe (PacketStreamM2S 1 ())] -fwdIn = [ - Just (PacketStreamM2S (0xAB :> Nil) Nothing () False) +fwdIn = + [ Just (PacketStreamM2S (0xAB :> Nil) Nothing () False) , Just (PacketStreamM2S (0xCD :> Nil) (Just 0) () False) , Just (PacketStreamM2S (0x01 :> Nil) Nothing () False) , Just (PacketStreamM2S (0x01 :> Nil) Nothing () False) @@ -65,17 +52,20 @@ fwdIn = [ , Just (PacketStreamM2S (0x01 :> Nil) Nothing () False) , Just (PacketStreamM2S (0x01 :> Nil) Nothing () False) , Just (PacketStreamM2S (0x01 :> Nil) Nothing () False) - , Just (PacketStreamM2S (0x01 :> Nil) Nothing () False)] L.++ L.repeat Nothing + , Just (PacketStreamM2S (0x01 :> Nil) Nothing () False) + ] + L.++ L.repeat Nothing bwdIn :: [PacketStreamS2M] bwdIn = fmap PacketStreamS2M (L.repeat True) expectedFwdOut :: [Maybe (PacketStreamM2S 1 ())] -expectedFwdOut = [ - Just (PacketStreamM2S (0xAB :> Nil) Nothing () False) - , Just (PacketStreamM2S (0xCD :> Nil) (Just 0) () False)] - L.++ L.replicate 12 Nothing - L.++ [Just (PacketStreamM2S (0x01 :> Nil) Nothing () False)] +expectedFwdOut = + [ Just (PacketStreamM2S (0xAB :> Nil) Nothing () False) + , Just (PacketStreamM2S (0xCD :> Nil) (Just 0) () False) + ] + L.++ L.replicate 12 Nothing + L.++ [Just (PacketStreamM2S (0x01 :> Nil) Nothing () False)] expectedBwdOut :: [PacketStreamS2M] expectedBwdOut = fmap PacketStreamS2M ([True, True] L.++ L.replicate 12 False L.++ [True]) @@ -92,7 +82,8 @@ en = enableGen fwdOut :: Signal System (Maybe (PacketStreamM2S 1 ())) bwdOut :: Signal System PacketStreamS2M (bwdOut, fwdOut) = toSignals ckt (fromList fwdIn, fromList bwdIn) - where ckt = exposeClockResetEnable (interpacketGapInserterC d12) clk rst en + where + ckt = exposeClockResetEnable (interpacketGapInserterC d12) clk rst en prop_12_cycles_no_data_after_last :: Property prop_12_cycles_no_data_after_last = property $ @@ -104,6 +95,7 @@ prop_12_cycles_backpressure_after_last = property $ tests :: TestTree tests = - localOption (mkTimeout 12_000_000 {- 12 seconds -}) - $ localOption (HedgehogTestLimit (Just 1_000)) - $(testGroupGenerator) + localOption (mkTimeout 20_000_000 {- 20 seconds -}) $ + localOption + (HedgehogTestLimit (Just 1_000)) + $(testGroupGenerator) diff --git a/test/Test/Cores/Ethernet/Mac/PaddingInserter.hs b/test/Test/Cores/Ethernet/Mac/PaddingInserter.hs index ec2b463..6d547c2 100644 --- a/test/Test/Cores/Ethernet/Mac/PaddingInserter.hs +++ b/test/Test/Cores/Ethernet/Mac/PaddingInserter.hs @@ -1,79 +1,89 @@ -{-# language FlexibleContexts #-} -{-# language NumericUnderscores #-} -{-# language RecordWildCards #-} +{-# LANGUAGE NumericUnderscores #-} -module Test.Cores.Ethernet.Mac.PaddingInserter where +module Test.Cores.Ethernet.Mac.PaddingInserter ( + tests, +) where -import Prelude +import Clash.Cores.Ethernet.Mac.PaddingInserter -import Clash.Prelude ( type (<=) ) -import qualified Clash.Prelude as C +import Clash.Prelude -import Hedgehog -import qualified Hedgehog.Range as Range +import qualified Data.List as L -import Test.Tasty -import Test.Tasty.Hedgehog ( HedgehogTestLimit(HedgehogTestLimit) ) -import Test.Tasty.Hedgehog.Extra ( testProperty ) -import Test.Tasty.TH ( testGroupGenerator ) +import Hedgehog (Property) +import qualified Hedgehog.Range as Range -import Protocols -import Protocols.PacketStream import Protocols.Hedgehog +import Protocols.PacketStream import Protocols.PacketStream.Hedgehog -import Clash.Cores.Ethernet.Mac.PaddingInserter +import Test.Tasty +import Test.Tasty.Hedgehog (HedgehogTestLimit (HedgehogTestLimit)) +import Test.Tasty.Hedgehog.Extra (testProperty) +import Test.Tasty.TH (testGroupGenerator) +paddingInserterModel :: + forall (dataWidth :: Nat). + (KnownNat dataWidth) => + (1 <= dataWidth) => + Int -> + [PacketStreamM2S dataWidth ()] -> + [PacketStreamM2S dataWidth ()] +paddingInserterModel padBytes fragments = + L.concatMap + (upConvert . fullPackets . insertPadding) + (chunkByPacket $ downConvert fragments) + where + padding = + PacketStreamM2S + { _data = repeat 0x00 + , _last = Nothing + , _meta = () + , _abort = False + } -model - :: forall (dataWidth :: C.Nat) - . C.KnownNat dataWidth - => 1 <= dataWidth - => Int - -> [PacketStreamM2S dataWidth ()] - -> [PacketStreamM2S dataWidth ()] -model padBytes fragments = concatMap (upConvert . setLasts . insertPadding) $ chunkByPacket $ downConvert fragments - where - insertPadding pkts = pkts ++ replicate (paddingNeeded pkts) padding - paddingNeeded pkts = max 0 (padBytes - length pkts) - padding = PacketStreamM2S {_data = C.repeat 0, _last = Nothing, _meta = (), _abort = False} - setLasts pkts = map (\pkt -> pkt{_last = Nothing}) (init pkts) ++ [(last pkts){_last = Just 0}] + insertPadding xs = + L.init xs + L.++ ( (L.last xs){_last = Nothing} + : L.replicate (max 0 (padBytes - L.length xs)) padding + ) -- | Test the padding inserter. -paddingInserterTest - :: forall dataWidth padBytes - . C.KnownNat padBytes - => 1 <= dataWidth - => 1 <= padBytes - => C.SNat dataWidth - -> C.SNat padBytes - -> Property -paddingInserterTest C.SNat padBytes = - propWithModelSingleDomain - @C.System +paddingInserterTest :: + forall dataWidth padBytes. + (KnownNat padBytes) => + (1 <= dataWidth) => + (1 <= padBytes) => + SNat dataWidth -> + SNat padBytes -> + Property +paddingInserterTest SNat padBytes = + idWithModelSingleDomain + @System defExpectOptions - (genValidPackets (Range.linear 1 10) (Range.linear 0 10) Abort) - (C.exposeClockResetEnable (model $ C.natToNum @padBytes)) - (C.exposeClockResetEnable @C.System ckt) - (===) - where - ckt :: forall (dom :: C.Domain) - . C.HiddenClockResetEnable dom - => Circuit (PacketStream dom dataWidth ()) (PacketStream dom dataWidth ()) - ckt = paddingInserterC padBytes + (genPackets (Range.linear 1 10) Abort (genValidPacket (pure ()) (Range.linear 0 10))) + (exposeClockResetEnable (paddingInserterModel $ natToNum @padBytes)) + (exposeClockResetEnable (paddingInserterC @dataWidth padBytes)) + +-- | dataWidth ~ padBytes +prop_paddinginserter_d1 :: Property +prop_paddinginserter_d1 = paddingInserterTest d1 d1 + +-- | dataWidth % padBytes ~ 0 +prop_paddinginserter_d2 :: Property +prop_paddinginserter_d2 = paddingInserterTest d2 d26 + +-- | dataWidth % padBytes > 0 +prop_paddinginserter_d7 :: Property +prop_paddinginserter_d7 = paddingInserterTest d7 d26 --- We test the edge case dataWidth = padBytes = 1, --- a case where dataWidth divides padBytes, --- a case where dataWidth does not divide padBytes, and --- a case where dataWidth is more than padBytes. -prop_paddinginserter_d1, prop_paddinginserter_d2, prop_paddinginserter_d5, prop_paddinginserter_d50 :: Property -prop_paddinginserter_d1 = paddingInserterTest C.d1 C.d1 -prop_paddinginserter_d2 = paddingInserterTest C.d2 C.d46 -prop_paddinginserter_d5 = paddingInserterTest C.d5 C.d46 -prop_paddinginserter_d50 = paddingInserterTest C.d50 C.d46 +-- | dataWidth > padBytes +prop_paddinginserter_d20 :: Property +prop_paddinginserter_d20 = paddingInserterTest d20 d10 tests :: TestTree tests = - localOption (mkTimeout 12_000_000 {- 12 seconds -}) - $ localOption (HedgehogTestLimit (Just 1_000)) - $(testGroupGenerator) + localOption (mkTimeout 20_000_000 {- 20 seconds -}) $ + localOption + (HedgehogTestLimit (Just 1_000)) + $(testGroupGenerator)