Subject: Accellera FV April 5th Meeting Minutes
From: Harry Foster (foster@rsn.hp.com)
Date: Wed May 02 2001 - 11:03:03 PDT
I just realized that I neglected to send out
the minutes for our previous meeting...
Attached are the minutes for our April 5th meeting.
Attendees:
=========
Meeting attendance shown in parens: (most recent leftmost).
Key: 'a'=attended in person;
'r'=represented by replacement;
'-'=skipped;
'.'=not yet participating;
'?'=unknown;
'*' indicates voting member
(by "3 of last 4 meetings attended" rule,
see October 2000 minutes for details);
***********************************************
NOTE: Please send me e-mail if you were left
off this list--so I can update it. -Harry
***********************************************
(a......) Bernard Deadman (SDV)
(a-aaaaa) Carl Pixley (Motorola) *
(raraaa-) Cindy Eisner (IBM) *
(a-aaaaa) Claudionor Coelho (Verplex) *
(aaaaaaa) Danny Geist (IBM) *
(a-aaaaa) Ed Clarke (CMU) *
(a-aaaaa) Erich Marschner (Cadence) *
(aaaaaaa) Harry Foster (HP) *
(aaaaaaa) Hillel Miller (Motorola) *
(a----rr) K.C.Chen (Verplex)
(aa.....) Limor Fix (Intel)
(aaaaaa-) Matthew Morley (Verisity) *
(-aaa...) Michael Siegel - Siemens CT *
(--aaaa-) Mike McNamara (Verisity) *
(aaa---a) Peter Flake (Co-Design) *
(-aaa...) Prakash Narain - RealIntent *
(aaraaa-) Shoham Ben David (IBM) *
(aaraaaa) Tom Anderson (0-in) *
(---aaaa) Tom Fitzpatrick (Cadence) *
(a---a-a) Vassilios Gerousis (Infineon)
(aaaaaar) Yaron Kashai (Verisity) *
(aaaaaa-) Yaron Wolfstal (IBM) *
Agenda
======
April Meeting Agenda Includes:
(1) Vote on motion to permit Intel to contribute FTL.
(2) Begin discussion on our potential DAC and CAV
face-to-face meeting.
(3) Yaron presented an overview of the Temporal 'e'
language.
Summary
=======
Carl Pixley mentioned that the donation letter between
Motorola and Accellera had been signed by Motorola
and was sent back to Accellera for signing. (NOTE:
the letter has now been signed by both parties).
Agenda:
(1) Vote on the motion to permit Intel to contribute FTL.
The committee voted to temporary open-up the language
contribution process to Intel to donate FTL (Yes: 12, No: 2),
with the constraint that all legal matters between
Intel and Accellera must be resolved by June 22.
(2) DAC and CAV face-to-face meeting
The committee discuss the possibility of meeting
at DAC and CAV.
For DAC, a majority of committee members did not
favor meeting between Monday June 18 and Thursday
June 21, since many of the members would be busy
working at the various EDA vendor booths. Friday
June 22 was suggested as a possibility--provided
we could secure a meeting space. Harry agreed
to look into these details.
For CAV, the committee explored two options. The
first option was to meet on the Monday after CAV,
(i.e., July 23). The second option was to meet on
Tuesday prior to CAV (i.e., July 17). Overall the
group favored the second option (Tuesday July 17),
provided we could secure meeting space. Harry
volunteered to work out the meeting space details.
(3) Yaron Kashai's Presentation:
NOTE: I've captured the main content of Yaron's
slides in the minutes for a permanent record.
If the presenters wish, I can link their
presentations off our web-page for future
referencing.
Slide 2:
Context of temporal expressions
Event
A monitor which becomes part of the model
Example: event rst is rise( top. rst)@ clk;
Expect
An assertion about the model
Needs to be true at all times (AG)
Assume
An assertion about the environment
Used to check input validity, assume- guarantee
reasoning, fairness constraints
Slide 3:
Scope of temporal constructs
Modular scope
In e temporal constructs are properties of
an object
In HDL they could be local to a module
All constructs in a scope are conjunctive
Expression scope
E supports two independent scopes:
Model scope - exp
E scope - exp
Slide 4:
Transition predicates
Change / fall / rise
Convert value transitions into temporal expressions
event clk is rise( some_ model_ variable);
// clk is used as a sampling event below
fall( exp)@ clk;
change( bus_ value)@ clk;
Slide 5:
Boolean predicates, events
True()
Converts state formulae into events
event P is true( bool_ cond);
The boolean expression is evaluated at the
samplin g event
Event occurrence
Succeeds upon success of the event
formula
Syntax: @P
Slide 6:
Sampling
Every temporal expression has a
samplin g event
Sampling latches success
event nrst is rise( nrst)@ any;
event sync_ nrst is @nrst@ clk;
Nested sampling is allowed (and used)
true( addr== my_ addr)@ trans_ start
@my_ clk;
Slide 7:
Sequencing
Chop
Sequences two temporal expressions
{TE1; TE2}
Yield
Implication combined with a cycle delay
TE1 => TE2
same as : ( fail( TE1) or {TE1; TE2} )
Slide 8:
Logical operators
Or
Succeeds if either expression succeed
And
Succeeds if both expressions succeed
to gether (I. e. there is a sequence that
satisfies both concurrently)
Fail
Succeed at the point where the TE would
fail
Slide 9:
Repeats
Simple repeat: [n] * TE
Same as sequencing the TE n times
[n] is shorthand for n cycles
Variable repeats
[n.. m]
[n..]
[.. m]
[..]
Slide 10:
First match repeat (until)
Variable repeat followed by a TE
[..] * TE1 ; TE2
Satisfying sequences will have n
repetitions of TE1 followed by TE2
Slide 11:
Infinite behavior
The last TE in a formula may match
ome ga words:
Infinite extensions of star words
{TE;~[..]}
Cyclic extension with acceptance
{TE; fail([..]* good_ TE; bad_ TE)}
Slide 12:
Some examples PCI (1)
-------- Spec: 3.5.4.1 (pg. 81)
A master is required to assert its IRDY# within 8 clocks from
any given data phase (initial and subsequent).
expect pci_ spec_ 8 is
@frame_ fall => { [.. 7]; @irdy_ assr } @qclk
Slide 13:
Some examples PCI (2)
-------- Spec: 3.3.3.1 (pg. 50)
The earliest a master can terminate a transaction with
Master- Abort is five clocks after FRAME# was first sampled
asserted.
expect pci_ spec_ 11 is
@frame_ fall => ({
[.. 15];@ data_ phase_ complete}
// normal data phase
} or {
[4..] * (fail @devsel_ fall);@ frame_ rise
// master abort
})@ qclk;
Slide 14:
Some examples PCI (3)
This event occures when a target aborts a
transaction
event target_ abort is {
@frame_ fall; // not a master abort
{[..] * fail @frame_ chng; @devsel_ fall};
{[..] * fail @devsel_ chng;
(@ devsel_ chng and @stop_ fall)}
}@ qclk;
Slide 15:
Another example - Microwave
(From: Model Checking, Clarke, Grumberg, Peled, Pp 39)
AG( start) -> AF( heat)
expect @start => {[..];@ heat};
AG( start)-> AF( heat) if operated correctly:
start & close & ~error hold infinitely often
expect @start => {[..]; @heat};
assume @open => {[..]; @close};
assume true( error) => {[..]; @reset};
assume true(~ start) => {[..]; @start};
This archive was generated by hypermail 2b28 : Wed May 02 2001 - 11:04:53 PDT