Formal Verification, 2nd Edition

Chapter 4: Formal property verification

Abstract

In Chapter 4, we introduce the basic concepts of formal property verification (FPV), a formal verification method that checks whether a set of properties, usually specified as assertions, is true of a given piece of register transfer level. 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 SystemVerilog Assertions cover properties, 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 ...