Generalize XLEN.

lion-formal/src/LionFV.hs

@@ -6,6 +6,9 @@ License     : BSD-3-Clause
 Maintainer  : standardsemiconductor@gmail.com
 -}
 
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+
 module LionFV where
 
 import Clash.Prelude
@@ -17,13 +20,14 @@ import Lion.Rvfi            ( Rvfi )
 
 lionFV
   :: HiddenClockResetEnable dom
-  => Signal dom (BitVector 32)   -- ^ mem_rdata
+  => (KnownNat xl, KnownNat (Log2 xl), 1 <= Div xl 8)
+  => Signal dom (BitVector xl)   -- ^ mem_rdata
   -> ( Signal dom Bool           -- mem_valid
      , Signal dom Bool           -- mem_instr
-     , Signal dom (BitVector 32) -- mem_addr
-     , Signal dom (BitVector 32) -- mem_wdata
-     , Signal dom (BitVector 4)  -- mem_wstrb
-     , Signal dom Rvfi           -- rvfi
+     , Signal dom (BitVector xl) -- mem_addr
+     , Signal dom (BitVector xl) -- mem_wdata
+     , Signal dom (BitVector (Div xl 8)) -- mem_wstrb
+     , Signal dom (Rvfi xl)      -- rvfi
      )
 lionFV memRData = 
   ( memValid
@@ -41,7 +45,7 @@ lionFV memRData =
     memWData = fromMaybe 0 . (memWrite =<<) <$> toMem fromCore
     memWStrb = maybe 0 memByteMask <$> toMem fromCore
 
-isInstr :: ToMem -> Bool
+isInstr :: ToMem xl -> Bool
 isInstr = (== InstrMem) . memAccess
 
 {-# NOINLINE topEntity #-}
@@ -54,7 +58,7 @@ topEntity
      , "mem_addr"  ::: Signal System (BitVector 32)
      , "mem_wdata" ::: Signal System (BitVector 32)
      , "mem_wstrb" ::: Signal System (BitVector 4)
-     , "rvfi"      ::: Signal System Rvfi
+     , "rvfi"      ::: Signal System (Rvfi 32)
      )
 topEntity clk rst = exposeClockResetEnable lionFV clk rst enableGen
 makeTopEntityWithName 'topEntity "LionFV"

lion-metric/src/Metric.hs

@@ -8,6 +8,9 @@ Maintainer  : standardsemiconductor@gmail.com
 Core top entity to observe yosys metrics when synthesized for iCE40
 -}
 
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+
 module Metric where
 
 import Clash.Prelude
@@ -16,15 +19,16 @@ import Lion.Core
 
 metric 
   :: HiddenClockResetEnable dom 
-  => Signal dom (BitVector 32) 
-  -> Signal dom (Maybe ToMem)
+  => (KnownNat xl, KnownNat (Log2 xl), 1 <= Div xl 8)
+  => Signal dom (BitVector xl) 
+  -> Signal dom (Maybe (ToMem xl))
 metric = toMem . core defaultCoreConfig
 
 {-# NOINLINE topEntity #-}
 topEntity 
   :: "clk"     ::: Clock System 
   -> "rst"     ::: Reset System
   -> "fromMem" ::: Signal System (BitVector 32)
-  -> "toMem"   ::: Signal System (Maybe ToMem) 
+  -> "toMem"   ::: Signal System (Maybe (ToMem 32)) 
 topEntity clk rst = withClockResetEnable clk rst enableGen metric
 makeTopEntityWithName 'topEntity "Metric"

lion-soc/lion-soc.cabal

@@ -55,6 +55,7 @@ library
     ViewPatterns
     TemplateHaskell
     TypeOperators
+    ScopedTypeVariables
 
 executable soc
     main-is:          Main.hs

lion-soc/src/Bus.hs

@@ -21,68 +21,69 @@ data Peripheral = Rom
   deriving stock (Generic, Show, Eq)
   deriving anyclass NFDataX
 
-data BusIn (p :: Peripheral) where
+data BusIn xl (p :: Peripheral) where
   ToRom :: Unsigned 8 -- ^ ROM word address
-        -> BusIn 'Rom -- ^ ROM access
+        -> BusIn xl 'Rom -- ^ ROM access
 
   ToLed :: BitVector 4 -- ^ LED IP register address
         -> BitVector 8 -- ^ LED IP register write data
         -> Bool        -- ^ LED IP enable
-        -> BusIn 'Led  -- ^ LED access
+        -> BusIn xl 'Led  -- ^ LED access
 
   ToUart :: BitVector 3         -- ^ UART mask
          -> Maybe (BitVector 8) -- ^ UART write value
-         -> BusIn 'Uart         -- ^ UART access
+         -> BusIn xl 'Uart         -- ^ UART access
 
   ToSpram :: BitVector 15 -- ^ SPRAM address
-          -> BitVector 32 -- ^ SPRAM dataIn
-          -> BitVector 8  -- ^ SPRAM mask write enable
+          -> BitVector xl -- ^ SPRAM dataIn
+          -> BitVector (Div xl 4) -- ^ SPRAM mask write enable
           -> Bit          -- ^ SPRAM write enable
-          -> BusIn 'Spram -- ^ SPRAM access
+          -> BusIn xl 'Spram -- ^ SPRAM access
 
-  ToSpi :: BitVector 4          -- ^ SPI mask
-        -> Maybe (BitVector 32) -- ^ SPI read/write, read=Nothing, write=Just value
-        -> BusIn 'Spi           -- ^ SPI access
+  ToSpi :: BitVector (Div xl 8) -- ^ SPI mask
+        -> Maybe (BitVector xl) -- ^ SPI read/write, read=Nothing, write=Just value
+        -> BusIn xl 'Spi           -- ^ SPI access
 
-data BusOut (p :: Peripheral) where
-  FromRom   :: BitVector 32 -> BusOut 'Rom
-  FromUart  :: BitVector 32 -> BusOut 'Uart
-  FromSpram :: BitVector 32 -> BusOut 'Spram
-  FromSpi   :: BitVector 32 -> BusOut 'Spi
+data BusOut xl (p :: Peripheral) where
+  FromRom   :: BitVector xl -> BusOut xl 'Rom
+  FromUart  :: BitVector xl -> BusOut xl 'Uart
+  FromSpram :: BitVector xl -> BusOut xl 'Spram
+  FromSpi   :: BitVector xl -> BusOut xl 'Spi
 
-romMap :: Maybe ToMem -> BusIn 'Rom
+romMap :: forall xl . KnownNat xl => Maybe (ToMem xl) -> BusIn xl 'Rom
 romMap = ToRom . wordAddr . maybe 0 memAddress
   where
-    wordAddr :: BitVector 32 -> Unsigned 8
-    wordAddr a = unpack $ slice d7 d0 $ a `shiftR` 2
+    wordAddr :: BitVector xl -> Unsigned 8
+    wordAddr a = unpack $ resize $ a `shiftR` 2
 
-uartMap :: Peripheral -> Maybe ToMem -> BusIn 'Uart
-uartMap Uart (Just (ToMem DataMem _ msk wrM)) = ToUart (slice d2 d0 msk) $ slice d7 d0 <$> wrM
+uartMap :: KnownNat xl => Peripheral -> Maybe (ToMem xl) -> BusIn xl 'Uart
+uartMap Uart (Just (ToMem DataMem _ msk wrM)) = ToUart (resize msk) $ resize <$> wrM
 uartMap _ _ = ToUart 0 Nothing
 
-ledMap :: Peripheral -> Maybe ToMem -> BusIn 'Led
-ledMap Led (Just (ToMem _ _ $(bitPattern "..11") (Just d))) = ToLed (slice d11 d8 d) (slice d7 d0 d) True
+ledMap :: KnownNat xl => Peripheral -> Maybe (ToMem xl) -> BusIn xl 'Led
+ledMap Led (Just (ToMem _ _ $(bitPattern "..11") (Just d'))) = ToLed (slice d11 d8 d) (slice d7 d0 d) True
+  where d = resize d' :: BitVector 12
 ledMap _ _ = ToLed 0 0 False
 
-spramMap :: Peripheral -> Maybe ToMem -> BusIn 'Spram
+spramMap :: KnownNat xl => Peripheral -> Maybe (ToMem xl) -> BusIn xl 'Spram
 spramMap _      Nothing    = ToSpram 0 0 0 0
 spramMap periph (Just mem) = case (periph, memWrite mem) of
-  (Spram, Just wr) -> ToSpram wordAddr wr nybMask 1
+  (Spram, Just wr) -> ToSpram wordAddr wr (resize nybMask) 1
   _                -> ToSpram wordAddr 0 0 0
   where
-    wordAddr = slice d14 d0 $ memAddress mem `shiftR` 2
+    wordAddr = resize $ memAddress mem `shiftR` 2
     nybMask = concatBitVector# $ map expandBit $ bv2v $ memByteMask mem
       where
         expandBit :: Bit -> BitVector 2
         expandBit b
           | b == high = 0b11
           | otherwise = 0b00
 
-spiMap :: Peripheral -> Maybe ToMem -> BusIn 'Spi
+spiMap :: KnownNat xl => Peripheral -> Maybe (ToMem xl) -> BusIn xl 'Spi
 spiMap Spi (Just (ToMem DataMem _ mask wrM)) = ToSpi mask wrM
 spiMap _   _                                 = ToSpi 0    Nothing 
 
-selectPeripheral :: Maybe ToMem -> Peripheral
+selectPeripheral :: forall xl . KnownNat xl => Maybe (ToMem xl) -> Peripheral
 selectPeripheral Nothing = Rom
 selectPeripheral (Just toMem)
   | checkRegion 17 = Spram
@@ -91,16 +92,17 @@ selectPeripheral (Just toMem)
   | checkRegion  2 = Uart
   | otherwise      = Led
   where
-    checkRegion :: Index 32 -> Bool
+    checkRegion :: Index xl -> Bool
     checkRegion = bitToBool . (memAddress toMem !)
 
 busMapOut 
-  :: BusOut 'Rom 
-  -> BusOut 'Uart 
-  -> BusOut 'Spram 
-  -> BusOut 'Spi
+  :: KnownNat xl
+  => BusOut xl 'Rom 
+  -> BusOut xl 'Uart 
+  -> BusOut xl 'Spram 
+  -> BusOut xl 'Spi
   -> Peripheral 
-  -> BitVector 32
+  -> BitVector xl
 busMapOut (FromRom   fromBios) 
           (FromUart  fromUart) 
           (FromSpram fromSpram) 

lion-soc/src/Soc.hs

@@ -1,3 +1,6 @@
+{-# LANGUAGE PartialTypeSignatures #-}
+{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
+
 {-|
 Module      : Soc
 Description : Lion SoC on the VELDT
@@ -10,6 +13,7 @@ module Soc where
 
 import Clash.Prelude
 import Clash.Annotations.TH
+import Control.Applicative ((<|>))
 import Data.Functor ( (<&>) )
 import Ice40.Clock
 import Ice40.Osc ( hf12Mhz )
@@ -32,7 +36,7 @@ data FromSoc dom = FromSoc
 ---------
 type Rgb = ("red" ::: Bit, "green" ::: Bit, "blue" ::: Bit)
 
-rgb :: HiddenClock dom => Signal dom (BusIn 'Led) -> Signal dom Rgb
+rgb :: HiddenClock dom => Signal dom (BusIn xl 'Led) -> Signal dom Rgb
 rgb mem = rgbPrim "0b0" "0b111111" "0b111111" "0b111111" (pure 1) (pure 1) r g b
   where
     (r, g, b, _) = led (pure 1) wr addr en (pure True)
@@ -43,40 +47,33 @@ rgb mem = rgbPrim "0b0" "0b111111" "0b111111" "0b111111" (pure 1) (pure 1) r g b
 -- ROM --
 ----------
 bios
-  :: HiddenClockResetEnable dom
-  => Signal dom (BusIn 'Rom)
-  -> Signal dom (BusOut 'Rom)
-bios mem = fmap FromRom $ concat4 <$> b3 <*> b2 <*> b1 <*> b0
+  :: forall dom xl . HiddenClockResetEnable dom
+  => Signal dom (BusIn xl 'Rom)
+  -> Signal dom (BusOut xl 'Rom)
+bios mem = fmap FromRom $ resize . concatBitVector# <$> bs
   where
-    b3 = romFilePow2 "_build/bios/bios.rom3" addr
-    b2 = romFilePow2 "_build/bios/bios.rom2" addr
-    b1 = romFilePow2 "_build/bios/bios.rom1" addr
-    b0 = romFilePow2 "_build/bios/bios.rom0" addr
+    bs :: Signal dom (Vec (Div xl 8) (BitVector 8))
+    bs = bundle $ (\ n -> romFilePow2 ("_build/bios/bios.rom" <|> show n) addr) <$> iterate (divSNat (SNat :: SNat xl) 8) succ (0 :: Int)
     addr = mem <&> \case
       ToRom a -> a
 
-concat4
-  :: KnownNat n
-  => BitVector n
-  -> BitVector n
-  -> BitVector n
-  -> BitVector n
-  -> BitVector (4 * n)
-concat4 b3 b2 b1 b0 = b3 ++# b2 ++# b1 ++# b0
-
 --------------
 -- Lion SoC --
 --------------
-{-# NOINLINE lion #-}
-lion :: HiddenClockResetEnable dom => Signal dom Bit -> FromSoc dom
-lion rxIn = FromSoc
+{-# NOINLINE lion32 #-}
+lion32 :: HiddenClockResetEnable dom => Signal dom Bit -> FromSoc dom
+lion32 = lion d32
+
+lion :: forall dom xl . (HiddenClockResetEnable dom, 1 <= Div xl 8, 1025 <= (2^xl)) => SNat xl -> Signal dom Bit -> FromSoc dom
+lion _ rxIn = FromSoc
   { rgbOut = fromRgb
   , txOut  = tx
   , spiIO  = spiio
   }
   where
     config :: CoreConfig 0x400 'Hard
     config = CoreConfig PipeConfig
+    fromBios :: _ (_ xl _)
     fromBios         = bios      $ romMap   <$> fromCore
     fromRgb          = rgb       $ ledMap   <$> peripheral <*> fromCore
     (tx, fromUart)   = uart rxIn $ uartMap  <$> peripheral <*> fromCore
@@ -97,7 +94,7 @@ lion rxIn = FromSoc
 topEntity 
   :: "uart_rx" ::: Signal Lattice12Mhz Bit
   -> FromSoc Lattice12Mhz
-topEntity = withClockResetEnable clk latticeRst enableGen lion
+topEntity = withClockResetEnable clk latticeRst enableGen lion32
   where
     clk = hf12Mhz (pure True :: Signal System Bool)
                   (pure True :: Signal System Bool)

lion-soc/src/Spi.hs

@@ -24,6 +24,7 @@ import Data.Monoid.Generic
 import qualified Ice40.Spi as S
 import Ice40.IO
 import Bus
+import Lion.Util.Clash
 
 data SpiIO = SpiIO ("biwo" ::: Bit)
                    ("bowi" ::: Bit)
@@ -32,24 +33,24 @@ data SpiIO = SpiIO ("biwo" ::: Bit)
   deriving stock (Generic, Show, Eq)
   deriving anyclass NFDataX
 
-data ToSysBus = ToSysBus
+data ToSysBus xl = ToSysBus
   { _sbAckO   :: Bool
   , _sbDatO   :: BitVector 8
-  , _fromCore :: BusIn 'Spi
+  , _fromCore :: BusIn xl 'Spi
   }
 makeLenses ''ToSysBus
 
-data FromSysBus = FromSysBus
+data FromSysBus xl = FromSysBus
   { _sbRWI  :: First Bool
   , _sbStbI :: First Bool
   , _sbAdrI :: First (BitVector 8)
   , _sbDatI :: First (BitVector 8)
-  , _toCore :: First (BitVector 32)
+  , _toCore :: First (BitVector xl)
   }
   deriving stock (Generic, Show, Eq)
   deriving anyclass NFDataX
-  deriving Semigroup via GenericSemigroup FromSysBus
-  deriving Monoid via GenericMonoid FromSysBus
+  deriving Semigroup via GenericSemigroup (FromSysBus xl)
+  deriving Monoid via GenericMonoid (FromSysBus xl)
 makeLenses ''FromSysBus
 
 data SysBus = SysBus 
@@ -63,7 +64,7 @@ makeLenses ''SysBus
 mkSysBus :: SysBus
 mkSysBus = SysBus Nothing 0
 
-sysBusM :: RWS ToSysBus FromSysBus SysBus ()
+sysBusM :: KnownNat xl => RWS (ToSysBus xl) (FromSysBus xl) SysBus ()
 sysBusM = do
   instr <- use sbInstr
 
@@ -87,22 +88,23 @@ sysBusM = do
         Just _  -> return () -- busy, ignore command
         Nothing ->           -- idle, execute command
           let isWrite = bitToBool $ wr!(16 :: Index 32)
-              adri = slice d15 d8 wr
-              dati = slice d7  d0 wr 
+              adri = slice' d15 d8 wr
+              dati = slice' d7  d0 wr
           in sbInstr ?= if isWrite
                then (adri, Just dati)
                else (adri, Nothing)
     ToSpi $(bitPattern "0100") Nothing -> -- read received
-      scribe toCore . First . Just =<< uses sbRecv ((`shiftL` 16).zeroExtend)
+      scribe toCore . First . Just =<< uses sbRecv ((`shiftL` 16).zeroResize)
     _ -> -- read status, default instruction
       scribe toCore $ First $ Just $ if isJust instr
         then 0x01000000
         else 0x00000000
 
 sysBus 
-  :: HiddenClockResetEnable dom
-  => Signal dom ToSysBus
-  -> Signal dom FromSysBus
+  :: KnownNat xl
+  => HiddenClockResetEnable dom
+  => Signal dom (ToSysBus xl)
+  -> Signal dom (FromSysBus xl)
 sysBus = mealy sysBusMealy mkSysBus
   where
     sysBusMealy s i = (s', o)
@@ -111,9 +113,9 @@ sysBus = mealy sysBusMealy mkSysBus
 
 {-# NOINLINE spi #-}
 spi
-  :: HiddenClockResetEnable dom
-  => Signal dom (BusIn 'Spi)
-  -> Unbundled dom (SpiIO, BusOut 'Spi)
+  :: (HiddenClockResetEnable dom, KnownNat xl)
+  => Signal dom (BusIn xl 'Spi)
+  -> Unbundled dom (SpiIO, BusOut xl 'Spi)
 spi toSpi = (spiIO, fromSpi)
   where
     fromSpi = fmap (FromSpi . fromMaybe 0) $ register Nothing $ getFirst . _toCore <$> fromSysBus