Subject: Re: Expressiveness of temporal e (was: Do we have the right rules?)
From: Atanas Parashkevov (Atanas.Parashkevov@motorola.com)
Date: Tue Aug 14 2001 - 00:45:00 PDT
Sandeep K. Shukla wrote:
> I think the best hope for formal methods to work in real design
> space is to make the designers work closely while doing the design
> with verification engineers, such that verification engineers can
> help them to formulate properties concisely, while they themselves
> learning the design well enough to later help the verification
> process via abstraction etc.
Bingo, you have just described (in a nutshell) how CBV is used in
the field.
Best regards,
Atanas
> >>-----Original Message-----
> >>From: owner-vfv@eda.org [mailto:owner-vfv@eda.org]On Behalf Of Danny
> >>Geist
> >>Sent: Monday, August 13, 2001 11:56 PM
> >>To: Harry D Foster
> >>Cc: vfv@eda.org
> >>Subject: Re: Expressiveness of temporal e (was: Do we have the right
> >>rules?)
> >>
> >>
> >>My experience is that its hard to get designers to do verification work
> >>(that includes simulation).
> >>However they find it easy to talk in sequences.
> >>Regards,
> >>Danny
> >>
> >>Daniel Geist
> >>IBM Haifa Research Lab. Phone:
> >>972-4-8296286
> >>MATAM - Advanced Technology Center Fax: 972-4-8296112
> >>Haifa, ISRAEL
> >>e-mail: geist@il.ibm.com
> >>
> >>
> >>"Harry D Foster" <foster@rsn.hp.com>@eda.org on 08/14/2001 06:24:39
> >>
> >>Please respond to "Harry D Foster" <foster@rsn.hp.com>
> >>
> >>Sent by: owner-vfv@eda.org
> >>
> >>
> >>To: "Yaron Kashai" <yaron@verisity.com>, "Bernard Deadman"
> >> <bdeadman@sdvinc.com>
> >>cc: <vfv@eda.org>
> >>Subject: Re: Expressiveness of temporal e (was: Do we have the right
> >> rules?)
> >>
> >>
> >>
> >>> Of course, each language has it's style, as demonstrated by the
> >>> example properties, and one may find a language to be easier to
> >>> write in regardless of the theoretical capabilities. To some
> >>> extent it is a matter of taste, as I think Carl was trying to
> >>> point out.
> >>>
> >>I've asked a group of engineers in my lab (a mixture of verification and
> >>design engineers -- these are real engineers not researchers or CAD dudes)
> >>to review the property examples document that our committee generated. I
> >>gave them access to the documentation for the various donated
> >>languages and
> >>answered many questions. The verification engineers tend to favor
> >>Temporal-e or ForSpec in our lab -- while the design engineers didn't like
> >>any of the languages. Keep in mind that many of the verification
> >>engineers
> >>were already biased due to their previous exposure to Specman. The design
> >>engineers also were biased having worked with our lower-level RTL
> >>assertion
> >>methodology. I'm sure if you asked the verification and design engineers
> >>from Motorola what they liked they would say CBV. Same idea for IBM, etc.
> >>It's hard finding an unbiased group.
> >>
> >>One thing I got out of this exercise is that the goals of the various
> >>stakeholders are different (i.e., the specification needs of the
> >>verification engineer were different than the design engineer's concerns).
> >>And their view of the design is different (verification engineers are
> >>thinking more abstractly while the design engineer's heads are deep into
> >>the
> >>implementation).
> >>
> >>-Harry
> >>
> >>
> >>
> >>
> >>
-- =================================================================== -- Atanas Parashkevov -- Product Architect, Formal Verification -- EDA Solutions and Products SBU -- Global Software Group -- -- email: Atanas.Parashkevov@motorola.com -- office: +61-8-8168 3687 fax: +61-8-8168 3501 -- switch: +61-8-8168-3500 -- addr: 2, Second Avenue, Mawson Lakes, Adelaide, 5095. Australia ===================================================================
This archive was generated by hypermail 2b28 : Tue Aug 14 2001 - 00:45:33 PDT