Notes from the SV-AC Face-to-Face Meeting, March 3,4, 2011
----------------------------------------------------------
I. Present:
Tom Thatcher, Dmitry Korchemny, Scott Little, Anupam Prabhakar
Erik Seligman
Gordon Vreugdenhil, Dave Rich
Attending by Phone:
Tapan Kapoor, Manisha Kulshrestha
II. Dmitry gave a presentation which outlined the SV-AC's wants/needs.
The presentation covered the following topics: Some discussion
is presented inline
- Checker output arguments
Needed for exporting status from a checker
- Continuous assignments, and blocking assignments.
- Procedural control and looping constructs within checkers
- Functions in checkers
Gord: Are you talking about automatic or static functions?
- Calling tasks from checkers
Need to limit this to $display
- Allow calling checkers from functions
- Would have to avoid output connections for checkers appearing
in functions.
- Would need to avoid static variables
- An alternative would be to use a macro in a package.
- Allow checker instances to appear in classes.
- Use checkers in a way consistent with UVM
- Gord: Classes have a defined point of creation, but no defined
point of destruction.
- Only the simplest checkers would work in a class.
- Allow forcing of design variables from checkers.
- Would allow formal verification to do pruning of design.
- Currently done by tool command.
- Why wouldn't you simply drive from checker output?
- Allow interfaces as checker arguments.
- Gord: Should be straightforward. Nothing new here.
III. Discussions of topics in Dmitry's presentation
- Sampling:
Dmitry had proposed a "more flexible" form of sampling.
For some types of variables, $sampled would mean the current value.
Gord: Don't mess with the definition of sampling. Rather, have very
clear semantics which define what types of variables are sampled.
To keep things concise, define the rules once and refer to them.
- Continous Assignmnets
Dmitry's slide had an example of how a a simulator could produce
inconsistent results because of the different regions that different
variables are updated. The slide said, "This should Pass"
Gord: I disagree, this should NOT pass.
- Deferred Assertions
Gord: Could move the deferred assertion reporting to the postponed
region. However, if an action block performs any signal
assignment, the update will not occur until the next
simulation time-step.
IV. Scott's Presentation
- Scott Little presented a proposal for the semantics of adding
concurrent assignments
- Goal: Keep checker rules consistent with the reset of
SystemVerilog.
- i.e continuous assignments would use current values of RHS
variables, and would update in the Reactive region.
- Rather than sampling at checker boundary, each construct within a
checker would have its sampling semantics
- assertions would sample all inputs.
- Non-blocking assignments would sample RHS variables
- Random checker: These would be solved asynchronously
V. Gord: Language Future
- It seems that there are two different worlds which use the language:
- The formal world, relies on a flattened, synthesized design
- The simulation world can't assume a flattened design.
- How do we bridge the gap?
- Should there be more of a split between formal verification and
simulation?
- Assertions as generators is a big problem.
- Action blocks that generate data
- Powerful constructs for formal verification may not work well in
simulation.
- One precedent is the synthesis sub-set.
Many simulation constructs were dis-allowed for synthesis.
- Perhaps we should create a formal super-set.
Would allow powerful formal constructs, while maintaining clean
simulation semantics.
- But don't know if the working group would agree to this direction
in the language.
- Dave Rich: But synthesis subset had problems. For example the
simulation/synthesis mismatch.
VI. More discussions
- Continuous Assignments: Do we need them in checkers?
- Dave: Can't we just fix let?
- Dmitry: example:
let a = b[15:0]; How can we reference a[5]
- Gord: Instead, define like this:
let a = {b[15:0]}; Now, the reference a[5] becomes legal
- Dmitry: example:
struct {
bit a;
bit b;
} s
Without assign, how can you set the struc elements?
- Gord & Dave:
typedef struct {
bit a;
bit b;
} s_t;
let s = s_t'{ . . ., . . .}
- Assignments needed for checker outputs:
Gord: Agree, outputs are the one compelling reason why
continous assignments are needed.
For a let, there is no process
Gord: Continuous assignments updating in the Reactive region should
be OK.
- In simulation, assigns could only target outputs of checker.
- Allow continuous assigns in checkers: needed for outputs.
- Can't expect assigns to update in time for assertion in the same
cycle.
- Can't expect that updated values will be seen by assertions.
i.e. Dmitry's example will still not work.
- Checkers appearing in tasks/functions
- Gord: In simulation - would need to limit to checkers containing
only deferred assertions.
- This would require the compiler to elaborate the statement.
- Essentially the same support requires as a generate block.
- Could different calls to the function result in different
elaborations of the checker?
- If the checker contains only deferred assertions, it should be OK.
- Can't allow anything which would require function inlining.
examples: $inferred_clk
- Alternative idea: treat checker as a parameterized type
example: checker check(. . ., p)
checker ck1 = check(. . ., 1)
- Note that in SystemVerilog, the whole universe of types is known
after elaboration.
- Checker argument Sampling:
- We got to checker input argument sampling because we wanted the
non-blocking assignments to sample their arguments.
- Manisha: What about checker inputs that have a const cast?
The const cast means the checker input is not sampled. it gets
the current value.
- Dave: Any place where a variable triggers a process should not
be sampled.
- Scott: Free checker variables are never sampled.
- Checker output arguments
- May be assigned only from a continous assignment.
- Should it be typed?
- Dave: It will have to be typed.
- Major use case supported:
Driving result indication to other parts of the model
- Dmitry: What about having action block drive assertion output.
- Anupam: Currently deferred assert may only have single subroutine
call.
- Why is deferred assertion action block limited to single subroutine
call?
Text mentions "no begin-end block" -- Seems arbitrary
Concurrent assertions don't have this restriction.
- Forcing in checkers
- Use cases:
1. Substituting module with abstract model in a system.
2. Pruning the design
- Checkers in classes
- Use case:
OVM/UVM allows monitors in classes. Why couldn't these be
implemented as checkers?
- Note: Only expect, and immediate assertions allowed in classes
- Dave: Note that immediate assertions are turned off by $assertoff
and other assertion control tasks. Thus, a monitor implemented
with assertions could also be turned off.
- He recommended against using assertions in the monitor
implementation.
- No defined destruction point for a class: A checker/assertion
could fail long after it is useful.
- Scott: Checkers might make sense in some static classes.
- Dave: Problem with clocking blocks: #1 sampling semantics.
- Vacuity
- Scott: We had discussed vacuity before.
However, research is not mature in this area.
We should just fix implies and leave the rest for later.
Day 2
=====
V. Discussions
- Local Variables: 3 Mantis items open
- 2555 is just a clarification
- 3057 Allows first-class local variables
- Would allow declaration within any parenthesized scope
- Annex F would already support this
- Manisha: Would conflicting definitions be well defined?
(local variables with same name defined in different scopes)
- 3195 Ben Cohen's proposal on local variable flow-out
- Ask Ben if he wants to write the proposal.
- AMS Assertions:
- Scott: Details of AMS Group
- Freescale developed realtime sequence syntax
- They just don't know how to implement it.
- Definition for non-overlapping implication needs work.
- Did a realtime LTL implementation
- Scott: Application to P1800
- Annex F does have unclocked support
- Published work on extending PSL for unclocked use.
- PSL has unclocked support.
However, nobody implements it because it would mean evaluating
every time step.
- Dmitry: It would be good to have a notion of stability.
(even for regular assertions: could use it to check for glitches)
- Dynamic data types in assertions
- Existing use: Inside procedural code, an automatic variable can
be considered an example of how this might work.
The value of the variable is captured and preserved throughout
the assertion attempt.
- Erik: Would similar mechanism work for dynamic data types?
- Scott: Might not want ot capture the value right away. What abou
a temporal assertion?
- Erik: But the object might be destroyed before the temporal
assertion attempt completes.
- What's the difference between these examples?
string s;
always @ (posedge clk)
if (s == "yes") . . .
and
string s;
assert property ( @(posedge clk) s == "yes" );
- One difference is sampling.
Sampling captures the value in the Preponed region
It doesn't refer to the original object.
- Could we sample dynamic types?
- If the index is not constant, we would have to sample the
entire array.
e.g. assert property ( myqueue[i] == 4 );
- Manisha: Same problem if we use a local variable for the index.
- Dmitry: Example
Would like to do something like this:
property p (x, set);
x inside set;
endproperty
assert property p(y, '{1,3,7});
- Dave: for this, you would need to declare the type of "set".
Can't have it untyped.
- Tom: What is the motivation for allowing dynamic types in
assertions?
- Scott: Would like to put assertions in test bench to catch
test bench bugs.
- Adding real types to assertions
- Dave: Language in other parts of the LRM say, "The expression
must return an integral type" Using language like this would
easily permit the referencing of real types in assertions.
- Dmitry: Displayed presentation slide, which proposed adding
an "integral" type. A formal argument typed "ingegral" would
accept any integral type, but would not accept arguments of
sequence & property, for example.
- Dave: But then what about real types?
- Dave: Note that you can already type an expression like this:
if ( type(x) == int )
- Dave: There is already the type "packed" Any packed type can
be interpreted as an integral type.
Probably need to discuss this more with the SV-BC.
- What about variables of type time
- Problem: If you use $time direcly in an assertion, you will get
the current value.
If you capture $time in a variable in a process, then try to
use that variable in an assertion, you will instead get the
sampled value of the variable, not the current time.
- Don't try to fix this. Variables of type time should be sampled
just as any other variable appearing in assertions. The user
will have to know that this is a problem. You can't capture
time in a variable, and refer to it in an assertion and expect
to get the correct time.
- Global Clocking
- Dmitry: Want to allow multiple global clocks.
- Tom: Doesn't this mean that global clock is now essentially the
same as default clocking?
- Anupam: This proposal requires that the global clock appears at
the very top level of the model. Before, global clock could
appear anywhere in the model, and it would affect the entire
design.
- Dave: Now the global clocking must be in a higher level of
hierarchy than the call to $global_clock
- Backward incompatibilities:
- Modules could get different global clock than they did before
- Modules which used to have a valid global clock might not have
one with this proposal.
- Assertions could get different values for future value functions
if the effective global clock changes.
- Assertionns and Covergroups
- Dmitry: Proposed temporal coverage
covergroup
A : coverpoint a { bins a[] = {1,2}; }
B : coverpoint b { bins b[] = {[1:3]}; }
cover property ( trig #-# A[*2] ##1 B[*2] );
endcovergroup
This cover property would report coverage for sequences where
coverpoint A matches 2 cycles in a row, and coverpoint B matches
in the following two cycles. In addition it would create a cross
over the different possible bins of coverpoints A and B.
- Tom: It's not really clear from the syntax that the cover
property is crossing the bins of A and B.
- Dave: There is already existing syntax for transition bins.
But the syntax only allows for transitions between one coverpoint
bin, and another bin in that same coverpoint.
- Dave: Maybe you need to include the cross somehow in the syntax.
- Dave: If this type of thing is needed, you should write up a
detailes spec of requirements, ignoring syntax.
- Dave: One other enhancement: it might be desireable to specify
that illegal bins in a cover point will act like an assertion,
and fire if they are hit.
-- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean.Received on Thu Mar 10 09:05:31 2011
This archive was generated by hypermail 2.1.8 : Thu Mar 10 2011 - 09:05:40 PST