Yehowshua/RiscV-Formal
Archived
2
0
Fork 0
Code Issues 8 Pull requests Projects Releases Packages Wiki Activity Actions

first commit

Browse source
This commit is contained in:
Yehowshua Immanuel 2025-02-12 23:54:15 -05:00
commit ef58d5b07e
34 changed files with 2210 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

44
hs/Util.hs Normal file
View file

@ -0,0 +1,44 @@
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ConstraintKinds #-}
module Util(
powerIndex32,
powerIndex64,
endianSwapWord) where
import Clash.Prelude
import Types(FullWord)
data ValidIndex32 (n :: Nat) where
ValidIndex32 :: (0 <= n, n <= 31) => SNat n -> ValidIndex32 n
mkValidIndex32 :: forall n. (KnownNat n, 0 <= n, n <= 31) => ValidIndex32 n
mkValidIndex32 = ValidIndex32 $ SNat @n
powerIndex32 :: forall n. (KnownNat n, 0 <= n, n <= 31) => SNat (31 - n)
powerIndex32 = case mkValidIndex32 @n of
ValidIndex32 _ -> SNat @(31 - n)
data ValidIndex63 (n :: Nat) where
ValidIndex63 :: (0 <= n, n <= 63) => SNat n -> ValidIndex63 n
mkValidIndex64 :: forall n. (KnownNat n, 0 <= n, n <= 63) => ValidIndex63 n
mkValidIndex64 = ValidIndex63 $ SNat @n
powerIndex64 :: forall n. (KnownNat n, 0 <= n, n <= 63) => SNat (63 - n)
powerIndex64 = case mkValidIndex64 @n of
ValidIndex63 _ -> SNat @(63 - n)
endianSwapWord :: FullWord -> FullWord
endianSwapWord x =
(byte0 `shiftL` 24) .|.
(byte1 `shiftL` 16) .|.
(byte2 `shiftL` 8) .|.
byte3
where
byte0 = (x .&. 0x000000FF)
byte1 = (x .&. 0x0000FF00) `shiftR` 8
byte2 = (x .&. 0x00FF0000) `shiftR` 16
byte3 = (x .&. 0xFF000000) `shiftR` 24