Global training solutions for engineers creating the world's electronics
Menu

Find a Training Course

Using Formal Verification on Packet Based Data Paths

Article from DVCon 2023 Formal Paper:

Doing the Impossible: Using Formal Verification on Packet Based Data Paths

by Senior Member Technical Staff, Doug Smith

Formal verification is known to work well in areas like control logic, interface protocols, and so on, but it is often dismissed for use on data paths since capacity becomes a significant issue. In particular, packet based protocols have potentially very large state spaces, which can pose a problem for formal. However, in this paper, a step by step process is presented, showing how to decompose a frame of data into simple formal constraints, modeling code, and assertions, which allows formal to fully explore the entire packet state space.

Paper Download

You welcome to Download the paper: Doing the Impossible: Using Formal Verification on Packet Based Data Paths »

Example Code Download

You can also download the coding used in paper using the following link. In exchange, we will ask you to enter some personal details. To read about how we use your details, click here. On the registration form, you will be asked whether you want us to send you further information concerning other Doulos products and services.

Download the source code for this paper »