# Assertion-Based Formal Debugging During RTL Development

- Institution: CERN
- Department: FPGA Developers' Forum (FDF)
- Speaker: N. Engelhardt
- Year: 2024
- Language: English
- Source: [CERN](https://videos.cern.ch/record/3012082)
- Licence: [CERN](http://copyright.web.cern.ch)
- Who can watch: Teens profiles and older (sources give no ratings; placed by Invisible Network from the source's own words)

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

0:18:44 Slide 10

0:20:31 Slide 11

0:21:59 Slide 12

0:25:26 Slide 13

0:26:40 Slide 14

## Lectures

1. [Assertion-Based Formal Debugging During RTL Development](https://invisiblenetwork.ai/learn/cern/3012082/c2891f3680e5), 33 min (CERN's player)