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