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

prune more warnings and re-org Decode files a bit

Browse source
This commit is contained in:
Yehowshua Immanuel 2025-03-05 00:09:04 -05:00
parent 67b44dedc0
commit 7f7ba49ee1
4 changed files with 55 additions and 62 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

108
hs/Isa/Decode.hs → hs/Decode.hs
View file

@ -1,60 +1,28 @@
{-# LANGUAGE DataKinds #-} {-# LANGUAGE DataKinds #-}
{-# LANGUAGE NumericUnderscores #-} {-# LANGUAGE NumericUnderscores #-}
module Isa.Decode(decode) where module Decode(decode) where
import Isa.Forms(
FUNCT7, RS2, RS1, FUNCT3, RD, OPCODE,
IMM12, IMM13, IMM20, IMM21,
import DecodeTypes(
RTypeFields(..), ITypeFields(..), STypeFields(..), RTypeFields(..), ITypeFields(..), STypeFields(..),
BTypeFields(..), UTypeFields(..), JTypeFields(..), BTypeFields(..), UTypeFields(..), JTypeFields(..),
Opcode(..) Opcode(..)
) )
import Clash.Prelude import Clash.Prelude
import Data.Functor.Contravariant (Op) import Types(Insn)
import Types(Mem, Addr, Insn)
import Distribution.Backpack.FullUnitId (FullDb)
getOpcode :: Insn -> Unsigned 7 decode :: Insn -> Opcode
getOpcode instr = bitCoerce $ slice d6 d0 (pack instr) decode insn =
decodeRType insn `orElse`
getImm12 :: Insn -> Unsigned 12 decodeIType insn `orElse`
getImm12 instr = bitCoerce $ slice d31 d20 (pack instr) decodeSType insn `orElse`
decodeBType insn `orElse`
getImm12SType :: Insn -> Unsigned 12 decodeUType insn `orElse`
getImm12SType instr = bitCoerce $ immediateUpper ++# immediateLower decodeJType insn
where where
immediateUpper = (slice d31 d25 (pack instr)) orElse :: Opcode -> Opcode -> Opcode
immediateLower = (slice d11 d7 (pack instr)) orElse Unimplemented y = y
orElse x _ = x
getImm20UType :: Insn -> Unsigned 20
getImm20UType instr = bitCoerce $ slice d31 d12 (pack instr)
getImm13BType :: Insn -> Unsigned 13
getImm13BType instr = bitCoerce $ imm12 ++# imm10_5 ++# imm4_1 ++# imm11 ++# zero
where
imm12 = slice d31 d31 (pack instr) -- imm[12]
imm10_5 = slice d30 d25 (pack instr) -- imm[10:5]
imm4_1 = slice d11 d8 (pack instr) -- imm[4:1]
imm11 = slice d7 d7 (pack instr) -- imm[11]
zero = 0 :: BitVector 1 -- LSB always zero for B-type
getFunct3 :: Insn -> Unsigned 3
getFunct3 instr = bitCoerce $ slice d14 d12 (pack instr)
getFunct7 :: Insn -> Unsigned 7
getFunct7 instr = bitCoerce $ slice d31 d25 (pack instr)
getRd :: Insn -> Unsigned 5
getRd instr = bitCoerce $ slice d11 d7 (pack instr)
getRs2 :: Insn -> Unsigned 5
getRs2 instr = bitCoerce $ slice d24 d20 (pack instr)
getRs1 :: Insn -> Unsigned 5
getRs1 instr = bitCoerce $ slice d19 d15 (pack instr)
decodeRType :: Insn -> Opcode decodeRType :: Insn -> Opcode
decodeRType insn = decodeRType insn =
@ -192,15 +160,41 @@ decodeJType insn =
rd = getRd insn rd = getRd insn
imm21 = getImm21JType insn imm21 = getImm21JType insn
orElse :: Opcode -> Opcode -> Opcode getOpcode :: Insn -> Unsigned 7
orElse Unimplemented y = y getOpcode instr = bitCoerce $ slice d6 d0 (pack instr)
orElse x _ = x
decode :: Insn -> Opcode getImm12 :: Insn -> Unsigned 12
decode insn = getImm12 instr = bitCoerce $ slice d31 d20 (pack instr)
decodeRType insn `orElse`
decodeIType insn `orElse` getImm12SType :: Insn -> Unsigned 12
decodeSType insn `orElse` getImm12SType instr = bitCoerce $ immediateUpper ++# immediateLower
decodeBType insn `orElse` where
decodeUType insn `orElse` immediateUpper = (slice d31 d25 (pack instr))
decodeJType insn immediateLower = (slice d11 d7 (pack instr))
getImm20UType :: Insn -> Unsigned 20
getImm20UType instr = bitCoerce $ slice d31 d12 (pack instr)
getImm13BType :: Insn -> Unsigned 13
getImm13BType instr = bitCoerce $ imm12 ++# imm10_5 ++# imm4_1 ++# imm11 ++# zero
where
imm12 = slice d31 d31 (pack instr) -- imm[12]
imm10_5 = slice d30 d25 (pack instr) -- imm[10:5]
imm4_1 = slice d11 d8 (pack instr) -- imm[4:1]
imm11 = slice d7 d7 (pack instr) -- imm[11]
zero = 0 :: BitVector 1 -- LSB always zero for B-type
getFunct3 :: Insn -> Unsigned 3
getFunct3 instr = bitCoerce $ slice d14 d12 (pack instr)
getFunct7 :: Insn -> Unsigned 7
getFunct7 instr = bitCoerce $ slice d31 d25 (pack instr)
getRd :: Insn -> Unsigned 5
getRd instr = bitCoerce $ slice d11 d7 (pack instr)
getRs2 :: Insn -> Unsigned 5
getRs2 instr = bitCoerce $ slice d24 d20 (pack instr)
getRs1 :: Insn -> Unsigned 5
getRs1 instr = bitCoerce $ slice d19 d15 (pack instr)

3
hs/Isa/Forms.hs → hs/DecodeTypes.hs
View file

@ -1,7 +1,7 @@
{-# LANGUAGE DataKinds #-} {-# LANGUAGE DataKinds #-}
{-# LANGUAGE NumericUnderscores #-} {-# LANGUAGE NumericUnderscores #-}
module Isa.Forms( module DecodeTypes(
FUNCT7, RS2, RS1, FUNCT3, RD, OPCODE, FUNCT7, RS2, RS1, FUNCT3, RD, OPCODE,
IMM12, IMM13, IMM20, IMM21, IMM12, IMM13, IMM20, IMM21,
@ -11,7 +11,6 @@ module Isa.Forms(
Opcode(..) Opcode(..)
) where ) where
import Clash.Prelude import Clash.Prelude
import Types(Mem, Addr, Insn)
type FUNCT7 = Unsigned 7 type FUNCT7 = Unsigned 7
type RS2 = Unsigned 5 type RS2 = Unsigned 5

2
hs/Simulation.hs
View file

@ -20,7 +20,7 @@ import Cpu(
RISCVCPU(..), RISCVCPU(..),
riscvCPUInit) riscvCPUInit)
import Fetch(fetchInstruction, FetchResult (..)) import Fetch(fetchInstruction, FetchResult (..))
import Isa.Decode(decode) import Decode(decode)
data Args = Args { data Args = Args {
firmware :: FilePath firmware :: FilePath

4
rv_formal.cabal
View file

@ -87,8 +87,8 @@ library
exposed-modules: exposed-modules:
Simulation Simulation
other-modules: other-modules:
Isa.Decode, Decode,
Isa.Forms, DecodeTypes,
Peripherals.Ram, Peripherals.Ram,
Peripherals.Uart, Peripherals.Uart,
Peripherals.UartCFFI, Peripherals.UartCFFI,