Artturin/RiscV-Formal
1
0
Fork 0
forked from Yehowshua/RiscV-Formal
Code Pull requests Activity

correct behavior of R type in execute

Browse source
This commit is contained in:
Yehowshua Immanuel 2025-03-13 16:26:03 -04:00
parent 4428f7f196
commit a76d6e24ec
1 changed files with 6 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
hs/Execute.hs
View file

@ -61,15 +61,18 @@ execute (Opcode opcode addr) = case opcode of
SLL (RTypeFields rd _ rs1 rs2 _) -> SLL (RTypeFields rd _ rs1 rs2 _) ->
let val1 = extractRegVal rs1 let val1 = extractRegVal rs1
val2 = extractRegVal rs2 val2 = extractRegVal rs2
in WriteBackGPR rd (val1 `shiftL` fromIntegral val2) shftAmt = fromIntegral |> slice d5 d0 val2
in WriteBackGPR rd (val1 `shiftL` shftAmt)
SRL (RTypeFields rd _ rs1 rs2 _) -> SRL (RTypeFields rd _ rs1 rs2 _) ->
let val1 = extractRegVal rs1 let val1 = extractRegVal rs1
val2 = extractRegVal rs2 val2 = extractRegVal rs2
in WriteBackGPR rd (val1 `shiftR` fromIntegral val2) shftAmt = fromIntegral |> slice d5 d0 val2
in WriteBackGPR rd (val1 `shiftR` shftAmt)
SRA (RTypeFields rd _ rs1 rs2 _) -> SRA (RTypeFields rd _ rs1 rs2 _) ->
let val1 = unpack (pack (extractRegVal rs1) :: BitVector 64) :: Signed 64 let val1 = unpack (pack (extractRegVal rs1) :: BitVector 64) :: Signed 64
val2 = extractRegVal rs2 val2 = extractRegVal rs2
in WriteBackGPR rd (bitCoerce (val1 `shiftR` fromIntegral val2)) shftAmt = fromIntegral |> slice d5 d0 val2
in WriteBackGPR rd (bitCoerce (val1 `shiftR` shftAmt))
SLT (RTypeFields rd _ rs1 rs2 _) -> SLT (RTypeFields rd _ rs1 rs2 _) ->
let val1 = unpack (pack (extractRegVal rs1) :: BitVector 64) :: Signed 64 let val1 = unpack (pack (extractRegVal rs1) :: BitVector 64) :: Signed 64
val2 = unpack (pack (extractRegVal rs2) :: BitVector 64) :: Signed 64 val2 = unpack (pack (extractRegVal rs2) :: BitVector 64) :: Signed 64