A new RISC-V system crate and minor core improvements.
I have released machine-check 0.7.1. The major addition is a new machine-check-riscv system crate, currently containing a proof-of-concept system description of a RISC-V microcontroller Renesas R9A02G021 and minor improvements to machine-check itself.
I had originally played with the idea of automatically translating the official RISC-V specifications for use in machine-check descriptions. However, for time reasons, I instead programmed the RISC-V core manually using the reference manual for now. In some respects, this was a good exercise in itself: the nice and not-so-nice parts of writing a description accepted by the machine_description macro became more apparent, especially since I originally wrote the AVR description in a custom description language and just ported it into Rust for machine-check-avr.
One of the things that is not encountered too much in 8-bit microcontrollers is the conversion between various variable sizes (and consequent fun with endianness). While bitwise concatenation and slicing can be expressed by unsigned extensions and bit-shift operations, this turns into a caveman approach with the cumbersome syntax needed to make the machine_description macro happy.
However, while it is annoying to write the system, it is quite possible. See the book chapter for an example of what can be verified. From testing out things, I have a feeling that it is certainly possible to verify some properties of simple programs, but the more complex usual initialisation compared to AVR makes things sluggish. The good thing is that the basic refinement approach works, but I feel that both practical performance improvements and devising better algorithms are really necessary to make things practically viable.
As for minor improvements to other parts:
- Fixed a
machine_descriptionmacro output error when writing to arrays within multiple nested if conditions. - Within
machine_description, if expressions as last expressions in blocks no longer require a semicolon after their last branch. (Returning a value from them is still not supported.) - machine-check-avr now takes uninitialised register and memory values from parameters, so it should properly signal when verification results depend on uninitialised memory. (The same thing is done in the new RISC-V system.)
This concludes my efforts for 2025, and I will discuss the progress that has been done during the year in the next blogpost.