Subject: additional comments on pages 40-66.
From: Anthony McIsaac (anthony.mcisaac@st.com)
Date: Fri Oct 11 2002 - 11:49:24 PDT
Further comments on just one section, 6.2.3 on page 63.
I agree with John that the description of replicated properties when the parameter is
an array isn't easy to follow, and can usefully be expanded as he suggests.
The example in the informal semantics could also perhaps be more helpful, as the
0 and 1 on the second line aren't related to the 0 and 1 on the first line. As a
minimum, they could be changed on the second line to "true" and "false" as in the
first example.
This example is also a special case in that 2+2 = 2x2 = 2^2.
Perhaps a longer example would help:
A forall i[0:2] in {4,5} : f(i) property is replicated to define eight instances
of the property f(i):
f({4,4,4}), f({4,4,5}), f({4,5,4}), f({4,5,5}), f({5,4,4}), f({5,4,5}), f({5,5,4}), f({5,5,5}).
(which suggests that the number of times the property is replicated isn't quite
as described on p63 line 44)
Perhaps a specific example can be included in the "Examples" section here, e.g.
forall i[0:3] in boolean:
request && (data_in == i) -> next(data_out == i)
This section also set me wondering about variables in ranges.
I guess that the syntax allows any HDL expression of type Number to appear
as the bound of a range.
So we will have forall i in [1:10] : forall j in [0:i] : .......
No problem there, but perhaps it could be mentioned in this section that all
the foralls must appear at the top level of the property.
It appears that the "forall" parameter can also appear in a range in the property:
forall N in [1:1000] :
always (request && (wait_time == N)) -> next_a[1:N](!response)
There's something like this in Property 49 of the old sample properties.
This is OK as long as everyone's happy to implement it.
But it seems to me that the following is also legal Sugar:
always (request -> next_a[1 : wait_time](!response)
and I don't think this is intended.
Perhaps the formal syntax and semantics can be more precise about what's
allowed here.
Anthony
This archive was generated by hypermail 2b28 : Fri Oct 11 2002 - 12:02:12 PDT