RE: [sv-ac] checker: why are parameters not allowed? Need to file a mantis?

Hi Ben,

I think that having many different ways to express the same thing may be misleading, but this issue is mostly religious :).

Regards,
Dmitry

From: Ben Cohen [mailto:hdlcohen@gmail.com]
Sent: Thursday, May 24, 2012 07:41
To: Korchemny, Dmitry
Cc: sv-ac@eda-stds.org; Eduard Cerny
Subject: Re: [sv-ac] checker: why are parameters not allowed? Need to file a mantis?

Dmitry, the topic is all about the use model,or application, of the checkers in the verification environment. In some applications, like the one you showed, one may want to build a library of checkers. In other applications, I can see the declaration of checkers in a package, or just within a verification unit. However, there are other applications where a checker is defined a la module style, and that checker is bound to a DUT. There, parameters would be useful because they mirror a structure familiar to SV engineers.
Why not using a module instead of a checker? One main reason I see is the access to free variables, and that allows for the definition of assertions in a style not allowed in modules. For example, local variables of a property do not flow across the "implies" operator, but I believe that we could use the rand const in formal to get that variable conceptually flow across.

Bottom line, parameters are clearly constants, whereas inputs are not. Using inputs for ranges is not explicitly clear that the actual is a constant. Adding parameters in the next PAR would be optional (just like parameters in modules) and we could still use inputs to pass constants. It would not hurt.
Ben Cohen
On Wed, May 23, 2012 at 5:04 AM, Korchemny, Dmitry <dmitry.korchemny@intel.com<mailto:dmitry.korchemny@intel.com>> wrote:
Hi Ben,

This mantis already exists, see http://www.eda-twiki.org/svdb/view.php?id=2111.

However, IMO there is little added value in introducing parameters to checkers. Checker invocation should be similar to a property's syntax, and not to a module's.

Say, you want to check that a request will be granted in n cycles. Then it is very natural to write it like this:

// invocation
request_granted rg1(req, gnt, 4, clk);

checker request_granted(request, grant, n, event clk);
                a: assert property (@clk request |-> ##n grant);
endchecker

Rather than to use this ugly syntax:
request_granted #(4) rg1 (req, gnt, clk);

checker request_granted #(n) (request, grant, event clk);
                a: assert property (@clk request |-> ##n grant);
endchecker

What is a benefit of introducing parameters for checkers in your opinion? Do you have a specific example?

Thanks,
Dmitry

From: Ben Cohen [mailto:hdlcohen@gmail.com<mailto:hdlcohen@gmail.com>]
Sent: Tuesday, May 22, 2012 22:12
To: sv-ac@eda-stds.org<mailto:sv-ac@eda-stds.org>; Korchemny, Dmitry; Eduard Cerny
Subject: [sv-ac] checker: why are parameters not allowed? Need tofile a mantis?

Dmitry,
Why are parameters not allowed in checkers, in the same style as module?
If we do allow them, would that bring more consistency in design style, and possibly simplify the design of tools because of this parallelism to modules?
Before I file a mantis for future exploration of this, I would like to hear your comments.
Thanks,
Ben
---------------------------------------------------------------------
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.