About
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..
0:00:00 Slide 1
0:01:50 Slide 2
0:03:32 Slide 3
0:04:33 Slide 4
0:05:37 Slide 5
0:07:48 Slide 6
0:09:07 Slide 7
0:16:14 Slide 8
0:17:30 Slide 9
The talk
Credits and licence
- Institution
- CERN
- Department
- FPGA Developers' Forum (FDF)
- Speaker
- Yann Thoma
- Year
- 2024
- Language
- English
- Source
- CERN
- Licence
- CERN, as CERN states it. CERN's terms
- Attribution
- © CERN. CERN provides its audiovisual media free of charge for educational and informational use, credited to CERN; this lecture is shown in CERN's own player.
- Who can watch
- CERN gives no rating. Invisible Network shows it to Teens profiles and older, judged from what the source says about it. How courses are placed