Add support for Sail unit tests

[Timmmm]

Note: This is a draft because it relies on this Sail compiler branch that I haven't finished yet.

---

This adds basic support for Sail unit tests. These have some pros and cons over C tests:

Pros:

• They don't require a RISC-V C compiler.
• They can test internal code (hence why I've called them unit tests).
• They can "cheat", e.g. to change privilege mode you can just magically cur_privilege = Supervisor. With C you have to implement a syscall, etc.

Cons:

• They are tied to internal code which will make refactoring more tedious because it means you are likely to need to update the tests. We can minimise that by using "high level" functions like execute(), read_CSR(), etc.
• They only run on the Sail model, so we can't e.g. verify them against SPIKE.

Given the sorry state of testing in this repo, and the fact that we don't have a way of writing C tests at all yet, I think this is probably a good medium term approach.

Currently the unit test executable reuses a load of code from the emulator, which is not ideal. When we have wrapped the model in a nice C++ library we can use that instead.

[jordancarlin]

Feels like these have the potential to be a lower barrier of entry for writing certain kinds of tests,(especially for tricky to reach edge cases of the system), so seems like a good idea to me. Once we get the C/assembly test situation sorted out we can think about what makes sense to run as a C test versus a unit test, but having both options seems like a net positive.

[jordancarlin]

@Timmmm Now that Sail 0.19 is released with unit test support, this is something that can be finished up if we still want it. Not sure that there are a whole lot of tests that should exist here instead of as first party assembly tests, but seems reasonable to include support for them.

[github-actions[bot]]

Test Results

401 tests  +1   401 ✅ +1   1m 32s ⏱️ +3s   1 suites ±0     0 💤 ±0    1 files   ±0     0 ❌ ±0 

Results for commit 359c327a. ± Comparison against base commit d8c3006f.

:recycle: This comment has been updated with latest results.

[Timmmm]

Rebased & README added.

[Timmmm]

I'll see if I can sort out the Lean errors.

[Timmmm]

Rebased but it's broken now and awkward to fix due to using the Sail generated header. Will probably have to wait until runtime XLEN is merged.

[Timmmm]

Rebased & tweaked a little to handle the changes since. I'll give this a couple of days before merging in case anyone wants to take a look.

[Timmmm]

Ah yeah good call - also since the XLEN stuff was merged I can move the generated C into the library. I renamed it to riscv_model since it's not just the support code now.

[jordancarlin]

Seems to have broken Lean:

error: build failed
✖ [45/46] Building LeanRV64D
trace: .> LEAN_PATH=/home/runner/work/sail-riscv/sail-riscv/build/model/Lean_RV64D/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4-nightly---nightly-2025-06-21/bin/lean --tstack=400000 /home/runner/work/sail-riscv/sail-riscv/build/model/Lean_RV64D/LeanRV64D.lean -R /home/runner/work/sail-riscv/sail-riscv/build/model/Lean_RV64D -o /home/runner/work/sail-riscv/sail-riscv/build/model/Lean_RV64D/.lake/build/lib/lean/LeanRV64D.olean -i /home/runner/work/sail-riscv/sail-riscv/build/model/Lean_RV64D/.lake/build/lib/lean/LeanRV64D.ilean -c /home/runner/work/sail-riscv/sail-riscv/build/model/Lean_RV64D/.lake/build/ir/LeanRV64D.c --setup /home/runner/work/sail-riscv/sail-riscv/build/model/Lean_RV64D/.lake/build/ir/LeanRV64D.setup.json --json
error: LeanRV64D.lean:171:32: unknown identifier 'undefined_RVFI_DII_Instruction_Packet'
error: LeanRV64D.lean:172:30: unknown identifier 'undefined_RVFI_DII_Execution_Packet_InstMetaData'
error: LeanRV64D.lean:173:28: unknown identifier 'undefined_RVFI_DII_Execution_Packet_PC'
error: LeanRV64D.lean:174:29: unknown identifier 'undefined_RVFI_DII_Execution_Packet_Ext_Integer'
error: LeanRV64D.lean:176:29: unknown identifier 'undefined_RVFI_DII_Execution_Packet_Ext_MemAccess'
error: LeanRV64D.lean:355:91: unknown identifier 'sail_main'
error: Lean exited with code 1

[Alasdair]

That's the same issue I've been having with my modules PR, so maybe the issue is unrelated if it's here too

[Timmmm]

Ok I had a look into this and the issue is that Lean is treating the very last function in the code as special. On master the LeanRV64D.lean file starts with

import LeanRV64D.Main

but on this branch it starts with

import LeanRV64D.TestMstatus

So the problem is I added a file after main.sail. I guess your PR does the same thing?

I'll reorder the files in this PR since it doesn't make much difference but that seems like something that should be fixed.