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.