Speaker
Description
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.
| Talk's Q&A | During the talk |
|---|---|
| Talk duration | 25'+12' |
| Will you be able to present in person? | Yes |
