RE: [sv-ac] sv[ac]: checker // if blocking timing and default clock then legal?

Also, I had replied to Ben, but there was a problem with the eda.org mail server at the time.
I wrote,
The LRM says,

"If no clocking event is specified in a procedural concurrent assertion, the leading clocking event of the assertion shall be inferred from the procedural context, if possible. If no clock can be inferred from the procedural context, then the clocks shall be inferred from the default clocking (14.12), as if the assertion were instantiated immediately before the procedure."

According to that, highest priority is given to inferring the clock from the procedural context. If the conditions for that are not fulfilled, then the default clocking is used, if there is one.
and Ben replied,
Thanks Shalom.
The .. " as if the assertion were instantiated immediately before the procedure."
thus just applies to the clock. However, the assertion is still sensitive to the "if" condition in the always procedure.
Regards,
Shalom

________________________________
From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Bresticker, Shalom
Sent: Tuesday, February 02, 2010 1:56 PM
To: sv-ac@server.eda.org
Subject: RE: [sv-ac] sv[ac]: checker // if blocking timing and default clock then legal?

John,

I think what Ben meant is that the clock from an always cannot always be inferred into an assertion.

Shalom

________________________________
From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Neil Korpusik
Sent: Tuesday, February 02, 2010 12:39 AM
To: sv-ac@server.eda.org
Subject: RE: [sv-ac] sv[ac]: checker // if blocking timing and default clock then legal?

<forwarding bounced email from Havlicek John>

-------- Original Message --------
Subject: RE: [sv-ac] sv[ac]: checker // if blocking timing and default clock then legal?
Date: Mon, 1 Feb 2010 13:05:17 -0700
From: "Havlicek John-R8AAAU" <r8aaau@freescale.com><mailto:r8aaau@freescale.com>
To: <ben@systemverilog.us><mailto:ben@systemverilog.us>, <sv-ac@eda.org><mailto:sv-ac@eda.org>
Cc: "Seligman, Erik" <erik.seligman@intel.com><mailto:erik.seligman@intel.com>,
        "Korchemny, Dmitry" <dmitry.korchemny@intel.com><mailto:dmitry.korchemny@intel.com>,
        "Eduard Cerny" <eduard.cerny@synopsys.com><mailto:eduard.cerny@synopsys.com>,
        "Srinivasan Venkataramanan" <svenka3@gmail.com><mailto:svenka3@gmail.com>,
        "lisa_piper" <lisa_piper@systemverilog.us><mailto:lisa_piper@systemverilog.us>

Hi Ben:

I didn't see that anyone replied to this yet.

I don't understand why you say that the LRM says that the clock from an
always cannot be inferred into an assertion. The part of the LRM that
you quote says that it can. I don't think that you grabbed all the
text:

A clock shall be inferred for the context of an always or initial
procedure that satisfies the following requirements:

1) There is no blocking timing control in the procedure.

2) There is exactly one event control in the procedure.

3) Within the event control of the procedure, there is exactly one event
expression that satisfies both of

the following conditions:

a) The event expression is of the form edge_identifier expression1 [ iff
expression2 ] and is not a

proper subexpression of an event expression of this form.

b) No term in expression1 appears anywhere else in the body of the
procedure.

If these requirements are satisfied, then the unique event expression
from the third requirement shall be the clock inferred for the context of the procedure.

Is your concern that clk appears in the body of the procedure? I'm not
sure whether passing clk into your checker instances counts as clk
appearing in the body of the procedure. I don't think this was the
intent of that part of the rule, but the rule is pretty clear as stated.

J.H.

--
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.
-------- Original Message --------
Subject:        [sv-ac] sv[ac]: checker // if blocking timing and default clock then legal?
Date:   Sat, 02 Jan 2010 18:34:21 -0800
From:   ben cohen <hdlcohen@gmail.com><mailto:hdlcohen@gmail.com>
Reply-To:       ben@systemverilog.us<mailto:ben@systemverilog.us>
To:     sv-ac@eda.org<mailto:sv-ac@eda.org>
CC:     Seligman, Erik <erik.seligman@intel.com><mailto:erik.seligman@intel.com>, Korchemny, Dmitry <dmitry.korchemny@intel.com><mailto:dmitry.korchemny@intel.com>, Eduard Cerny <eduard.cerny@synopsys.com><mailto:eduard.cerny@synopsys.com>, Srinivasan Venkataramanan <svenka3@gmail.com><mailto:svenka3@gmail.com>, lisa_piper <lisa_piper@systemverilog.us><mailto:lisa_piper@systemverilog.us>
Question:
LRM 16.15.6 (see below) states that the clock from an always cannot be inferred into an assertion.
What if I have a default clocking ?
What if I use a checker?
Thus, is the following legal?
checker chk_test(logic a, clk);
   default clocking default_clk @ (posedge clk); endclocking
    ap_a: assert property(a);
 endchecker : chk_test
checker chk_test_better(logic a, clk);
    ap_a: assert property(@ (posedge clk) a); // DO I NEED TO BE EXPLICIT ON THE clocking event ??
 endchecker : chk_test_better
module m(logic x, clk);
  logic v, c, w, y;
always @(posedge clk) begin
  v=1;
  if(w) chk_test chk_test_c(c, clk); // checker instantiation // LEGAL?
  if(y) chk_test chk_test_v(v, clk);  // or ILLEGAL because of no clock ?
end
endmodule : m
LRM 16.15.6 Embedding concurrent assertions in procedural code
A clock shall be inferred for the context of an always or initial procedure that satisfies the following requirements:
1) There is no blocking timing control in the procedure.
2) There is exactly one event control in the procedure.
--
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.
--
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.
-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.