Formal property verification
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 ...
Get Formal Verification now with the O’Reilly learning platform.
O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.
