[sanxiyn]

This uses riscv-formal. The default way to use riscv-formal is bounded model checking. It verifies all single instructions and some consistency checks, e.g. register read matches last logical register write in presence of reordering.

[the_duke]

Wouldn't many bugs only surface in multi-instruction and status register interactions?

But those are also probably way harder to verify.

[sanxiyn]

Consistency checks do check multiple instructions. Status registers are work in progress.

[GregarianChild]

That's interesting!

What kind of consistency checks (other than register state being preserved by commands that do not write to the register in question)? Is there some standard best practise?