The abstract grammar for
clocked sequences is
S ::= @(b) R //
"clock" form
| (
S ) // "parenthesized" form
| ( S ##1 S ) // "concatenation" form
Each instance of R in this production must be a non-degenerate
unclocked sequence. In the "sequence" form, R must not be tightly satisfied by the
empty word. See H.3.2 and H.3.5
for the definitions of non-degeneracy and tight satisfaction.
Each instance of S in this production must be a non-degenerate
clocked sequence. In the "sequence" form, S must not be tightly satisfied by the empty word. See H.3.2 and H.3.5 for the definitions of non-degeneracy and
tight satisfaction.
Throughout the sequel, the following
notational conventions will be used: b, c denote boolean expressions; v denotes a
local variable name; e denotes an expression; N, N1, N2 denote negation
specifiers; R, R1, R2 denote unclocked sequences; S, S1, S2 denote clocked
sequences; P, P1,
P2 denotes an unclocked property properties;
Q denotes a clocked property; A denotes an assertion; i, j, k, m, n denote
non-negative integer constants.
• ( S1 |=> Q ) ((S1 ##1 @(1) 1 ) |-> Q ) .
• b [*->m:n] ( !b [*0:$] ##1 b )[*m:n] .
• b [*->m:$] (
!b [*0:$] ##1 b )[*m:$] .
• b [*->m] ( !b [*0:$] ##1 b)[*m] .
• b [*=m:n] ( b [*->m:n] ##1 !b [*0:$] ) .
• b [*=m:$] ( b [*->m:$] ##1 !b [*0:$] ) .
• b [*=m] ( b [*->m] ##1 !b [*0:$] )
• ( S1 ## S2 ) |-à ( S1 ##1 S2 ) .
first bullet under "Neutral satsifaction
of assertions". Change {\overline{w}}^i to \overline{w}^i The braces "{}" should
not appear. Here, w and i are both italic. I am
writing "\overline{w}" to mean w with an overline,
but no braces. The braces in "\overline{w}" just show that only w is overlined.
The result of this change should be that
\overline{w}^i |= b
looks just like the preceding
\overline{w}^i |= c
with the exception that "b" appears instead of
"c".
...
w, L_0, L_1 |== R implies dom(L_1)
= flow
(dom(L_0),
R)
If
possible, keep "flow(dom(L_0),
R)" on the same line. Breaking after "=" is fine.
last two bullets of H.3.6.1. The keywords "or"
and "and" should be in courier bold rather than roman bold.
• w j @(c)$stable(e) iff there
exists 0 < i < j such that w i, j
, {}, {} (c ##1 c [*->1]) and
e[w i] = e[w j].
• w j @(c)$rose(e) iff b[w j] = 1 and (if there
exists 0 < i < j such that w i, j
,{}, {} (c ##1 c [*->1]) then b[w i] 1), where b is the least-significant bit of e.
• w j @(c)$fell(e) iff b[w j] = 0 and (if there
exists 0 < i < j such that w i, j
,{}, {} (c ##1 c [*->1]) then b[w i] 0), where b is the least-significant bit of e.
• Let n > 1. If there exist
0 < i < j such that w i, j
, {}, {} (c ##1 c [*->n – 1]), then @(c)$past(e, n)[w j] = e[w i]. Otherwise, @(c)$past(e, n)[w j] has the value x.
Defined Named property p is
said to depend on defined named property q if there exist n >
0 and defined named
properties p0,...,pn such that p0
= p, pn = q, and for all 0 < i
< n, the definition declaration of property pi instantiates
property pi+1. In particular, by taking q = p and n
= 0, it follows that property p depends on property p.
A defined named
property p has an associated dependency digraph. The nodes of the
digraph are all the defined named properties on which p depends. If q and
r are nodes of the digraph, then there is an arc from q to r for
each instance of r in the definition declaration of q. Such an arc is labelled by the minimum number of timesteps
that are guaranteed from the beginning of the definition
declaration of q until the
particular instance r. For example, if q is defined declared
by:
A defined named
property p is called recursive if its
node appears on a cycle in the dependency digraph of p.
Let p(X) be
an instance of a recursive defined named property p, where X denotes the
actual arguments of the instance. For k > 0, the k-fold
approximation to p(X), denoted p[k](X), is an instance of a non-recursive property p[k]
defined inductively as follows.
—
The definition declaration
of p[0] is obtained from the definition declaration
of p by replacing the body property_expr
with the literal 1’b1.
—
For k >
0, the definition declaration of p[k] is obtained from the definition declaration
of p by replacing each instance of a recursive property by its (k –
1)-fold approximation.