Re: [sv-ac] Proposal updated for Mantis 2656 (Ballot Comment #84)

>
> *[Korchemny, Dmitry] $falling_gclk(clk) is present in Table 16-2, and in
> your table it appears twice. I don’t think that we need to consider all
> ticks of the global clock in this table. If you disagree, you are welcome
> to  open a Mantis item with your suggestion. Unfortunately, we are not
> authorized to address it now.*
>
I have version IEEE P1800/D7a
Below is the heading of Table 16.2.  I see $falling_gclk(sig),but
not $falling_gclk(*clk*)
Perhaps I am looking at an earlier version of the P1800-2009 .
page 334:
*Time $sampled(sig) $future_gclk(sig) $rising_gclk(sig)
$falling_gclk(sig) $changing_gclk(sig)
$steady_gclk(sig) *

> **
>
>
>
> Since most designs use a single edge of the clock, rather thatn both edges,
> I suggest that we modify the example from:  global clocking @clk;
> endclocking
>
> **
>
> To the following    global clocking @ (posedge clk); endclocking
>
> **
>
> assert property(@$global_clock a);   // the assertion states that a is true
> at each tick of the global clock. In simulation, tThis assertion is
> logically equivalent to
>
**
>
> assert property(@ (posedge clk)  a);**
>
>  *[Korchemny, Dmitry] *I think that *global clocking @clk; endclocking*also makes sense. The global clock reflects the primary clock, and the
> primary clock normally should tick at least at each change of clk. Consider
> the following assertion: the clock always ticks. You can implement it as:
>
> assert property (@$global_clock $rising_gclk(clk)); (or $changing_gclk,
> $falling_gclk).
>
>  According to the definition you suggest this assertion will be violated,
> since the sampled value of clk is always 0 @(posedge clk).
>
*[Ben Cohen]* I must have a misconception in the use of the @$global_clock.
If my understanding is correct, if I have a portion of my design that is
synchronous to one clock, I could in simulation and in formal verification
declare a global clocking, and use the @$global_clock as my clocking event.
 Thus, if my FF trigger on positive edge, I could state
 global clocking @ (posedge clk); endclocking
  p1: assert property (@$global_clock req |=> ack);
p1 may or may not necessarily hold on each edge of the clock.
The use of "*global clocking @clk; endclocking*" may be implying that this
is the way to use a global clocking.  Yet, from the 16.5 update: *A
reference to $global_clock  (see 14.14 ) is understood to be a reference to
the clocking_event  defined in the global clocking  declaration. The global
clock behaves just as any other clocking event. In formal verification,
however, $global_clock  has additional significance, as it is considered to
be the primary system clock (see F.5.1 ). Thus, in the following example *
* **global clocking @clk; endclocking*
*.** **..*
* **assert property(@$global_clock a);*
*the assertion states that a  is true at each tick of the global clock. In
simulation, tThis assertion is equivalent to*
* **assert property(@clk a);*


>
>

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.