Formal Verification and Models - SVA: The Power of Assertions in SystemVerilog - page 458

of minterms, a D .a ^: b ^: c/ _ .a ^ b ^: c/ _ .a ^: b ^ c/ _ .a ^ b ^ c/. The property
p requires a to be true at each position of the trace, whereas the variables b and c
may have arbitrary values. t

We say that M satisfies the property p, or that M is a model for p, or that p is
valid on M , and write M ˆ p, iff all traces that M accepts also satisfy p.

Example 21.14. Let p be defined as the property always i |=> !o . The FV
model M corresponding to the module m from Example 21.8 satisfies p, i.e.,
M ˆ p, since every trace accepted by M satisfies p.

t

There are two important special cases of properties: true and false (correspond-
ing to SystemVerilog 1'b1 and 1'b0 , respectively). The property true is satisfied
on any trace. Therefore, its language consists of all possible traces defined by a
given set of variables. The property false is not satisfied on any trace. Therefore, its
language is empty.
In Chap. 4 , we introduced SystemVerilog assertion statements: assertions,
assumptions, and cover. From the formal point of view, all these statements are
properties used in different contexts. Below we discuss their formal meaning.

21.3.1 Asserts

When we check the validity of a property, it plays the role of an assert , as explained
in Chap. 4 . From the definition of M ˆ p, it follows that the property is valid iff
the language defined by this property contains the language defined by the model,
i.e., iff L.M / L.p/. For any model M ˆ true , and M 6ˆ false .

21.3.2 Assumes

As a property defines its own infinitary language, it is possible to check validity of an
assertion relative to this property instead of checking its validity on a model. We say
that the property p is valid assuming the property q, and write q ˆ p, iff all traces
satisfying q also satisfy p. When the validity of a property is assumed, it plays
theroleofan assumption , as explained in Chap. 4 . Note that for any assertion p,
false ˆ p since ; L.p/.
q ˆ p is equivalent to L.q/ L.p/. As we have seen in Example 21.8 ,an
assumption may replace a model in the sense that it defines the same language
(i.e., set of traces) as the model. More formally, the FV model M Dh V; Q; I; R i
is equivalent to the following assumption:

initial assume property (I and always R);