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

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]
Sent: Wednesday, July 28, 2010 12:41 PM
To: Surrendra Dudani
Cc: Tapan Kapoor; Havlicek John-R8AAAU; Dana Fisman; 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> 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] 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> 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] On Behalf Of ben
cohen
Sent: Tuesday, July 27, 2010 11:58 PM
To: Havlicek John-R8AAAU
Cc: Dana Fisman; 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> 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.