Meeting Minutes For SV-AC F2F, 2008-05- 14-15
Day 1
Present:
Gordon Vreugdenhil, Mentor Graphics
Dmitry Korchemny, Intel
Manisha Kulshrestha, Mentor Graphics
Erik Seligman, Intel
Neil Korpusik, Sun Microsystems
Jin Yang, Intel
Abigail Morehouse,
Dave Rich, Mentor Graphics
Mark Hartoog, Synopsys
Tom Thatcher, Sun Microsystems
Michael Burns, Freescale
On Phone:
John Havlicek, Freescale
Lisa Piper, Cadence
Fransoise, Martinolle, Cadence
Don Mills,
Mirek forczek, Aldec
Ed Cerny, Synopsys
Steven Sharp, Cadence
Stuart Sutherland, Sutherland HDL
NOTE: This is a non-voting meeting, and attendance at this meeting is not
counted towards attaining or maintaining voting rights.
1. Gord's presentation on assertions in procedural code
Proposal is that an assertion in a procedural context will be enabled to
start a new attempt on the next clock event when the procedural flow passes
the point of instantiation of that assertion.
- If code passes the instantiation point multiple times, (i.e. in a
loop)
multiple attempts will be scheduled to begin on the next assertion
clocking event.
- If procedure is re-entered, all scheduled attempts will be flushd
(This prevents glitch-like behavior on the assertions)
- Need a new syntax to specify which signals will not use sampled values.
(For example, when passing loop variables as arguments to assertion)
e.g. "const i"
The constant variables would pass current value at time of scheduling,
This value would remain unchanged through the entire assertion attempt.
- Could have some smart defaults: automatic variables always const, etc.
John: Likes the proposal
Mark: Likes the proposal. It's not backward compatible, but only in
ill-defined cases.
What syntax form should be used for unsampled?
Suggestions:
1. Assertion syntax form: assert property const(i)
2. Simple const cast on actual argument passed to property
3. Dmitry: New $unsampled() system function
Mark: Could we use outside procedure?
Tom: This would fix Steve's example.
Dmitry: Would need to define formal semantics
Dmitry: What about using $unsampled within seq prop
Gord: Don't want to create a situation where you have to know the
instantiation context to code the assertion correctly
Neil What about delays in process which go over clock delays
Gord: Would execute candidates queued to that point..
Abby: Seesm funny that assertion attempts disappear invisibly
Maybe you want to see all the assertion attempts
Gord, Steven: We don't really need that kind of control
Erik: If you want to see every execution attempt, use immediate assertions
Neil: Likes the proposal
Jin: What is the implication for formal verification?
Dmitry: Should not affect formal verif.
Gord: Would allow new forms of expression which formal verificatin tools
could not handle
Dmitry: What about assertions instantiated in combinational procedural
code which is affected by test bench inputs
Tom: Display Example 2:
(Sent to sv-sc reflector on 5/8/2008, with the title
"Examples of Assertion Usage")
The example describes a regular 2-procedure state machine. The
sequential part of the state machine is an always_ff procedure, the
combinational part is doen with an always_comb. The assertion
appears in the always_comb block.
Here's how it works:
- The current state variable would change in NBA region. This triggers
the always_comb procedure.
- The always_comb executes, passes the assertion location, and
schedules an assertion evaluation at the next clocking event.
- Assertion would be executed in Observed because the clocking event
has occurred in this clock cycle.
- The req signal changes in the Reactive region because it is driven by
test bench code
- We return to the Active region. The always_comb block runs again.
Another assertion attempt is sceduled for the next clock edge.
- Back to observed region. Does the scheduled assertion attempt start
now because the clocking event occurred in this timestep?
(NOTE: on later reflection, it seems that the second assertion
attempt does not start here, but must wait for the next clocking
event. After all, just because we loop back to active region,
doesn't mean that always_ff procedures will execute again. The
always_ff procedures have already processed their clock events,
and would not run a second time in the time step. Likewise, the
assertion clock event was processed the first time the simulator
passed through observed region, and thus, the scheduled assertion
attempt must wait for the next clock event)
Erik: Are we ready to write a proposal for this?
Gord: It's going to be complicated. It may touch several areas of the
standard, and several proposals which are not in the draft yet.
Dmitry: Doesn't this change the assertion clock?
Gord: We are not changing the clock: We are simply not attempting
assertions at timesteps where the assertion would otherwise evaluate
to true vacuously.
Gord: Another way to explain this. For assertions in a loop:
Consider N, with range 1--Maxint. The enable for the assertion is i<N.
Dmitry: I'm less confused
Erik: Could we split up and research the impact of this
Gord: Impact may be broad. Should we wait for Draft 6
Neil: Draft 6 scheduled for May 28.
Erik: Don't want to wait that long.
AI: Reveiw Draft 5 and current proposal: Will split up current proposals
as follows:
Abby: 2336 2250 2246 1599
Steve: 2335 2188
Ed: 2175 2171
JOhn 2168 Draft5 Annex F 1667 1668 1549
Manisha 2150 1731 1729
Lisa 2100 2091
Tom: 2090 2069
Mark: 2033 1987
Dave: 1901 1800
Jin: 1769 1758
Neil: 1757 1737
Dmitry: 1932 1683 1682
Gord 1698 1687 1686
Mike: 1681 1641 1601
Erik: 2005 1932
Chapter 16 Review Ch 21/22 has $assert_on, etc.
16.14.5: will be the replaced section.
AI: Erik: will work with Gord to create a rev0 proposal.
2. Gord's presentation "Typing of Assertions Constructs"
The proposal discussed the possible typing problems caused by untyped
arguments and the substitutions semantics of sequences and properties.
- An untyped argument to a sequence or property could take on more than
one type internally.
- Propose that assertions use the self-determined type of the actual
arguments
Gord: Should a property definition be parsable on its own, independent of
any instantiation context?
Gord: Should a property instance be parsable, regardless of internals of
that property?
Steven: This seems kind of like the difference between value & ref args
Gord: This is something new, not like pass by value, not like pass by
reference.
Gord: Self-determined type should solve many of these problems.
With current setup each actual would have an unknown set of types.
John: How is this different from using a type parameter?
Gord: With a type parameter each instance would have a single type for
an actual argument. With sequence & properties, each instance
has an unknown set of types for the untyped argument.
John: Explicit management of actual is a better way to go
What about untyped integer idea? (This came up at previous sv-sc
meeting)
Gord: Self-typed expression may eliminate the need for this.
Dmitry: But local variables defined using substitution semantics
John: But local variables are all typed. There are no untyped local
variables.
John: Dmitry may be thinking of the old way of passing local
variables:
example:
property p(foo,bar);
a ##1 (b, foo=(bar-1));
endproperty
Gord: We are not changing very much.
Mark: This will be a subtle change that people ar not going to understand.
there may be problems with Signed numbers, left-shift, etc.
AI: Mark: will mail some potentially problematic examples to the reflector.
John: Covergroups: coverpoint expressions are self-determined.
Gord: So covergroups in checkers would be incompatible!
Abby: Doesn't like the ida of poly-morphic types
Dmitry: Doesn't clock inference imply a substitution semantic?
Gord: Don't need substitution to explain this:
Dmitry: example
sequence s1 (bit a,b);
a ##1 b;
endsequence
sequence s2(bit a,b)
@clk1 s1(a,b) ##1 @clk2 s1(a,b);
endsequence
Dmitry: s1 instanced twice with 2 different clocks.
Dmitry: Would have trouble with LTL expressions
John: LTL is not dealing with same problems as verilog
Gord: LTL implementation could use substitution, but simply expand
parameters using self-determinted type
Dmitry: Do all sequences, prop have same type eg sequence, property?
Erik: What about this.
property p (mystruct)
mystruct.foo ##1 mystruct.bar;
Gord: Not a big issue. Semantics are that self-determined type of
actual must be a type compatible with member select.
Dmitry: What about
struct b;
let a = top.unit1.subunit.b
assert property (..a.ready ...)
Gord: Defer this till we talk about let.
Erik: Are we ready to start on a proposal for this?
Gord: There is some disagreement. Would prefer to get consensus before
working on proposal.
Straw poll:
Tom: in favor,
Mark: concerned about backward compatibility, Would be great if we had
done this in the first place.
Dave: in favor,
Abby: in favor,
Jin: worth exploring,
Neil: concerned about backward compatibility: We need to quantify impact.
If impact is too great, we may want to reconsider
Manisha: fix,
Erik: leaning negative, concerned about huge change in addition to
assertion change,
Dmitry: Likes proposal, concern about backward compatibility. It is
cleaner than what we have now. Would want to defer this to next
revision of the standard.
Gord: in favor
Mike: Likes fixint broken things. Thinks thins are defined. defer
to john
John: This should be fixed now.
Francsois: In favor
Don:
Stu: In favor
Steven: A godd way to go.
Dmitry. This is a complicated change. It will require more extension.
Neil No more extensions, 5 year rule
Gord: If we don't fix this, would not be in favor of other assertion
enhancements.
Neil: Gord, don't you have concerns about backward compatibility?
Gord: Some concern There will be some occurrence of problems
Most problems are bit-width problems. Only problem is when using
expressions passed as formals
Don't see this too much. People don't tend to pass expressions.
Dave: Could examination of OVL library to determine the exposure.
Erik: Would this show anything? OVL is modules:
AI: Tom will look at existing code. Michael or John to look at some existing
code. Erik or Jin will look at Intel code
AI: Mark to look at or create some examples
AI: All: Review assigned Mantis items with this change in mind.
Gord: Thinks that proposal should be pretty simple. Possibly a one
sentence change which says that the formal argument retains
the self-determined type of the actual.
AI: Gord will write up first proposal.
John: What about annex F? 1549 includes a specific re-write algorithm.
Would this have to change?
Gord: Not sure if changes are necessary. Would have to examine it.
John: LTL is a flat language. May just need to delete paragraph in 1594
talking about substitution.
John: maybe right answer is to scale back annex F.
(NOTE: John sent e-mail later saying that Annex F is talking about
an abstract syntax. It's not dealing at all with parsing or type
determinations at all. So this change probably doesn't apply to
Annex F)
3. Use remaining time to discuss checker variables, and create
a list of issues to discuss the following day.
Gord: Is there any need to at all to reference checker variables
hierarchically
Dmitry: no
Erik: What about a checker within a checker: Code in checker could
reference a signal in the instance checker.
Gord: Not concerned too much about this
Dave Rich: Concerns are:
Wants checkers to be simple encapsulation of otherwise legal
constructs. Doesn't want to create special constructs just for
checkers.
Mark: What about action blocks: Are they part of assertion context?
Could they reference checker variables.
Could they hierarchically access checker variable
functions only called in checker action blocks.
Dave: Are freevars same as checker variables?
Dave: couldn't we just use rand?
Tom: Agree
Gord: would it be reasonable to simply set all freevars to zero
Dmitry: But could use assume property to set legal cases for freevars
Gord: There are some unsolvable cases:
Gord: Could we solve just the boolean constraints. If you run into a
dead-end that's okay
Dmitry: Needs of formal people are different from simulation people. Need
some constructs for formal verification, but these may not be
useful for simulation
Mark: What about random stability for freevars?
Dave: What about always_check, initial_check?
Seems you are using the construct to change an event expression
Dmitry: Checker instantiation semantics
Gord: covergroups inside checkers
Gord: concerned about covergroup type, untyped formals what constitutes
the same covergroup type.
Adjourn the meeting for the day.
Day 2
Present: Mark, Erik, Jin, Neil, Gord, Michael, Tom, Dmitry,
On Phone: Lisa, Steve, John, Don, Manisha
1. Let: Dmitry's presentation on motivation for let
Presentation covered various motiviations for let
1. Template for immediate assertions, like property for concurrent
assertions
2. Shortcut for assertion modeling
3. It doesn't create a wire, which would be synthesized.
Characteristics of let
1. It is a macro
2. It is local in scope
3. Allows for default arguments.
Gord: What you want is a scoped macro. You define something, give
it a name, and use it.
If you want let behave as a macro then let must exist at compile
time
We can't allow hierarchical references to let.
Dave: Would need to assign let to a signal to have it available.
Tom: Why is this more problematic than `define?
Gord: It's not a pure text macro
Because escaping references are bound at point of declaration
Michael: Both let definition and use have to obey grammar.
Dave: What about using alias construct
Gord: Alias is different. alias simply defines two nets to be
equivalent. Two symbols that point to the same variable.
Don: Why is let not synthesizable? It sounds like something any
designer would like to use.
Gord: If we solve the problems we could extend to the whole language.
Michael: Could you call a function with Let?
Gord: Sure. Function definition is resolved at point of let definition,
resolve function call at point of let use.
Mark: Function doesn't have to exist at time of let declaration.
Gord: Potential gotcha: let base = top.unit1.subunit1.base
Macro substitution resolved at declaration.
If user expects resolution at point of use, will be surprised.
Steven: IF You did let mylet = foo, variable foo resolved at point of
definition.
Michael: Could they appear in class, exposing protected members to
outside world?
Gord: Let in a class might be bad idea, but let in a class method may
be ok.
Gord: Let could appear in design unit scopes (module, generate).
Procedural scope: no big issues
Michael: Could they refer to automatics
Gord: No reason why not.
Mark: What about constant expressions?
Gord: All terms of let must also be constant
Mark: How about reference into let in a generate block
Gord: Forbid this just like other hierarchical references
Mark: How about with interface ports
Gord: This would be equivalent to hierarchical references.
Steven: You couldn't export with modports.
Francois: What is difference between let and `define
Gord: These are scoped, binding rules for escaping names.
Frans: Definition and use must be in same scope?
Gord: Declaration, use could be in different scope
e.g. A let defined in a package.
Gord: This would allow you to export something under a different name.
Michael: Why don't we just allow functions with untyped args
Gord: Doesn't like this
Wants to see consistent set of rules for overloaded functions.
No one would be able to understand this.
Mark: People will ask for if and case within let next.
Don: You're saying it's intractable to combine let & functions.
Gord: This would take a lot of time to figure out.
Doesn't think it is tractable.
Dave: Binding rules for let are very different from functions.
would make this very difficult to do.
Mark: Let is bound at compile time, functions are bound at elaboration
time.
Tom: What are specific changes that must be made to the let proposal?
Dave: Move to expressions chapter. Make it applicable to entire design
space.
Gord: Hierarchical reference to lets should be forbidden.
AI: Dmitry: Consult with Dave to find new home for Let. Revise proposal
2. Checker issues
a. Checkers just encapsulation mechanism
Dave: What is reason for checkers? encapsulation? Why not use a module?
Is this simply to be able to put them in procedural code?
Gord: Checkers currently in module namespace. This is an error.
If this is true, we couldn't put them in a package. Module names
are global.
Checkers should not be in module name space.
Result: can't apply configuration to a checker
checkers not first-class participants in name resolution
Gord: Name resolution of checker should follow sequence and property
names.
Gord: Should sequence & property behave like functions?
Gord: Instance vs. declaration: difference between referencing checker
internals, vs checker declaration.
Gord: Would like to forbid hier reference to checker name to instantiate
it. Checker declaration should be in a package
This is more restrictive than rules for sequence & property.
Gord: Checkers are actual hierarchical constructs, as opposed to
sequences & properties, that's why they require more rules.
Gord: May also want to apply self-determined types constraints that
we discussed yesterday to checkers as well.
Gord: We have two sets of rules:
sequences & properties: formals use self-determined type of actual
let: smart macro approach
Mark: Verilog: tries to automatically size expression.
VHDL : doesn't do anything for you.
self-determined type is going to be unexpected for Verilog users
Michael: Let is using different rules.
Gord: This is because let is essentially a macro.
Erik: Summary: If we go with self-determined types for seq & prop,
checkers should be consistent.
Michael: problem of losing bits should be "lint-able"
b. Bind of checkers
Gord: Question. Is it legal to bind a nested module into a different
place?
Mark: How would you access the module name?
Gord: I hope this is illegal.
Gord: Likewise, binding a checker defined inside non-package scope
should be illegal.
Checkers defined within a package should be fine.
i.e. checker defined within module. can't be bound elsewhere
Tom: What about compilation unit scope?
Gord: This is OK. Compilation unit scope is almost the same as a package.
Tom, Dmitry: seems reasonable
Gord: Would have a problem allowing bind into a procedural scope.
Tom, Dmitry: No real reason to do this
c. Checker instantiation in procedural code
Steven: What about fork-join blocks?
Mark: We don't allow assertions in fork-join at all.
Gord: What about procedural blocks within checkers when checker
instantiated within procedural code?
Tom: Original proposal: loop index variables may be used only in
assertions, not in modeling code. Modeling code was not
duplicated. Modeling code executed independently of checker
instantiation context.
Erik: Should checkvars, & procedural code be duplicated for multiple
scheduled attempts
Dmitry: there is a use case for this
i.e. generic checker put in a for loop
Gord: Think of checker as a class, with static, and automatic variables
i.e. when procedural code flow passes a checker instance, a new
"instance" of the checker "class" would be created. Static
variables are not duplicated, there is one copy for the class,
automatic variables are duplicated with each class instance.
Procedural blocks within a checker are the "static" variables,
assertions are the "automatics".
Neil: When would "instance" go away
Gord: When attempt terminates.
Erik: Doesn't always_check run forever?
Gord: but always_check can't reference const variables
It is the "static" part of the checker "class"
Steven: What about $inferred_enable
With new flow, there could be inconsistencies
Gord: Now there is no reason for $inferred_enable
Mark: When do assignments actually occur
Gord: for a static: because it always exists: easy to describe
Automatic: initialized at construction.
Automatics can only be used in assertions.
Automatics associated with a given attempt
Michael: Sequence match item calling function which modifies variable
we already have problem of mismatch
Gord: Don't talk about sampled values of checkvars
Erik: Summary
Have static and automatic variables within checkers
static variable and procedures are free running
automatic variables and assignments of these are based on
attempts (arming by procedural code).
Break for Lunch
Gord: Class metaphor breaks down when checker instantiated multiple places
Erik: What about assert instance in module with an automatic?
Gord: Could do that, but doesn't make sense.
Automatics only created once.
Steven: May need to come up with examples to see how this works.
Gord: Need to test scenario of assertions in checker w/ different clocks
Gord: Could have a restriction that a checker with an automatic variable
is illegal in a module context. This could be ugly.
Michael: Checkers allow assertions within always_check.
Erik: But we only allow nB assignments in always_check.
Dmitry: No, assertions are allowed in always_check to infer clock.
Gord: Always_check: When clocking event occurs, where does activity
occur?
Mark: Continuous checker variable assigns: Where do they occur?
Gord: If continuous assigns occur in Observed, you would need to evaluate
them first, before assertion evaluations. This is a potential
race condition.
Erik: What is solution?
Gord: Short term solution: Don't worry about races.
User would be responsible for writing race-free code
Gord: Assigments to checker variables in observed region is problematic.
A region is defined as a bucket of events in which any event can
be processed in any order
Erik: Tool vendor could put in additional rules to make it work.
Gord: AAR, SAR rules specify an ordering of event processing, this is
counter to the whole idea of a region
Erik: Could remove AAR SAR from language requirements
These could be tool vendor additional requirements.
Manisha: Couldn't we just remove races by moving checker variable
assignments to the reactive region?
Manisha: Then to evaluate expression using .ended, would need to use
and then use .triggered, instead.
Gord: sequence: s1; a ##1 s2.ended
This is a race condition! There's no guarantee that s2.ended
will return the correct value.
This is because call to s2.ended could occur before s2 is
processed, and the .ended function may not return a true.
Dmitry, Tom: IF this is the case then .ended is broken, and unusable.
Even .triggered is unusable.
Tom: The .ended construct is a method, correct? The method could be
implemented to guarantee the correct result is returned. It could:
a. wait for s2 to be processed
b. pull s2 off the queue and process it before returning.
Gord: Fix for ended: schedule things which are independent first
Then schedule other dependent things.
AI: Gord Write a proposal to fix this.
Checker Variables:
Dave: Couldn't checker continuous assignments be replaced completely by
let?
Dmitry: What about different assignments to bits of an array?
Dave: Yes, you would have to use concatenations in this case
Gord: Another idea: use:
program always @ (posedge clk)
b <= a
Would cause NBA to be executed in the reactive region because it
is now a testbench construct.
Dave: Why are special checker variables needed for sequential assignments
Dmitry: So that update will occur in observed region
Tom: Couldn't they behave like normal NBA assignments? Update the values
in NBA region
Dmitry: might work.
Dmitry: Need an always @ (edge clk)
Dave Separate issue. We'll talk about that later
Gord: Couldn't we eliminate "checkvar", but just adjust scheduling
semantics within checkers.
Mickael: We did the same in other areas
Dmitry: What about checkvars outside of checkers?
Gord: Is the only reason for modified semantics to assign a variable to
seq.ended?
Dmitry: Willing to do without continuous assigns.
Dmitry: What about edge
Rich: Edge already a keyword, but we could use it.
Dmitry: This would allow clocking on both edges of a clock.
Sometimes this is needed in assertions
Tom: Sometimes it's also needed to model exotic flip-flop designs.
Gord: Free-variables: Could we just have random vars by not initiazing
Michale: or we initialize value to $free.
Gord: We have to be careful here
Conclusion: No need for checker vars
NBA's will follow std NBA semantics
No continuous assignss
Use Let to replace continuous designs
No requirements for initialization
In Checker:
always, initial
NBA assignments
no continuous freevars
assertions
Random variables
Dave: Why not use rand()?
Gord: Don't want to perturb randoms stability for design.
Erik: How would this work? Like this?
always @(gclk)
a <= <random>
Gord: Normal procedure is to solve for randoms at beginning
Gord: Random stability
May need to have random variables have a separate seed.
would random stability of module be affected by a bind?
Insertion of assertion into design should not affect
random stability. -- Need a statement to this effect.
Covergroups:
Gord: If we extend class metaphor of checkers, how do covergroups
fit in?
Covergroup instantiation creates new covergroup type
In classes: you have embedded vs instantiated covergroups.
Is a covergroup declaration in a checker always considered
an embedded covergroup
One covergroup type within checker per covergroup declaration.
Tom: Covergroups declarations were removed from checkers. Only
instances
of covergroups were allowed.
Gord: Probably need to put them back in. Otherwise this will cause us
to lose data about the coverage. Some coverage info is
bound to the covergroup type, not to the covergroup instance.
Tom: Have we solved the problems that caused us to ban declarations of
covergroups within checkers?
Gord: Discussions on automatic/static variables have resolved
problems.
AI: Tom: Update covergroup proposal to permit declarations in checkers
Dmitry: Example: Use of let may give different results for concurrent
assertions vs. immediate assertion.
Tom: Reason for discrepancy is that we plan to have sequences and
properties use self-determined type, while let is just a
straight macro-substitution.
Neil: We need a list of things to scan for in reviewing mantis items.
--
ErikSeligman - 19 May 2008