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

Hi Ben,
Just a clarification, the default clocking does not apply to property/sequence declarations, but only to the instances where they are used in assertions (Except in the case where a sequence/property is defined in a clocking block which is declared as default clocking)
Surrendra

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of ben cohen
Sent: Wednesday, July 28, 2010 8:56 AM
To: Tapan Kapoor
Cc: Havlicek John-R8AAAU; Dana Fisman; sv-ac@eda.org
Subject: Re: [sv-ac] clock on disable iff condition

My point is that I don't see a confusion issue in using a default clocking on an unclocked sequence as shown in my example for P3
 default clocking default_clk @ (posedge clk); endclocking
  sequence q_rst_default; rst; endsequence : q_rst_default
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

On 7/28/10, Tapan Kapoor <tkapoor@cadence.com<mailto:tkapoor@cadence.com>> wrote:
[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.

Section 16.14.3 / page 389 says "The scope of a clocking event does not flow into the disable condition of disable iff."

Warm regards,
Tapan
"You must be the change you want to see in the world" : Mahatma Gandhi
From: owner-sv-ac@eda.org<mailto:owner-sv-ac@eda.org> [mailto:owner-sv-ac@eda.org<mailto:owner-sv-ac@eda.org>] On Behalf Of ben cohen
Sent: Tuesday, July 27, 2010 11:58 PM
To: Havlicek John-R8AAAU
Cc: Dana Fisman; sv-ac@eda.org<mailto:sv-ac@eda.org>
Subject: 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<mailto: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<http://www.mailscanner.info/>, and is
believed to be clean.
--
This message has been scanned for viruses and
dangerous content by MailScanner<http://www.mailscanner.info/>, and is
believed to be clean.
-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.