July 2015
Intermediate to advanced
408 pages
11h 7m
English
In Chapter 4, we introduce the basic concepts of Formal Property Verification (FPV), an FV method that checks whether a set of properties, usually specified as assertions, is true of a given piece of RTL. To make the discussion more concrete, we describe FPV in terms of a combination lock design, where we want to determine that there is truly a unique combination that opens the lock. We show how to build a set of useful properties, constructing SVA cover points, assumptions, and assertions related to our example. We then show how to combine this information with clock and reset specifications to create a viable FPV environment, and demonstrate typical results of running FPV on this example. Based on this ...
Read now
Unlock full access