Chapter 6: Effective FPV for verification
Abstract
In this chapter, we describe how to effectively use formal property verification (FPV) for bug hunting, where we supplement simulation to try to find tricky corner case bugs. Using the example of a simple arithmetic logic unit design, we then show how to create a plan for Bug Hunting FPV on this model, exploring and expanding upon the parallels with the Design Exercise FPV discussed in the previous chapter. We walk through the process of planning, wiggling, and expanding FPV verification, in order to be able to gain confidence that we have verified the basic requirements of our logic, and prevented common errors that would cause incomplete coverage. Finally, we discuss changes that would ...
Get Formal Verification, 2nd Edition 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.
