Re: [sv-ac] call to vote on 1698

Hi Tom:

> In the clock inference section, what does this phrase mean???
> 
> 	"the event expression is maximal among those of these forms"

The technical point I am trying to capture can be illustrated by the
following example, which already appeared in the proposal before I 
made my revisions:

   property r3;
      (q != d);
   endproperty
   always_ff @(posedge clock iff reset == 0 or posedge reset) begin
      r1 <= reset ? 0 : r1 + 1;
      q <= $past(d1);
      r3_p: assert property (r3);
   end

According to the text in the proposal, the inferred clock is 

   posedge clock iff reset == 0

The question is, what rule tells us that this is the inferred clock
and not, say, just 

   posedge clock

?

In thinking about how to write this, I did not find a better way
to express the rule that would ensure that if 

  posedge clock iff reset == 0

and 

  posedge clock

both satisfy all the other rules, then you must take 
  
  posedge clock iff reset == 0

as the inferred clock, not just "posedge clock".  I am open to suggestions.

> Also, I want to understand better the motivation behind the changes in 
> this section.

My understanding is that these changes are intended to address
Jonathan Bromley's suggestions to improve the clock inference
rules.

> In 16.8.3, I would keep the sentence "The value of $sampled is . . ."

The full sentence that you are referring to is 

  The value of $sampled is updated in the Preponed scheduling region
  in every simulation time step.

The point of view I took in revising this proposal is that $sampled,
$rose, $past, etc. are functions, not data objects.  As such, we talk
about the value returned from a call to the function rather than when
a data object is updated.  In order to make it clear what these
functions return when called from various places inside and outside of
assertions, I thought that what was needed was simply clear statments
of the value returned by the functions in terms of the timesteps in
which they are called and the values of various expressions at that or
previous timesteps.  

Defining a data object associated with the function and saying when
the data object updates is really an implementation.  I thought it
better to leave these choices to the tool developers.

> Also in 16.8.3,  I liked the original wording better:  "The clocking 
> event is used to obtain . . ."
> In my first reading, I missed the final clause of the revised sentence 
> "in which a clocking event occurs" and was ready to vote no before I 
> re-read the sentence.

This text could be recrafted, but my opinion is that the new text is
much more precise than the old text and does a better job of
explaining what the value change functions return when called inside 
or outside of assertions.

> Also in 1.8.3,  How about "first occurence of the clocking event", 
> rather than "first simulation timestep in which the clocking event occurs"

Recrafting of the text is possible.  The new text should still meet
the goal of giving a precise description of what the functions return
when called inside or outside of assertions.

J.H.

> Date: Fri, 15 Feb 2008 18:11:46 -0800
> From: Thomas Thatcher <Thomas.Thatcher@Sun.COM>
> Sender: Thomas.Thatcher@Sun.COM
> Cc: sv-ac@eda.org, dmitry.korchemny@intel.com
> Reply-to: Thomas.Thatcher@Sun.COM
> X-OriginalArrivalTime: 16 Feb 2008 02:12:06.0804 (UTC) FILETIME=[54358D40:01C87041]
> 
> I vote no on 1698
> 
> I don't quite understand the new rules for inferring clocks from 
> procedural blocks.   For example:
> 
> In the clock inference section, what does this phrase mean???
> 
> 	"the event expression is maximal among those of these forms"
> 
> Also, I want to understand better the motivation behind the changes in 
> this section.
> 
> I have the following friendly amendments:
> 
> In 16.8.3, I would keep the sentence "The value of $sampled is . . ."
> 
> 
> Also in 16.8.3,  I liked the original wording better:  "The clocking 
> event is used to obtain . . ."
> In my first reading, I missed the final clause of the revised sentence 
> "in which a clocking event occurs" and was ready to vote no before I 
> re-read the sentence.
> 
> Also in 1.8.3,  How about "first occurence of the clocking event", 
> rather than "first simulation timestep in which the clocking event occurs"
> 
> I'm also trying to come up with a more understandable replacement for
> "sampled in the Preponed region of a particular timestep strictly prior
> to the one in which $past is evaluated"
> But I haven't come up with anything better yet.
> 
> 
> 
> Tom

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