formal skeptic at work

As a digital circuit designer, Matthew Ballance  had a theoretical understanding of formal methods, but never did see enough use in it to really look into.

When having the opportunity to design a Risc-V core, just out of curiosity he asked himself:

  • Would formal methods be more easily applied as a designer tool vs a tool for verifiers?
  • Could Formal be used as a turbo-charged unit test suite?

When he decided to create his Formal unit test suite, he expected it to help him in quickly identifying regressions as he made changes to the design. But, Formal lived up to its exhaustive-checking reputation and found a couple of corner case bugs that neither his simulation test suite, the RISC-V compliance test suite, nor running the Zephyr RTOS encountered.

Link to his Blog article which contains a lot more details.

Leave a Reply

Your email address will not be published. Required fields are marked *