[fuklief]

So what kind of formal verification is it ? Is it proof assistant, model checking ? And what does it verify ? It's not really clear from a first glance.

[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?