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.
Edmund Humenberger is Co-Founder and CEO of Symbiotic EDA – a software company for formal-verification- and FPGA-design-tools to reduce risk for decision makers and engineers in the chip design and hardware manufacturing industry. @ Symbiotic GmbH All rights reserved