Subject: [sv-ac] Re: Accellera FVTC March 19 Meeting
From: John Havlicek (john.havlicek@motorola.com)
Date: Fri Mar 07 2003 - 07:03:00 PST
Hi Anthony:
Just a few comments interspersed below.
Best regards,
John Havlicek
> 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.
In a recent vote, both proposals to address the unary/binary
delay issue were defeated, so unary/binary delays in SVA
are as represented in revision 0.80.
Proposals to move sequence implication to the property
level and to eliminate nested sequence implication passed.
>
> 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 believe that the OVA/ForSpec 2.0 Technical Language Specification
defines the languages of regular expressions, including those built
with first_match, as sets of finite sequences of boolean expressions.
The definition for first_match is somewhat complicated, but I have no
evidence that it is wrong. So my opinion is that what you are asking
for has already been done for first_match.
Roy Armoni of Intel should be able to field technical questions about
the OVA/ForSpec 2.0 definition.
>
> I suggest:
> - first, that the proposal to move sequence implication to
> a top-level construct is confirmed;
This has been done in SV-AC.
> - 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.
See comments above on first_match.
>
> 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 McIsaac
>
>
> STMicroelectronics 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 - 07:05:51 PST