[sv-ac] Re: R58c - access to past values ... with enable

Subject: [sv-ac] Re: R58c - access to past values ... with enable
From: Bassam Tabbara (bassam@novas.com)
Date: Thu Sep 19 2002 - 15:08:27 PDT

Adam,

Thx for the example, 2 things.

1) I think you are making a statement about -sampling-, so as I said earlier, I do not see why this is limited to "prev", you are giving one example using that construct, if there is an enhancement to sampling I'm sure there are other examples of this symptom.
2) In the example, I'm afraid I don't see why doing:

.... prev(expr, 1)@(posedge (clk) && clk_en) does not do what you want to do for:

always @(posedge clk)                     (2)
    if (clk_en)  p_expr <= expr;

does not catch what you want ???  Note, I am not thinking "gated clock" above, although I am thinking of a let me call it "(event) expression" sampling. If the issue is indeed sampling then an expression there should fix it.

-Bassam.

Adam Krolnik wrote:

Hello Bassam and Cindy;

Requirement 58c is to support access of past state
when working in a design that uses enabled registers.
E.g.

  always @(posedge clk)
    if (enable)  q <= d;

Suppose you write a property:

always assert (done -> {theout[2:0] == prev(thein[2:0], 2)})
   @(posedge clk);

Here I want to compare theout to a prior (2 cycles) value. Now how
do I modify this for the case where an enabled register may have
caused a value to not update. I would want to change the number
of cycles into the past 1 additional clock for each cycle the
enable is not asserted.

Now when you start talking about gated clocks and enabled registers,
you may be talking about two different things. For example,
when you say gated clock, are you expecting the clock gating signal
to be zero skew with the clock signal, such that when the clock gate
signal is asserted (whichever polarity) the clock is not allowed to
transition. If this is what is expected, then shouldn't this statement
accurately represent a gated clock?

  p_expr = prev(expr, 1)@(posedge (clk && clk_en))

  always @(posedge (clk && clk_en))         (1)
     p_expr <= expr;

But if the clock gating signal is not expected to have zero skew with
the clock signal, then the gating will be applied to the following
(active) clock edge. This is what an enabled register expects to
use when one codes the following:

  always @(posedge clk)                     (2)
    if (clk_en)  p_expr <= expr;

As you see, the verilog coding is different, and their effect is
different.
Consider these waveforms.

clk       HH LL HH LL HH LL HH LL HH LL HH LL HH LL HH
clk_en    ------------______--------------------------------
expr      1     2     3     4     5     6

#1p_expr        1           3     4     5
#2p_expr        1     2           4     5

We have designs where the enable for registers is derived from
combinatorial logic and thus can not affect the current cycle.
So their effect is as #2 shows. If one drives a clock enable
from a register (not from combinatorial logic) then one can
control it such that it affects the current cycle.

I see a need for both

prev(expr, 1)@(posedge (clk && clk_en))
prev(expr, 1, clk_en)@(posedge clk)

   Thanks.

    Adam Krolnik
    Verification Mgr.
    LSI Logic Corp.
    Plano TX. 75074

-- 
Dr. Bassam Tabbara
Technical Manager, R&D

Novas Software, Inc.
bassam@novas.com
(408) 467-7893
 

This archive was generated by hypermail 2b28 : Thu Sep 19 2002 - 15:09:56 PDT