RE: [sv-ac] my notes from the face-to-face

Hi John/All,

About the note:  
"- VPI traversal needs to be understood.  VPI may descend into
sequential
  statement where there is a checker instance.  Currently sequential
blocks
  only lead to sequential structure.  SV-CC needs to look at this." 

Also note 1 in Lisa's notes -- "1.      VPI access to checker instances
and sequence and properties in procedural code is an issue that needs to
be addressed so we will open an independent MANTIS item that is assigned
to SV-CC (get help from Bassam).").

I think the VPI support can mimic what's there for immediate assertion
-- see 36.51 (Atomic Statement) in draft3a.

Thx.
-Bassam.

-----Original Message-----
From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of John
Havlicek
Sent: Tuesday, October 09, 2007 5:01 AM
To: sv-ac@eda-stds.org
Subject: [sv-ac] my notes from the face-to-face

Hi Folks:

I scribbled some notes on paper during the face-to-face.
Not all of them make sense to me now, but I have tried to capture what
does make (some) sense.  See below.  

J.H.

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

2007-10-02
----------

1900 (Checkers)
---------------

- Does .* binding win over default actual argument if the formal
  name matches in the instantiation context?

- Suppose that you instantiate a checker in a context where there
  are automatics.  What does the continuous assignment mean?

- Is it required only to reference static variables in checkers?

- Can a checker be instantiated in an always with fork/join/none?
  Fork/join/none can reference a task automatic.  It is possible for
  the automatic to outlive the task.

- What is the semantics of a constant freevar in simulation?

- What is the granularity of determination of continuous vs.
non-continuous
  assignment?  Is it at the packed boundary, as in the rest of the
language?

- Bitwise data flow analysis needs to be well defined.  This could be
  expensive.

- We should allow more types to be passed to checkers.

- An example:

     always_check@(clk) a <= b;  

  behaves "like" 

     a <= clk != $next_gclk(clk) ? b : a;

- Should strings be allowed as arguments to checkers?  What about
properties?
  What limitations should be made?

- There is a possibility of omitting the continous freevar.

- TT:  What about using ordinary modeling constructs?  DK:  This is
non-trivial.

- There are special rules about hierarchical references; name must begin
with
  a scope.

- What about putting the declaration of a checker in a sequential
context?  Is
  this allowed?  Is it feasible?  Is it desirable?

- How does cross connect between checkers work?  There is language
limiting
  defparams that may be useful in limiting cross connect between
checkers.

     "a hierarchical reference to a checker shall not pass outside the
      checker hierarchy"

- Are hierarchical names in a checker declaration resolved from the
declaration?
  If not, then checkers diverge from sequences and properties, which may
be
  bad.

- $unit does not have a location in the hierarchy.

- Possible restriction:

    "It shall be illegal to reference an automatic variable in a checker

    instance"

- There are troubles with using rewriting to define checker
instantiation.
  Name referencing is problematic in comparing the rewrite to the
original.
  There are rules about referencing anonymous generate blocks, e.g.

- VPI traversal needs to be understood.  VPI may descend into sequential
  statement where there is a checker instance.  Currently sequential
blocks
  only lead to sequential structure.  SV-CC needs to look at this.

- SAR (single assignment rule) has a higher degree of precision than
other
  assignment rules.  Checkers are proposing this at bit level.  Rules
for
  the rest of the language are at packed level.  What does SAR do with
  a reference like b[a+:5] ?  The rule needs to be defined carefully for
  indexed part selects.  See 11.5.3, 9.2.2.2.

- Are genvars allowed in checkers?

- GV:  Does the functionality of checkers subsume the functionality of
let?
  DK:  No.

- The behavior of a tool option may be defined even though mechanisms by
  which the option is specified are not defined.

- Possibly one can map to fork/join/none threads; see Mantis 1336, 1615.
  Thread creation is not permitted in a function called in a continuous
  assignment.



2007-10-03
----------

2005 (Glitch-free Assertions)
-----------------------------

- Glitching and clocking are separate problems.  It may be bad to try to
  correlate their solutions.

- There is a fundamental problem in trying to define these through
rewrites
  with limitations related to synthesizability.  This is not well
defined,
  and the frontier of synthesizable is not constant.

- Mantis 890 overhauled clocking blocks.

- $tick occurs once per timestep in the pre-active region.

- What about putting these assertions in postponed?

- GV:  Another approach is the following:  if the assertion line is
  reached, then schedule it to evaluate in the next observed region
  with the values in that observed region.

  . There can be multiple active settlings followed by observed
executions
    in a timestep.  E.g., active can settle from events scheduled from
    a prior timestep, then observed, then reactive applies stimulus, 
    then active settles, then observed.
  . DK and ES did not think the glitch-free assertion should be
evaluated
    at each observed in this way.
  . JH asked, "why not"?  The design doesn't know if the stimulus will
be
    applied.  If the stimulus is not applied, then you will get the
checks
    after the first settling.  If you are happy with this, then why do
you
    become unhappy with it in case the stimulus is applied?  It seems as

    though you will be missing checks that you actually want.

- Discussion of the need to define an equivalence relation among the
  evaluations of these assertions in a single timestep so that the last
  result can be taken.
 
  . DK suggested a definition motivated from an implementation model
    that takes the stack trace for the evaluation as a signature.  If
    two evaluations have the same signature, then they are equivalent,
    and the later replaces the earlier.

- GV:  Another approach is the following:  Use processes to group the
  evaluations.  If the process that reaches the assertion evaluates
  again, then throw away the old results.  Processes include always @,
  always_comb, etc.

- Naming needs to be standardized.

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