3 ms·
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. reg
by 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 agoWouldn't many bugs only surface in multi-instruction and status register interactions? But those are also probably way harder to verify.
- sanxiyn 6y agoConsistency checks do check multiple instructions. Status registers are work in progress.
- GregarianChild 6y agoThat'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?