----------------------------------------------------------

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.