Hacker News Reader

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.

View on HN

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.

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

But those are also probably way harder to verify.

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

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?

Reply on news.ycombinator.com