Subject: RE: [vhdl-200x] Call for Advisory Vote: Simple Subset of PSL
From: Erich Marschner (erichm@cadence.com)
Date: Thu Sep 11 2003 - 06:17:48 PDT
Alex,
As always, I appreciate your comments - both issues and compliments!
I think part of the problem here is that the notion of causality itself is philosophically challenging. Scientific analysis to confirm causal relationships - or at least, to demonstrate the probability of a causal relationship - can be quite complex. Without looking at the implementation and tracing the low-level flow of events, it is difficult to state unequivocally that there is a higher level causal relationship. And even then, there may be multiple causes or exceptions that cloud the issue.
Practically speaking, I think we need to be concerned with predictability rather than causality - i.e., "it is always the case that, if a rises, then b will also rise", rather than "a rising causes b to rise". Whether one causes the other or they both result from a common cause, the observer (either human or downstream hardware) sees the same effect, and that's all that matters.
But it is certainly a thought-provoking question.
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 5:25 AM
| To: Erich Marschner; Bailey, Stephen; vhdl-200x@eda.org
| Subject: Re: [vhdl-200x] Call for Advisory Vote: Simple Subset of PSL
|
|
| 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 - 06:21:17 PDT