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

The automaton in Fig. 21.7 differs from the automaton in Fig. 21.4 in several
points:

￿ There is a self-loop in the state s 2 labeled with : c, which reflects the automaton
waiting for the clock c to transition to the state s 3 .
￿ There is an additional guard c on the edges s 1 ! s 2 and s 2 ! s 3 allowing the
state transitions only at a clock tick.

The automaton reaches its accepting state s 3 iff the property fails. For the
property to fail, the clock must tick enough times to allow the transition from the
initial state to the accepting state.
It is quite natural that the automaton of the complement of the clocked property
is more complex than that of the unclocked property, and therefore FV of clocked
properties is more expensive than FV of the unclocked ones. The main penalty of the
verification of the clocked properties is due to the fact that their clock is considered
to be an arbitrary signal. In practice, however, the waveform of the clock is often
well known, and can be expressed through the system clock in a regular manner.
For example, the clock may tick each second tick of the global clock. In such a case,
FV of clocked properties can be made much more efficient. Therefore, many FV
tools ask for a clock pattern. Some of them may also derive this information from
the global clocking statement and RTL. However, some FV tools may ignore the
global clocking statement.

21.5 Weak and Strong Operators

Temporal operators behave differently relative to their clock: some of them require
their clock to tick enough times to witness success, whereas others just require no
evidence of failure while the clock is ticking. The operators belonging to the first
group are called strong , and the operators from the second group are called weak .
The weak operators considered so far are weak , |-> , |=> , nexttime , always ,
until , and until_with . The operators strong , s_nexttime , s_eventually ,
s_until , and s_until_with are strong. The suffix conjunction operators #-#
and #=# are also strong. All strong operators denoted by keywords have a special
mnemonics: their names begin with the prefix s_ , except for the operator strong .
The weak operators, when they are not in the scope of a negation, yield only safety
properties.

Example 21.26. Consider the following properties:

1. @clk s_nexttime a
2. @$global_clock s_nexttime a
3. @clk a s_until b
4. @$global_clock a s_until b
5. @clk (a s_until b) or always a .