Subject: More Info for the Assertions Meeting 9-11 July
From: Stephen Bailey (SBailey@model.com)
Date: Thu Jul 03 2003 - 09:17:27 PDT
Location: Mentor Graphics, Wilsonville, OR.
http://www.mentor.com/corp_info/headquarters.html
Building: D, Conference room Madras (D1348) Building D is the building
with the flag poles in front of it. It also has a full-time receptionist
which you will need to check in with. I will probably be hanging out in the
reception area in the mornings. Please be sure to have my mobile phone
number ready in case you can't find the building or encounter other
problems: 303-775-1655.
We should plan on arriving at 9am every morning.
However, Rob Anderson is driving down from Seattle on Wed morning and has
requested that we not start Erich's PSL overview and thoughts on integrating
PSL with VHDL's existing assertion facility until after he arrives. The
agenda below takes this request into consideration.
We will have morning and afternoon snacks/drinks.
Lunch will be brought in on Wed. I thought we all could use a change of
scenary by noon on Thursday and am planning on going out to a local
restaraunt for lunch on Thursday.
I'm planning on hosting (at a restaraunt -- I don't live in
Portland/Wilsonville) everyone for dinner Wednesday or Thursday, assuming
all are available. We can discuss this Wed morning. (I will be looking for
recommendations from Dennis Brophy on where to go for dinner. He's the
expert on matters culinary ;-)
THE AGENDA
Wednesday:
9am: Arrive, coffee, etc.
9:15 - 10am: Introductions/Discuss the agenda for the meeting
10am - noon (or however long Erich needs): PSL overview/thoughts on
integrating with VHDL
Lunch break
Afternoon: Identify all aspects of VHDL that will be impacted by ABV
Examples: Reading OUT mode ports; API for functional coverage data; PSL
extensions to VHDL (assuming std_logic value '1' is TRUE and std_logic value
'0' is FALSE); need for additional support packages to allow testbench
writers to query about functional coverage -- adaptive/reactive testbenches,
use of assume/restrict directives in generating stimulus, disable/enable
directives/properties, etc.
We are fortunate to have Richard Wallace joining us. Richard has an
extensive formal background and I will be looking for him and Erich to
provide us with guidance in how we can do things to facilitate formal
verification techniques.
This work may continue on into Thursday morning.
THURSDAY:
Outline the technical proposal.
Setup technical proposal according to LRM sections impacted.
Identify need for new LRM sections.
Identify key corner cases (if any) as well as general approach for each
section.
Efficiency of implementation considerations (tool performance as well as
level of effort to implement).
FRIDAY:
Assignments and action items to complete technical proposal.
A brief bibliography of references:
Sugar (PSL predecessor): www.haifa.il.ibm.com/projects/verification/sugar
SystemVerilog 3.1 LRM: www.eda.org/sv-ec/SystemVerilog_3.1_final.pdf
(www.systemverilog.org has other links) and www.eda.org/sv-ac is web site of
SystemVerilog Assertions Committee
Accellera Formal Property Language Technical Committee: www.eda.org/vfv
(Requirements link is interesting); more importantly, you can access the
1.01 PSL LRM from www.eda.org/vfv/docs
Ben Cohen has a book on PSL: www.vhdlcohen.com The examples from his book
can be downloaded at http://members.aol.com/pslcohen/psl_cohen.tar. He also
has PSL quick reference cards for VHDL and Verilog flavors available in PDF
format at: http://members.aol.com/vhdlcohen/vhdl/Models.html.
For the really curious, all the formal languages can trace their history
back at least to Z Notation. (Spivey, J.M., "The Z Notation: A Reference
Manual," Hemel Hempstead, Prentice Hall. Diller, Antoni, "Z: An
Introduction to Formal Methods," John Wiley & Sons.)
And Richard Wallace provides this information: The language Larch shares
similarities with PSL. Information on Larch can be found at:
www.sds.lcs.mit.edu/spd/larch. He also points out a web page that is "one
of the best, if not the best, pages of links on formal methods"
www.afm.sbu.ac.uk.
And, of course, there is Harry Foster's book on "Assertion-Based Design"
available from Kluwer.
---- Stephen A. Bailey TME, Model Technology 1811 Pike Road, Building #2, Suite F Longmont, CO 80501 sbailey@model.com 303-775-1655 (mobile) 720-494-1202 (office) 720-494-0457 (fax) www.model.com
This archive was generated by hypermail 2b28 : Thu Jul 03 2003 - 09:18:33 PDT