Re: Group B issues action item. prev,rose,fell semantics.

Hi Erich, all

Based on yesterday's discussion I propose the following wording for the
3 first paragraps of section 5.2.3.1

# 5.2.3.1 prev()
#
# The built-in function prev() takes an expression of any type as argument
# and returns the value of that expression as evaluated in a previous
# cycle. With a single argument, the built-in function prev() gives the
# value of the expression in the previous cycle, with respect to the clock
# of its context. If a second argument is specified and has the value i,
# the built-in function prev() gives the value of the expression in the
# ith previous cycle, with respect to the clock of its context.
#
# The clock context may be provided by the PSL property in which the
# function call is nested, or by a relevant default clock declaration. If
# the context does not specify a clock, the relevant clock is that
# corresponding to the granularity of time as seen by the verification
# tool.
#
# If there is no (ith) previous clock cycle or that clock cycle is not at
# intitialization time or later and if a value is given to the expression
# for time points prior to initialization time by the simulation semantics
# for the HDL underlying the PSL flavor in question then the value of the
# built-in function prev() should conform to that value.
#
# NOTE: ....
#

Best Regards, Johan M.

On Tue, Dec 28, 2004 at 04:40:08PM +0100, Johan Mårtensson wrote:
> Hi Erich, All,
>
> The following is the LRM changes I propose for the group B issues.
>
> I propose to put the following paragraph after the two initial
> paragraphs of section 5.2.3.1
>
> # If there is no (ith) previous clock cycle or that clock cycle is not at
> # intitialization time or later then the value of the built-in function
> # prev() should conform to the value given to the signal for negative time
> # points by the simulation semantics for the HDL underlying the PSL flavor
> # in question.
>
>
>
> # 5.2.3.1 prev()
> #
> # The built-in function prev() takes an expression of any type as argument
> # and returns a previous value of that expression. With a single argument,
> # the built-in function prev() gives the value of the expression in the
> # previous cycle, with respect to the clock of its context. If a second
> # argument is specified and has the value i, the built-in function prev()
> # gives the value of the expression in the ith previous cycle, with
> # respect to the clock of its context.
> #
> #
> # The clock context may be provided by the PSL property in which the
> # function call is nested, or by a relevant default clock declaration. If
> # the context does not specify a clock, the relevant clock is that
> # corresponding to the granularity of time as seen by the verification
> # tool.
> #
> # If there is no (ith) previous clock cycle or that clock cycle is not at
> # intitialization time or later then the value of the built-in function
> # prev() should conform to the value given to the signal for negative time
> # points by the simulation semantics for the HDL underlying the PSL flavor
> # in question.
> #
> # NOTE: ....
>
> This is much less explicit than what we discussed at the meeting. On the
> other hand a more explicit description might put to much focus on what
> is a corner case and make the text lopsided. I think though that we
> should consider providing a formal semantics for clocked prevs and
> endpoints.
>
> With regard to the prev(v(i)) issue I don't think anything needs to be
> added to clarify the meaning of prev(v(i)) in light of what is stated in
> the first paragraph of 5.2.3.1.
>
> I note that there still is an SVA alignment issue w.r.t. to the
> definition of rose (2.5.3.4) and fell (2.5.3.5). I propose that we leave
> this for now pending a more thorough investigation of the consequences
> of a change.
>
> Best Regards, Johan M
>
> >
> >
> >
> >
> >
> >
> >
> >
> >
> > On Wed, Dec 15, 2004 at 12:11:07PM +0100, Johan Mårtensson wrote:
> > > Hi Erich, All,
> > >
> > > The following is the specification of the Group B action item w.r.t prev
> > > that I promised to compile at yesterday's extensions meeting.
> > >
> > > 1) The LRM text should state that for each PSL flavor the value of
> > > prev(s)@TRUE at the 0 time point should conform to the simulation
> > > semantics of the HDL underlying that flavor. One could perhaps exemplify
> > > with e.g. what is stated about VHDL in IEEE 1076, (IEEE 1076-1993
> > > section 12.6.4. I do not have access to the 2002 version.) namely that
> > > the effective value of each signal is assumed to have been the same as
> > > the effective value at initialization time for infinite time, and that
> > > this implies that (for VHDL) the value of prev(s)@TRUE at time 0 is the
> > > same as the value of s at time 0, if indeed it does.
> > >
> > > 2) The LRM should state that if there are less than i previous cycles
> > > with respect to the clock of its context the value of the expression
> > > 'prev(s,i)' should by definition be the same as the value at time 0 of
> > > prev(s)@TRUE.
> > >
> > > Best Regards, Johan M.
> > >
> > >
> > > On Tue, Dec 07, 2004 at 03:41:48PM +0100, Johan Mårtensson wrote:
> > > > Hi All,
> > > >
> > > > I am responsible for the LRM change action item for the Group B issues.
> > > > I have started to work with the first part namely the semantics of prev,
> > > > rose and fell at the first time point (issues 9 and 10). Although we
> > > > resolved the issue at an extensions meeting about a month back I think
> > > > this resolution was not complete and somewhat problematic so I think we
> > > > need to discuss these problems before I go on and formulate the LRM
> > > > changes.
> > > >
> > > > I will indicate what I think are the problems with our resolution by
> > > > commenting on the description of the committee resolution in
> > > >
> > > > http://www.eda.org/ieee-1850/Issues/Group-B.html
> > > >
> > > > > Discussion
> > > > >
> > > > > There is general interest in alignment with SystemVerilog where possible.
> > > > > (However, it is not clear that the SystemVerilog LRM defines these details.)
> > > > > Being consistent with VHDL (e.g., s'last_value) is also desirable. In VHDL, all
> > > > > signals are considered to have been stable for infinite time into the past,
> > > >
> > > > This is indeed in accordance with IEEE 1076-1993 section 12.6.4 in which
> > > > the simulation semantics for the initialization phase of the simulation
> > > > cycle is described.
> > > >
> > > > > so
> > > > > s'last_value is defined to return s at time 0.
> > > >
> > > > This statement doesn't seem to be correct in light of the previous
> > > > comment and the definition of the result of application of 'last_value
> > > > in section 14.1 of IEEE 1076-1993. There the result of s'last_value is
> > > > defined as "The previous value of s, immediatly before the last change
> > > > of s". But given 12.6.4 there was no last change of s at timepoint 0 so
> > > > s'last_value seems to be undefined at timepoint 0.
> > > >
> > > > So perhaps we should decide that for the VHDL flavor unclocked prev(s)
> > > > should have the value s at the 0 time point (not because it conforms to
> > > > 'last_value which it doesn't) but because it conforms to the simulation
> > > > semantics described in 12.6.4.
> > > >
> > > > But this gives no guidance for how this should be resolved for the other
> > > > flavors. Perhaps we should simply state that the value of prev(s) at
> > > > time 0 for a certain PSL flavor should conform to the simulation
> > > > semantics for the corresponding HDL.
> > > >
> > > > > Similarly, prev(s) should return
> > > > > the initial value of s, and prev(s,clk) at the first tick of clk should return
> > > > > the initial value of s.
> > > >
> > > > Here we have the additional problem that the clock never ticks prior to
> > > > timepoint 1 according to the VHDL simulation semantics, but I guess one
> > > > may still argue for the above by "had the clock ticked before the 0 time
> > > > point (which it admittedly cannot) then the value of s at that negative
> > > > time point would have been the same as the initial value of s.
> > > >
> > > > Again this reasoning does not necessarily apply to PSL flavors different
> > > > from the VHDL one. A way to get a definition that is agnostic with
> > > > respect to different simulation semantics would be to simply define:
> > > >
> > > > prev(s,n)@clk at or before the first clk tick
> > > > = prev(s)@TRUE at time 0?
> > > >
> > > >
> > > > > Resolution
> > > > >
> > > > > 1. Prev(s) == initial value of s at time zero.
> > > > > 2. Prev(s,clk) == initial value of s at the first tick of clk
> > > > >
> > > > > 3. Given the definition of Prev(s), then unclocked rose/fell are False
> > > > > at time 0
> > > >
> > > > With respect to rose and fell there is an explicit disagreement between
> > > > the informal semantics of SVA 3.1a and PSL 1.1. In the SV 3.1a LRM
> > > > 17.7.3 (Sampled value functions) there is stated that
> > > >
> > > > - $rose returns true if the least significant bit of the expression
> > > > changed to 1. Otherwise, it returns false.
> > > >
> > > > - $fell returns true if the least significant bit of the expression
> > > > changed to 0. Otherwise, it returns false.
> > > >
> > > > whereas in the PSL 1.1. LRM section 5.2.3.4 rose(s) is defined to be
> > > > true if(f) "the arguments value is 1 at the current cycle and 0 in the
> > > > previous cycle", or in other words if s=1 and prev(s)=0.
> > > >
> > > > If signals can only have the values 0 and 1 the definitions seem to give
> > > > the same result but if other values are allowed then they may differ.
> > > > This is the case for example with respect to the example near the top of
> > > > page 213 of the SV 3.1a LRM where it is stated w.r.t. $rose, $fell and
> > > > $stable that "When these functions are called at or before the first
> > > > clock tick of the clocking event, the results are computed by comparing
> > > > the current sampled value of the expression to X." In this situation if
> > > > s=1 the SVA value of $rose(s) is 1 but the PSL value of rose is 0 and if
> > > > s=0 the SVA value of $fell(s) is 1 but the PSL value of fell is 0.
> > > >
> > > > (...)
> > > > >
> > > > > 6. In all of the above cases, we should check that this is consistent
> > > > > with SystemVerilog definitions
> > > >
> > > > Summary:
> > > >
> > > > I'd like to summarize the comments made above in a list of questions
> > > > that I think the extensions committee should answer before I can go on
> > > > and try to formulate the LRM changes.
> > > >
> > > > 1) It seems we decided to define prev(s) at the first cycle in
> > > > conformity with the simulation semantics. It is unclear whether we
> > > > decided that all flavors should conform to the simulation semantics for
> > > > VHDL or to that of the respective underlying HDL. This needs to be
> > > > clarified.
> > > >
> > > > 2) Assuming we decide that the value of prev(s) should conform to
> > > > whatever value the simulation semantics for the underlying HDL assigns
> > > > to s at the last negative timepoint, should we be explicit about what
> > > > that value is or should we simply state that such conformity is
> > > > presupposed.
> > > >
> > > > 3) Should we decide that prev(s,n) = prev(s) at time 0 for all flavors?
> > > >
> > > > 4) Should we decide that prev(s,n)@clk = prev(s)@TRUE at time 0?
> > > >
> > > > 5) Should we not align the semantics of PSL rose and fell with that of SVA
> > > > $rose and $fell? This will only make a difference in cases where other
> > > > values than 1 and 0 may occur?
> > > >
> > > >
> > > > Best Regards, Johan Martensson
> > > >
> > > > >
> > > >
> > > > --
> > > > ------------------------------------------------------------
> > > > Johan Martensson, PhD Office: +46 31 7451913
> > > > R&D Mobile: +46 703749681
> > > > Safelogic AB Fax: +46 31 7451939
> > > > Arvid Hedvalls Backe 4 johan.martensson@safelogic.se
> > > > SE-411 33 Gothenburg, SWEDEN
> > > > PGP key ID A8857A60
> > > > www.safelogic.se
> > > > ------------------------------------------------------------
> > >
> > > --
> > > ------------------------------------------------------------
> > > Johan Martensson, PhD Office: +46 31 7451913
> > > R&D Mobile: +46 703749681
> > > Safelogic AB Fax: +46 31 7451939
> > > Arvid Hedvalls Backe 4 johan.martensson@safelogic.se
> > > SE-411 33 Gothenburg, SWEDEN
> > > PGP key ID A8857A60
> > > www.safelogic.se
> > > ------------------------------------------------------------
> >
> > --
> > ------------------------------------------------------------
> > Johan Martensson, PhD Office: +46 31 7451913
> > R&D Mobile: +46 703749681
> > Safelogic AB Fax: +46 31 7451939
> > Arvid Hedvalls Backe 4 johan.martensson@safelogic.se
> > SE-411 33 Gothenburg, SWEDEN
> > PGP key ID A8857A60
> > www.safelogic.se
> > ------------------------------------------------------------
>
> --
> ------------------------------------------------------------
> Johan Martensson, PhD Office: +46 31 7451913
> R&D Mobile: +46 703749681
> Safelogic AB Fax: +46 31 7451939
> Arvid Hedvalls Backe 4 johan.martensson@safelogic.se
> SE-411 33 Gothenburg, SWEDEN
> PGP key ID A8857A60
> www.safelogic.se
> ------------------------------------------------------------

-- 
------------------------------------------------------------
Johan Martensson, PhD            Office: +46 31 7451913    	
R&D                              Mobile: +46 703749681
Safelogic AB                     Fax: +46 31 7451939
Arvid Hedvalls Backe 4           johan.martensson@safelogic.se
SE-411 33 Gothenburg, SWEDEN 
PGP key ID A8857A60
www.safelogic.se
------------------------------------------------------------