Re: [sv-ac] Checker instantiation in always procedures

From: ben cohen <hdlcohen_at_.....>
Date: Wed Jul 15 2009 - 15:01:20 PDT
I submitted a mantis on this issue.  I hope that Neil will approve the
change.  If, because of scheduling or other issue, this change cannot be
made at this time, I would like to see this committee tune this mantis
(i.e., agree to it or improve it) so that at least tool vendors will have a
guideline to base their tools on (on this issue).
Ben
 0002810 <http://www.eda-stds.org/svdb/view.php?id=2810> ClarificationSV-AC
minor new 2009-07-15 Checker instantiation in an always or initial procedure
Change in 17.5 *FROM*: An always procedure in a checker body may contain
deferred and concurrent assertions, nonblocking variable assignments (see
17.7.1) and a procedural timing control statement using an event control.
All other statements shall not appear inside an always procedure. *TO*: An
always or *an initial procedure* in a checker body may contain deferred and
concurrent assertions, nonblocking variable assignments (see 17.7.1), *a
checker instantiation,* and a procedural timing control statement using an
event control. All other statements shall not appear inside an always
procedure. *Rationale*: It was always the intent to be able to instantiate
in an always or initial procedure checkers. LRM makes no mention of the
initial procedure. In fact, section 17.3 supports this premise: “A checker
may be instantiated wherever a concurrent assertion may appear (see 16.15)
with the following exceptions: it shall be illegal to instantiate checkers
in fork...join, fork...join_any, or fork...join_none blocks. “ Since
concurrent assertions can be instantiated in an always or initial procedure,
and always procedures are allowed in checkers, then the above LRM statement
implies that a checker can be instantiated in an always procedure of another
checker.

On Wed, Jul 15, 2009 at 10:45 AM, Korchemny, Dmitry <
dmitry.korchemny@intel.com> wrote:

>  Hi Ben,
>
>
>
> I think, your second question has been answered by Shalom. As for the first
> one, it depends on the vendor. From a contradictory statement it is possible
> to infer everythingJ. Usually an explicit example is a better argument
> than an abstract statement.
>
>
>
> Regards,
>
> Dmitry
>
>
>
> *From:* ben cohen [mailto:hdlcohen@gmail.com]
> *Sent:* Tuesday, July 14, 2009 6:32 PM
>
> *To:* Korchemny, Dmitry
> *Cc:* sv-ac@server.eda.org
> *Subject:* Re: [sv-ac] Checker instantiation in always procedures
>
>
>
>  Dmitry,
>
> Agree that it should be revisited in the future.  The question I have
> though right now is:
>
> *What should a tool vendor implement?  He could implement what is in
> 17.3.2 *
>
> *"However, a checker shall be evaluated statically or procedurally
> depending on its placement in the parent checker".*
>
> Specifically, as shown in (a modification to what is in 17.3.2)
>
> *checker *c3(event clk, logic a);  p3: assert property (@clk
> a); endchecker
>
> *checker *c2(event clk, logic a);
>
>   c3 c3_stat(clk, a);
>
>   *always *@(clk) begin
>
>     c3 c3_proc(clk, a); // LEGAL if c2 is instantiated as below
>
>   *end*
>
> *endchecker*
>
>
>
> *module *m2(logic clk, logic [3:0] d);**
>
>   *always *@(*posedge *clk) begin**
>
>   c2 check_d1(posedge clk, d[1]);  // OK here ? **
>
> *  end*
>
> *endmodule *: m2**
>
> * *
>
> On a separate issue, in current LRM, 17.3.2 shows the following.  Where is
> "in1"  declared?  Don't we mean "posedge clk" instead? **
>
> module m2(logic clk, logic [3:0] d);
>
>   always @(posedge clk) begin
>
>     for (int i = 0; i < 4; i++) begin
>
> *      c2 check_loop(in1, d [const'(i)]);*
>
>    end
>
>   end
>
> endmodule : m2
>
> Ben Cohen
>
>
>
> On Tue, Jul 14, 2009 at 7:45 AM, Korchemny, Dmitry <
> dmitry.korchemny@intel.com> wrote:
>
> Hi all,
>
>
>
> In 17.5 Checker procedures it is written:
>
>
>
> An *always *procedure in a checker body may contain deferred and
> concurrent assertions, nonblocking variable
>
> assignments (see 17.7.1) and a procedural timing control statement using
> an event control. All other
>
> statements shall not appear inside an *always *procedure.
>
>
>
> From here I understand that a checker cannot be instantiated in an always
> procedure of another checker.
>
>
>
> Nevertheless, 17.3.2 Nested checker instantiations explicitly discusses
> what happens if one checker is instantiated in another checker.
>
>
>
> It looks to be a contradiction that should be fixed (in the future).
>
>
>
> What do you think?
>
>
>
> 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.
>
>
>
> ---------------------------------------------------------------------
> 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.
Received on Wed Jul 15 15:04:17 2009

This archive was generated by hypermail 2.1.8 : Wed Jul 15 2009 - 15:05:29 PDT