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

Example 21.12. The transition relation i ˚ o 0 of the module m from Example 21.8
may be represented in SystemVerilog as i != $future_gclk(o) , and the module
m is equivalent to the following assumption m1
m1: assume property (@$global_clock i != $future_gclk(o));
This equivalence should be understood in the following sense: the set of infinite
traces (relative to the global clock) consistent with the module m is identical to the
set of the traces satisfying the assumption m1 . t

The global clocking future sampled value functions do not require any additional
modeling. They are already built into the FV model. On the contrary, the past
sampled value functions do require additional modeling. For example, the function
$past(a,,,@( posedge clk)) , is represented as follows:
type (a) pa;
always @( posedge clk)pa<=a;
As we have seen, each past value of a one-bit expression effectively adds a new
variable to the FV model, and thus doubles the total number of the model states!

Efficiency Tip. In FV, future value functions are more efficient than their past value
counterparts. 5
Note, however, that using future value functions in simulation may have the
opposite effect. It may increase the simulation load. Therefore, when writing
assertions keep in mind the target verification tool.

21.3 Properties

In Sect. 21.2 , we saw that an FV model M defines an infinitary language L.M /,the
set of infinite traces it accepts. Each property p also defines an infinitary language
L.p/, the set of infinite traces that satisfy it.

Example 21.13. If V Df a; b; c g , the property p D always a defines a language

L.p/ Df a ! g , that is, a set of all infinite traces aa:::. The notation a !

means

repetition of a infinitely many times.
The alphabet of this language is ˙ D 2 V , the set of all subsets of the set f a; b; c g .
aa::: is therefore not a single trace, but a family of traces, as a is a symbolic
representation of the set of the letters ff a g ; f a; b g ; f a; c g ; f a; b; c gg . As a disjunction

5 Some FV tools represent the transition relations not between current and next variables, but
between past and current variables. However, this approach is inconsistent with the SystemVerilog
semantics requiring the past value of a bit variable be 0 at the initial moment.