Subject: Re: Accellera FVTC March 19 Meeting
From: Anthony McIsaac (anthony.mcisaac@st.com)
Date: Fri Mar 07 2003 - 06:33:24 PST
Harry and all,
Following your notice of this meeting, and your earlier request
for comments about issues of alignment between PSL and SVA,
I've got a couple of points to make. I have a comment
below concerning sequential expressions, and will
send more comments in separate messages. Can Faisal
kindly forward this message to sv-ac?
First, two issues that appeared problematical to me in
SVA 0.8 were unary/binary delays and nested sequence
implication. From the mail reflector, it appears that
these issues are being addressed, and I won't raise
them directly myself.
I have an issue concerning the nature of sequential expressions.
The proposal says (11.4):
A sequence is a list of ... boolean expressions ....
A sequential expression describes one or more sequences ....
This suggests that there is a mapping "expand" from sequential expressions
to lists of boolean expressions, e.g.
a * [1:2] -> {a}, {a,a}
This is consistent with the common understanding of regular expressions
(a shorthand for sets of syntactic objects).
It suggests that semantics of sequential expressions on traces
(lists of design states) could be defined by first applying this
mapping, and then saying that a sequential expression e matches
a trace t = (state1, state2 ... staten) if at least one of the lists
of boolean expressions {b1, b2, ) in expand(e) is satisfied state
by state in t: i.e. b1 is true in state1, b2 is true in state2 ,....
In fact, the semantics of sequential expressions is defined directly
on traces, and is not consistent with the account above.
PSL also defines the semantics directly on traces; however, in PSL it
is clear how the semantics could be factored through a mapping from
sequential expressions to lists of boolean expressions, whereas
there are SVA constructs for which this is not clear - in
particular, first_match and sequential implication.
If sequential implication is modified so that it yields a property
rather than another sequential expression, this issue is
removed. It remains for first_match:
We should be able to define the meaning of first_match e in terms
of the meaning of e.
This is easy if the meaning is defined as a set of traces:
a trace t satisfies first_match e if t satisfies e and no proper
prefix of t satisfies e.
It is hard if the meaning is defined as a set of lists of
boolean expressions:
The meaning of *[1:2] a is {true,a}, {true,true,a} - but how do we
derive the meaning of first_match (*[1:2] a) from this?
(N.B. It's not hard to define first_match (*[1:2] a) as a set
of lists of boolean expressions : {true,a}, {true, !a, a}; the problem
is how this is derived in a systematic way from the definition of
(*[1,2] a))
So it is not easy to see how the sequential expression first_match e
describes a list of boolean expressions. This construct goes
against the account of sequential expressions in 11.4, and against
the intuitive concept of regular expression. I believe that this
point is important, because it makes it much harder for people
to understand what a sequential expression is.
I suggest:
- first, that the proposal to move sequence implication to
a top-level construct is confirmed;
- second that SV-AC considers whether first_match is really
necessary - or perhaps whether it's only really required for
matches of booleans, and some other simpler cnstruct would
be adequate for this.
Anthony
harry@verplex.com wrote:
>
> Next Meeting:
> ============
> Date: Wednesday March 19, 2003
> Time: 9:00am PDT (Pacific Time).
> Domestic Dial-In #: 866-262-1846
> Intl Dial-In #: 205-354-0107
> Room #: *9724233186*
>
> Agenda:
> ======
> (1) Discuss PSL 1.1 LRM roadmap
>
> FVTC PSL 1.1 LRM plan approved by Accellera Board:
>
> Goal: Alignment with System Verilog Assertions
> Focused on overlap between PSL and SVA domains
> #0 goal - To maintain a sound formal semantic foundation
> #1 goal - To avoid different semantics for same syntax
> #2 goal - To allow same syntax for same semantics
>
> Plan:
> Coordinate with SV-AC to resolve SVA LRM issues
> Support SVA formal semantics committee
> Work with SV-AC to define area of overlap
> Develop proposed changes to align PSL and SVA
> Release PSL v1.1 within 1-2 months after SVA LRM stabilizes
> By DAC 2003 if possible
>
> -Harry
-- 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 Mar 07 2003 - 06:42:18 PST