Re: [sv-ac] RE: New version of 3213 uploaded

Dmitry,
I rephrased the question with a model.
*module* m3213;
 *logic* clk=0, request=1'b1, go=1;
 initial forever #10 clk=!clk;
 *sequence* req_seq;
   @ (posedge clk) request;
 *endsequence*
 ap_qst0: *assert property*(@ (*posedge* clk) *$stable*( request ) |-> go;
 chk chk1(req_seq, go, *posedge* clk);
endmodule : m3213

*checker* chk((*sequence* req_seq, *logic* go, *event* ev);
  *let* req = req_seq.triggered;
  ap_qst1: assert property(@ (ev) $stable( req ) |-> go;
  *// Questions: In which region is $stable(req)*
* // (or $stable(req_seq.triggered) ) evaluated in the assertion? *
* // req_seq.triggered and the assertion are evaluated in the Observed
region. *
* *
*// [3213] A value change function detects a change (or, in the case of
$stable,*
*// lack of change) in the sampled value of an expression. The change (or
lack of change) *
*// is determined by comparing the sampled value of the expression with the
sampled *
*// value of the expression from the Postponed region of the most recent
strictly *
*// prior time step in which the clocking event occurred.*
* *
*// [Ben] So when is the sampled value of req_seq.triggered?*
*// [Korchemny, Dmitry] Its sampled value is its current value. It depends
where you call it.*
*
*
// [Ben_2] Consider *ap_qst0, that assertion will be true at every cycle.*
//* Consider ap_qst1, we have "$stable(req_seq.triggered". what is it's
value?*
//* Will ap_qst1 always be vacuous? *
// Since this is an assertion, I can reason that the expression *
req_seq.triggered* is
// evaluated in the* Prepone region, and thus will always be 0*
// Am I correct on this?
endchecker : chk
Ben Cohen

On Mon, May 23, 2011 at 6:50 AM, Korchemny, Dmitry <
dmitry.korchemny@intel.com> wrote:

> Hi Ben,
>
>
>
> Please, see below.
>
>
>
> Thanks,
>
> Dmitry
>
>
>
> *From:* ben cohen [mailto:hdlcohen@gmail.com]
> *Sent:* Monday, May 23, 2011 12:27
> *To:* Korchemny, Dmitry
> *Cc:* Eduard Cerny; sv-ac@eda-stds.org
>
> *Subject:* Re: [sv-ac] RE: New version of 3213 uploaded
>
>
>
> Dmitry,
>
> Thinking this problem out, consider your example in a checker:
>
> // Assume that we have this outside the checker
>
> sequence req_seq;
>
> @ (posedge clk) request;
>
> endsequence
>
>
>
> // We then pass to a checker the argument *req_seq*
>
> // In the checker:
>
> let req = req_seq.triggered;
>
> assert property(@ (posedge clk) $stable( req ) |-> go;
>
>
>
> // Questions: In which region is $stable(req) (or *$stable*(*
> req_seq.triggered*) ) evaluated in the assertion?
>
> // req_seq.triggered and the assertion are evaluated in the
> Observed region.
>
>
>
> [3213] *A value change function detects a change (or, in the case of
> $stable, lack of change) in the sampled value of an expression. The change
> (or lack of change) is determined by comparing the sampled value of the
> expression with the sampled value of the expression from the Postponed
> region of the most recent strictly prior time step in which the clocking
> event occurred.*
>
>
>
> *[Ben] So when is the sampled value of req_seq.triggered?*
>
> *[Korchemny, Dmitry] Its sampled value is its current value. It depends
> where you call it.*
>
> * *
>
> * All in the Observed region? Also, would $stable(request) be the same as
> $stable(req_seq.triggered)?*
>
> *[Korchemny, Dmitry] What is request?*
>
>
>
> *request is sampled @ (posedge clk). *
>
> *req_seq.triggered sampled at ? *
>
> *[Korchemny, Dmitry] at the time it is called.*
>
> *what about **$stable(req_seq.triggered, posedge clk ). *
>
> *[Korchemny, Dmitry] ?*
>
> *If in a checker with an event, wouldn't *
>
> * $stable(req_seq.triggered) be same as *
>
> * $stable(req_seq.triggered, event)? // or the default clocking? *
>
> *[Korchemny, Dmitry] *What is a checker with an event?
>
> *Ben *
>
>
>
>
>
>
>
>
>
> On Mon, May 23, 2011 at 1:10 AM, Korchemny, Dmitry <
> dmitry.korchemny@intel.com> wrote:
>
> Hi Ben,
>
>
>
> I don’t think that $stable(s.triggered) is useful per se, but it is useful
> when you pass it as an argument to a checker, especially when you write a
> library checker. Consider an example when a checker gets a request and a
> grant as its arguments and does some checking. E.g., it may check that the
> request should remain stable during several cycles. The corresponding actual
> argument may be a Boolean or a sequence. Therefore inside a checker we will
> have something similar to:
>
>
>
> let req = req_seq.triggered;
>
>
>
> and later
>
>
>
> assert property (…$stable(req)…);
>
>
>
> Regards,
>
> Dmitry
>
>
>
> *From:* ben cohen [mailto:hdlcohen@gmail.com]
> *Sent:* Friday, May 20, 2011 06:47
> *To:* Eduard Cerny
> *Cc:* Korchemny, Dmitry; sv-ac@eda-stds.org
> *Subject:* Re: [sv-ac] RE: New version of 3213 uploaded
>
>
>
> ..16.9.3: $stable(s.triggered) will change value depending whether it is
> called in the active or observed region. Is it not a race between the
> update of s.triggered and the use of it? Should there be a sentence that
> says something about ordering the evaluations?
>
>
>
> Ed,
>
> Good point. What's you're saying can be shown in this example (for
> discussion purposes)
>
> always begin : testcase1
>
> wait (s1.triggerred);
>
> *// Now in Observed region *
>
> x=$stable(s.triggered);
>
> end
>
>
>
> always begin : testcase2
>
> @ (posedge clk)
>
> *// Now in active region *
>
> x=$stable(s.triggered);
>
> end
>
>
>
> LRM changes:
>
> The situation is different when the argument of $stable is s.triggered,
> where s is a named sequence. The sampled value of s.triggered is its current
> value, and $stable(s.triggered) compares the current value of
> $stable(s.triggered)with its value from the Postponed region of the previous
> clock tick.
>
> In testcase, current value ==1
>
> In testcase2, current value==0
>
> Question: Is $stable(s.triggered) useful?
>
> Ben
>
>
>
> *From:* owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] *On Behalf Of *Korchemny,
> Dmitry
> *Sent:* Thursday, May 19, 2011 10:41 AM
> *To:* 'sv-ac@eda-stds.org'
> *Subject:* [sv-ac] New version of 3213 uploaded
>
>
>
> Hi all,
>
>
>
> I uploaded the new version of 3213
> http://www.eda-stds.org/mantis/file_download.php?file_id=5053&type=bugfollowing Scott’s and Anupam’s comments.
>
>
>
> Thanks,
>
> Dmitry
>
> ---------------------------------------------------------------------
> Intel Israel (74) Limited
>
> This e-mail and any attachments may contain confidential material for
> the sole use of the intended recipient(s). Any review or distribution
> by others is strictly prohibited. If you are not the intended
> recipient, please contact the sender and delete all copies.
> --
> 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.
>
>
>
> ---------------------------------------------------------------------
> Intel Israel (74) Limited
>
> This e-mail and any attachments may contain confidential material for
> the sole use of the intended recipient(s). Any review or distribution
> by others is strictly prohibited. If you are not the intended
> recipient, please contact the sender and delete all copies.
>
>
> ---------------------------------------------------------------------
> Intel Israel (74) Limited
>
> This e-mail and any attachments may contain confidential material for
> the sole use of the intended recipient(s). Any review or distribution
> by others is strictly prohibited. If you are not the intended
> recipient, please contact the sender and delete all copies.
>

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.