Jun 11 – 13, 2024
Europe/Zurich timezone
There is a live webcast for this event.
FDF2024 pictures are online! Click the link in the side bar

Assertion-Based Formal Debugging During RTL Development

Jun 13, 2024, 9:40 AM
30/7-018 - Kjell Johnsen Auditorium (CERN)

30/7-018 - Kjell Johnsen Auditorium


Show room on map
HDL verification and simulation tools HDL development, verification, and simulation tools


N. Engelhardt (YosysHQ)


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

Primary author

N. Engelhardt (YosysHQ)

Presentation materials