Subject: Re: [vhdl-200x] Call for Advisory Vote: Simple Subset of PSL
From: Gabe Moretti (gmoretti@comcast.net)
Date: Thu Sep 11 2003 - 07:00:21 PDT
Erich,
I think a better wording of your response to Alex with respect to causality
would have been:
instead of "it is always the case that, if a rises, then b will also rise",
rather than "a rising causes b to rise".
To say: "it is always the case that, if a rises, then b will also rise",
rather than "a rising is the only cause for b to rise".
The second predicate can be tested is other ways beside using assertions.
We must not forget that asking one method to do everything generally means
overcomplicating the problem. Quality, and thus design verification is
achieved by aggregating a number of means, not by building the ultimate
verifier.
Gabe Moretti
----- Original Message -----
From: "Erich Marschner" <erichm@cadence.com>
To: "Alex Zamfirescu" <hxml@pacbell.net>; "Bailey, Stephen"
<SBailey@model.com>; <vhdl-200x@eda.org>
Sent: Thursday, September 11, 2003 9:17 AM
Subject: RE: [vhdl-200x] Call for Advisory Vote: Simple Subset of PSL
> 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 - 07:04:44 PDT