diff --git a/bittide/src/Bittide/DoubleBufferedRAM.hs b/bittide/src/Bittide/DoubleBufferedRAM.hs index 88a9e3c87..3c9004d5a 100644 --- a/bittide/src/Bittide/DoubleBufferedRAM.hs +++ b/bittide/src/Bittide/DoubleBufferedRAM.hs @@ -2,7 +2,7 @@ -- -- SPDX-License-Identifier: Apache-2.0 -{-# OPTIONS_GHC -fconstraint-solver-iterations=5#-} +{-# OPTIONS_GHC -fconstraint-solver-iterations=6#-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE NamedFieldPuns #-} @@ -99,13 +99,14 @@ blockRamByteAddressable initRAM readAddr newEntry byteSelect = writeBytes = unbundle $ splitWriteInBytes <$> newEntry <*> byteSelect readBytes = bundle $ (`blockRam` readAddr) <$> initBytes <*> writeBytes +-- | register with wishbone interface, the third argument determines the source of the +-- output signal. If the third argument is Just (Signal dom a), writing from the wishbone +-- bus to the register is not possible. registerWB :: forall dom a bs aw . ( HiddenClockResetEnable dom , Paddable a - , KnownNat (Regs a (bs * 8)) , 1 <= (Regs a (bs * 8)) - , Regs a 8 ~ (bs * Regs a (bs*8)) , KnownNat bs , 1 <= bs , KnownNat aw @@ -136,11 +137,15 @@ registerWB initVal wbIn (Just newVal) = unbundle . mealy go initVal $ bundle (ne registerWB initVal wbIn Nothing = (regOut, wbOut) where - regOut = registerByteAddressable initVal (repeatedBVsAsData <$> wbIn) byteEnables + regOut = andEnable (writeEnable <$> wbIn) $ registerByteAddressable initVal (repeatedBVsAsData <$> wbIn) byteEnables repeatedBVsAsData = registersToData . RegisterBank . repeat . writeData (byteEnables, wbOut) = unbundle $ go <$> regOut <*> wbIn - go val WishboneM2S{..} = (pack byteEnables0, WishboneS2M{acknowledge, err, readData}) + go :: + a -> + WishboneM2S bs aw -> + (BitVector (Regs a 8), WishboneS2M bs) + go val WishboneM2S{..} = (resize $ pack byteEnables0, WishboneS2M{acknowledge, err, readData}) where (alignedAddress, alignment) = split @_ @(aw - 2) @2 addr wordAligned = alignment == 0 @@ -153,7 +158,7 @@ registerWB initVal wbIn Nothing = (regOut, wbOut) wbAddr :: Index (Regs a (bs * 8)) wbAddr = unpack . resize $ pack alignedAddress - byteEnables0 = replace wbAddr busSelect (repeat 0) + byteEnables0 = reverse $ replace wbAddr busSelect (repeat @(Regs a (bs*8)) 0) readData = case paddedToRegisters $ Padded val of RegisterBank vec -> vec !! wbAddr diff --git a/bittide/tests/Tests/DoubleBufferedRAM.hs b/bittide/tests/Tests/DoubleBufferedRAM.hs index 4dfec7453..a03a22f0d 100644 --- a/bittide/tests/Tests/DoubleBufferedRAM.hs +++ b/bittide/tests/Tests/DoubleBufferedRAM.hs @@ -27,13 +27,16 @@ import Test.Tasty.Hedgehog import qualified Data.List as L import qualified Data.Set as Set import qualified GHC.TypeNats as TN -import qualified Hedgehog.Gen as Gen +import qualified Hedgehog.Gen as Gen hiding (resize) import qualified Prelude as P +import Data.Proxy +import Data.Type.Equality (type (:~:)(Refl)) +import Contranomy.Wishbone +import Data.String import Bittide.SharedTypes import Bittide.DoubleBufferedRAM import Clash.Hedgehog.Sized.Index -import Data.String ramGroup :: TestTree ramGroup = testGroup "DoubleBufferedRAM group" @@ -48,7 +51,11 @@ ramGroup = testGroup "DoubleBufferedRAM group" , testPropertyNamed "Byte addressable double buffered blockRam matches behavioral model." "doubleBufferedRAMByteAddressable0" doubleBufferedRAMByteAddressable0 , testPropertyNamed "Byte addressable double buffered blockRam with always high byteEnables behaves like 'doubleBufferedRAM'" - "doubleBufferedRAMByteAddressable1" doubleBufferedRAMByteAddressable1] + "doubleBufferedRAMByteAddressable1" doubleBufferedRAMByteAddressable1 + , testPropertyNamed "Byte addressable register can be written to and read from with byte enables." + "readWriteRegisterByteAddressable" readWriteRegisterByteAddressable + , testPropertyNamed "registerWB can be written to and read from with byte enables." + "registerWBWriteWishbone" registerWBWriteWishbone] genRamContents :: (MonadGen m, Integral i) => i -> m a -> m (SomeVec 1 a) genRamContents depth = genSomeVec (Range.singleton $ fromIntegral (depth - 1)) @@ -232,6 +239,86 @@ doubleBufferedRAMByteAddressable1 = property $ do (duvOut, refOut) = L.unzip simOut duvOut === refOut +readWriteRegisterByteAddressable :: Property +readWriteRegisterByteAddressable = property $ do + bytes <- forAll $ Gen.enum 1 10 + case TN.someNatVal bytes of + SomeNat p -> case compareSNat d1 (snatProxy p) of + SNatLE -> go p + _ -> error "readWriteRegisterByteAddressable: Amount of bytes == 0." + where + go :: forall bytes m . (KnownNat bytes, 1 <= bytes, KnownNat (bytes*8), 1 <= (bytes * 8), Monad m) => Proxy bytes -> PropertyT m () + go Proxy = + case sameNat (Proxy @bytes) (Proxy @(Regs (Vec bytes Byte) 8)) of + Just Refl -> do + simLength <- forAll $ Gen.enum 1 100 + let + writeGen = genNonEmptyVec @_ @bytes $ genDefinedBitVector @_ @8 + initVal <- forAll writeGen + writes <- forAll $ Gen.list (Range.singleton simLength) writeGen + byteEnables <- forAll $ Gen.list (Range.singleton simLength) $ genDefinedBitVector @_ @(Regs (Vec bytes Byte) 8) + let + topEntity (unbundle -> (newVal, byteEnable))= + withClockResetEnable @System clockGen resetGen enableGen $ + registerByteAddressable initVal newVal byteEnable + expectedOut = P.scanl simFunc initVal $ P.zip writes byteEnables + simFunc olds (news,unpack -> bools) = (\(bool,old,new) -> if bool then new else old) <$> zip3 bools olds news + simOut = simulateN simLength topEntity $ P.zip writes byteEnables + simOut === P.take simLength expectedOut + _ -> error "readWriteRegisterByteAddressable: Amount of bytes not equal to registers required." + +-- | +registerWBWriteWishbone :: Property +registerWBWriteWishbone = property $ do + bits <- forAll $ Gen.enum 1 100 + case TN.someNatVal bits of + SomeNat p -> case compareSNat d1 (snatProxy p) of + SNatLE -> go p + _ -> error "registerWBWriteWishbone: Amount of bits == 0." + where + go :: forall bits m . (KnownNat bits, 1 <= bits, Monad m) => Proxy bits -> PropertyT m () + go Proxy = case compareSNat d1 $ SNat @(Regs (BitVector bits) 32) of + SNatLE -> do + let regs = (natToNum @(DivRU bits 32)) + initVal <- forAll $ genDefinedBitVector @_ @bits + writes <- forAll $ Gen.list (Range.constant 1 25) $ genDefinedBitVector @_ @bits + let + simLength = L.length writes * regs + 1 + topEntity wbIn = fst $ withClockResetEnable clockGen resetGen enableGen $ + registerWB @System @_ @4 @32 initVal wbIn Nothing + topEntityInput = L.concatMap wbWrite writes <> L.repeat idleM2S + simOut = L.tail $ simulateN simLength topEntity topEntityInput + filteredOut = everyNth regs simOut + footnote . fromString $ "simOut: " <> showX simOut + footnote . fromString $ "filteredOut:" <> showX filteredOut + footnote . fromString $ "input:" <> showX (L.take simLength topEntityInput) + footnote . fromString $ "expected" <> showX writes + writes === filteredOut + _ -> error "registerWBWriteWishbone: Registers required to store bitvector == 0." + where + wbWrite v = L.zipWith bv2WbWrite (L.reverse [0.. L.length l - 1]) l + where + RegisterBank (toList -> l) = paddedToRegisters $ Padded v + everyNth n l | L.length l >= n = x : everyNth n xs + | otherwise = [] + where + (x:xs) = L.drop (n-1) l + +bv2WbWrite :: (BitPack a, Enum a) => + a + -> ("DAT_MOSI" ::: BitVector 32) + -> WishboneM2S 4 32 +bv2WbWrite i v = (wishboneM2S @4 @32 SNat SNat) + { addr = resize (pack i) ++# (0b00 :: BitVector 2) + , writeData = v + , writeEnable = True + , busCycle = True + , busSelect = maxBound + } + +idleM2S :: (KnownNat aw, KnownNat bs) => WishboneM2S bs aw +idleM2S = wishboneM2S SNat SNat + -- | Model for 'byteAddressableRAM', it stores the inputs in its state for a one cycle delay -- and updates the RAM based on the the write operation and byte enables. -- Furthermore it contains read-before-write behavior based on the readAddr. @@ -254,10 +341,10 @@ byteAddressableRAMBehavior :: forall bits depth bytes . byteAddressableRAMBehavior state input = (state', ram !! readAddr) where ((readAddr, writeOp, byteEnable), ram) = state - (writeAddr, writeData) = fromMaybe (0, 0b0) writeOp + (writeAddr, writeData0) = fromMaybe (0, 0b0) writeOp writeTrue = isJust writeOp RegisterBank oldData = getRegs $ ram !! writeAddr - RegisterBank newData = getRegs writeData + RegisterBank newData = getRegs writeData0 newEntry = getData $ zipWith (\ sel (old,new) -> if sel then new else old) (unpack byteEnable) $ zip oldData newData @@ -295,13 +382,12 @@ byteAddressableDoubleBufferedRAMBehavior state input = (state', pack $ bufA0 !! ((switchBuffers, readAddr, writeOp, byteEnable), bufA, bufB) = state (bufA0, bufB0) = if switchBuffers then (bufB, bufA) else (bufA, bufB) - (writeAddr, writeData) = fromMaybe (0, 0b0) writeOp + (writeAddr, writeData0) = fromMaybe (0, 0b0) writeOp writeTrue = isJust writeOp RegisterBank oldData = getRegs $ bufB0 !! writeAddr - RegisterBank newData = getRegs writeData - newEntry = getData $ zipWith - (\ sel (old,new) -> if sel then new else old) - (unpack byteEnable) $ zip oldData newData + RegisterBank newData = getRegs writeData0 + newEntry = getData $ zipWith (\ sel (old,new) -> if sel then new else old) (unpack byteEnable) $ + zip oldData newData bufB1 = if writeTrue then replace writeAddr newEntry bufB0 else bufB0 state' = (input, bufA0, bufB1) diff --git a/contranomy/src/Contranomy/Wishbone.hs b/contranomy/src/Contranomy/Wishbone.hs index e362e5790..7a867d553 100644 --- a/contranomy/src/Contranomy/Wishbone.hs +++ b/contranomy/src/Contranomy/Wishbone.hs @@ -37,7 +37,7 @@ data WishboneM2S bytes addressWidth , cycleTypeIdentifier :: "CTI" ::: CycleTypeIdentifier -- | BTE , burstTypeExtension :: "BTE" ::: BurstTypeExtension - } deriving (Generic, NFDataX, Show, Eq) + } deriving (Generic, NFDataX, Show, Eq, ShowX) data WishboneS2M bytes = WishboneS2M @@ -47,9 +47,9 @@ data WishboneS2M bytes , acknowledge :: "ACK" ::: Bool -- | ERR , err :: "ERR" ::: Bool - } deriving (Generic, NFDataX, Show, Eq) + } deriving (Generic, NFDataX, Show, Eq, ShowX) -newtype CycleTypeIdentifier = CycleTypeIdentifier (BitVector 3) deriving (Generic, NFDataX, Show, Eq) +newtype CycleTypeIdentifier = CycleTypeIdentifier (BitVector 3) deriving (Generic, NFDataX, Show, Eq, ShowX) pattern Classic, ConstantAddressBurst, IncrementingBurst, EndOfBurst :: CycleTypeIdentifier pattern Classic = CycleTypeIdentifier 0 @@ -62,7 +62,7 @@ data BurstTypeExtension | Beat4Burst | Beat8Burst | Beat16Burst - deriving (Generic, NFDataX, Show, Eq) + deriving (Generic, NFDataX, Show, Eq, ShowX) wishboneM2S :: SNat bytes -> SNat addressWidth -> WishboneM2S bytes addressWidth wishboneM2S SNat SNat = WishboneM2S