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

Compare commits

base: Yehowshua:fa03829139735e544ef2b35a2590da990ded6aec
Branches Tags
Yehowshua:main
...
compare: Yehowshua:0960ceb53ac076d313d65d0279274a8b801f8a96
Branches Tags
Yehowshua:main

37 commits
fa03829139 ... 0960ceb53a

Author SHA1 Message Date
Artturin 0960ceb53a rv_tests/hello_world: Rename PREFIX var to CROSS_PREFIX and make it configurable 
And set it in devShell
 2025-03-14 01:17:11 +02:00
Artturin ac8a2ea238 flake.nix: Comments 2025-03-14 01:17:07 +02:00
Artturin 56a80fe749 Riscv config 2025-03-14 00:59:26 +02:00
Artturin 2b9895f1cc Use newer ghc 
Old output of
`cabal run main --ghc-options="-D_RAM_DEPTH=2048" -- --firmware=./rv_tests/hello_world/hello.bin`

```
Simulating Machine
Decoded instruction: AUIPC (UTypeFields 23 11 0) | Binary: 0b0000_0000_0000_0000_0000_0101_1001_0111 (1431)
Decoded instruction: ADDI (ITypeFields 19 11 0 11 28) | Binary: 0b0000_0001_1100_0101_1000_0101_1001_0011 (29722003)
Decoded instruction: LBU (ITypeFields 3 10 4 11 0) | Binary: 0b0000_0000_0000_0101_1100_0101_0000_0011 (378115)
Decoded instruction: Unimplemented | Binary: 0b0000_0010_1011_0111_1100_0101_0001_1001 (45597977)
Decoded instruction: Unimplemented | Binary: 0b1000_0000_0010_0011_0001_0000_0000_0000 (2149781504)
Decoded instruction: Unimplemented | Binary: 0b0000_0101_1000_0101_0000_0000_1010_0010 (92602530)
Decoded instruction: Unimplemented | Binary: 0b1010_0000_0000_0001_1011_1111_1100_0101 (2684469189)
Decoded instruction: Unimplemented | Binary: 0b0110_1100_0110_1100_0110_0101_0100_1000 (1819043144)
Decoded instruction: JAL (JTypeFields 111 24 975876) | Binary: 0b0111_0111_0010_0000_0010_1100_0110_1111 (1998597231)
Decoded instruction: JAL (JTypeFields 111 4 822670) | Binary: 0b0110_0100_0110_1100_0111_0010_0110_1111 (1684828783)
Decoded instruction: Unimplemented | Binary: 0b0000_0000_0000_0000_0000_1010_0010_0001 (2593)
Decoded instruction: Unimplemented | Binary: 0b0000_0000_0000_0000_0000_0000_0000_0000 (0)
Decoded instruction: Unimplemented | Binary: 0b0000_0000_0000_0000_0000_0000_0000_0000 (0)
Decoded instruction: Unimplemented | Binary: 0b0000_0000_0000_0000_0000_0000_0000_0000 (0)
Decoded instruction: Unimplemented | Binary: 0b0000_0000_0000_0000_0000_0000_0000_0000 (0)
Last state: Machine {cpu = RISCVCPU {pc = 60, gpr = 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> Nil, fpr = 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0:> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> Nil, privilegeLevel = MachineMode}, peripherals = Peripherals {ram = 3 :> 29722003 :> 378115 :> 45597977 :> 2149781504 :> 92602530 :> 2684469189 :> 1819043144 :> 1998597231 :> 1684828783 :> 2593 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> Nil}}
Executed for 16 cycles
Simulation complete
```

New output

```
Simulating Machine
Decoded instruction: AUIPC (UTypeFields 23 11 0) | Binary: 0b0000_0000_0000_0000_0000_0101_1001_0111 (1431)
Decoded instruction: ADDI (ITypeFields 19 11 0 11 28) | Binary: 0b0000_0001_1100_0101_1000_0101_1001_0011 (29722003)
Decoded instruction: LBU (ITypeFields 3 10 4 11 0) | Binary: 0b0000_0000_0000_0101_1100_0101_0000_0011 (378115)
Decoded instruction: Unimplemented | Binary: 0b0000_0010_1011_0111_1100_0101_0001_1001 (45597977)
Decoded instruction: Unimplemented | Binary: 0b1000_0000_0010_0011_0001_0000_0000_0000 (2149781504)
Decoded instruction: Unimplemented | Binary: 0b0000_0101_1000_0101_0000_0000_1010_0010 (92602530)
Decoded instruction: Unimplemented | Binary: 0b1010_0000_0000_0001_1011_1111_1100_0101 (2684469189)
Decoded instruction: Unimplemented | Binary: 0b0110_1100_0110_1100_0110_0101_0100_1000 (1819043144)
Decoded instruction: JAL (JTypeFields 111 24 975876) | Binary: 0b0111_0111_0010_0000_0010_1100_0110_1111 (1998597231)
Decoded instruction: JAL (JTypeFields 111 4 822670) | Binary: 0b0110_0100_0110_1100_0111_0010_0110_1111 (1684828783)
Decoded instruction: Unimplemented | Binary: 0b0000_0000_0000_0000_0000_1010_0010_0001 (2593)
Decoded instruction: Unimplemented | Binary: 0b0000_0000_0000_0000_0000_0000_0000_0000 (0)
Decoded instruction: Unimplemented | Binary: 0b0000_0000_0000_0000_0000_0000_0000_0000 (0)
Decoded instruction: Unimplemented | Binary: 0b0000_0000_0000_0000_0000_0000_0000_0000 (0)
Decoded instruction: Unimplemented | Binary: 0b0000_0000_0000_0000_0000_0000_0000_0000 (0)
Last state: Machine {cpu = RISCVCPU {pc = 60, gpr = 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> Nil, fpr = 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0:> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> Nil, privilegeLevel = MachineMode}, peripherals = Peripherals {ram = 3 :> 29722003 :> 378115 :> 45597977 :> 2149781504 :> 92602530 :> 2684469189 :> 1819043144 :> 1998597231 :> 1684828783 :> 2593 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> 0 :> Nil}}
Executed for 16 cycles
Simulation complete
```

As you can see both are the same
 2025-03-14 00:59:26 +02:00
Artturin c75ad4fa70 Remove stack.yaml 
Seems unneeded

```
trace: haskell-nix.project : both 'stack.yaml' and 'cabal.project' files exist.  Using 'cabal.project'. set 'projectFileName = "stack.yaml";' to override this.'
```
 2025-03-14 00:59:26 +02:00
Artturin c82dfbe2a7 hello_world: Fix stat with coreutils(linux) 
the development nix shell has coreutils
 2025-03-14 00:23:30 +02:00
Artturin 3c14139753 Rename rv_formal.cabal to rvFormal 
It appears that the convention is to use the package name as the
filename

```
error: path '/nix/store/3bljihq1ighvsr9ghaw5fvflcdapsrff-haskell-project-plan-to-nix-pkgs/.plan.nix/rvFormal.nix' does not exist
```
 2025-03-14 00:23:30 +02:00
Artturin fec992cf2a Add flake 
`haskell.nix` is quite different from normal nix infra but seems to be
working fine here.

Works with ghc 9.6.6
 2025-03-14 00:23:30 +02:00
Artturin ad34d49f3d Fix shell.nix 
```
[nix-shell:~/joyofhardware/RiscV-Formal]$ riscv64-unknown-linux-gnu-gcc
bash: /nix/store/xq4q2vv9ii7z2k2qp82jd180xdb0r4fv-gcc-riscv64-unknown-linux-gnu-14-20241116/bin/riscv64-unknown-linux-gnu-gcc: cannot execute binary file: Exec format error
```

`pkgs.pkgsCross.riscv64` is for running on riscv64
`pkgs.pkgsCross.riscv64.buildPackages` is for running on the build
system and compiling code for riscv64

`nativeBuildInputs` is for packages which run on the build system and
compile code for riscv64

with `__splicedPackages` we can avoid having to specify `buildPackages`
and have the dependency attributes (`nativeBuildInputs`) pick the
`buildHost` version of the package
 2025-03-14 00:23:30 +02:00
Yehowshua Immanuel a76d6e24ec correct behavior of R type in execute 2025-03-13 16:26:03 -04:00
Yehowshua Immanuel 4428f7f196 fixed execution of R type instructions 2025-03-13 14:31:38 -04:00
Yehowshua Immanuel 7066df0936 Grok mostly wrote execute - will test later... 2025-03-10 23:00:23 -04:00
Yehowshua Immanuel 69f5cdee6a added needed context and getting ready to implement execute 2025-03-10 22:26:38 -04:00
Yehowshua Immanuel b95b2b962a read seemingly complete 2025-03-10 17:46:06 -04:00
Yehowshua Immanuel ad751a5039 read is getting there... 2025-03-10 17:22:51 -04:00
Yehowshua Immanuel 171fcece98 reduce debug in sim and add PREFIX to makefile 2025-03-07 22:04:40 -05:00
Yehowshua Immanuel 63a73d3f71 now fetching from ram correctly as ram is 32 bit word not byte indexed 2025-03-07 21:41:46 -05:00
Yehowshua Immanuel 3f50fe32f8 still compiling after refactoring field types 2025-03-07 20:31:41 -05:00
Yehowshua Immanuel 73d5e1204c stopping point before re-factoring decoder types 2025-03-07 18:41:55 -05:00
Yehowshua Immanuel 6b81cd28ee working on adding read stage 2025-03-07 12:09:08 -05:00
Yehowshua Immanuel 4cc8c8d430 Forgot to replace $ operator in Uart.hs 2025-03-06 08:44:28 -05:00
Yehowshua Immanuel 0792bf3c7d Replacing $ operator with more readable |> operator 2025-03-06 08:41:00 -05:00
Yehowshua Immanuel 2b1c486c17 created Decode result 2025-03-05 09:04:54 -05:00
Yehowshua Immanuel a6c435791a improve instructions to simulate in README 2025-03-05 00:10:56 -05:00
Yehowshua Immanuel 7f7ba49ee1 prune more warnings and re-org Decode files a bit 2025-03-05 00:09:04 -05:00
Yehowshua Immanuel 67b44dedc0 clean up warnings a bit 2025-03-04 23:54:30 -05:00
Yehowshua Immanuel 30650b870c replace/update relevant fetch types and functions 2025-03-04 23:43:35 -05:00
Yehowshua Immanuel eb79210863 now using bus and new FetchResult type 2025-03-04 23:37:33 -05:00
Yehowshua Immanuel 4729d79b23 refactoring towards types that can handle exceptions between stages 2025-03-04 23:05:52 -05:00
Yehowshua Immanuel d7d698a28c save progress before switching to new bus architecture 2025-03-04 08:12:59 -05:00
Yehowshua Immanuel 88ec010f98 initial support for exceptions 2025-03-02 23:12:02 -05:00
Yehowshua Immanuel 5552ad3d4a bus architecture re-built I think 2025-02-26 13:05:02 -05:00
Yehowshua Immanuel c8b192cade prep for notable re-org 2025-02-26 02:24:23 -05:00
Yehowshua Immanuel 024115e389 Uart now has correct write implementation presumably 2025-02-26 01:51:33 -05:00
Yehowshua Immanuel 8d5cd862ab more progress on UART read 2025-02-25 23:47:00 -05:00
Yehowshua Immanuel 7265728932 read getting closer to being done 2025-02-25 19:09:37 -05:00
Yehowshua Immanuel 1f9bd2f015 hopefully progressing to a more scalable bus architecture 2025-02-25 14:24:54 -05:00
33 changed files with 1890 additions and 546 deletions
Show stats Expand all files Collapse all files

1
.gitignore vendored
View file

@ -10,6 +10,7 @@ dist-newstyle/
cabal-dev
/cabal.project.local
.ghc.environment.*
*.elf
*.o
*.o-boot
*.hi

4
Notes.md Normal file
View file

@ -0,0 +1,4 @@
# Notes
In OOO design(or maybe even pipelined 5 stage design), the regfile
should have a variant of `Borrowed`.

17
README.md
View file

@ -11,6 +11,9 @@ Note that this repository is currently very much W.I.P. That being said,
this is how you would currently run a simulation:
```bash
pushd rv_tests/hello_world/
make
popd
cabal run main --ghc-options="-D_RAM_DEPTH=2048" -- --firmware=./rv_tests/hello_world/hello.bin
```
@ -22,20 +25,14 @@ essence forms the context of our micro-op machinery.
Change instructions to support Nix
## Disassembling
```
riscv64-unknown-elf-objdump -D -b binary -m riscv:rv64 ./rv_tests/hello_world/hello.bin > hello.asm
```
# TODO
- [ ] 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
- [ ] Some forms may be redundant(may need to remove some)

4
bin/Main.hs
View file

@ -12,7 +12,7 @@ import Data.Maybe (listToMaybe)
import Data.List (isPrefixOf)
import Text.Show.Pretty (ppShow)
import Simulation (simulation, Args(..), Simulation(..))
import Simulation (simulation, Args(..), Simulation(..), RISCVCPU(..), Machine(..))
main :: IO ()
main = do
@ -23,7 +23,7 @@ main = do
case simResult of
Success states -> do
-- mapM_ (putStrLn . ppShow) states -- Uncomment to print each state, if needed.
putStrLn $ "Last state: " ++ show (last states)
putStrLn $ "GPR last state: " ++ (show $ gpr $ cpu $ last states)
putStrLn $ "Executed for " ++ show (length states) ++ " cycles"
putStrLn "Simulation complete"
Failure err -> do

11
c/uart_sim_device.c
View file

@ -6,6 +6,9 @@
#include <stdbool.h>
static volatile bool ctrl_c_received = false;
static char last_char = '\0';
int is_char_available();
void sigint_handler(int sig_num) {
ctrl_c_received = true;
@ -37,8 +40,10 @@ void restore_terminal() {
}
char get_char_from_terminal() {
char c = getchar();
return c;
if (is_char_available()) {
last_char = getchar(); // Update last_char if new character is available
}
return last_char; // Return the last available character (or '\0' initially)
}
void write_char_to_terminal(char chr) {
@ -71,4 +76,4 @@ int is_char_available() {
// No character available
return 0;
}
}
}

2
cabal.project
View file

@ -1,5 +1,5 @@
packages:
rv_formal.cabal
rvFormal.cabal
packages: .
builddir: build

577
flake.lock Normal file
View file

@ -0,0 +1,577 @@
{
"nodes": {
"HTTP": {
"flake": false,
"locked": {
"lastModified": 1451647621,
"narHash": "sha256-oHIyw3x0iKBexEo49YeUDV1k74ZtyYKGR2gNJXXRxts=",
"owner": "phadej",
"repo": "HTTP",
"rev": "9bc0996d412fef1787449d841277ef663ad9a915",
"type": "github"
},
"original": {
"owner": "phadej",
"repo": "HTTP",
"type": "github"
}
},
"cabal-32": {
"flake": false,
"locked": {
"lastModified": 1603716527,
"narHash": "sha256-X0TFfdD4KZpwl0Zr6x+PLxUt/VyKQfX7ylXHdmZIL+w=",
"owner": "haskell",
"repo": "cabal",
"rev": "48bf10787e27364730dd37a42b603cee8d6af7ee",
"type": "github"
},
"original": {
"owner": "haskell",
"ref": "3.2",
"repo": "cabal",
"type": "github"
}
},
"cabal-34": {
"flake": false,
"locked": {
"lastModified": 1645834128,
"narHash": "sha256-wG3d+dOt14z8+ydz4SL7pwGfe7SiimxcD/LOuPCV6xM=",
"owner": "haskell",
"repo": "cabal",
"rev": "5ff598c67f53f7c4f48e31d722ba37172230c462",
"type": "github"
},
"original": {
"owner": "haskell",
"ref": "3.4",
"repo": "cabal",
"type": "github"
}
},
"cabal-36": {
"flake": false,
"locked": {
"lastModified": 1669081697,
"narHash": "sha256-I5or+V7LZvMxfbYgZATU4awzkicBwwok4mVoje+sGmU=",
"owner": "haskell",
"repo": "cabal",
"rev": "8fd619e33d34924a94e691c5fea2c42f0fc7f144",
"type": "github"
},
"original": {
"owner": "haskell",
"ref": "3.6",
"repo": "cabal",
"type": "github"
}
},
"cardano-shell": {
"flake": false,
"locked": {
"lastModified": 1608537748,
"narHash": "sha256-PulY1GfiMgKVnBci3ex4ptk2UNYMXqGjJOxcPy2KYT4=",
"owner": "input-output-hk",
"repo": "cardano-shell",
"rev": "9392c75087cb9a3d453998f4230930dea3a95725",
"type": "github"
},
"original": {
"owner": "input-output-hk",
"repo": "cardano-shell",
"type": "github"
}
},
"flake-compat": {
"flake": false,
"locked": {
"lastModified": 1672831974,
"narHash": "sha256-z9k3MfslLjWQfnjBtEtJZdq3H7kyi2kQtUThfTgdRk0=",
"owner": "input-output-hk",
"repo": "flake-compat",
"rev": "45f2638735f8cdc40fe302742b79f248d23eb368",
"type": "github"
},
"original": {
"owner": "input-output-hk",
"ref": "hkm/gitlab-fix",
"repo": "flake-compat",
"type": "github"
}
},
"ghc-8.6.5-iohk": {
"flake": false,
"locked": {
"lastModified": 1600920045,
"narHash": "sha256-DO6kxJz248djebZLpSzTGD6s8WRpNI9BTwUeOf5RwY8=",
"owner": "input-output-hk",
"repo": "ghc",
"rev": "95713a6ecce4551240da7c96b6176f980af75cae",
"type": "github"
},
"original": {
"owner": "input-output-hk",
"ref": "release/8.6.5-iohk",
"repo": "ghc",
"type": "github"
}
},
"hackage": {
"flake": false,
"locked": {
"lastModified": 1740097423,
"narHash": "sha256-DsGw8i2CJIw+AaMDn01tDS6frU2d80u5LXmGHuW3kUM=",
"owner": "input-output-hk",
"repo": "hackage.nix",
"rev": "83d083a4931b48b5ba555e52b1bbbf4da55f1a24",
"type": "github"
},
"original": {
"owner": "input-output-hk",
"repo": "hackage.nix",
"type": "github"
}
},
"hackage-for-stackage": {
"flake": false,
"locked": {
"lastModified": 1740097413,
"narHash": "sha256-R8387ERJhPpy6Q/BM6EOHNl/AZ7a8KjippJhil2NsUg=",
"owner": "input-output-hk",
"repo": "hackage.nix",
"rev": "e10eff533209542e11345b2930404938d4a9fe8d",
"type": "github"
},
"original": {
"owner": "input-output-hk",
"ref": "for-stackage",
"repo": "hackage.nix",
"type": "github"
}
},
"haskellNix": {
"inputs": {
"HTTP": "HTTP",
"cabal-32": "cabal-32",
"cabal-34": "cabal-34",
"cabal-36": "cabal-36",
"cardano-shell": "cardano-shell",
"flake-compat": "flake-compat",
"ghc-8.6.5-iohk": "ghc-8.6.5-iohk",
"hackage": "hackage",
"hackage-for-stackage": "hackage-for-stackage",
"hls-1.10": "hls-1.10",
"hls-2.0": "hls-2.0",
"hls-2.2": "hls-2.2",
"hls-2.3": "hls-2.3",
"hls-2.4": "hls-2.4",
"hls-2.5": "hls-2.5",
"hls-2.6": "hls-2.6",
"hls-2.7": "hls-2.7",
"hls-2.8": "hls-2.8",
"hls-2.9": "hls-2.9",
"hpc-coveralls": "hpc-coveralls",
"iserv-proxy": "iserv-proxy",
"nixpkgs": [
"haskellNix",
"nixpkgs-unstable"
],
"nixpkgs-2305": "nixpkgs-2305",
"nixpkgs-2311": "nixpkgs-2311",
"nixpkgs-2405": "nixpkgs-2405",
"nixpkgs-2411": "nixpkgs-2411",
"nixpkgs-unstable": "nixpkgs-unstable",
"old-ghc-nix": "old-ghc-nix",
"stackage": "stackage"
},
"locked": {
"lastModified": 1740099110,
"narHash": "sha256-6sEIo/jd7UgbILXNqaiwN/GilAfks8FBaH79uq0nkZw=",
"owner": "input-output-hk",
"repo": "haskell.nix",
"rev": "81eb79ff6065dfd00b7e5ce46d636fc32a1efef4",
"type": "github"
},
"original": {
"owner": "input-output-hk",
"repo": "haskell.nix",
"type": "github"
}
},
"hls-1.10": {
"flake": false,
"locked": {
"lastModified": 1680000865,
"narHash": "sha256-rc7iiUAcrHxwRM/s0ErEsSPxOR3u8t7DvFeWlMycWgo=",
"owner": "haskell",
"repo": "haskell-language-server",
"rev": "b08691db779f7a35ff322b71e72a12f6e3376fd9",
"type": "github"
},
"original": {
"owner": "haskell",
"ref": "1.10.0.0",
"repo": "haskell-language-server",
"type": "github"
}
},
"hls-2.0": {
"flake": false,
"locked": {
"lastModified": 1687698105,
"narHash": "sha256-OHXlgRzs/kuJH8q7Sxh507H+0Rb8b7VOiPAjcY9sM1k=",
"owner": "haskell",
"repo": "haskell-language-server",
"rev": "783905f211ac63edf982dd1889c671653327e441",
"type": "github"
},
"original": {
"owner": "haskell",
"ref": "2.0.0.1",
"repo": "haskell-language-server",
"type": "github"
}
},
"hls-2.2": {
"flake": false,
"locked": {
"lastModified": 1693064058,
"narHash": "sha256-8DGIyz5GjuCFmohY6Fa79hHA/p1iIqubfJUTGQElbNk=",
"owner": "haskell",
"repo": "haskell-language-server",
"rev": "b30f4b6cf5822f3112c35d14a0cba51f3fe23b85",
"type": "github"
},
"original": {
"owner": "haskell",
"ref": "2.2.0.0",
"repo": "haskell-language-server",
"type": "github"
}
},
"hls-2.3": {
"flake": false,
"locked": {
"lastModified": 1695910642,
"narHash": "sha256-tR58doOs3DncFehHwCLczJgntyG/zlsSd7DgDgMPOkI=",
"owner": "haskell",
"repo": "haskell-language-server",
"rev": "458ccdb55c9ea22cd5d13ec3051aaefb295321be",
"type": "github"
},
"original": {
"owner": "haskell",
"ref": "2.3.0.0",
"repo": "haskell-language-server",
"type": "github"
}
},
"hls-2.4": {
"flake": false,
"locked": {
"lastModified": 1699862708,
"narHash": "sha256-YHXSkdz53zd0fYGIYOgLt6HrA0eaRJi9mXVqDgmvrjk=",
"owner": "haskell",
"repo": "haskell-language-server",
"rev": "54507ef7e85fa8e9d0eb9a669832a3287ffccd57",
"type": "github"
},
"original": {
"owner": "haskell",
"ref": "2.4.0.1",
"repo": "haskell-language-server",
"type": "github"
}
},
"hls-2.5": {
"flake": false,
"locked": {
"lastModified": 1701080174,
"narHash": "sha256-fyiR9TaHGJIIR0UmcCb73Xv9TJq3ht2ioxQ2mT7kVdc=",
"owner": "haskell",
"repo": "haskell-language-server",
"rev": "27f8c3d3892e38edaef5bea3870161815c4d014c",
"type": "github"
},
"original": {
"owner": "haskell",
"ref": "2.5.0.0",
"repo": "haskell-language-server",
"type": "github"
}
},
"hls-2.6": {
"flake": false,
"locked": {
"lastModified": 1705325287,
"narHash": "sha256-+P87oLdlPyMw8Mgoul7HMWdEvWP/fNlo8jyNtwME8E8=",
"owner": "haskell",
"repo": "haskell-language-server",
"rev": "6e0b342fa0327e628610f2711f8c3e4eaaa08b1e",
"type": "github"
},
"original": {
"owner": "haskell",
"ref": "2.6.0.0",
"repo": "haskell-language-server",
"type": "github"
}
},
"hls-2.7": {
"flake": false,
"locked": {
"lastModified": 1708965829,
"narHash": "sha256-LfJ+TBcBFq/XKoiNI7pc4VoHg4WmuzsFxYJ3Fu+Jf+M=",
"owner": "haskell",
"repo": "haskell-language-server",
"rev": "50322b0a4aefb27adc5ec42f5055aaa8f8e38001",
"type": "github"
},
"original": {
"owner": "haskell",
"ref": "2.7.0.0",
"repo": "haskell-language-server",
"type": "github"
}
},
"hls-2.8": {
"flake": false,
"locked": {
"lastModified": 1715153580,
"narHash": "sha256-Vi/iUt2pWyUJlo9VrYgTcbRviWE0cFO6rmGi9rmALw0=",
"owner": "haskell",
"repo": "haskell-language-server",
"rev": "dd1be1beb16700de59e0d6801957290bcf956a0a",
"type": "github"
},
"original": {
"owner": "haskell",
"ref": "2.8.0.0",
"repo": "haskell-language-server",
"type": "github"
}
},
"hls-2.9": {
"flake": false,
"locked": {
"lastModified": 1720003792,
"narHash": "sha256-qnDx8Pk0UxtoPr7BimEsAZh9g2WuTuMB/kGqnmdryKs=",
"owner": "haskell",
"repo": "haskell-language-server",
"rev": "0c1817cb2babef0765e4e72dd297c013e8e3d12b",
"type": "github"
},
"original": {
"owner": "haskell",
"ref": "2.9.0.1",
"repo": "haskell-language-server",
"type": "github"
}
},
"hpc-coveralls": {
"flake": false,
"locked": {
"lastModified": 1607498076,
"narHash": "sha256-8uqsEtivphgZWYeUo5RDUhp6bO9j2vaaProQxHBltQk=",
"owner": "sevanspowell",
"repo": "hpc-coveralls",
"rev": "14df0f7d229f4cd2e79f8eabb1a740097fdfa430",
"type": "github"
},
"original": {
"owner": "sevanspowell",
"repo": "hpc-coveralls",
"type": "github"
}
},
"iserv-proxy": {
"flake": false,
"locked": {
"lastModified": 1717479972,
"narHash": "sha256-7vE3RQycHI1YT9LHJ1/fUaeln2vIpYm6Mmn8FTpYeVo=",
"owner": "stable-haskell",
"repo": "iserv-proxy",
"rev": "2ed34002247213fc435d0062350b91bab920626e",
"type": "github"
},
"original": {
"owner": "stable-haskell",
"ref": "iserv-syms",
"repo": "iserv-proxy",
"type": "github"
}
},
"nixpkgs": {
"locked": {
"lastModified": 1735821806,
"narHash": "sha256-cuNapx/uQeCgeuhUhdck3JKbgpsml259sjUQnWM7zW8=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "d6973081434f88088e5321f83ebafe9a1167c367",
"type": "github"
},
"original": {
"owner": "NixOS",
"ref": "nixpkgs-unstable",
"repo": "nixpkgs",
"type": "github"
}
},
"nixpkgs-2305": {
"locked": {
"lastModified": 1705033721,
"narHash": "sha256-K5eJHmL1/kev6WuqyqqbS1cdNnSidIZ3jeqJ7GbrYnQ=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "a1982c92d8980a0114372973cbdfe0a307f1bdea",
"type": "github"
},
"original": {
"owner": "NixOS",
"ref": "nixpkgs-23.05-darwin",
"repo": "nixpkgs",
"type": "github"
}
},
"nixpkgs-2311": {
"locked": {
"lastModified": 1719957072,
"narHash": "sha256-gvFhEf5nszouwLAkT9nWsDzocUTqLWHuL++dvNjMp9I=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "7144d6241f02d171d25fba3edeaf15e0f2592105",
"type": "github"
},
"original": {
"owner": "NixOS",
"ref": "nixpkgs-23.11-darwin",
"repo": "nixpkgs",
"type": "github"
}
},
"nixpkgs-2405": {
"locked": {
"lastModified": 1735564410,
"narHash": "sha256-HB/FA0+1gpSs8+/boEavrGJH+Eq08/R2wWNph1sM1Dg=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "1e7a8f391f1a490460760065fa0630b5520f9cf8",
"type": "github"
},
"original": {
"owner": "NixOS",
"ref": "nixpkgs-24.05-darwin",
"repo": "nixpkgs",
"type": "github"
}
},
"nixpkgs-2411": {
"locked": {
"lastModified": 1737255904,
"narHash": "sha256-r3fxHvh+M/mBgCZXOACzRFPsJdix2QSsKazb7VCXXo0=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "eacdab35066b0bb1c9413c96898e326b76398a81",
"type": "github"
},
"original": {
"owner": "NixOS",
"ref": "nixpkgs-24.11-darwin",
"repo": "nixpkgs",
"type": "github"
}
},
"nixpkgs-unstable": {
"locked": {
"lastModified": 1737110817,
"narHash": "sha256-DSenga8XjPaUV5KUFW/i3rNkN7jm9XmguW+qQ1ZJTR4=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "041c867bad68dfe34b78b2813028a2e2ea70a23c",
"type": "github"
},
"original": {
"owner": "NixOS",
"ref": "nixpkgs-unstable",
"repo": "nixpkgs",
"type": "github"
}
},
"old-ghc-nix": {
"flake": false,
"locked": {
"lastModified": 1631092763,
"narHash": "sha256-sIKgO+z7tj4lw3u6oBZxqIhDrzSkvpHtv0Kki+lh9Fg=",
"owner": "angerman",
"repo": "old-ghc-nix",
"rev": "af48a7a7353e418119b6dfe3cd1463a657f342b8",
"type": "github"
},
"original": {
"owner": "angerman",
"ref": "master",
"repo": "old-ghc-nix",
"type": "github"
}
},
"root": {
"inputs": {
"haskellNix": "haskellNix",
"nixpkgs": "nixpkgs",
"utils": "utils"
}
},
"stackage": {
"flake": false,
"locked": {
"lastModified": 1740096702,
"narHash": "sha256-fwXgQnLUbL3U8091RaskwGeTe0pRLCaAPh8ZkIiaTBc=",
"owner": "input-output-hk",
"repo": "stackage.nix",
"rev": "64d492737ba6c3eecf7f81dc9184dc8c1482fd06",
"type": "github"
},
"original": {
"owner": "input-output-hk",
"repo": "stackage.nix",
"type": "github"
}
},
"systems": {
"locked": {
"lastModified": 1681028828,
"narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
"owner": "nix-systems",
"repo": "default",
"rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
"type": "github"
},
"original": {
"owner": "nix-systems",
"repo": "default",
"type": "github"
}
},
"utils": {
"inputs": {
"systems": "systems"
},
"locked": {
"lastModified": 1731533236,
"narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=",
"owner": "numtide",
"repo": "flake-utils",
"rev": "11707dc2f618dd54ca8739b309ec4fc024de578b",
"type": "github"
},
"original": {
"owner": "numtide",
"repo": "flake-utils",
"type": "github"
}
}
},
"root": "root",
"version": 7
}

85
flake.nix Normal file
View file

@ -0,0 +1,85 @@
{
inputs = {
nixpkgs = {
url = "github:NixOS/nixpkgs/nixpkgs-unstable";
};
utils.url = "github:numtide/flake-utils";
haskellNix.url = "github:input-output-hk/haskell.nix";
};
outputs =
inputs:
inputs.utils.lib.eachDefaultSystem (
system:
let
pkgs = import inputs.nixpkgs {
localSystem = system;
overlays = [
inputs.haskellNix.overlay
(_: prev: {
riscv-formal = prev.callPackage (
{
haskell-nix,
qemu,
}:
haskell-nix.hix.project {
compiler-nix-name = "ghc966";
src = builtins.path {
path = ./.;
name = "riscv-formal-source";
};
shell =
let
riscv64-linux = prev.pkgsCross.riscv64-embedded.__splicedPackages;
# Everything here builds and runs without needing the below crossSystem
#riscv64-linux = (import prev.pkgs.path {
# localSystem = system;
# crossSystem = {
# config = "riscv64-none-elf";
# libc = "newlib";
# gcc = {
# # Both sets work to build and run hello_world
# # This matches what is in the makefile
# #arch = "rv64ima";
# #abi = "lp64";
# # This matches what you asked for on matrix
# #arch = "rv64g";
# #abi = "lp64d";
# };
# };
#}).__splicedPackages;
in
{
tools = {
cabal = { };
hlint = { };
};
nativeBuildInputs = [
qemu
riscv64-linux.gcc
riscv64-linux.binutils
riscv64-linux.glibc
];
shellHook = ''
export CROSS_PREFIX="riscv64-none-elf"
'';
};
}
) { };
})
];
};
flake = pkgs.riscv-formal.flake { };
in
flake
);
nixConfig = {
# https://input-output-hk.github.io/haskell.nix/tutorials/getting-started-flakes.html#setting-up-the-binary-cache
extra-substituters = [ "https://cache.iog.io" ];
extra-trusted-public-keys = [ "hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ=" ];
allow-import-from-derivation = true;
};
}

95
hs/Bus.hs Normal file
View file

@ -0,0 +1,95 @@
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
module Bus(
Peripherals(..),
ReadResponse,
WriteResponse,
Bus.read,
Bus.write,
) where
import Clash.Prelude
import Peripherals.Ram(Ram, RamLine, read, RamAddr)
import Peripherals.Uart(UartAddr, read, write)
import BusTypes(
BusError(..),
TransactionSize(..),
WriteRequest(..),
ReadRequest(..),
BusVal(..),
)
import Types(Addr)
import Peripherals.Ram(write, bytesInRam)
import Util((|>))
data Peripherals = Peripherals
{
ram :: Ram
}
deriving (Generic, Show, Eq, NFDataX)
type ReadResponse = Either BusError BusVal
type WriteResponse = Either BusError Peripherals
busValToTransactionSize :: BusVal -> TransactionSize
busValToTransactionSize (BusByte _) = SizeByte
busValToTransactionSize (BusHalfWord _) = SizeHalfWord
busValToTransactionSize (BusFullWord _) = SizeFullWord
busValToTransactionSize (BusDoubleWord _) = SizeDoubleWord
busValToTransactionSize (BusQuadWord _) = SizeQuadWord
alignCheck :: Addr -> TransactionSize -> Bool
alignCheck _ SizeByte = True
alignCheck addr SizeHalfWord = addr `mod` 2 == 0
alignCheck addr SizeFullWord = addr `mod` 4 == 0
alignCheck addr SizeDoubleWord = addr `mod` 8 == 0
alignCheck addr SizeQuadWord = addr `mod` 16 == 0
-- address space follows QEMU behavior for now
(ramStart, ramEnd) = (0x80000000 :: Addr, ramStart + (bytesInRam - 1))
(uartStart, uartEnd) = (0x10000000 :: Addr, uartStart + 7)
-- reading/writing from/to UART is implemented as reading/writing
-- from/to stdin/stdout, so we need IO.
read :: ReadRequest -> Peripherals -> IO ReadResponse
read (ReadRequest addr size) peripherals
| not (alignCheck addr size) = return |> Left UnAligned
| (addr >= ramStart) && (addr <= ramEnd) =
return |> Right |> Peripherals.Ram.read size ramWordAddr (ram peripherals)
| (addr >= uartStart) && (addr <= uartEnd) =
fmap Right (Peripherals.Uart.read size uartAddr)
| otherwise = return |> Left UnMapped
where
ramAddrNoOffset = addr - ramStart
ramAddr :: RamAddr
ramAddr = resize ramAddrNoOffset
ramWordAddr :: RamAddr
ramWordAddr = resize |> ramAddrNoOffset `shiftR` 2
uartAddrNoOffset = addr - uartStart
uartAddr :: UartAddr
uartAddr = resize uartAddrNoOffset
write :: WriteRequest -> Peripherals -> IO WriteResponse
write (WriteRequest addr val) peripherals
| not (alignCheck addr |> busValToTransactionSize val) = return |> Left UnAligned
| (addr >= uartStart) && (addr <= uartEnd) =
do
Peripherals.Uart.write val uartAddr
return |> Right peripherals
| (addr >= ramStart) && (addr <= ramEnd) =
return |> Right |>
peripherals {
ram = Peripherals.Ram.write val ramAddr (ram peripherals)
}
| otherwise = return |> Left UnMapped
where
ramAddrNoOffset = addr - ramStart
ramAddr :: RamAddr
ramAddr = resize ramAddrNoOffset
uartAddrNoOffset = addr - uartStart
uartAddr :: UartAddr
uartAddr = resize uartAddrNoOffset

41
hs/BusTypes.hs Normal file
View file

@ -0,0 +1,41 @@
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
module BusTypes(
BusError(..),
TransactionSize(..),
ReadRequest(..),
WriteRequest(..),
BusVal(..),
) where
import Clash.Prelude
import Types(Addr,
Byte, HalfWord, FullWord, DoubleWord, QuadWord)
import Util((|>))
data BusError
= UnMapped
| UnAligned
deriving (Generic, Show, Eq, NFDataX)
data TransactionSize
= SizeByte
| SizeHalfWord
| SizeFullWord
| SizeDoubleWord
| SizeQuadWord
deriving (Generic, Show, Eq, NFDataX)
data ReadRequest = ReadRequest Addr TransactionSize
deriving (Generic, Show, Eq, NFDataX)
data WriteRequest = WriteRequest Addr BusVal
deriving (Generic, Show, Eq, NFDataX)
-- data WriteRequest
data BusVal
= BusByte Byte
| BusHalfWord HalfWord
| BusFullWord FullWord
| BusDoubleWord DoubleWord
| BusQuadWord QuadWord
deriving (Generic, Show, Eq, NFDataX)

39
hs/Cpu.hs Normal file
View file

@ -0,0 +1,39 @@
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NumericUnderscores #-}
module Cpu(
RISCVCPU(..),
Endian(..),
riscvCPUInit) where
import Clash.Prelude
import Types(Pc)
import RegFiles(GPR, FPR, CSR, gprInit, fprInit, csrInit)
data Endian = Big | Little
deriving (Generic, Show, Eq, NFDataX)
data PrivilegeLevel
= MachineMode
| SuperVisorMode
| UserMode
deriving (Generic, Show, Eq, NFDataX)
data RISCVCPU = RISCVCPU
{ pc :: Pc,
gpr :: GPR,
fpr :: FPR,
csr :: CSR,
privilegeLevel :: PrivilegeLevel
}
deriving (Generic, Show, Eq, NFDataX)
riscvCPUInit :: RISCVCPU
riscvCPUInit =
RISCVCPU
{ pc = 0x8000_0000
, gpr = gprInit
, fpr = fprInit
, csr = csrInit
, privilegeLevel = MachineMode
}

218
hs/Decode.hs Normal file
View file

@ -0,0 +1,218 @@
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NumericUnderscores #-}
module Decode(decode, DecodeResult(..)) where
import DecodeTypes(
RTypeFields(..), ITypeFields(..), STypeFields(..),
BTypeFields(..), UTypeFields(..), JTypeFields(..),
Opcode(..)
)
import Clash.Prelude
import Fetch(FetchResult (Instruction, InstructionException))
import Exceptions(Exception(..))
import Types(Insn, Addr)
import RegFiles(RegVal(..))
import Util((|>))
data DecodeResult = Opcode {opcode :: Opcode, insnAddr :: Addr}
| DecodeException {exception :: Exception, insnAddr :: Addr}
| InstructionException {exception :: Exception, insnAddr :: Addr}
deriving (Generic, Show, Eq, NFDataX)
decode :: FetchResult -> DecodeResult
decode (Instruction insn addr) =
case insnToOpcode insn of
Just opcode -> Opcode opcode addr
Nothing -> DecodeException (IllegalInstruction insn) addr
decode (Fetch.InstructionException exception addr) =
Decode.InstructionException exception addr
insnToOpcode :: Insn -> Maybe Opcode
insnToOpcode insn =
decodeRType insn `chainAndTry`
decodeIType insn `chainAndTry`
decodeSType insn `chainAndTry`
decodeBType insn `chainAndTry`
decodeUType insn `chainAndTry`
decodeJType insn
where
chainAndTry :: Maybe Opcode -> Maybe Opcode -> Maybe Opcode
chainAndTry (Just left) _ = Just left
chainAndTry Nothing (Just right) = Just right
chainAndTry _ _ = Nothing
decodeRType :: Insn -> Maybe Opcode
decodeRType insn =
case opcode of
0b0110011 ->
case funct3 of
0x00 -> case funct7 of
0x00 -> Just |> ADD (RTypeFields rd funct3 rs1 rs2 funct7)
0x20 -> Just |> SUB (RTypeFields rd funct3 rs1 rs2 funct7)
_ -> Nothing
0x04 -> Just |> XOR (RTypeFields rd funct3 rs1 rs2 funct7)
0x06 -> Just |> OR (RTypeFields rd funct3 rs1 rs2 funct7)
0x07 -> Just |> AND (RTypeFields rd funct3 rs1 rs2 funct7)
0x01 -> Just |> SLL (RTypeFields rd funct3 rs1 rs2 funct7)
0x05 -> case funct7 of
0x00 -> Just |> SRL (RTypeFields rd funct3 rs1 rs2 funct7)
0x20 -> Just |> SRA (RTypeFields rd funct3 rs1 rs2 funct7)
_ -> Nothing
0x02 -> Just |> SLT (RTypeFields rd funct3 rs1 rs2 funct7)
0x03 -> Just |> SLTU (RTypeFields rd funct3 rs1 rs2 funct7)
_ -> Nothing
_ -> Nothing
where
opcode = getOpcode insn
rd = getRd insn
funct3 = getFunct3 insn
rs1 = getRs1 insn
rs2 = getRs2 insn
funct7 = getFunct7 insn
decodeIType :: Insn -> Maybe Opcode
decodeIType insn = case opcode of
0b0010011 -> case funct3 of
0x0 -> Just |> ADDI (ITypeFields rd funct3 rs1 imm)
0x4 -> Just |> XORI (ITypeFields rd funct3 rs1 imm)
0x6 -> Just |> ORI (ITypeFields rd funct3 rs1 imm)
0x7 -> Just |> ANDI (ITypeFields rd funct3 rs1 imm)
0x1 -> if slice d31 d25 (pack insn) == 0
then Just |> SLLI (ITypeFields rd funct3 rs1 imm)
else Nothing
0x5 -> case slice d31 d25 (pack insn) of -- Distinguish SRLI and SRAI
0x00 -> Just |> SRLI (ITypeFields rd funct3 rs1 imm)
0x20 -> Just |> SRAI (ITypeFields rd funct3 rs1 imm)
_ -> Nothing
0x2 -> Just |> SLTI (ITypeFields rd funct3 rs1 imm)
0x3 -> Just |> SLTIU (ITypeFields rd funct3 rs1 imm)
_ -> Nothing
0b0000011 -> case funct3 of
0x0 -> Just |> LB (ITypeFields rd funct3 rs1 imm)
0x1 -> Just |> LH (ITypeFields rd funct3 rs1 imm)
0x2 -> Just |> LW (ITypeFields rd funct3 rs1 imm)
0x4 -> Just |> LBU (ITypeFields rd funct3 rs1 imm)
0x5 -> Just |> LHU (ITypeFields rd funct3 rs1 imm)
_ -> Nothing
0b1100111 -> case funct3 of
0x0 -> Just |> JALR (ITypeFields rd funct3 rs1 imm)
_ -> Nothing
0b1110011 -> case imm of
0x000 -> Just |> ECALL (ITypeFields rd funct3 rs1 imm)
0x001 -> Just |> EBREAK (ITypeFields rd funct3 rs1 imm)
_ -> Nothing
_ -> Nothing
where
opcode = getOpcode insn
rd = getRd insn
funct3 = getFunct3 insn
rs1 = getRs1 insn
imm = getImm12 insn
decodeSType :: Insn -> Maybe Opcode
decodeSType insn =
case opcode of
0b0100011 -> case funct3 of
0x0 -> Just |> SB (STypeFields funct3 rs1 rs2 imm12) -- Store Byte
0x1 -> Just |> SH (STypeFields funct3 rs1 rs2 imm12) -- Store Halfword
0x2 -> Just |> SW (STypeFields funct3 rs1 rs2 imm12) -- Store Word
_ -> Nothing
_ -> Nothing
where
opcode = getOpcode insn
funct3 = getFunct3 insn
rs1 = getRs1 insn
rs2 = getRs2 insn
imm12 = getImm12SType insn
decodeBType :: Insn -> Maybe Opcode
decodeBType insn =
case opcode of
0b1100011 -> case funct3 of
0x0 -> Just |> BEQ (BTypeFields funct3 rs1 rs2 imm13) -- Branch if equal
0x1 -> Just |> BNE (BTypeFields funct3 rs1 rs2 imm13) -- Branch if not equal
0x4 -> Just |> BLT (BTypeFields funct3 rs1 rs2 imm13) -- Branch if less than
0x5 -> Just |> BGE (BTypeFields funct3 rs1 rs2 imm13) -- Branch if greater or equal
0x6 -> Just |> BLTU (BTypeFields funct3 rs1 rs2 imm13) -- Branch if less than (unsigned)
0x7 -> Just |> BGEU (BTypeFields funct3 rs1 rs2 imm13) -- Branch if greater or equal (unsigned)
_ -> Nothing
_ -> Nothing
where
opcode = getOpcode insn
funct3 = getFunct3 insn
rs1 = getRs1 insn
rs2 = getRs2 insn
imm13 = getImm13BType insn
decodeUType :: Insn -> Maybe Opcode
decodeUType insn = case opcode of
0b0110111 -> Just |> LUI (UTypeFields rd imm20) -- LUI
0b0010111 -> Just |> AUIPC (UTypeFields rd imm20) -- AUIPC
_ -> Nothing
where
opcode = getOpcode insn
rd = getRd insn
imm20 = getImm20UType insn
decodeJType :: Insn -> Maybe Opcode
decodeJType insn =
case opcode of
0b1101111 -> Just |> JAL (JTypeFields rd imm21) -- JAL
_ -> Nothing
where
opcode = getOpcode insn
rd = getRd insn
imm21 = getImm21JType insn
getImm21JType :: Insn -> Unsigned 21
getImm21JType instr = bitCoerce |> imm20 ++# imm10_1 ++# imm11 ++# imm19_12 ++# zero
where
imm20 = slice d31 d31 (pack instr) -- imm[20]
imm10_1 = slice d30 d21 (pack instr) -- imm[10:1]
imm11 = slice d20 d20 (pack instr) -- imm[11]
imm19_12 = slice d19 d12 (pack instr) -- imm[19:12]
zero = 0 :: BitVector 1 -- LSB always zero for J-type
getOpcode :: Insn -> Unsigned 7
getOpcode instr = bitCoerce |> slice d6 d0 (pack instr)
getImm12 :: Insn -> Unsigned 12
getImm12 instr = bitCoerce |> slice d31 d20 (pack instr)
getImm12SType :: Insn -> Unsigned 12
getImm12SType instr = bitCoerce |> immediateUpper ++# immediateLower
where
immediateUpper = (slice d31 d25 (pack instr))
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 -> RegVal
getRs2 instr = Unpopulated |> bitCoerce |> slice d24 d20 (pack instr)
getRs1 :: Insn -> RegVal
getRs1 instr = Unpopulated |> bitCoerce |> slice d19 d15 (pack instr)

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

@ -1,7 +1,7 @@
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NumericUnderscores #-}
module Isa.Forms(
module DecodeTypes(
FUNCT7, RS2, RS1, FUNCT3, RD, OPCODE,
IMM12, IMM13, IMM20, IMM21,
@ -11,13 +11,13 @@ module Isa.Forms(
Opcode(..)
) where
import Clash.Prelude
import Types(Mem, Addr, Insn)
import RegFiles(RegFileIdx, RegVal)
type FUNCT7 = Unsigned 7
type RS2 = Unsigned 5
type RS1 = Unsigned 5
type RS2 = RegVal
type RS1 = RegVal
type RD = RegFileIdx
type FUNCT3 = Unsigned 3
type RD = Unsigned 5
type OPCODE = Unsigned 7
type IMM12 = Unsigned 12
@ -25,12 +25,12 @@ type IMM13 = Unsigned 13
type IMM20 = Unsigned 20
type IMM21 = Unsigned 21
data RTypeFields = RTypeFields OPCODE RD FUNCT3 RS1 RS2 FUNCT7 deriving (Generic, Show, Eq, NFDataX)
data ITypeFields = ITypeFields OPCODE RD FUNCT3 RS1 IMM12 deriving (Generic, Show, Eq, NFDataX)
data STypeFields = STypeFields OPCODE FUNCT3 RS1 RS2 IMM12 deriving (Generic, Show, Eq, NFDataX)
data BTypeFields = BTypeFields OPCODE FUNCT3 RS1 RS2 IMM13 deriving (Generic, Show, Eq, NFDataX)
data UTypeFields = UTypeFields OPCODE RD IMM20 deriving (Generic, Show, Eq, NFDataX)
data JTypeFields = JTypeFields OPCODE RD IMM21 deriving (Generic, Show, Eq, NFDataX)
data RTypeFields = RTypeFields RD FUNCT3 RS1 RS2 FUNCT7 deriving (Generic, Show, Eq, NFDataX)
data ITypeFields = ITypeFields RD FUNCT3 RS1 IMM12 deriving (Generic, Show, Eq, NFDataX)
data STypeFields = STypeFields FUNCT3 RS1 RS2 IMM12 deriving (Generic, Show, Eq, NFDataX)
data BTypeFields = BTypeFields FUNCT3 RS1 RS2 IMM13 deriving (Generic, Show, Eq, NFDataX)
data UTypeFields = UTypeFields RD IMM20 deriving (Generic, Show, Eq, NFDataX)
data JTypeFields = JTypeFields RD IMM21 deriving (Generic, Show, Eq, NFDataX)
data Opcode
=
@ -84,6 +84,4 @@ data Opcode
-- U-Type
| LUI UTypeFields
| AUIPC UTypeFields
| Unimplemented
deriving (Generic, Show, Eq, NFDataX)

90
hs/Exceptions.hs Normal file
View file

@ -0,0 +1,90 @@
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NumericUnderscores #-}
module Exceptions(
Exception(..),
exceptionCode,
isSynchronousException
) where
import Clash.Prelude
import Types(Addr, Insn)
data Exception =
SupervisorSoftwareInterrupt
| MachineSoftwareInterrupt
| SupervisorTimerInterrupt
| MachineTimerInterrupt
| SupervisorExternalInterrupt
| MachineExternalInterrupt
| CounterOverflowInterrupt
| InstructionAddressMisaligned
| InstructionAccessFault
| IllegalInstruction {insn :: Insn}
| Breakpoint
| LoadAddressMisaligned
| LoadAccessFault
| StoreAMOAddressMisaligned
| StoreAMOAccessFault
| EnvironmentCallFromUMode
| EnvironmentCallFromSMode
| EnvironmentCallFromMMode
| InstructionPageFault
| LoadPageFault
| StoreAMOPageFault
| DoubleTrap
| SoftwareCheck
| HardwareError
deriving (Generic, Show, Eq, NFDataX)
exceptionCode :: Exception -> Unsigned 6
exceptionCode SupervisorSoftwareInterrupt = 1
exceptionCode MachineSoftwareInterrupt = 3
exceptionCode SupervisorTimerInterrupt = 5
exceptionCode MachineTimerInterrupt = 7
exceptionCode SupervisorExternalInterrupt = 9
exceptionCode MachineExternalInterrupt = 11
exceptionCode CounterOverflowInterrupt = 13
exceptionCode InstructionAddressMisaligned = 0
exceptionCode InstructionAccessFault = 1
exceptionCode (IllegalInstruction _) = 2
exceptionCode Breakpoint = 3
exceptionCode LoadAddressMisaligned = 4
exceptionCode LoadAccessFault = 5
exceptionCode StoreAMOAddressMisaligned = 6
exceptionCode StoreAMOAccessFault = 7
exceptionCode EnvironmentCallFromUMode = 8
exceptionCode EnvironmentCallFromSMode = 9
exceptionCode EnvironmentCallFromMMode = 11
exceptionCode InstructionPageFault = 12
exceptionCode LoadPageFault = 13
exceptionCode StoreAMOPageFault = 15
exceptionCode DoubleTrap = 16
exceptionCode SoftwareCheck = 18
exceptionCode HardwareError = 19
isSynchronousException :: Exception -> Bool
isSynchronousException SupervisorSoftwareInterrupt = False
isSynchronousException MachineSoftwareInterrupt = False
isSynchronousException SupervisorTimerInterrupt = False
isSynchronousException MachineTimerInterrupt = False
isSynchronousException SupervisorExternalInterrupt = False
isSynchronousException MachineExternalInterrupt = False
isSynchronousException CounterOverflowInterrupt = False
isSynchronousException InstructionAddressMisaligned = True
isSynchronousException InstructionAccessFault = True
isSynchronousException (IllegalInstruction _) = True
isSynchronousException Breakpoint = True
isSynchronousException LoadAddressMisaligned = True
isSynchronousException LoadAccessFault = True
isSynchronousException StoreAMOAddressMisaligned = True
isSynchronousException StoreAMOAccessFault = True
isSynchronousException EnvironmentCallFromUMode = True
isSynchronousException EnvironmentCallFromSMode = True
isSynchronousException EnvironmentCallFromMMode = True
isSynchronousException InstructionPageFault = True
isSynchronousException LoadPageFault = True
isSynchronousException StoreAMOPageFault = True
isSynchronousException DoubleTrap = True
isSynchronousException SoftwareCheck = True
isSynchronousException HardwareError = True

215
hs/Execute.hs Normal file
View file

@ -0,0 +1,215 @@
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NumericUnderscores #-}
module Execute(execute) where
import Clash.Prelude
import Decode(DecodeResult(..))
import DecodeTypes(
Opcode(..),
RTypeFields(..), ITypeFields(..), STypeFields(..),
BTypeFields(..), UTypeFields(..), JTypeFields(..)
)
import Types(Addr, DoubleWord)
import Exceptions(Exception(..))
import BusTypes(
WriteRequest(..),
ReadRequest(..),
TransactionSize(..),
BusVal(..)
)
import RegFiles(RegFileIdx, RegVal(..))
import Util((|>))
data ExecuteResult = ReadRequest {readRequest :: ReadRequest, insnAddr :: Addr}
| WriteRequest {writeRequest :: WriteRequest, insnAddr :: Addr}
| WriteBackGPR {idx :: RegFileIdx, val :: DoubleWord}
| Jump { targetAddr :: Addr }
| DecodeException {exception :: Exception, insnAddr :: Addr}
| InstructionException {exception :: Exception, insnAddr :: Addr}
deriving (Generic, Show, Eq, NFDataX)
-- Helper functions to extract values from RegVal
extractRegVal :: RegVal -> DoubleWord
extractRegVal (Value _ val) = val
extractRegVal (Unpopulated _) = undefined
-- Execute function
execute :: DecodeResult -> ExecuteResult
execute (Opcode opcode addr) = case opcode of
-- R-Type Instructions
ADD (RTypeFields rd _ rs1 rs2 _) ->
let val1 = extractRegVal rs1
val2 = extractRegVal rs2
in WriteBackGPR rd (val1 + val2)
SUB (RTypeFields rd _ rs1 rs2 _) ->
let val1 = extractRegVal rs1
val2 = extractRegVal rs2
in WriteBackGPR rd (val1 - val2)
XOR (RTypeFields rd _ rs1 rs2 _) ->
let val1 = extractRegVal rs1
val2 = extractRegVal rs2
in WriteBackGPR rd (val1 `xor` val2)
OR (RTypeFields rd _ rs1 rs2 _) ->
let val1 = extractRegVal rs1
val2 = extractRegVal rs2
in WriteBackGPR rd (val1 .|. val2)
AND (RTypeFields rd _ rs1 rs2 _) ->
let val1 = extractRegVal rs1
val2 = extractRegVal rs2
in WriteBackGPR rd (val1 .&. val2)
SLL (RTypeFields rd _ rs1 rs2 _) ->
let val1 = extractRegVal rs1
val2 = extractRegVal rs2
shftAmt = fromIntegral |> slice d5 d0 val2
in WriteBackGPR rd (val1 `shiftL` shftAmt)
SRL (RTypeFields rd _ rs1 rs2 _) ->
let val1 = extractRegVal rs1
val2 = extractRegVal rs2
shftAmt = fromIntegral |> slice d5 d0 val2
in WriteBackGPR rd (val1 `shiftR` shftAmt)
SRA (RTypeFields rd _ rs1 rs2 _) ->
let val1 = unpack (pack (extractRegVal rs1) :: BitVector 64) :: Signed 64
val2 = extractRegVal rs2
shftAmt = fromIntegral |> slice d5 d0 val2
in WriteBackGPR rd (bitCoerce (val1 `shiftR` shftAmt))
SLT (RTypeFields rd _ rs1 rs2 _) ->
let val1 = unpack (pack (extractRegVal rs1) :: BitVector 64) :: Signed 64
val2 = unpack (pack (extractRegVal rs2) :: BitVector 64) :: Signed 64
in WriteBackGPR rd (if val1 < val2 then 1 else 0)
SLTU (RTypeFields rd _ rs1 rs2 _) ->
let val1 = extractRegVal rs1
val2 = extractRegVal rs2
in WriteBackGPR rd (if val1 < val2 then 1 else 0)
-- I-Type Instructions
ADDI (ITypeFields rd _ rs1 imm) ->
let val1 = extractRegVal rs1
immVal = signExtend imm
in WriteBackGPR rd (val1 + immVal)
XORI (ITypeFields rd _ rs1 imm) ->
let val1 = extractRegVal rs1
immVal = signExtend imm
in WriteBackGPR rd (val1 `xor` immVal)
ORI (ITypeFields rd _ rs1 imm) ->
let val1 = extractRegVal rs1
immVal = signExtend imm
in WriteBackGPR rd (val1 .|. immVal)
ANDI (ITypeFields rd _ rs1 imm) ->
let val1 = extractRegVal rs1
immVal = signExtend imm
in WriteBackGPR rd (val1 .&. immVal)
SLLI (ITypeFields rd _ rs1 imm) ->
let val1 = extractRegVal rs1
shamt = imm .&. 0x3F
in WriteBackGPR rd (val1 `shiftL` fromIntegral shamt)
SRLI (ITypeFields rd _ rs1 imm) ->
let val1 = extractRegVal rs1
shamt = imm .&. 0x3F
in WriteBackGPR rd (val1 `shiftR` fromIntegral shamt)
SRAI (ITypeFields rd _ rs1 imm) ->
let val1 = unpack (pack (extractRegVal rs1) :: BitVector 64) :: Signed 64
shamt = imm .&. 0x3F
in WriteBackGPR rd (bitCoerce (val1 `shiftR` fromIntegral shamt))
SLTI (ITypeFields rd _ rs1 imm) ->
let val1 = unpack (pack (extractRegVal rs1) :: BitVector 64) :: Signed 64
immVal = unpack (pack (signExtend imm) :: BitVector 64) :: Signed 64
in WriteBackGPR rd (if val1 < immVal then 1 else 0)
SLTIU (ITypeFields rd _ rs1 imm) ->
let val1 = extractRegVal rs1
immVal = signExtend imm
in WriteBackGPR rd (if val1 < immVal then 1 else 0)
LB (ITypeFields rd _ rs1 imm) ->
let baseAddr = extractRegVal rs1
offset = signExtend imm
in Execute.ReadRequest (BusTypes.ReadRequest (baseAddr + offset) SizeByte) addr
LH (ITypeFields rd _ rs1 imm) ->
let baseAddr = extractRegVal rs1
offset = signExtend imm
in Execute.ReadRequest (BusTypes.ReadRequest (baseAddr + offset) SizeHalfWord) addr
LW (ITypeFields rd _ rs1 imm) ->
let baseAddr = extractRegVal rs1
offset = signExtend imm
in Execute.ReadRequest (BusTypes.ReadRequest (baseAddr + offset) SizeFullWord) addr
LBU (ITypeFields rd _ rs1 imm) ->
let baseAddr = extractRegVal rs1
offset = signExtend imm
in Execute.ReadRequest (BusTypes.ReadRequest (baseAddr + offset) SizeByte) addr
LHU (ITypeFields rd _ rs1 imm) ->
let baseAddr = extractRegVal rs1
offset = signExtend imm
in Execute.ReadRequest (BusTypes.ReadRequest (baseAddr + offset) SizeHalfWord) addr
JALR (ITypeFields rd _ rs1 imm) ->
let baseAddr = extractRegVal rs1
offset = signExtend imm
target = baseAddr + offset
in if rd /= 0 then WriteBackGPR rd (addr + 4) else Jump target
ECALL (ITypeFields _ _ _ _) ->
Execute.DecodeException EnvironmentCallFromMMode addr -- Assuming Machine mode for now
EBREAK (ITypeFields _ _ _ _) ->
Execute.DecodeException Breakpoint addr
-- S-Type Instructions
SB (STypeFields _ rs1 rs2 imm12) ->
let baseAddr = extractRegVal rs1
offset = signExtend imm12
val = extractRegVal rs2
in Execute.WriteRequest (BusTypes.WriteRequest (baseAddr + offset) (BusByte (resize val))) addr
SH (STypeFields _ rs1 rs2 imm12) ->
let baseAddr = extractRegVal rs1
offset = signExtend imm12
val = extractRegVal rs2
in Execute.WriteRequest (BusTypes.WriteRequest (baseAddr + offset) (BusHalfWord (resize val))) addr
SW (STypeFields _ rs1 rs2 imm12) ->
let baseAddr = extractRegVal rs1
offset = signExtend imm12
val = extractRegVal rs2
in Execute.WriteRequest (BusTypes.WriteRequest (baseAddr + offset) (BusFullWord (resize val))) addr
-- B-Type Instructions
BEQ (BTypeFields _ rs1 rs2 imm13) ->
let val1 = extractRegVal rs1
val2 = extractRegVal rs2
offset = signExtend imm13
in if val1 == val2 then Jump (addr + offset) else Jump (addr + 4)
BNE (BTypeFields _ rs1 rs2 imm13) ->
let val1 = extractRegVal rs1
val2 = extractRegVal rs2
offset = signExtend imm13
in if val1 /= val2 then Jump (addr + offset) else Jump (addr + 4)
BLT (BTypeFields _ rs1 rs2 imm13) ->
let val1 = unpack (pack (extractRegVal rs1) :: BitVector 64) :: Signed 64
val2 = unpack (pack (extractRegVal rs2) :: BitVector 64) :: Signed 64
offset = signExtend imm13
in if val1 < val2 then Jump (addr + offset) else Jump (addr + 4)
BGE (BTypeFields _ rs1 rs2 imm13) ->
let val1 = unpack (pack (extractRegVal rs1) :: BitVector 64) :: Signed 64
val2 = unpack (pack (extractRegVal rs2) :: BitVector 64) :: Signed 64
offset = signExtend imm13
in if val1 >= val2 then Jump (addr + offset) else Jump (addr + 4)
BLTU (BTypeFields _ rs1 rs2 imm13) ->
let val1 = extractRegVal rs1
val2 = extractRegVal rs2
offset = signExtend imm13
in if val1 < val2 then Jump (addr + offset) else Jump (addr + 4)
BGEU (BTypeFields _ rs1 rs2 imm13) ->
let val1 = extractRegVal rs1
val2 = extractRegVal rs2
offset = signExtend imm13
in if val1 >= val2 then Jump (addr + offset) else Jump (addr + 4)
-- U-Type Instructions
LUI (UTypeFields rd imm20) ->
let val = shiftL (resize imm20) 12
in WriteBackGPR rd val
AUIPC (UTypeFields rd imm20) ->
let val = addr + shiftL (resize imm20) 12
in WriteBackGPR rd val
-- J-Type Instructions
JAL (JTypeFields rd imm21) ->
let offset = signExtend imm21
in if rd /= 0 then WriteBackGPR rd (addr + 4) else Jump (addr + offset)
execute (Decode.DecodeException e addr) = Execute.DecodeException e addr
execute (Decode.InstructionException e addr) = Execute.InstructionException e addr

59
hs/Fetch.hs
View file

@ -3,24 +3,49 @@
module Fetch(
fetchInstruction,
FetchResult(..)) where
debugInsn,
FetchResult(..),
) where
import Clash.Prelude
import Types(Mem, Addr, Insn)
import Util(endianSwapWord)
import qualified Prelude as P
import Types(Addr, Insn)
import Bus(read)
import Bus(Peripherals(..))
import BusTypes(
ReadRequest(..),
TransactionSize(..),
BusVal(..),
BusError(..))
import Exceptions(Exception(..))
import Util((|>))
data FetchResult = Instruction Insn
| Misaligned Addr
data FetchResult = Instruction {insn :: Insn, insnAddr :: Addr}
| InstructionException {exception :: Exception, addr :: Addr}
deriving (Generic, Show, Eq, NFDataX)
fetchInstruction :: KnownNat n => Mem n -> Addr -> FetchResult
fetchInstruction mem addr =
let
isWordAligned = addr .&. 3 == 0
addrWordAligned = addr `shiftR` 2
insn = mem !! addrWordAligned
-- TODO : check if instruction is word aligned and create type
-- to capture if its not.
in
case isWordAligned of
True -> Instruction insn
False -> Misaligned addr
fetchInstruction :: Peripherals -> Addr -> IO FetchResult
fetchInstruction peripherals addr =
do
readReasponse <-Bus.read (BusTypes.ReadRequest addr BusTypes.SizeFullWord) peripherals
case readReasponse of
Right (BusFullWord insn) ->
pure |> Instruction insn addr
Left UnAligned ->
pure |> InstructionException InstructionAddressMisaligned addr
Left UnMapped ->
pure |> InstructionException InstructionAccessFault addr
Right _ ->
pure |> InstructionException InstructionAccessFault addr
debugInsn :: FetchResult -> String
debugInsn = show
-- case fetchResult of
-- Instruction insn ->
-- "Instruction raw binary | "
-- P.++ binaryInsn
-- P.++ " (" P.++ show insn P.++ ")"
-- where
-- binaryInsn = show (bitCoerce insn :: BitVector 32)
-- InstructionException e -> show e

206
hs/Isa/Decode.hs
View file

@ -1,206 +0,0 @@
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NumericUnderscores #-}
module Isa.Decode(decode) where
import Isa.Forms(
FUNCT7, RS2, RS1, FUNCT3, RD, OPCODE,
IMM12, IMM13, IMM20, IMM21,
RTypeFields(..), ITypeFields(..), STypeFields(..),
BTypeFields(..), UTypeFields(..), JTypeFields(..),
Opcode(..)
)
import Clash.Prelude
import Data.Functor.Contravariant (Op)
import Types(Mem, Addr, Insn)
import Distribution.Backpack.FullUnitId (FullDb)
getOpcode :: Insn -> Unsigned 7
getOpcode instr = bitCoerce $ slice d6 d0 (pack instr)
getImm12 :: Insn -> Unsigned 12
getImm12 instr = bitCoerce $ slice d31 d20 (pack instr)
getImm12SType :: Insn -> Unsigned 12
getImm12SType instr = bitCoerce $ immediateUpper ++# immediateLower
where
immediateUpper = (slice d31 d25 (pack instr))
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)
decodeRType :: Insn -> Opcode
decodeRType insn =
case opcode of
0b0110011 ->
case funct3 of
0x00 -> case funct7 of
0x00 -> ADD (RTypeFields opcode rd funct3 rs1 rs2 funct7)
0x20 -> SUB (RTypeFields opcode rd funct3 rs1 rs2 funct7)
_ -> Unimplemented
0x04 -> XOR (RTypeFields opcode rd funct3 rs1 rs2 funct7)
0x06 -> OR (RTypeFields opcode rd funct3 rs1 rs2 funct7)
0x07 -> AND (RTypeFields opcode rd funct3 rs1 rs2 funct7)
0x01 -> SLL (RTypeFields opcode rd funct3 rs1 rs2 funct7)
0x05 -> case funct7 of
0x00 -> SRL (RTypeFields opcode rd funct3 rs1 rs2 funct7)
0x20 -> SRA (RTypeFields opcode rd funct3 rs1 rs2 funct7)
_ -> Unimplemented
0x02 -> SLT (RTypeFields opcode rd funct3 rs1 rs2 funct7)
0x03 -> SLTU (RTypeFields opcode rd funct3 rs1 rs2 funct7)
_ -> Unimplemented
_ -> Unimplemented
where
opcode = getOpcode insn
rd = getRd insn
funct3 = getFunct3 insn
rs1 = getRs1 insn
rs2 = getRs2 insn
funct7 = getFunct7 insn
decodeIType :: Insn -> Opcode
decodeIType insn = case opcode of
0b0010011 -> case funct3 of
0x0 -> ADDI (ITypeFields opcode rd funct3 rs1 imm)
0x4 -> XORI (ITypeFields opcode rd funct3 rs1 imm)
0x6 -> ORI (ITypeFields opcode rd funct3 rs1 imm)
0x7 -> ANDI (ITypeFields opcode rd funct3 rs1 imm)
0x1 -> if slice d31 d25 (pack insn) == 0
then SLLI (ITypeFields opcode rd funct3 rs1 imm)
else Unimplemented
0x5 -> case slice d31 d25 (pack insn) of -- Distinguish SRLI and SRAI
0x00 -> SRLI (ITypeFields opcode rd funct3 rs1 imm)
0x20 -> SRAI (ITypeFields opcode rd funct3 rs1 imm)
_ -> Unimplemented
0x2 -> SLTI (ITypeFields opcode rd funct3 rs1 imm)
0x3 -> SLTIU (ITypeFields opcode rd funct3 rs1 imm)
_ -> Unimplemented
0b0000011 -> case funct3 of
0x0 -> LB (ITypeFields opcode rd funct3 rs1 imm)
0x1 -> LH (ITypeFields opcode rd funct3 rs1 imm)
0x2 -> LW (ITypeFields opcode rd funct3 rs1 imm)
0x4 -> LBU (ITypeFields opcode rd funct3 rs1 imm)
0x5 -> LHU (ITypeFields opcode rd funct3 rs1 imm)
_ -> Unimplemented
0b1100111 -> case funct3 of
0x0 -> JALR (ITypeFields opcode rd funct3 rs1 imm)
_ -> Unimplemented
0b1110011 -> case imm of
0x000 -> ECALL (ITypeFields opcode rd funct3 rs1 imm)
0x001 -> EBREAK (ITypeFields opcode rd funct3 rs1 imm)
_ -> Unimplemented
_ -> Unimplemented
where
opcode = getOpcode insn
rd = getRd insn
funct3 = getFunct3 insn
rs1 = getRs1 insn
imm = getImm12 insn
decodeSType :: Insn -> Opcode
decodeSType insn =
case opcode of
0b0100011 -> case funct3 of
0x0 -> SB (STypeFields opcode funct3 rs1 rs2 imm12) -- Store Byte
0x1 -> SH (STypeFields opcode funct3 rs1 rs2 imm12) -- Store Halfword
0x2 -> SW (STypeFields opcode funct3 rs1 rs2 imm12) -- Store Word
_ -> Unimplemented
_ -> Unimplemented
where
opcode = getOpcode insn
funct3 = getFunct3 insn
rs1 = getRs1 insn
rs2 = getRs2 insn
imm12 = getImm12SType insn
decodeBType :: Insn -> Opcode
decodeBType insn =
case opcode of
0b1100011 -> case funct3 of
0x0 -> BEQ (BTypeFields opcode funct3 rs1 rs2 imm13) -- Branch if equal
0x1 -> BNE (BTypeFields opcode funct3 rs1 rs2 imm13) -- Branch if not equal
0x4 -> BLT (BTypeFields opcode funct3 rs1 rs2 imm13) -- Branch if less than
0x5 -> BGE (BTypeFields opcode funct3 rs1 rs2 imm13) -- Branch if greater or equal
0x6 -> BLTU (BTypeFields opcode funct3 rs1 rs2 imm13) -- Branch if less than (unsigned)
0x7 -> BGEU (BTypeFields opcode funct3 rs1 rs2 imm13) -- Branch if greater or equal (unsigned)
_ -> Unimplemented
_ -> Unimplemented
where
opcode = getOpcode insn
funct3 = getFunct3 insn
rs1 = getRs1 insn
rs2 = getRs2 insn
imm13 = getImm13BType insn
decodeUType :: Insn -> Opcode
decodeUType insn = case opcode of
0b0110111 -> LUI (UTypeFields opcode rd imm20) -- LUI
0b0010111 -> AUIPC (UTypeFields opcode rd imm20) -- AUIPC
_ -> Unimplemented
where
opcode = getOpcode insn
rd = getRd insn
imm20 = getImm20UType insn
getImm21JType :: Insn -> Unsigned 21
getImm21JType instr = bitCoerce $ imm20 ++# imm10_1 ++# imm11 ++# imm19_12 ++# zero
where
imm20 = slice d31 d31 (pack instr) -- imm[20]
imm10_1 = slice d30 d21 (pack instr) -- imm[10:1]
imm11 = slice d20 d20 (pack instr) -- imm[11]
imm19_12 = slice d19 d12 (pack instr) -- imm[19:12]
zero = 0 :: BitVector 1 -- LSB always zero for J-type
decodeJType :: Insn -> Opcode
decodeJType insn =
case opcode of
0b1101111 -> JAL (JTypeFields opcode rd imm21) -- JAL
_ -> Unimplemented
where
opcode = getOpcode insn
rd = getRd insn
imm21 = getImm21JType insn
orElse :: Opcode -> Opcode -> Opcode
orElse Unimplemented y = y
orElse x _ = x
decode :: Insn -> Opcode
decode insn =
decodeRType insn `orElse`
decodeIType insn `orElse`
decodeSType insn `orElse`
decodeBType insn `orElse`
decodeUType insn `orElse`
decodeJType insn

75
hs/Machine.hs
View file

@ -1,75 +0,0 @@
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NumericUnderscores #-}
module Machine(
Machine(..),
RISCVCPU(..),
Peripherals(..),
Endian(..),
machineInit) where
import Clash.Prelude
import Types(Pc, Mem)
import RegFiles(GPR, FPR, CSR, gprInit, fprInit, csrInit)
import Peripherals.Ram(Ram)
data Endian = Big | Little
deriving (Generic, Show, Eq, NFDataX)
data PrivilegeLevel
= MachineMode
| SuperVisorMode
| UserMode
deriving (Generic, Show, Eq, NFDataX)
data Peripherals = Peripherals
{
ram :: Ram
}
deriving (Generic, Show, Eq, NFDataX)
data RISCVCPU = RISCVCPU
{ pc :: Pc,
gpr :: GPR,
fpr :: FPR,
privilegeLevel :: PrivilegeLevel
}
deriving (Generic, Show, Eq, NFDataX)
data Machine = Machine
{ cpu :: RISCVCPU,
peripherals :: Peripherals
}
deriving (Generic, Show, Eq, NFDataX)
riscvCPUInit :: RISCVCPU
riscvCPUInit =
RISCVCPU
0
gprInit
fprInit
MachineMode
machineInit :: Peripherals -> Machine
machineInit peripherals =
Machine
riscvCPUInit
peripherals
memInit :: Vec 14 (Unsigned 32)
memInit =
0x0000A03C
:> 0x3000A5E8
:> 0x1A002038
:> 0x18002598
:> 0x10002588
:> 0x01002170
:> 0xF8FF8141
:> 0x08002588
:> 0x01002138
:> 0x00002598
:> 0xE8FFFF4B
:> 0x00000060
:> 0x002000C0
:> 0x00000000
:> Nil

150
hs/Peripherals/Ram.hs
View file

@ -3,14 +3,28 @@
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TemplateHaskell #-}
module Peripherals.Ram(initRamFromFile, Ram) where
module Peripherals.Ram(
initRamFromFile,
RamAddr,
Ram,
RamLine,
bytesInRam,
read,
write,
) where
import Clash.Prelude
import Clash.Prelude hiding (empty, read)
import qualified Prelude as P
import qualified Data.ByteString.Lazy as BL
import Data.Binary.Get
import Data.Int (Int32)
import qualified Clash.Sized.Vector as Vec
import Types(Addr, FullWord, DoubleWord)
import BusTypes(
TransactionSize(..),
BusVal(..),
)
import Util((|>))
-- vector depth has to be known statically at compile time
#ifndef _RAM_DEPTH
@ -19,6 +33,101 @@ import qualified Clash.Sized.Vector as Vec
-- TODO : replace Unsigned 32 with BusVal types later...
type Ram = Vec _RAM_DEPTH (Unsigned 32)
type RamAddr = Unsigned (CLog 2 _RAM_DEPTH)
type RamLine = Unsigned 32
bytesInRam :: Addr
bytesInRam = _RAM_DEPTH * 4
read :: TransactionSize -> RamAddr -> Ram -> BusVal
read SizeByte addr ram = BusByte |> unpack byte
where
word = ram !! addr
byteOffset :: BitVector 2
byteOffset = slice d1 d0 addr
byte = case byteOffset of
0b00 -> slice d31 d24 word
0b01 -> slice d23 d16 word
0b10 -> slice d15 d8 word
0b11 -> slice d7 d0 word
read SizeHalfWord addr ram = BusHalfWord |> unpack halfWord
where
word = ram !! addr
halfWordOffset :: Unsigned 1
halfWordOffset = unpack |> slice d0 d0 addr
halfWord = case halfWordOffset of
0b0 -> slice d31 d16 word
0b1 -> slice d15 d0 word
read SizeFullWord addr ram = BusFullWord fullWord
where
fullWord = ram !! addr
read SizeDoubleWord addr ram = BusDoubleWord doubleWord
where
doubleWord = bitCoerce |> bitCoerce word0 ++# bitCoerce word1
word0 = readFullWordHelper ram addr
word1 = readFullWordHelper ram (addr + 1)
read SizeQuadWord addr ram = BusQuadWord quadWord
where
quadWord = bitCoerce |> bitCoerce dword0 ++# bitCoerce dword1
dword0 = readDoubleWordHelper ram addr
dword1 = readDoubleWordHelper ram (addr + 2)
readFullWordHelper :: Ram -> RamAddr -> FullWord
readFullWordHelper ram addr = ram !! addr
readDoubleWordHelper :: Ram -> RamAddr -> DoubleWord
readDoubleWordHelper ram addr = bitCoerce |> bitCoerce word0 ++# bitCoerce word1
where
word0 = readFullWordHelper ram addr
word1 = readFullWordHelper ram (addr + 1)
write :: BusVal -> RamAddr -> Ram -> Ram
write (BusByte byte) addr ram = replace addr updatedWord ram
where
word = ram !! addr
byteOffset :: BitVector 2
byteOffset = slice d1 d0 addr
updatedWord = case byteOffset of
0b00 -> setSlice d31 d24 (pack byte) word
0b01 -> setSlice d23 d16 (pack byte) word
0b10 -> setSlice d15 d8 (pack byte) word
0b11 -> setSlice d7 d0 (pack byte) word
write (BusHalfWord halfWord) addr ram = replace addr updatedWord ram
where
word = ram !! addr
halfWordOffset :: Unsigned 1
halfWordOffset = unpack |> slice d0 d0 addr
updatedWord = case halfWordOffset of
0b0 -> setSlice d31 d16 (pack halfWord) word
0b1 -> setSlice d15 d0 (pack halfWord) word
write (BusFullWord fullWord) addr ram = replace addr fullWord ram
write (BusDoubleWord doubleWord) addr ram = ram''
where
(word0, word1) = bitCoerce doubleWord
ram' = replace addr word0 ram
ram'' = replace (addr + 1) word1 ram'
write (BusQuadWord quadWord) addr ram = ram''''
where
(dword0 :: DoubleWord, dword1 :: DoubleWord) =
bitCoerce quadWord
(word0 :: FullWord, word1 :: FullWord) =
bitCoerce dword0
(word2 :: FullWord, word3 :: FullWord) =
bitCoerce dword1
ram' = replace addr word0 ram
ram'' = replace (addr + 1) word1 ram'
ram''' = replace (addr + 2) word2 ram''
ram'''' = replace (addr + 3) word3 ram'''
initRamFromFile :: FilePath -> IO (Maybe Ram)
initRamFromFile filePath =
@ -28,7 +137,7 @@ initRamFromFile filePath =
do
bs <- readFileIntoByteString filePath
let ints = getInts bs
pure $ populateVectorFromInt32 ints initRam
pure |> populateVectorFromInt32 ints initRam
readFileIntoByteString :: FilePath -> IO BL.ByteString
readFileIntoByteString filePath = BL.readFile filePath
@ -55,39 +164,6 @@ populateVectorFromInt32 ::
populateVectorFromInt32 ls v = Vec.fromList adjustedLs
where
vecLen = length v
adjustedLs = fromIntegral <$> adjustLength vecLen ls
adjustedLs = fmap fromIntegral (adjustLength vecLen ls)
adjustLength :: Int -> [Int32] -> [Int32]
adjustLength n xs = P.take n (xs P.++ P.repeat 0)
-- Function to increment each element of a Clash vector
-- prepareVector :: KnownNat n => [Int32] -> Vec n (Unsigned 32)
-- prepareVector xs = let
-- unsigneds = map (fromIntegral :: Int32 -> Unsigned 32) xs -- Step 1: Convert Int32 to Unsigned 32
-- len = length unsigneds
-- in case compare len (snatToNum (SNat @n)) of -- Step 2: Adjust the length of the list
-- LT -> takeI unsigneds ++ repeat 0 -- Pad with zeros if the list is shorter
-- GT -> takeI unsigneds -- Truncate if the list is longer
-- EQ -> takeI unsigneds -- No padding or truncation needed
-- Function to load firmware
-- loadFirmware :: KnownNat n => [Int32] -> Vec n (Unsigned 32)
-- loadFirmware (x:xs) = vecHead ++ vecTail
-- where
-- vecHead = singleton (fromIntegral x)
-- vecTail = loadFirmware xs
-- loadFirmware [] = takeI $ repeat 0
-- loadFirmware xs = v
-- where
-- mapped :: [Unsigned 32] = Clash.Prelude.fromIntegral <$> xs
-- c = takeI (mapped ++ repeat 0)
-- v = takeI $ (mapped ++ repeat 0)
-- -- Example usage
-- someList :: [Int32]
-- someList = [1, 2, 3, 4, 5]
-- mem :: Vec 16 (Unsigned 32)
-- mem = loadFirmware someList

7
hs/Peripherals/Setup.hs
View file

@ -7,6 +7,7 @@ import Peripherals.UartCFFI(initTerminal)
import Peripherals.Ram (initRamFromFile, Ram)
import Control.Exception (try)
import System.IO.Error (ioeGetErrorString)
import Util((|>))
type FirmwareFilePath = FilePath
@ -20,10 +21,10 @@ setupPeripherals firmwareFilePath = do
initTerminal
result <- try (initRamFromFile firmwareFilePath)
return $ case result of
return |> case result of
Right (Just ram) -> InitializedPeripherals ram
Right Nothing -> InitializationError $ firmwareFilePath ++ failure ++ suggestion
Left e -> InitializationError $ firmwareFilePath ++ failure ++ suggestion ++ " Error: " ++ ioeGetErrorString e
Right Nothing -> InitializationError |> firmwareFilePath ++ failure ++ suggestion
Left e -> InitializationError |> firmwareFilePath ++ failure ++ suggestion ++ " Error: " ++ ioeGetErrorString e
where
failure = ": Failed to initialize RAM from file!"
suggestion = " Is the file 4-byte aligned?"

77
hs/Peripherals/Uart.hs Normal file
View file

@ -0,0 +1,77 @@
module Peripherals.Uart (read, write, UartAddr) where
import Clash.Prelude hiding (read)
import Types (Byte)
import Data.Char (ord, chr)
import Peripherals.UartCFFI (
getCharFromTerminal,
writeCharToTerminal,
isCharAvailable,
)
import BusTypes (
TransactionSize(..),
BusVal(..),
)
import Util((|>))
-- based on a 16550 UART which has an address space of 8 bytes
type UartAddr = Unsigned 3
-- Receiver Buffer Register address (commonly 0x0 for 16550 UART)
rbrAddr :: UartAddr
rbrAddr = 0x0
thrAddr :: UartAddr
thrAddr = 0x0
-- Line Status Register address
lsrAddr :: UartAddr
lsrAddr = 0x5
-- Helper function to convert Byte to BusVal based on TransactionSize
busValFromByte :: TransactionSize -> Byte -> BusVal
busValFromByte size val = case size of
SizeByte -> BusByte val
SizeHalfWord -> BusHalfWord (resize val)
SizeFullWord -> BusFullWord (resize val)
SizeDoubleWord -> BusDoubleWord (resize val)
SizeQuadWord -> BusQuadWord (resize val)
-- Reads a character from the terminal (RBR equivalent)
buildRBR :: IO Byte
buildRBR = do
c <- getCharFromTerminal
return |> fromIntegral (ord c) -- Convert Char to Byte
-- Reads the Line Status Register (LSR) to check character availability
buildLSR :: IO Byte
buildLSR = do
(char_available :: Byte) <- fmap fromIntegral isCharAvailable
-- highly unlikely that we overflow stdout buffer, so we set
-- transmit to always ready
let (transmit_ready :: Byte) = 0b0010_0000
return (char_available .|. transmit_ready)
-- Updated 'read' function to handle RBR and LSR reads
read :: TransactionSize -> UartAddr -> IO BusVal
read size addr
| addr == rbrAddr = fmap (busValFromByte size) buildRBR
| addr == lsrAddr = fmap (busValFromByte size) buildLSR
| otherwise = return |> busValFromByte size 0x00
extractLowestByte :: BusVal -> Byte
extractLowestByte (BusByte b) = b
extractLowestByte (BusHalfWord hw) = resize hw
extractLowestByte (BusFullWord fw) = resize fw
extractLowestByte (BusDoubleWord dw) = resize dw
extractLowestByte (BusQuadWord qw) = resize qw
byteToChar :: Byte -> Char
byteToChar = chr . fromIntegral
write :: BusVal -> UartAddr -> IO ()
write val addr
| addr == thrAddr = writeCharToTerminal |> byteToChar |> extractLowestByte val
| otherwise = return ()

9
hs/Peripherals/UartCFFI.hs
View file

@ -7,13 +7,12 @@ module Peripherals.UartCFFI (
writeCharToTerminal,
isCharAvailable,
setupSigintHandler,
wasCtrlCReceived
ctrlCReceived
) where
import Prelude
import Util((|>))
import Foreign.C.Types
import Foreign.C.String
import Foreign.Ptr
import Data.Char (chr, ord)
-- Foreign imports directly corresponding to the C functions
@ -36,7 +35,7 @@ getCharFromTerminal :: IO Char
getCharFromTerminal = fmap (chr . fromEnum) c_getCharFromTerminal
writeCharToTerminal :: Char -> IO ()
writeCharToTerminal char = c_writeCharToTerminal (toEnum $ ord char)
writeCharToTerminal char = c_writeCharToTerminal (toEnum |> ord char)
isCharAvailable :: IO Int
isCharAvailable = fmap fromEnum c_isCharAvailable
@ -49,4 +48,4 @@ wasCtrlCReceived = fmap fromEnum c_wasCtrlCReceived
-- Improved version of the ctrlCReceived to use the new wasCtrlCReceived signature
ctrlCReceived :: IO Bool
ctrlCReceived = fmap (/= 0) wasCtrlCReceived
ctrlCReceived = fmap (/= 0) wasCtrlCReceived

109
hs/Read.hs Normal file
View file

@ -0,0 +1,109 @@
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NumericUnderscores #-}
module Read(Read.read) where
import DecodeTypes(
Opcode(..),
RTypeFields(..), ITypeFields(..), STypeFields(..),
BTypeFields(..), UTypeFields(..), JTypeFields(..),
)
import Clash.Prelude
import Decode(DecodeResult(..))
import Cpu(RISCVCPU(..))
import RegFiles (RegVal(..), GPR)
read :: DecodeResult -> RISCVCPU -> DecodeResult
read (Opcode opcode addr) riscvCPU =
let
gprRegFile = gpr riscvCPU
opcode' = case opcode of
-- R-Type
ADD fields -> (ADD (readRTypeFields fields gprRegFile))
SUB fields -> (SUB (readRTypeFields fields gprRegFile))
XOR fields -> (XOR (readRTypeFields fields gprRegFile))
OR fields -> (OR (readRTypeFields fields gprRegFile))
AND fields -> (AND (readRTypeFields fields gprRegFile))
SLL fields -> (SLL (readRTypeFields fields gprRegFile))
SRL fields -> (SRL (readRTypeFields fields gprRegFile))
SRA fields -> (SRA (readRTypeFields fields gprRegFile))
SLT fields -> (SLT (readRTypeFields fields gprRegFile))
SLTU fields -> (SLTU (readRTypeFields fields gprRegFile))
-- I-Type
ADDI fields -> (ADDI (readITypeFields fields gprRegFile))
XORI fields -> (XORI (readITypeFields fields gprRegFile))
ORI fields -> (ORI (readITypeFields fields gprRegFile))
ANDI fields -> (ANDI (readITypeFields fields gprRegFile))
SLLI fields -> (SLLI (readITypeFields fields gprRegFile))
SRLI fields -> (SRLI (readITypeFields fields gprRegFile))
SRAI fields -> (SRAI (readITypeFields fields gprRegFile))
SLTI fields -> (SLTI (readITypeFields fields gprRegFile))
SLTIU fields -> (SLTIU (readITypeFields fields gprRegFile))
LB fields -> (LB (readITypeFields fields gprRegFile))
LH fields -> (LH (readITypeFields fields gprRegFile))
LW fields -> (LW (readITypeFields fields gprRegFile))
LBU fields -> (LBU (readITypeFields fields gprRegFile))
LHU fields -> (LHU (readITypeFields fields gprRegFile))
JALR fields -> (JALR (readITypeFields fields gprRegFile))
ECALL fields -> (ECALL (readITypeFields fields gprRegFile)) -- No regs needed, but consistent
EBREAK fields -> (EBREAK (readITypeFields fields gprRegFile)) -- Ditto
-- S-Type
SB fields -> (SB (readSTypeFields fields gprRegFile))
SH fields -> (SH (readSTypeFields fields gprRegFile))
SW fields -> (SW (readSTypeFields fields gprRegFile))
-- B-Type
BEQ fields -> (BEQ (readBTypeFields fields gprRegFile))
BNE fields -> (BNE (readBTypeFields fields gprRegFile))
BLT fields -> (BLT (readBTypeFields fields gprRegFile))
BGE fields -> (BGE (readBTypeFields fields gprRegFile))
BLTU fields -> (BLTU (readBTypeFields fields gprRegFile))
BGEU fields -> (BGEU (readBTypeFields fields gprRegFile))
-- U-Type
LUI fields -> (LUI (readUTypeFields fields gprRegFile))
AUIPC fields -> (AUIPC (readUTypeFields fields gprRegFile))
-- J-Type
JAL fields -> (JAL (readJTypeFields fields gprRegFile))
in
Opcode opcode' addr
read (DecodeException e addr) _ = DecodeException e addr
read (InstructionException e addr) _ = InstructionException e addr
readRTypeFields :: RTypeFields -> GPR -> RTypeFields
readRTypeFields (RTypeFields rd funct3 rs1 rs2 funct7) gprRegFile =
let rs1_val = fetchGPRRegVal rs1 gprRegFile
rs2_val = fetchGPRRegVal rs2 gprRegFile
in RTypeFields rd funct3 rs1_val rs2_val funct7
readITypeFields :: ITypeFields -> GPR -> ITypeFields
readITypeFields (ITypeFields rd funct3 rs1 imm) gprRegFile =
let rs1_val = fetchGPRRegVal rs1 gprRegFile
in ITypeFields rd funct3 rs1_val imm
readSTypeFields :: STypeFields -> GPR -> STypeFields
readSTypeFields (STypeFields funct3 rs1 rs2 imm12) gprRegFile =
let rs1_val = fetchGPRRegVal rs1 gprRegFile
rs2_val = fetchGPRRegVal rs2 gprRegFile
in STypeFields funct3 rs1_val rs2_val imm12
readBTypeFields :: BTypeFields -> GPR -> BTypeFields
readBTypeFields (BTypeFields funct3 rs1 rs2 imm13) gprRegFile =
let rs1_val = fetchGPRRegVal rs1 gprRegFile
rs2_val = fetchGPRRegVal rs2 gprRegFile
in BTypeFields funct3 rs1_val rs2_val imm13
readUTypeFields :: UTypeFields -> GPR -> UTypeFields
readUTypeFields fields@(UTypeFields rd imm20) _ = fields
readJTypeFields :: JTypeFields -> GPR -> JTypeFields
readJTypeFields fields@(JTypeFields rd imm21) _ = fields
fetchGPRRegVal :: RegVal -> GPR -> RegVal
fetchGPRRegVal (Unpopulated idx) gprVal = Value idx (gprVal !! idx)
fetchGPRRegVal val@(Value _ _) _ = val -- Already populated, no change

104
hs/RegFiles.hs
View file

@ -1,7 +1,20 @@
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NumericUnderscores #-}
-- | This module defines the register files used in a RISC-V core, including:
-- General Purpose Registers (GPR), Floating Point Registers (FPR), and Control & Status Registers (CSR).
--
-- In RISC-V, besides the GPR, FPR, and CSR, we may also encounter
-- the following which are not modeled in this codebase:
-- * VRF (Vector Registers File) for vector processing.
-- * Debug Registers (DBR) for hardware debugging.
-- * Shadow Registers for fast context switching (optional).
-- * MPU Registers for memory protection.
-- * Counter/Timer Registers for time/cycle counting.
-- * Hypervisor Registers (HPR) for guest virtualization.
module RegFiles(
RegFileIdx,
RegVal(..),
GPR,
FPR,
CSR,
@ -11,19 +24,20 @@ module RegFiles(
) where
import Clash.Prelude
import Util((|>))
import Types(DoubleWord)
-- In RISC-V, besides the GPR, FPR, and CSR, we may also encounter
-- the following which are not modeled in this codebase.
-- * VRF(Vector Registers File) for vector processing.
-- * Debug Registers (DBR) for hardware debugging.
-- * Shadow Registers for fast context switching (optional).
-- * MPU Registers for memory protection.
-- * Counter/Timer Registers for time/cycle counting.
-- * Hypervisor Registers (HPR) for guest virtualization.
type RegFileIdx = Unsigned 5
data RegVal = Value {
regFileIdx :: RegFileIdx,
regVal :: DoubleWord
}
| Unpopulated {regFileIdx :: RegFileIdx}
deriving (Generic, Show, Eq, NFDataX)
type GPR = Vec 32 (Unsigned 64)
type FPR = Vec 32 (Unsigned 64)
type CSR = Vec 4096 (Unsigned 64)
type GPR = Vec 32 (Unsigned 64) -- General Purpose Registers
type FPR = Vec 32 (Unsigned 64) -- Floating Point Registers
type CSR = Vec 4096 (Unsigned 64) -- Control and Status Registers
gprInit :: GPR
gprInit = repeat 0
@ -31,26 +45,54 @@ gprInit = repeat 0
fprInit :: FPR
fprInit = repeat 0
-- TODO: CSR can't actually be all 0 during initialization.
-- We need to revisit the following and properly initialize
-- various registers later.
-- | The 'CSRName' data type enumerates a subset of RISC-V CSRs (Control and Status Registers)
-- that are modeled in this codebase. Each variant represents a particular CSR.
data CSRName =
STVEC -- ^ Supervisor Trap-Vector Base Address: Base address for supervisor mode exception handlers.
| SEPC -- ^ Supervisor Exception Program Counter: Holds the return address for supervisor mode exceptions.
| MSTATUS -- ^ Machine Status Register: Contains global machine status flags and control bits.
| MISA -- ^ Machine ISA Register: Indicates the supported ISA extensions and width.
| MTVEC -- ^ Machine Trap-Vector Base Address: Base address for machine mode exception handlers.
| MEPC -- ^ Machine Exception Program Counter: Holds the return address for machine mode exceptions.
| MVENDORID -- ^ Machine Vendor ID: Identifies the vendor of the processor.
| MARCHID -- ^ Machine Architecture ID: Identifies the architecture of the processor.
| MIMPID -- ^ Machine Implementation ID: Identifies the implementation of the processor.
deriving (Generic, Show, Eq, NFDataX)
-- | Map each 'CSRName' variant to its corresponding CSR address.
csrNameToAddr :: CSRName -> Integer
csrNameToAddr STVEC = 0x105 -- Address for Supervisor Trap-Vector
csrNameToAddr SEPC = 0x141 -- Address for Supervisor Exception PC
csrNameToAddr MSTATUS = 0x300
csrNameToAddr MISA = 0x301
csrNameToAddr MTVEC = 0x305
csrNameToAddr MEPC = 0x341 -- Address for Machine Exception PC
csrNameToAddr MVENDORID = 0xF11
csrNameToAddr MARCHID = 0xF12
csrNameToAddr MIMPID = 0xF13
-- | Initial CSR values.
-- Note: The CSR registers are not all zero during proper initialization; these values
-- are placeholders to be revisited for proper initialization later.
csrInit :: CSR
csrInit =
replace (0x301 :: Integer) misa_init
$ replace (0x300 :: Integer) mstatus_init
$ replace (0x305 :: Integer) mtvec_init
$ replace (0xF11 :: Integer) mvendorid_init
$ replace (0xF12 :: Integer) marchid_init
$ replace (0xF13 :: Integer) mimpid_init
$ replace (0x701 :: Integer) mtime_init
$ replace (0x321 :: Integer) mtimecmp_init
$ repeat 0
replace (csrNameToAddr STVEC) stvec_init |>
replace (csrNameToAddr SEPC) sepc_init |>
replace (csrNameToAddr MSTATUS) mstatus_init |>
replace (csrNameToAddr MISA) misa_init |>
replace (csrNameToAddr MTVEC) mtvec_init |>
replace (csrNameToAddr MEPC) mepc_init |>
replace (csrNameToAddr MVENDORID) mvendorid_init |>
replace (csrNameToAddr MARCHID) marchid_init |>
replace (csrNameToAddr MIMPID) mimpid_init |>
repeat 0
where
misa_init = 0x8000000000001104 -- `RV64IMAFD`
mstatus_init = 0x0000000000001800 -- Default `mstatus`
mtvec_init = 0x0000000000001000 -- Trap vector base
mvendorid_init = 0x00000000
marchid_init = 0x00000000
mimpid_init = 0x00000000
mtime_init = 0x0000000000000000
mtimecmp_init = 0xFFFFFFFFFFFFFFFF
stvec_init = 0x0000000000002000 -- Supervisor mode trap vector base address.
sepc_init = 0x0000000000000000 -- Supervisor Exception PC initial value.
mstatus_init = 0x0000000000001800 -- Default machine status.
misa_init = 0x8000000000001104 -- RV64IMAFD: Machine ISA with standard extensions.
mtvec_init = 0x0000000000001000 -- Machine mode trap vector base address.
mepc_init = 0x0000000000000000 -- Machine Exception PC initial value.
mvendorid_init = 0x00000000 -- Vendor-specific ID.
marchid_init = 0x00000000 -- Architecture-specific ID.
mimpid_init = 0x00000000 -- Implementation-specific ID.

95
hs/Simulation.hs
View file

@ -3,26 +3,26 @@
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ConstraintKinds #-}
module Simulation(Args(..), simulation, Simulation(..)) where
module Simulation(
Args(..),
simulation,
RISCVCPU(..),
Machine(..),
Simulation(..)
) where
import qualified Prelude as P
import Peripherals.Setup(setupPeripherals, InitializedPeripherals(..))
import Peripherals.Teardown(teardownPeripherals)
import Text.Printf (printf)
import Clash.Prelude
import Machine(
Machine(..),
import Bus(Peripherals(..))
import Read(read)
import Cpu(
RISCVCPU(..),
Peripherals(..),
machineInit, RISCVCPU (RISCVCPU))
import Fetch(fetchInstruction, FetchResult (Instruction, Misaligned))
import Isa.Decode(decode)
import Isa.Forms(Opcode(..))
import Peripherals.UartCFFI(writeCharToTerminal)
import Control.Concurrent (threadDelay)
import Debug.Trace
import Types (Mem, Addr)
riscvCPUInit)
import Fetch(fetchInstruction, debugInsn)
import Decode(decode)
import qualified Prelude as P
import Util((|>))
data Args = Args {
firmware :: FilePath
@ -32,53 +32,40 @@ data Simulation
= Success [Machine]
| Failure String
deriving (Show)
data Machine = Machine
{ cpu :: RISCVCPU,
peripherals :: Peripherals
}
deriving (Generic, Show, Eq, NFDataX)
-- machine :: Machine
-- machine = machineInit
machine' :: Machine -> Machine
machine' machine =
let
machinePeripherals = peripherals machine
machineMem = ram $ machinePeripherals
machineCPU = cpu machine
machinePC = pc machineCPU
addr = 0 :: Integer
mem' = replace addr (3) machineMem
peripherals' = machinePeripherals { ram = mem' }
cpu' = machineCPU { pc = machinePC + 4 }
instruction =
case (fetchInstruction machineMem machinePC) of
Instruction i -> i
_ -> undefined
in
case (fetchInstruction machineMem machinePC) of
Instruction insn ->
let binaryInsn = show (bitCoerce insn :: BitVector 32)
in trace ("Decoded instruction: " P.++ show opcode
P.++ " | Binary: " P.++ binaryInsn
P.++ " (" P.++ show insn P.++ ")") $
machine { cpu = cpu', peripherals = peripherals' }
where
opcode = decode insn
Misaligned addr -> undefined
simulationLoop :: Int -> Machine -> IO [Machine]
simulationLoop 0 state = return [state]
simulationLoop n state = do
let newState = machine' state
rest <- simulationLoop (n - 1) newState
return (state : rest)
simulationLoop 0 machine = return [machine]
simulationLoop n machine = do
let machinePeripherals = peripherals machine
currPc = pc |> cpu machine
fetchResult <- fetchInstruction machinePeripherals currPc
let decodeResult = Read.read (decode fetchResult) (cpu machine)
putStrLn |> show decodeResult -- P.++ debugInsn fetchResult
let pc' = currPc + 4
cpu' = (cpu machine) { pc = pc' }
machine' = machine { cpu = cpu' }
rest <- simulationLoop (n - 1) machine'
return (machine : rest)
simulation :: Args -> IO Simulation
simulation args = do
initializedPeripherals <- setupPeripherals (firmware args)
case initializedPeripherals of
InitializationError e -> return $ Failure e
InitializedPeripherals ram -> do
InitializationError e -> return |> Failure e
InitializedPeripherals ramDevice -> do
let initState = machineInit $ Machine.Peripherals ram
let initState =
Machine {
cpu = riscvCPUInit,
peripherals = Bus.Peripherals ramDevice
}
sim <- simulationLoop 15 initState
teardownPeripherals
return $ Success sim
return |> Success sim

22
hs/Types.hs
View file

@ -1,7 +1,11 @@
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NumericUnderscores #-}
module Types(Pc, BusVal(..), Mem, FullWord, Insn, Addr) where
module Types(
Pc, Mem, Insn, Addr,
Byte, HalfWord, FullWord, DoubleWord, QuadWord
)
where
import Clash.Prelude
@ -10,16 +14,8 @@ type HalfWord = Unsigned 16
type FullWord = Unsigned 32
type DoubleWord = Unsigned 64
type QuadWord = Unsigned 128
type Insn = FullWord
type Insn = FullWord
data BusVal
= BusByte Byte
| BusHalfWord HalfWord
| BusWord FullWord
| BusDoubleWord DoubleWord
| BusQuadWord QuadWord
deriving (Generic, Show, Eq, NFDataX)
type Pc = DoubleWord
type Addr = DoubleWord
type Mem n = Vec n FullWord
type Pc = DoubleWord
type Addr = DoubleWord
type Mem n = Vec n FullWord

46
hs/Util.hs
View file

@ -1,44 +1,10 @@
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE NumericUnderscores #-}
module Util(
powerIndex32,
powerIndex64,
endianSwapWord) where
(|>),
) 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
(|>) :: (a -> b) -> a -> b
f |> x = f x
infixr 0 |>

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)

14
rv_formal.cabal → rvFormal.cabal
View file

@ -87,16 +87,22 @@ library
exposed-modules:
Simulation
other-modules:
Isa.Decode,
Isa.Forms,
Fetch,
Decode,
DecodeTypes,
Execute,
Read,
Peripherals.Ram,
Peripherals.Uart,
Peripherals.UartCFFI,
Peripherals.Setup,
Peripherals.Teardown,
Types,
Machine,
Bus,
BusTypes,
Cpu,
RegFiles,
Fetch,
Exceptions,
Util
c-sources: c/uart_sim_device.c
include-dirs: c

13
rv_tests/hello_world/Makefile
View file

@ -1,12 +1,13 @@
# RISC-V toolchain
CC = riscv64-unknown-elf-gcc
AS = riscv64-unknown-elf-as
LD = riscv64-unknown-elf-ld
OBJCOPY = riscv64-unknown-elf-objcopy
CROSS_PREFIX ?= riscv64-unknown-elf
CC = $(CROSS_PREFIX)-gcc
AS = $(CROSS_PREFIX)-as
LD = $(CROSS_PREFIX)-ld
OBJCOPY = $(CROSS_PREFIX)-objcopy
QEMU = qemu-system-riscv64
# Compilation flags
ARCH_FLAGS = -march=rv64imac -mabi=lp64
ARCH_FLAGS = -march=rv64ima -mabi=lp64
LDSCRIPT = linker.ld
# Output files
@ -27,7 +28,7 @@ $(ELF): $(SRC) $(LDSCRIPT)
$(BIN): $(ELF)
$(OBJCOPY) -O binary $(ELF) $(BIN)
# Pad the binary to a multiple of 4 bytes
size=$$(stat -f%z $(BIN)); \
size=$$(stat -c %s $(BIN)); \
padding=$$(( (4 - (size % 4)) % 4 )); \
[ $$padding -ne 0 ] && dd if=/dev/zero bs=1 count=$$padding >> $(BIN) || true

BIN
rv_tests/hello_world/hello.elf
View file

Binary file not shown.

16
shell.nix
View file

@ -1,16 +0,0 @@
{ pkgs ? import <nixpkgs> {} }:
let
riscv64-linux = pkgs.pkgsCross.riscv64;
in
pkgs.mkShell {
buildInputs = [
riscv64-linux.gcc
riscv64-linux.binutils
riscv64-linux.glibc
];
shellHook = ''
echo "RISC-V Linux cross-compilation environment initialized!"
'';
}

10
stack.yaml
View file

@ -1,10 +0,0 @@
resolver: lts-21.20
extra-deps:
- GenericPretty-1.2.2
- clash-ghc-1.8.1
- clash-prelude-1.8.1
- clash-lib-1.8.1
- concurrent-supply-0.1.8
- prettyprinter-interp-0.2.0.0
- pretty-show-1.10