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

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