Subject: [sv-ac] R58c - access to past values ... with enable
From: Adam Krolnik (krolnik@lsil.com)
Date: Thu Sep 19 2002 - 14:14:28 PDT
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
This archive was generated by hypermail 2b28 : Thu Sep 19 2002 - 14:23:14 PDT