[sv-bc] [Fwd: Notes from meeting w/ Dmitry and SV-BC and SV-EC members]

Hello Everyone,

Dmitry Korchemny and Tom Thatcher from the SV-AC met informally with
members of the SV-BC and SV-EC to explain features of the SV-AC
proposals, and try to work out any possible problems in these
proposals.  Here are the notes I took from the meeting.  Hopefully, I
took the notes down accurately.  Let me know if you have any corrections.

Sincerely,

Tom

Notes from Meeting:

Present:
Dmitry Korchemny, Intel
Karen Peiper
Dave Scott, Mentor
Dave Rich, Mentor
Ray Ryan, Mentor
Tom Thatcher
Matt Hartoog

On Phone:
Erik Seligman
Stuart Sutherland
Shalom Bresticker
Alex Gran
And others?

1.  Dmitry's presentation: Motivation
    Packaging
    Glitches on immediate assertions
    Boolean assertion:  concurrent assertions are not safety properties
    More intuitive syntax for common cases  "until", etc.

Dave (Dave Rich):   Nobody is questioning motivation:  People want to
ensure that there is a unified language.
  Checker proposal does affect other areas of the language.
  May need to to re-do these proposals to ensure they fit into the language.

2.  Concurrent assertions in procedural context
   Confusion over meaning of assertions

       example:
       if (en) begin
          a <=1 1;
          assert property (a)
          a <= 0;
       end

       Karen:  People would expect that assert property will get first
assigned value of a:
       Dmitry: This is not true.  Assertion will get the sampled value.
This semantics has
          been in the standard since 19000-2005

    Question about resolving functions and tasks up through the
hierarchy.  Will it be consistent?  How is this done?
    Dmitry:  There is no mention of this in the proposal.

3.  Checkers inherit context from declaration point
    Use $inferred* functions to inherit from instantiation context.

4.  Checker Modeling:  initial_check, always_check
    Dave:  Are regular always & initial procedures allowed within checker?
    Dave:  Why do you need separate keyword?  Why not use always_ff?
    Dmitry: allows to use @clk for clocking events  (@clk assumed to be
level sensitive)
       Standard says the no clock is inferred from always (@clk).
    Mark: Doesn't see backward incompatibility?  Clocking block would
allow for @clk
       This is simply taking something that was illegal and making it legal.
       Mark:  always @clk could be used if clk is a clocking block signal.

5.  Checker Modeling
    Dmitry: Explaining checker variables.
    Free Variables: Lots of questions on how they work.
    Can they be observed from outside? Could they be assigned from
outside?  Dmitry: No

6.  Single-Assignment Rule, Acyclic Assignment rule
    Questions on sampling rules. It's confusing.
    Continuous checker variables: never sample
    non-blocking: always sampled.
    Scheduling: If a depends on b: it is evaluated before b.
    Mark: Why do we need these special rules for scheduling?
    Dmitry: One reason: avoid glitches
    Mark, Dave:  Why SAR?  Already illegal to have two continuous
assignments to a logic?

    Mark: Define functions in checker.  Can you call these from outside
a checker.?  What happens?
    Would function get sampled values?
    Would be better off saying that you cannot call function from
outside the checker.
    Dave: Functions run in the timestep they are called.

    Dmitry:  Without this, can't use seq.ended() because the value is
only available in observed region.

    Ray: Seems like there's no blocking
    Dave: Would people want these features outside of checkers?  Why not
have separate proposals for
       Checkers and for checker variables/always_check procedures.?
       Example of specify blocks: Was a quick implementation, but hurt
the language in the long run.
    Dmitry: We could allow checker variables outside. Nothing prevents
us from allowing these outside a checker later.
    What is difference between logic with initialization and a checker
variable with initial value?
    Dmitry: Separation between design and verification:  checkvars are
the verification code.
    Ray,Dave: Is correct behavior due to "checker variable" or due to
"always_check procedure"?
    Mark, Dave:  Seems like we need a way to do "always @ (edge clk)"
or "always_ff @(clk)".  That would unify
       always & always_check
    Tom:  I have seen the need for this when trying to model exotic
flip-flop designs.
    Dmitry:  Always_check introduced for clock inference, nothing more
(i.e.  always_check @(clk)  ).

7.  Full RTL support
    Regular RTL not supported inside checker
    Mark:  Regular RTL support would simplify proposal.  Wouldn't need
special rules.
    Mark:  Will you be able to $display a checker variable from
outside?  Would you see a result that would be
       explainable?
    Ray:  Could you do  "@ (posedge check_instname.checvar)"?   Dmitry:
Not forbidden
    Dmitry:   Could also do "always @sequence"
    Mark: Assignments in action block:  performed in Reactive region.
Dmitry: should use $sampled to display values

8. Assertions in Procedural Loops
    Mark: Essentially,because you are treating loop index as a constant,
you are essentially "unrolling" the loop.
       Automatic loop index variablewould otherwise be gone by the time
assertion evaluates.
    Dave:  Would not be able to use automatic variable for part select.
       e.g. for (int i=0; i<3; i++) assert property (@clk a[i:i+2])
    Mark: Many people against putting assertions into loops.  Have to be
be careful of the hierarchical naming.
    Dmitry: Current proposal was developed with a lot of help from Gord
    Mark: Can't differentiate between module instantiation and checker
instantiation.
    Mark:  Nothing wrong with extending rules to unrollable loops.
    Dave: Issue is not putting assertion into loop:  Issue is the
semantics of how this occurs.
       Outside of loop:  No correlation between procedural context and
operation of loop.
       In a loop: Now operation depends on the loop itself.
    Ray: Now there seems to be shared state between loop and assertion
    Dave:  Because the definition is a single assertion executed
multiple times, coverage information is not complete
    Ray: Don't understand "a concurrent assertion is executed multiple times
    Dave: Nothing prevents us from going back to a generate semantic.
       Would need to be distinct instances of action block for different
iterations.
       e.g. counter in action block counts number of fails.  No way to
create independent counts for different iterations.

9.  Checkers in loops
    Extending from assertions in loops.
    Dave:  People have wanted "generate" within procedural code for some
time.
       eg array of interfaces
    Dave: If we solve this problem for assertions, would this not solve
similar problems for other constructs?
    Mark: Depends.
    Dave: What if you forced a label on any assertion within loop? Could
you force a label that would guarantee legal naming.

    Dmitry: Feels that this definition of checkers in loops is
harmless.  It could be seamlessly replaced with something better.
    Dave: Ambiguities as to what coverage data is stored.
    Dave: Need to resolve naming issues.
    Dave S: For coverage database: Need to be defined as different
assertions for accurate coverage reporting


10.  Responses to Gord's comments

a.  $inferred_enable: Not discussed in 1900:  Type of $inferred_enable
is the type of the underlying expression.
b.  Hierarchical names:  Proposal says "Variables used in a checker that
are neither formal arguments to the checker
    or internal variables are resolved according to the scoing rules
from the scope in hwich the checker is declardd.
c.  Hierarchical names referencing checker internals should not be
checker actual args
d.  Hierarchical names referencing checker internals are allowed
    e.g. $assertoff
e.  Checker variable assignments and forcing:  Should we allow external
assignment or forcing of checker variables.
    Assignments of variables from checker internals:  a = checkinst.v
    Ray: What if sibling checkers referenced each other through
hierarchical references?  AAR violation
    Dmitry: Yes.  AAR checking has to be global.
    Mark:  Could you write to these variables from VPI?
    Dmitry:  Not restricted now
f.  VCD for checker variables is the same as for regular variables.
    Can you dump interfaces?
    Anything special needed to dump a checker?
    LRM talks about list of modules only for $dumpvars.

g.  Gord's comment:  "Would like simple list of rules"
    1.  Immediate assertions:  execute procedurally as an if statement
       (Exception:  you can $disable an immediate assertion, you can't
$disable an "if" statement)
    2.  Deferred Assertions:  Same as immediate assertion, but only the
latest result is reported.
       Reporting is done in the reactive region.
    3. Concurrent assertions:
       Execute according to the clocking event:  A clocking event is
required.
       Can infer clocking event from an always, initial, always_ff, and
always_check/initial_check


Stu: General comment: Standard has already slipped into 2009.  Doesn't
matter if it's beginning of 2009, or end of 2009.  Take the time to do
it right.



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