Subject: Re: [vhdl-200x] Call for Advisory Vote: Simple Subset of PSL
From: Alex Zamfirescu (hxml@pacbell.net)
Date: Thu Sep 11 2003 - 02:24:49 PDT
Erich:
Sorry if I might confused anybody with my negativity.
What I wanted to say is best represented by an example.
Let's say we have two signals a and b, going up and down
with the same period. Signal b is half period after a.
How can I make sure that the change in b is caused by
a change in a?
I can say that if a fails to work b will fail also but that
can be interpreted as a and b sharing same power line
(also it asserts a condition that does not occur since
a and b are assumed OK and periodic).
So how can I specify that a "causes" b to change.
This is not verifiable by simulation, but might be
a critical requirement to be proved in safety systems.
Again, please do not interpret my "mumbling" as anything
negative about PSL. I always wanted to congratulate you and
your team for delivering PSL.
Best regards,
Alex Z
----- Original Message -----
From: "Erich Marschner" <erichm@cadence.com>
To: "Alex Zamfirescu" <hxml@pacbell.net>; "Bailey, Stephen"
<SBailey@model.com>; <vhdl-200x@eda.org>
Sent: Wednesday, September 10, 2003 10:47 PM
Subject: RE: [vhdl-200x] Call for Advisory Vote: Simple Subset of PSL
> 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 : Thu Sep 11 2003 - 02:29:01 PDT