Subject: comments on pages 63-78: replicated properties
From: Anthony McIsaac (anthony.mcisaac@st.com)
Date: Fri Oct 18 2002 - 08:33:28 PDT
I'm putting my comments on replicated properties, verification unit
types, and the modelling language, in three separate messages.
p 63, line 36, section on replicated properties:
Following the points in my comments last week:
(i) I suggest (possibly under Restrictions) a note along the lines:
Replication of a property can only occur at the top level of
the property. Nested replications are allowed, but they must all be
at the top level.
For example:
forall i in boolean:
forall j in {0..7}
forall k in {0..j}
f(i,j,k)
Question: do we want an example of illegal usage ?
always (request -> forall i in boolean: next_e[1.10](response[i]))
(ii) If it is the case that the Numbers in ranges for
properties like next_e must be expressions such that the only
variables in them are parameters of some "forall" governing the
property, then this should be stated, either once and for all
at some point, or as a restriction in the section for each
property of this type.
(iii) It may be helpful to indicate how "forall" differs from
macro preprocessing. As I understand it, forall could be implemented
through simple textual replication before compilation; but it also
allows other implementations. For example:
- in formal verification, giving the parameter the status of a signal
whose value is arbitrary but constant. This is why I wondered about
allowing things like
always (request && (wait_time == N)) -> next_a[1:N](!response))
which can't obviously be implemented like that.
But perhaps compilers can easily distinguish between cases when
the replication can be imnplemented through an extra variable, and
when it has to be done explicitly. I'm not a tool expert, and wouldn't
know.
- in simulation, by implementing checkers that are triggered on
certain conditions, and assign a specific value to the replication
parameter at that point; these checkers then stay alive and monitor
for the satisfaction of some other condition involving this value,
after which they terminate. As I mentioned in an earlier message,
I believe that some restriction could be specified for properties
in the "simple" subset that is supposed to be easy to verify in
simulation:
OK to implement:
forall x in {0:4095}
always ((accept & data_in = x) -> next (transmit and data_out = 11x + 9))
requires algorithm for finding values of x satisfying equations:
forall x in {0:4095}
always((u = 7x + 3 and v = 5x + 2) -> ........
-- Anthony McIsaacSTMicroelectronics Limited 1000 Aztec West Almondsbury Bristol BS32 4SQ
Tel: ++44 (0)1454 462466 Fax: ++44 (0)1454 617910
Email: Anthony.McIsaac@st.com
This archive was generated by hypermail 2b28 : Fri Oct 18 2002 - 08:38:17 PDT