Yehowshua/RiscV-Formal
2
0
Fork 1
Code Issues 8 Pull requests Actions Packages Projects Releases Wiki Activity
An attempt at a formal model of the Risc-V ISA in Clash Haskell.
44 commits 1 branch 0 tags 301 KiB
Haskell 87.5%
Nix 4.6%
C 2.8%
Shell 2.4%
Makefile 1.7%
Other 1%
Find a file
Yehowshua 39780a1ac2 Add prep_for_llm.sh
2025-03-14 16:40:46 +00:00
bin initial support for exceptions 2025-03-02 23:12:02 -05:00
c Uart now has correct write implementation presumably 2025-02-26 01:51:33 -05:00
hs correct behavior of R type in execute 2025-03-13 16:26:03 -04:00
rv_tests/hello_world rv_tests/hello_world: Rename PREFIX var to CROSS_PREFIX and make it configurable 2025-03-14 01:17:11 +02:00
tables first commit 2025-02-12 23:54:15 -05:00
tests first commit 2025-02-12 23:54:15 -05:00
.gitignore hopefully progressing to a more scalable bus architecture 2025-02-25 14:24:54 -05:00
cabal.project Rename rv_formal.cabal to rvFormal 2025-03-14 00:23:30 +02:00
flake.lock Add flake 2025-03-14 00:23:30 +02:00
flake.nix flake.nix: Remove cross glibc 2025-03-14 01:43:26 +02:00
gen.sh first commit 2025-02-12 23:54:15 -05:00
LICENSE first commit 2025-02-12 23:54:15 -05:00
Notes.md hopefully progressing to a more scalable bus architecture 2025-02-25 14:24:54 -05:00
prep_for_llm.sh Add prep_for_llm.sh 2025-03-14 16:40:46 +00:00
README.md fixed execution of R type instructions 2025-03-13 14:31:38 -04:00
references.md fixed execution of R type instructions 2025-03-13 14:31:38 -04:00
rvFormal.cabal Rename rv_formal.cabal to rvFormal 2025-03-14 00:23:30 +02:00
Setup.hs first commit 2025-02-12 23:54:15 -05:00

README.md

About

An attempt at a formal reference model for the RISC-V ISA written in Clash Haskell.

Getting Started

This works with ghc 9.4.8

The clash compiler is basically a modified version of ghc designed to allow for first class support of haskell code as circuits.

Note that this repository is currently very much W.I.P. That being said, this is how you would currently run a simulation:

pushd rv_tests/hello_world/
make
popd
cabal run main --ghc-options="-D_RAM_DEPTH=2048" -- --firmware=./rv_tests/hello_world/hello.bin

Notes

All the context that we pick up as we execute an instruction in essence forms the context of our micro-op machinery.

Installing GCC-RISC-V Toolchain on [Insert Platform Here]

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

Grant Notes

  • Some forms may be redundant(may need to remove some)

Quality of Life Enhancements

  • turn off derive generics
  • update commands to use flags that prevent ghc intermediate outputs from littering source tree
  • enable Phoityne debug
  • learn to use trace and jupyter
  • draw conclusions on feasibility of debugging without VCD viewer