Hardware Reference
In-Depth Information
Example 22.22. Let D my_always(a) , where a is a Boolean. Show that for w a
word without any special letter > or ? , w ˆ iff w ˆ always a in the unclocked
semantics.
Solution: By definition, w ˆ iff for all k >0, w ˆ [k] . Also by definition,
[k] D my_always[k](a)
By the preceding example, for all k >0,
my_always[k](a) ( always [0:k-1] a) and nexttime [k] 1'b1
Since w has no special letter, w ˆ nexttime [k] 1'b1 for all k >0, and so
for all 0 i< j w j ; w i
w ˆ
iff
ˆ a
On the contrary, always a is formally defined as a until 0 in Annex F of the
LRM. Since w has no special letter, w i::
0 for all 0 i< j w j . Therefore,
for all 0 i< j w j ; w i
w ˆ always a iff
ˆ a
t
Example 22.23. Let a and b be Booleans, and let q be declared by
property q( property p);
a |-> p;
endproperty
Determine the unclocked formal semantics of the property
D q(my_always(q(b)))
Solution: By definition, w ˆ iff for all k >0, w ˆ [k] . Also by definition,
[k] D q[k](my_always[k](q[k](b)))
The declaration of q instantiates no named property, so for all k >0, q[k] D q .
Therefore, for all k >0,
[k] q(my_always[k](q(b)))
a |-> my_always[k](a |-> b)
a |-> (( always [0:k-1] a |-> b) and nexttime [k] 1'b1)
w ˆ nexttime [k] 1'b1 iff either j w j < k or w k
6D? . Therefore, w ˆ iff
either
1. j w jD 0,or
2. N w 0
a ,or
3.
both
Search WWH ::




Custom Search