Global training solutions for engineers creating the world's electronics
KnowHow
Free Technical Resources
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 »
