Artturin/RiscV-Formal
1
0
Fork 0
forked from Yehowshua/RiscV-Formal
Code Pull requests Activity
An attempt at a formal model of the Risc-V ISA in Clash Haskell.
10 commits 2 branches 0 tags 149 KiB
Haskell 85.7%
C 4.9%
Makefile 3.3%
Shell 3.3%
Assembly 1.9%
Other 0.9%
Find a file
Artturin 67fcd15f42 After make clean and make, this file changes 
`make run` works

I think it is due to a compiler update.

nixpkgs gcc is 14

https://chatgpt.com/share/67ba3552-3434-800d-a9cf-bf246b8619db

`diffoscope old-hello.elf new-hello.elf`

```
--- old-hello.elf
+++ new-hello.elf
├── readelf --wide --file-header {}
│ @@ -6,15 +6,15 @@
│    OS/ABI:                            UNIX - System V
│    ABI Version:                       0
│    Type:                              EXEC (Executable file)
│    Machine:                           RISC-V
│    Version:                           0x1
│    Entry point address:               0x80000000
│    Start of program headers:          64 (bytes into file)
│ -  Start of section headers:          4600 (bytes into file)
│ +  Start of section headers:          4632 (bytes into file)
│    Flags:                             0x1, RVC, soft-float ABI
│    Size of this header:               64 (bytes)
│    Size of program headers:           56 (bytes)
│    Number of program headers:         2
│    Size of section headers:           64 (bytes)
│    Number of section headers:         7
│    Section header string table index: 6
├── readelf --wide --program-header {}
│ @@ -1,14 +1,14 @@
│
│  Elf file type is EXEC (Executable file)
│  Entry point 0x80000000
│  There are 2 program headers, starting at offset 64
│
│  Program Headers:
│    Type           Offset   VirtAddr           PhysAddr           FileSiz  MemSiz   Flg Align
│ -  RISCV_ATTRIBUT 0x00102b 0x0000000000000000 0x0000000000000000 0x000032 0x000000 R   0x1
│ +  RISCV_ATTRIBUT 0x00102b 0x0000000000000000 0x0000000000000000 0x000045 0x000000 R   0x1
│    LOAD           0x001000 0x0000000080000000 0x0000000080000000 0x00002b 0x00002b R E 0x1000
│
│   Section to Segment mapping:
│    Segment Sections...
│     00     .riscv.attributes
│     01     .text .rodata
├── readelf --wide --sections {}
│ @@ -1,16 +1,16 @@
│ -There are 7 section headers, starting at offset 0x11f8:
│ +There are 7 section headers, starting at offset 0x1218:
│
│  Section Headers:
│    [Nr] Name              Type            Address          Off    Size   ES Flg Lk Inf Al
│    [ 0]                   NULL            0000000000000000 000000 000000 00      0   0  0
│    [ 1] .text             PROGBITS        0000000080000000 001000 00001c 00  AX  0   0  2
│    [ 2] .rodata           PROGBITS        000000008000001c 00101c 00000f 00   A  0   0  1
│ -  [ 3] .riscv.attributes RISCV_ATTRIBUTES 0000000000000000 00102b 000032 00      0   0  1
│ -  [ 4] .symtab           SYMTAB          0000000000000000 001060 000108 18      5  10  8
│ -  [ 5] .strtab           STRTAB          0000000000000000 001168 00004f 00      0   0  1
│ -  [ 6] .shstrtab         STRTAB          0000000000000000 0011b7 00003b 00      0   0  1
│ +  [ 3] .riscv.attributes RISCV_ATTRIBUTES 0000000000000000 00102b 000045 00      0   0  1
│ +  [ 4] .symtab           SYMTAB          0000000000000000 001070 000108 18      5  10  8
│ +  [ 5] .strtab           STRTAB          0000000000000000 001178 000062 00      0   0  1
│ +  [ 6] .shstrtab         STRTAB          0000000000000000 0011da 00003b 00      0   0  1
│  Key to Flags:
│    W (write), A (alloc), X (execute), M (merge), S (strings), I (info),
│    L (link order), O (extra OS processing required), G (group), T (TLS),
│    C (compressed), x (unknown), o (OS specific), E (exclude),
│    D (mbind), p (processor specific)
├── readelf --wide --symbols {}
│ @@ -3,12 +3,12 @@
│     Num:    Value          Size Type    Bind   Vis      Ndx Name
│       0: 0000000000000000     0 NOTYPE  LOCAL  DEFAULT  UND
│       1: 0000000080000000     0 SECTION LOCAL  DEFAULT    1 .text
│       2: 000000008000001c     0 SECTION LOCAL  DEFAULT    2 .rodata
│       3: 0000000000000000     0 SECTION LOCAL  DEFAULT    3 .riscv.attributes
│       4: 0000000000000000     0 FILE    LOCAL  DEFAULT  ABS hello.o
│       5: 0000000010000000     0 NOTYPE  LOCAL  DEFAULT  ABS UART_BASE
│ -     6: 0000000080000000     0 NOTYPE  LOCAL  DEFAULT    1 $xrv64i2p1_m2p0_a2p1_c2p0_zmmul1p0
│ +     6: 0000000080000000     0 NOTYPE  LOCAL  DEFAULT    1 $xrv64i2p1_m2p0_a2p1_c2p0_zmmul1p0_zaamo1p0_zalrsc1p0
│       7: 000000008000001c     0 NOTYPE  LOCAL  DEFAULT    2 message
│       8: 0000000080000008     0 NOTYPE  LOCAL  DEFAULT    1 loop
│       9: 000000008000001a     0 NOTYPE  LOCAL  DEFAULT    1 exit
│      10: 0000000080000000     0 NOTYPE  GLOBAL DEFAULT    1 _start
├── strings --all --bytes=8 {}
│ @@ -1,6 +1,6 @@
│  Hello, world!
│ -rv64i2p1_m2p0_a2p1_c2p0_zmmul1p0
│ +rv64i2p1_m2p0_a2p1_c2p0_zmmul1p0_zaamo1p0_zalrsc1p0
│  UART_BASE
│ -$xrv64i2p1_m2p0_a2p1_c2p0_zmmul1p0
│ +$xrv64i2p1_m2p0_a2p1_c2p0_zmmul1p0_zaamo1p0_zalrsc1p0
│  .shstrtab
│  .riscv.attributes
├── readelf --wide --decompress --hex-dump=.riscv.attributes {}
│ @@ -1,7 +1,8 @@
│
│  Hex dump of section '.riscv.attributes':
│ -  0x00000000 41310000 00726973 63760001 27000000 A1...riscv..'...
│ +  0x00000000 41440000 00726973 63760001 3a000000 AD...riscv..:...
│    0x00000010 05727636 34693270 315f6d32 70305f61 .rv64i2p1_m2p0_a
│    0x00000020 3270315f 63327030 5f7a6d6d 756c3170 2p1_c2p0_zmmul1p
│ -  0x00000030 3000                                0.
│ +  0x00000030 305f7a61 616d6f31 70305f7a 616c7273 0_zaamo1p0_zalrs
│ +  0x00000040 63317030 00                         c1p0.
├── readelf --wide --decompress --hex-dump=.strtab {}
│ @@ -1,8 +1,10 @@
│
│  Hex dump of section '.strtab':
│    0x00000000 0068656c 6c6f2e6f 00554152 545f4241 .hello.o.UART_BA
│    0x00000010 53450024 78727636 34693270 315f6d32 SE.$xrv64i2p1_m2
│    0x00000020 70305f61 3270315f 63327030 5f7a6d6d p0_a2p1_c2p0_zmm
│ -  0x00000030 756c3170 30006d65 73736167 65006c6f ul1p0.message.lo
│ -  0x00000040 6f700065 78697400 5f737461 727400   op.exit._start.
│ +  0x00000030 756c3170 305f7a61 616d6f31 70305f7a ul1p0_zaamo1p0_z
│ +  0x00000040 616c7273 63317030 006d6573 73616765 alrsc1p0.message
│ +  0x00000050 006c6f6f 70006578 6974005f 73746172 .loop.exit._star
│ +  0x00000060 7400                                t.
```
2025-02-22 22:37:34 +02:00
bin getting closer... 2025-02-19 09:06:40 -05:00
c first commit 2025-02-12 23:54:15 -05:00
hs works even better now 2025-02-19 18:28:08 -05:00
rv_tests/hello_world After make clean and make, this file changes 2025-02-22 22:37:34 +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 first commit 2025-02-12 23:54:15 -05:00
cabal.project Rename rv_formal.cabal to rvFormal 2025-02-22 22:33:26 +02:00
flake.lock Add flake 2025-02-22 22:33:26 +02:00
flake.nix Add flake 2025-02-22 22:33: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
README.md first commit 2025-02-12 23:54:15 -05:00
rvFormal.cabal Rename rv_formal.cabal to rvFormal 2025-02-22 22:33:26 +02:00
Setup.hs first commit 2025-02-12 23:54:15 -05:00
stack.yaml 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:

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

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)

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