Claire Xen  🏳️‍⚧️ 🏳️‍🌈 🧙🏻‍♀️ BLM  🏴 🚩

Best thing is: The MIT model has at least one bug that riscv-formal would catch immediately. But they don't know that because they 1/2

have not formally verified their model against ANYTHING yet. I'm not telling them bc I want to "find it with riscv-formal" first. :) 2/2

But I can't yet. Because so far they can't interface their model with anything that would actually allow me to use formal methods on it..

You’re saying there is a bug in the spec they are verifying against?

Yes. But they aren't verifying their spec against anything (yet). Their primary focus is on proofing abstract properties of the ISA..

And that is also very important of course, but I think the first step should be proving that the spec actually matches the implementation.

But but but... all the hard bits of specs and of processors are in exception handling. If you skip that bit, you’re doing the easy 10%