4 ms·

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 6y ago
  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 6y ago
    Wouldn't many bugs only surface in multi-instruction and status register interactions? But those are also probably way harder to verify.
    • sanxiyn 6y ago
      Consistency checks do check multiple instructions. Status registers are work in progress.
      • GregarianChild 6y ago
        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?