Formal Verification

Chapter 5

Effective FPV for design exercise

Now that the reader is familiar with the general concepts of FPV, we use this chapter to describe FPV usage for the specific goal of providing “instant testbenches” for early exercise and testing of RTL designs. Using the motivating example of a small traffic light controller implemented with a set of interacting state machines, we walk through the typical steps of design exercise FPV. First we create a design exercise plan, a lightweight collection of goals, properties, complexity staging ideas, and exit criteria. Then we develop the design exercise FPV environment, which includes building the model, creating suitable properties, and other details such as clocks and resets. Once this preparation ...