Hardware Reference
In-Depth Information
Chapter 20
Introduction to Assertion-Based
Formal Verification
The man of science has learned to believe in justification, not by
faith, but by verification.
Thomas Huxley
In this and the following chapter, we probe deeper into the principles of formal
assertion-based verification: its methods of application, formal semantics of asser-
tions, and underlying models and algorithms. In this chapter our objective is to
familiarize the reader with the terminology as well as the methodologies that have
proven to be indispensable for many design groups. 1
There is a common opinion that only experts can do formal verification (FV), but
nobody claims that to simulate an RTL design one has to be an expert in simulation.
Indeed, it is not that difficult to run a simulator, but in some forms it is not more
difficult to run an FV tool either. Therefore, even people without special expertise
can carry out FV to some extent.
To run lightweight FV on an RTL block, it is only necessary to formulate
adequate assumptions constraining the inputs of the block. This is the trickiest
and the most effort consuming step in the verification. After that, running a formal
verification tool is not very different from running a simulation.
In contrast, an exhaustive formal verification of a design is a full-time job.
It requires model reduction and pruning, often writing abstract models for parts
of the design, checking specification completeness, iterative refinements, and
algorithm tuning. Perhaps in the future, if FV tool capacity drastically grows
or FV-friendly design methodologies are developed, exhaustive FV will become
automated, but currently it is not. Therefore, exhaustive verification is performed
1 This chapter and the next discuss special questions of formal verification and may be skipped.
However, this chapter explains further the nature of assertions, and it should be useful even for
readers who are interested only in simulation.
Search WWH ::




Custom Search