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

fixed execution of R type instructions

Browse source
This commit is contained in:
Yehowshua Immanuel 2025-03-13 14:31:38 -04:00
parent 7066df0936
commit 4428f7f196
3 changed files with 5 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
README.md
View file

@ -30,20 +30,9 @@ Change instructions to support Nix
riscv64-unknown-elf-objdump -D -b binary -m riscv:rv64 ./rv_tests/hello_world/hello.bin > hello.asm riscv64-unknown-elf-objdump -D -b binary -m riscv:rv64 ./rv_tests/hello_world/hello.bin > hello.asm
``` ```
# TODO # TODO
- [ ] fetch should invoke mem read function - [ ] fetch should invoke mem read function
# Organization Thoughts
- Potential functions
1. BitPat -> Opcode
2. Opcode -> Fields
3. Fields -> Field Vals
4. Field Vals -> Reg Vals
# Thoroughness
- [ ] Check that all forms get used!! Remove unused forms!!
# Grant Notes # Grant Notes
- [ ] Some forms may be redundant(may need to remove some) - [ ] Some forms may be redundant(may need to remove some)

8
hs/Execute.hs
View file

@ -61,15 +61,15 @@ 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 .&. 0x3F)) in WriteBackGPR rd (val1 `shiftL` fromIntegral val2)
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 .&. 0x3F)) in WriteBackGPR rd (val1 `shiftR` fromIntegral val2)
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 .&. 0x3F))) in WriteBackGPR rd (bitCoerce (val1 `shiftR` fromIntegral val2))
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
@ -209,4 +209,4 @@ execute (Opcode opcode addr) = case opcode of
in if rd /= 0 then WriteBackGPR rd (addr + 4) else Jump (addr + offset) in if rd /= 0 then WriteBackGPR rd (addr + 4) else Jump (addr + offset)
execute (Decode.DecodeException e addr) = Execute.DecodeException e addr execute (Decode.DecodeException e addr) = Execute.DecodeException e addr
execute (Decode.InstructionException e addr) = Execute.InstructionException e addr execute (Decode.InstructionException e addr) = Execute.InstructionException e addr

1
references.md Normal file
View file

@ -0,0 +1 @@
* [RISC-V Card](https://www.cs.sfu.ca/~ashriram/Courses/CS295/assets/notebooks/RISCV/RISCV_CARD.pdf)