Re: [sv-ac] clock on disable iff condition

[John] If a clock flows into the disable iff expression, then to
which subexpressions of the disable iff expression does the clock apply
and is there a way to make this intuitive to the user? In order to be
able to represent asynchronous resets, I think that the clock should not
apply to subexpressions that are not sampled value functions. But then
this rule is not really consistent with the body of the assertion.

[Ben] The clock flow should not apply to the disable iff. I don't know
where it says that in the LRM, but it should.
Thus, we can allow a default clocking to apply for the definition of an end
point, regardless of where it is applied if that sequence does not have an
explicit clocking event. Below is an example.
module dis;
  logic clk=1, rst=0, a=1, b=1, c=0;
  *default clocking default_clk @ (posedge clk); endclocking*
  sequence q_rst_default; rst; endsequence : q_rst_default

  property P;
   @ (posedge clk)
     disable iff(rst) // clock does not flow into the disable iff, async
reset
     a |=> ##2 b;
  endproperty : P
  ap_P: assert property(P);

  sequence q_rst; @ (negedge clk) rst; endsequence : q_rst
  property P2;
   @ (posedge clk)
     disable iff(q_rst.triggered) // reset at posedge when end point ==1
     a |=> ##2 b;
  endproperty : P2
  ap_P2: assert property(P2);

 * property P3; *
* @ (posedge clk) // clock does not flow into disable iff *
* disable iff(q_rst_default.triggered) // default clocking used *
* a |=> ##2 b; *
* endproperty : P3 *
* ap_P3: assert property(P3);*

  initial forever #10 clk=!clk;

  initial begin
@ (posedge clk);
    #3 rst=1;
  end
 endmodule : dis

On Tue, Jul 27, 2010 at 10:36 AM, Havlicek John-R8AAAU <r8aaau@freescale.com
> wrote:

> Hi Dana:
>
> A question that I was not able to ask in today's meeting is the
> following: If a clock flows into the disable iff expression, then to
> which subexpressions of the disable iff expression does the clock apply
> and is there a way to make this intuitive to the user? In order to be
> able to represent asynchronous resets, I think that the clock should not
> apply to subexpressions that are not sampled value functions. But then
> this rule is not really consistent with the body of the assertion.
>
> J.H.
>
>
>
> --
> This message has been scanned for viruses and
> dangerous content by MailScanner, and is
> believed to be clean.
>
>
>

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