Generalize XLEN.

It's not RV64I yet, for it has no `*w` instructions (`addw` and such).

Author: strake

lion-formal/src/LionFV.hs

@@ -6,6 +6,9 @@ License     : BSD-3-Clause
 Maintainer  : [email protected]
 -}
 
+{-# 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  : [email protected]
 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/src/Bus.hs

@@ -50,21 +50,21 @@ data BusOut (p :: Peripheral) where
   FromSpram :: BitVector 32 -> BusOut 'Spram
   FromSpi   :: BitVector 32 -> BusOut 'Spi
 
-romMap :: Maybe ToMem -> BusIn 'Rom
+romMap :: Maybe (ToMem 32) -> BusIn 'Rom
 romMap = ToRom . wordAddr . maybe 0 memAddress
   where
     wordAddr :: BitVector 32 -> Unsigned 8
     wordAddr a = unpack $ slice d7 d0 $ a `shiftR` 2
 
-uartMap :: Peripheral -> Maybe ToMem -> BusIn 'Uart
+uartMap :: Peripheral -> Maybe (ToMem 32) -> BusIn 'Uart
 uartMap Uart (Just (ToMem DataMem _ msk wrM)) = ToUart (slice d2 d0 msk) $ slice d7 d0 <$> wrM
 uartMap _ _ = ToUart 0 Nothing
 
-ledMap :: Peripheral -> Maybe ToMem -> BusIn 'Led
+ledMap :: Peripheral -> Maybe (ToMem 32) -> BusIn 'Led
 ledMap Led (Just (ToMem _ _ $(bitPattern "..11") (Just d))) = ToLed (slice d11 d8 d) (slice d7 d0 d) True
 ledMap _ _ = ToLed 0 0 False
 
-spramMap :: Peripheral -> Maybe ToMem -> BusIn 'Spram
+spramMap :: Peripheral -> Maybe (ToMem 32) -> BusIn '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
@@ -78,11 +78,11 @@ spramMap periph (Just mem) = case (periph, memWrite mem) of
           | b == high = 0b11
           | otherwise = 0b00
 
-spiMap :: Peripheral -> Maybe ToMem -> BusIn 'Spi
+spiMap :: Peripheral -> Maybe (ToMem 32) -> BusIn 'Spi
 spiMap Spi (Just (ToMem DataMem _ mask wrM)) = ToSpi mask wrM
 spiMap _   _                                 = ToSpi 0    Nothing 
 
-selectPeripheral :: Maybe ToMem -> Peripheral
+selectPeripheral :: Maybe (ToMem 32) -> Peripheral
 selectPeripheral Nothing = Rom
 selectPeripheral (Just toMem)
   | checkRegion 17 = Spram

lion.cabal

@@ -24,6 +24,7 @@ library
   other-modules:   Lion.Alu
                  , Lion.Instruction
                  , Lion.Pipe
+                 , Lion.Util.Clash
   hs-source-dirs: src
   default-language: Haskell2010
   build-depends: 

src/Lion/Alu.hs

@@ -11,44 +11,46 @@ Configurable alu, choose between soft and hard adders/subtractors
 module Lion.Alu where
 
 import Clash.Prelude
+import Data.Bool ( bool )
 import Data.Function ( on )
 import Data.Proxy
 import Ice40.Mac 
 import Lion.Instruction
+import Lion.Util.Clash
 
 -- | ALU configuration
 data AluConfig = Hard -- ^ use hard adder and subtractor from iCE40 SB_MAC16
                | Soft -- ^ use generic adder and subtractor: (+) and (-)
   deriving stock (Generic, Show, Eq)
 
-class Alu (config :: AluConfig) where
-  alu :: HiddenClockResetEnable dom 
+class Alu (xl :: Nat) (config :: AluConfig) where
+  alu :: (KnownNat xl, KnownNat (Log2 xl))
+      => HiddenClockResetEnable dom 
       => Proxy (config :: AluConfig)
       -> Signal dom Op
-      -> Signal dom (BitVector 32)
-      -> Signal dom (BitVector 32)
-      -> Signal dom (BitVector 32)
+      -> Signal dom (BitVector xl)
+      -> Signal dom (BitVector xl)
+      -> Signal dom (BitVector xl)
 
-instance Alu 'Soft where
+instance Alu xl 'Soft where
   alu _ op in1 = register 0 . liftA3 aluFunc op in1 
     where
       aluFunc = \case 
         Add  -> (+)
         Sub  -> (-)
         Sll  -> \x y -> x `shiftL` shamt y
-        Slt  -> boolToBV ... (<) `on` sign
-        Sltu -> boolToBV ... (<)
+        Slt  -> bool 0 1 ... (<) `on` sign
+        Sltu -> bool 0 1 ... (<)
         Xor  -> xor
         Srl  -> \x y -> x `shiftR` shamt y
         Sra  -> \x y -> pack $ sign x `shiftR` shamt y
         Or   -> (.|.)
         And  -> (.&.)
         where
-          shamt = unpack . resize . slice d4 d0
-          sign = unpack :: BitVector 32 -> Signed 32
+          shamt = fromEnum . resizeTo (SNat :: SNat (Log2 xl))
           (...) = (.).(.)
 
-instance Alu 'Hard where
+instance Alu 32 'Hard where
   alu _ op in1 in2 = mux isAddSub adderSubtractor $ register 0 $ baseAlu op in1 in2
     where
       isAdd = (Add == ) <$> op
@@ -57,24 +59,25 @@ instance Alu 'Hard where
       adderSubtractor = hardAddSub (boolToBit <$> isSub) in1 in2
 
 baseAlu
-  :: Signal dom Op
-  -> Signal dom (BitVector 32)
-  -> Signal dom (BitVector 32)
-  -> Signal dom (BitVector 32)
+  :: forall dom xl
+   . (KnownNat xl, KnownNat (Log2 xl))
+  => Signal dom Op
+  -> Signal dom (BitVector xl)
+  -> Signal dom (BitVector xl)
+  -> Signal dom (BitVector xl)
 baseAlu = liftA3 $ \case 
   Add  -> \_ _ -> 0
   Sub  -> \_ _ -> 0
   Sll  -> \x y -> x `shiftL` shamt y
-  Slt  -> boolToBV ... (<) `on` sign
-  Sltu -> boolToBV ... (<)
+  Slt  -> bool 0 1 ... (<) `on` sign
+  Sltu -> bool 0 1 ... (<)
   Xor  -> xor
   Srl  -> \x y -> x `shiftR` shamt y
   Sra  -> \x y -> pack $ sign x `shiftR` shamt y
   Or   -> (.|.)
   And  -> (.&.)
   where
-    shamt = unpack . resize . slice d4 d0
-    sign = unpack :: BitVector 32 -> Signed 32
+    shamt = fromEnum . resizeTo (SNat :: SNat (Log2 xl))
     (...) = (.).(.)
 
 -- | addSub32PipelinedUnsigned

src/Lion/Core.hs

@@ -5,7 +5,7 @@ Copyright   : (c) David Cox, 2021
 License     : BSD-3-Clause
 Maintainer  : [email protected]
 
-The Lion core is a 32-bit [RISC-V](https://riscv.org/about/) processor written in Haskell using [Clash](https://clash-lang.org). Note, all peripherals and memory must have single cycle latency. See [lion-soc](https://github.com/standardsemiconductor/lion/tree/main/lion-soc) for an example of using the Lion core in a system.
+The Lion core is a xl-bit [RISC-V](https://riscv.org/about/) processor written in Haskell using [Clash](https://clash-lang.org). Note, all peripherals and memory must have single cycle latency. See [lion-soc](https://github.com/standardsemiconductor/lion/tree/main/lion-soc) for an example of using the Lion core in a system.
 -}
 
 module Lion.Core 
@@ -49,20 +49,21 @@ defaultCoreConfig = CoreConfig
   }
 
 -- | Core outputs
-data FromCore dom = FromCore
-  { toMem  :: Signal dom (Maybe P.ToMem) -- ^ shared memory and instruction bus, output from core to memory and peripherals
-  , toRvfi :: Signal dom Rvfi -- ^ formal verification interface output, see [lion-formal](https://github.com/standardsemiconductor/lion/tree/main/lion-formal) for usage
+data FromCore dom xl = FromCore
+  { toMem  :: Signal dom (Maybe (P.ToMem xl)) -- ^ shared memory and instruction bus, output from core to memory and peripherals
+  , toRvfi :: Signal dom (Rvfi xl) -- ^ formal verification interface output, see [lion-formal](https://github.com/standardsemiconductor/lion/tree/main/lion-formal) for usage
   }
 
--- | RISC-V Core: RV32I
+-- | RISC-V Core: RV(32, 64)I
 core
-  :: forall a startPC dom
-   . HiddenClockResetEnable dom
-  => Alu a
-  => (KnownNat startPC, startPC <= 0xFFFFFFFF)
+  :: forall a startPC dom xl
+   . (KnownNat xl, KnownNat (Log2 xl), 1 <= Div xl 8)
+  => HiddenClockResetEnable dom
+  => Alu xl a
+  => (KnownNat startPC, startPC + 1 <= 2^xl)
   => CoreConfig (startPC :: Nat) (a :: AluConfig) -- ^ core configuration
-  -> Signal dom (BitVector 32)   -- ^ core input, from memory/peripherals
-  -> FromCore dom                -- ^ core output
+  -> Signal dom (BitVector xl)   -- ^ core input, from memory/peripherals
+  -> FromCore dom xl             -- ^ core output
 core config toCore = FromCore
   { toMem  = getFirst . P._toMem <$> fromPipe
   , toRvfi = fromMaybe mkRvfi . getFirst . P._toRvfi <$> fromPipe
@@ -87,11 +88,12 @@ core config toCore = FromCore
 
 -- | Register bank
 regBank
-  :: HiddenClockResetEnable dom
+  :: KnownNat xl
+  => HiddenClockResetEnable dom
   => Signal dom (Unsigned 5)                        -- ^ Rs1 Addr
   -> Signal dom (Unsigned 5)                        -- ^ Rs2 Addr
-  -> Signal dom (Maybe (Unsigned 5, BitVector 32))  -- ^ Rd Write
-  -> Unbundled dom (BitVector 32, BitVector 32)     -- ^ (Rs1Data, Rs2Data)
+  -> Signal dom (Maybe (Unsigned 5, BitVector xl))  -- ^ Rd Write
+  -> Unbundled dom (BitVector xl, BitVector xl)     -- ^ (Rs1Data, Rs2Data)
 regBank rs1Addr rs2Addr rdWrM = (regFile rs1Addr, regFile rs2Addr)
   where
     regFile = flip (readNew (blockRamPow2 (repeat 0))) rdWrM