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, and is
believed to be clean.