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 ------------------------------------------------------------Received on Wed Dec 15 03:11:17 2004
This archive was generated by hypermail 2.1.8 : Wed Dec 15 2004 - 03:11:18 PST