Re: [sv-ac] Notes from SV-AC Face-to-Face Meeting

on "- 3195 Ben Cohen's proposal on local variable flow-out
           - Ask Ben if he wants to write the proposal."
I'll try to get something by Tuesday, if not, it will be a week later. I'll
miss our telecon on this Tuesday.
Ben Cohen

On Thu, Mar 10, 2011 at 9:04 AM, Thomas J Thatcher <
thomas.thatcher@oracle.com> wrote:

>
>
> 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.
>
>

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.