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

Hi Ben,
It expands to
ap_P4c: assert property(
   @(posedge clk1) (rst) |=> a);
Default clocking is not applied.
Surrendra

From: ben cohen [mailto:hdlcohen@gmail.com]
Sent: Thursday, July 29, 2010 12:24 PM
To: Havlicek John-R8AAAU
Cc: Surrendra Dudani; Tapan Kapoor; Dana Fisman; sv-ac@eda.org
Subject: Re: [sv-ac] clock on disable iff condition

OOps , I meant to use the default clocking for the definition of the sequence. Let me rephrase my question
default clocking default_clk @ (negedge clk); endclocking
  sequence q_rst_default; rst; endsequence : q_rst_default
ap_P4 : assert property(@ (posedge clk1) q_rst_default |=> a);
  // expands to
  " ap_P4a : assert property(
        @ (posedge clk1) @ (negedge clk) rst |=> a);"
  // or expands to:
  " ap_P4b : assert property(
        @ (posedge clk1) rst |=> a);"
Essentially, where is the clock flow.
I would lean on not making any changes to the LRM. The other option is to apply an unclocked sequence to the end points (.triggered, .matched).
Apologies for the previous error in my question.
Ben

On Thu, Jul 29, 2010 at 9:07 AM, Havlicek John-R8AAAU <r8aaau@freescale.com<mailto:r8aaau@freescale.com>> wrote:
Hi Ben:

ap_P4 does not expand to either of the options you have shown. It expands to

ap_P4c: assert property(
   @(posedge clk1) (@(negedge clk) rst) |=> a);

Clock flow rules say that this is equivalent to

ap_P4d: assert property(
   @(negedge clk) rst |=> @(posedge clk1) a);

Best regards,

John H.

From: ben cohen [mailto:hdlcohen@gmail.com<mailto:hdlcohen@gmail.com>]
Sent: Wednesday, July 28, 2010 12:41 PM
To: Surrendra Dudani
Cc: Tapan Kapoor; Havlicek John-R8AAAU; Dana Fisman; sv-ac@eda.org<mailto:sv-ac@eda.org>

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

Surrendra,
Agree. After more thoughts, I can a confusion when an unclocked sequence declaration is used in an assertion. For example
 sequence q_rst; @ (negedge clk) rst; endsequence : q_rst
  ap_P4 : assert property(@ (posedge clk1) q_rst_default |=> a);
  // expands to
  " ap_P4a : assert property(
        @ (posedge clk1) @ (negedge clk) rst |=> a);"
  // or expands to:
  " ap_P4b : assert property(
        @ (posedge clk1) rst |=> a);"
Essentially, where is the clock flow.
I would lean on not making any changes to the LRM. The other option is to apply an unclocked sequence to the end points (.triggered, .matched).
Ben

On Wed, Jul 28, 2010 at 6:14 AM, Surrendra Dudani <Surrendra.Dudani@synopsys.com<mailto:Surrendra.Dudani@synopsys.com>> wrote:
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> [mailto: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<mailto: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.