About
Traditionally, assertion-based formal verification is performed after RTL development is complete, by a separate team of verification engineers, to comprehensively prove conformance of a design. While this provides the highest safety guarantees, it is also a lengthy endeavour. But it is not necessary to aim to fully prove everything about a design to take advantage of property checkers' abilities. Instead, they can also be used as "simulation on steroids".
Using the SBY property checker from YosysHQ, this talk will demonstrate some approaches for incorporating formal tools as a debugging aid into the process of RTL development, complementary to simulation. This includes: - using cover statements to create testbenches - using properties to confirm invariants that the design relies on - validating subsystem interactions - bug hunting with assertions
If you've ever stared at an ILA trace and thought "But how can it get into this state? That's not possible!", this talk is for you..
0:00:00 Slide 1
0:01:30 Slide 2
0:02:40 Slide 3
0:03:45 Slide 4
0:05:56 Slide 5
0:07:40 Slide 6
0:09:50 Slide 7
0:11:10 Slide 8
0:17:19 Slide 9
The talk
Credits and licence
- Institution
- CERN
- Department
- FPGA Developers' Forum (FDF)
- Speaker
- N. Engelhardt
- 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