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

Open source formal verification with SymbiYosis

Jun 13, 2024, 10:15 AM
30m
30/7-018 - Kjell Johnsen Auditorium (CERN)

30/7-018 - Kjell Johnsen Auditorium

CERN

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

Speaker

Yann Thoma (HEIG-VD)

Description

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.

Talk's Q&A During the talk
Talk duration 20'+10'
Will you be able to present in person? Yes

Primary author

Yann Thoma (HEIG-VD)

Presentation materials