Subject: RE: [vhdl-200x] Call for Advisory Vote: Simple Subset of PSL
From: Erich Marschner (erichm@cadence.com)
Date: Wed Sep 10 2003 - 22:47:27 PDT
Alex,
Can you elaborate on your statement about it being hard to define events for which you don't care about the order?
I can write in PSL the following sequence:
{{a[=1]} && {b[=1]}}
which holds only on a path on which both a and b occur once, and there is no relative order specified for a and b. Is this what you have in mind? If so, do you view the above syntax as overly difficult? Why?
Regards,
Erich
-------------------------------------------
Erich Marschner, Cadence Design Systems
Senior Architect, Advanced Verification
Phone: +1 410 750 6995 Email: erichm@cadence.com
Vmail: +1 410 872 4369 Email: erichm@comcast.net
| -----Original Message-----
| From: Alex Zamfirescu [mailto:hxml@pacbell.net]
| Sent: Thursday, September 11, 2003 1:28 AM
| To: Bailey, Stephen; vhdl-200x@eda.org
| Subject: Re: [vhdl-200x] Call for Advisory Vote: Simple Subset of PSL
|
|
| Steve and all there VHDL lovers:
|
| PSL is indeed a solid framework.
| Unfortunately, the wide applicability forced
| its designers to "totalize" timepoints relations
| in the core. That makes hard to specify events
| for which you do not care about their order.
| This is what Dr. Wills probably meant by
| its (PSL) closeness to simulation.
| In modern design there is a need to specify
| relations like causality and concurrency. PSL
| core choices make that difficult.
| Second, even for VHDL simulation the relation
| "between" is more general including delta. I have
| defined it for pairs (time, delta) during the proofs
| about postponed processes done for VHDL 93 validation.
| Getting inspiration from PSL is a good idea, but
| VHDL and its associated assertions deserve closer
| attention when it comes to re-using the PSL core.
| Therefore, if I had to (and could) vote I would vote no, with
| the comment, "let's do it right for VHDL design and let
| PSL address the process manufacturing, etc."
|
| Best regards,
|
| Alex Zamfirescu
| CTO ASC
| IEC USNC TA
| hxml@pacbell.net
| Cell: 415 412 6903
| ----- Original Message -----
| From: "Bailey, Stephen" <SBailey@model.com>
| To: <vhdl-200x@eda.org>
| Sent: Wednesday, September 10, 2003 12:48 PM
| Subject: [vhdl-200x] Call for Advisory Vote: Simple Subset of PSL
|
|
| > The assertions team has decided to pursue the
| incorporation and integration
| of the simple subset of PSL as the best way to enhance the
| assert statement
| into a broader assertion-based verification capability. The
| simple subset
| limits the properties that can be expressed to only those in
| which time moves
| monotonically forward (which is the only way simulators know
| how to deal with
| time).
| >
| > Because we do not yet have a detailed proposal on the
| specifics of the PSL
| incorporation and integration, this Call for Vote is NOT a
| final CfV. Instead,
| it is best viewed as an advisory vote; the purpose of which
| is to provide some
| assurance to the assertions team that they won't be wasting
| their time in
| pursuing PSL as the basis for the detailed proposal. (By
| assurance, I mean
| that we won't later find out that a majority or very
| significant minority would
| never vote to approve the detailed proposal due solely to
| the fact that the
| proposal is based on PSL.)
| >
| > Also, from a practical perspective, I am in the process of
| submitting 3
| different papers for possible publication and presentation
| at conferences and
| EE Times. These papers will all reference the fact that PSL
| has been chosen as
| the basis for VHDL's ABV capabilities. While I don't
| anticipate a negative
| response to this advisory vote, I would rather have the vote
| than be made a
| fool (and waste alot of people's time over the next several months)!
| >
| > As the papers are in process of review and this is an
| advisory vote, I
| require a quick turnaround on this vote:
| >
| > Friday, 12 Sep 03, 0900 EDT.
| >
| > The question to be voted on:
| >
| > Should the assertions team continue constructing a
| detailed language
| change proposal based on incorporating and integrating PSL into VHDL?
| >
| > Yes replies require no comments. However, I request any
| no responses to
| provide rationale for the no comment. Replies can be sent to me
| (mailto:sbailey@model.com) or to the email reflector
| (mailto:vhdl-200x@eda.org).
| >
| > DASC WG voting rules apply. You must be a DASC member.
| To confirm your
| membership in DASC, see
http://www.dasc.org/DASC-roster.html. The DASC home
page has a link to the membership application.
>
> Thank you for your prompt consideration.
>
> ------------
> Stephen Bailey
> TME, Mentor Graphic's Model Technology Group
> sbailey@model.com
> 303-775-1655 (mobile, preferred)
> 720-494-1202 (office)
> www.model.com
>
This archive was generated by hypermail 2b28 : Wed Sep 10 2003 - 22:54:51 PDT