Hi Erich, all,
Here's the sharpening of the last part of the third paragraph of
the proposal that we agreed on in yesterday's discussion. I have changed
the last part of the third paragraph from
.. then the value of the built-in function prev() should conform to that value.
to
.. then the built-in function prev() should return that value.
Updated proposal (first 3 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 built-in
# function prev() should return that value.
#
# NOTE: ....
On Wed, Dec 29, 2004 at 11:19:07AM +0100, Johan Mårtensson wrote:
> 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
> ------------------------------------------------------------
-- ------------------------------------------------------------ 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 ------------------------------------------------------------Received on Wed Jan 5 08:48:42 2005
This archive was generated by hypermail 2.1.8 : Wed Jan 05 2005 - 08:48:58 PST