A Roadmap for Formal Property

What is formal property verification? A natural language such as English allows
us to interpret the term formal property verification in two ways, namely:
• Verification of formal properties, or
• Formal methods for property verification
This inherent ambiguity in natural languages has been the source of many
logical bugs in chip designs. Design specifications are sometimes interpreted
in different ways by different designers with the result that the design’s architectural
intent is not implemented correctly. In an era where bugs are more
costly than transistors, the industry is beginning to realize the value of using
formal specifications.
In practice there are indeed two ways in which property verification is
done today. These are static Assertion-based Verification (ABV) and dynamic
Assertion-based Verification (ABV). In both forms, formal properties specify
the correctness requirements of the design, and the goal is to check whether a
given implementation satisfies the properties. Static ABV techniques formally
verify whether all possible behaviors of the design satisfy the given properties.
Dynamic ABV is a simulation-based approach, where the properties are
checked over a simulation run – the verification is thereby confined to only
those behaviors that are encountered during the simulation. In this book, we
shall refer to static ABV as formal property verification (FPV), and continue
to use dynamic ABV to refer to the simulation based property verification
approach.
The main tasks for a practitioner of property verification are as follows:
1. Development of the formal property specification. The main challenge here
is to express key features of the design intent in terms of formal properties.
2. Verifying the consistency and completeness of the specification. This is a
necessary step, because the first task is a non-trivial one and subject to
errors and oversights.
3. Verifying the implementation against the formal property specification. In
order to perform this task effectively, a verification engineer must be aware
of the limitations of the verification tool and must know the best way to
use the tool under various types of constraints.
All the above tasks are replete with open issues – the focus of this book is to
consider some of these issues and attempt to forecast the roadmap for FPV
and dynamic ABV within the existing design verification flows of chip design
companies. This chapter will summarize some of the major challenges. Let us
use the following case as a running example for our discussion.
Example 1.1. Let us consider the specification of a 2-way priority arbiter having
the following interface:
mem-arbiter( input r1, r2, clk, output g1, g2 )
r1 and r2 are the request lines, g1 and g2 are the corresponding grant lines,
and clk is the clock on which the arbiter samples its inputs and performs the
arbitration.We assume that the arbitration decision for the inputs at one cycle
is reflected by the status of the grant lines in the next cycle. Let us suppose
that the specification of the arbiter contains the following requirements:
1. Request line r1 has higher priority than request line r2. Whenever r1 goes
high, the grant line g1 must be asserted for the next two cycles.
2. When none of the request lines are high, the arbiter parks the grant on
g2 in the next cycle.
3. The grant lines, g1 and g2, are mutually exclusive.
It is difficult to locate a book on formal verification that does not have an
arbiter example - we hereby follow the tradition!