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

Fig. 21.5 Automaton for
complement of property
always a |=> ##2 b

a true true ¬ b

s 1 s 2 s 3 s 4 s 5

true

may start whenever. It will be non-vacuous only if a holds when it starts. Then, the
automaton moves to state s 2 . If in the next tick of the global clock b does not hold,
the automaton moves to state s 3 , which is the bad state of the automaton.

t

Example 21.19. Synthesize the automaton from Fig. 21.4 (Example 21.18 )into

RTL.

Solution:

logic s1 = 1'b1, s2 = 1'b0, s3 = 1'b0;
always @$global_clock begin
s1 <= s1;
s2 <= s1 && a;
s3 <= s2 && !b;
end

Discussion: This code implies that s1 always equals to 1'b1 and therefore its
computation is redundant. The optimized code is:

logic s2 = 1'b0, s3 = 1'b0;
always @$global_clock begin
s2 <= a;
s3 <= s2 && !b;
end
s3 == 1 is a bad state: if s3 becomes 1'b1 , the assertion fails .

t

The fact that a safety property may be synthesized into RTL reflects the well-
known practice of implementing assertions in RTL as an instrumented code. This
practice was common before the assertion specification languages became widely
accepted (Chap. 1 ).

Example 21.20. Build an automaton for the complement of the property always

a |=> ##2 b .
Solution: Its automaton is depicted in Fig. 21.5 .

t

As we can see from the comparison of Examples 21.18 and 21.20 ,themore
complex the property is and the bigger its bounded time windows are, the more
states its automaton has. Interestingly, infinite time windows do not introduce many
additional states as illustrated in the following example.

Example 21.21. Build an automaton of the complement of the property always
a[+] ##1 b |=> c .