logo.png
LINKS
ABOUT

Symbiotic GmbH 
Alaudagasse 11/107/6 
1100 Vienna 
Austria

ATU73115835

SOCIAL

© 2019 All rights reserved - find out more about our privacy policy

Formal skeptic at work

Updated: May 16, 2019




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.



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

56 views