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

Fig. 21.3 Formal verification
model explicitly clocked by
$global_clock

io

i

o

21.2.1 Time

To complete the picture, we need to introduce the notion of time. We assume that
RTL models are synchronous , i.e., that there is a global clock , called also the primary
system clock that synchronizes all the system transitions. Any signal change may
happen only at a tick of the global clock. This assumption is applicable even if
the system has several clock domains. For example, if there are two clock domains
controlled by clocks clk1 and clk2 , then the global clock should be defined as
an event clk1 or clk2 . In SystemVerilog, the global clock is introduced with
global clocking , and it can be referenced as $global_clock (Sect. 4.4.2 ). The
mapping of the global clock to events using global clocking is important in
simulation, but in FV this mapping is not necessary. In this chapter, we refer to
the global clock even if global clocking has not been defined in the design.
One might wonder why ticks of the global clock are not identified with simulation
ticks. Sometimes this is a good idea, but if all interesting signals are synchronized
by a relatively slow clock, then this mapping is too inefficient. Another reason may
be that we need to map the system clock to some clock in simulation to ignore
transitions that happen between ticks of the global clock.
The time in FV of RTL is discrete, and it is defined in terms of the ticks of
the global clock. Time 0 corresponds to the initial tick of the global clock, time 1
corresponds to the next one, etc. It is also assumed that the global clock never stops
ticking. Therefore, unlike in simulation, the time in FV is infinite.

All transitions in formal verification models are synchronized by

$global_clock .

Example 21.8. The model in Example 21.7 is controlled by an arbitrary clock
posedge c .If posedge c is the global clock, as in the code snippet below, then
the FV model can be simplified: V Df i; o g , Q Df; ; f i g ; f o g ; f i; o gg , I D Q.The
transitions of this model are depicted in Fig. 21.3 :

module m( input logic i, c, output o);
wire a=!i;
global clocking @( posedge c); endclocking