Speaker
Description
Verification of digital systems is an art, and often implemented through testbenches and functional verification.
Formal verification is an alternative approach where we describe properties representing the expected behaviour of the system. It allows to prove these properties are fulfilled through assertions. It complements traditional behavioural simulations and allows to detect issues that can be very hard to find with traditional methods, as well as to exhaustively validate properties which would otherwise imply prohibitively-long simulations
In this presentation we will show how we used SymbiYosis, an open source tool, to formally prove the correctness of parts of a space probe FPGA design thanks to assertions written in PSL.
Through some practical examples, easily understandable for FPGA developers, we will illustrate the power of formal verification as well as its complementarity with respect to traditional testbenches.
| Talk's Q&A | During the talk |
|---|---|
| Talk duration | 20'+10' |
| Will you be able to present in person? | Yes |
