Formal Semantics - SVA: The Power of Assertions in SystemVerilog - page 476

Chapter 22
Formal Semantics

I don't want to get bogged down in semantics causing problems.
— Pervez Musharraf

To enable formal verification of assertions, the assertions must be formally defined:
it must be possible to unambiguously tell whether a specific DUT behavior satisfies
a given assertion or not. The formal definition of the meaning of an assertion is
called its formal semantics . Our intuition works well for simple assertions, but
to understand the exact meaning of complex assertions requires knowledge of
the formal semantics. This chapter is dedicated to the description of the formal
semantics of sequences, properties, and assertions.
This chapter can be skipped on the first reading, but those who wish to obtain
deep insight into SystemVerilog assertions need to carefully study it. Some of
the aspects of this chapter are useful primarily to people who deal with formal
verification, but others are important also for simulation. Throughout this chapter,
unless otherwise specified, we make the same notational assumptions as in Chap. 21 .
We also continue to assume that variables and expressions are 2-state and that global
clocking applies to all properties unless otherwise specified.

22.1 Formal Semantics of Properties

We have seen that a property defines its own language, we now need to describe this
language precisely for every property that can be expressed in SVA. The formal defi-
nition of the language is called the formal semantics of the property. Understanding
the formal semantics of each SVA property is important to understanding the exact
meaning of each temporal formula. In Chaps. 5 and 10 we described the semantics
of the properties informally. In this chapter, we provide the formal description.