[sv-bc] Problems addressed by the checker proposal

Hi all,

 

I had an action item at the last meeting to list the features addressed
by the checker proposal. Here they are:

 

*	Be able to package several assertions statements (assertions,
assumptions, cover) together along with the modeling code to create a
library checker. Think about a typical OVL checker as an example. This
feature is gating for the ABV methodology.
	Why the existing SV constructs are not sufficient for this
purpose?

	*	Using a single assertion as a library checker is not
always sufficient

		*	In many cases coverage collection is required
along with the assertions.
		*	A library checker may contain several
assertions, and the number of enabled assertions may vary according to
the values of the library checker arguments/parameters.
		*	Also many library checkers are not pure
assertions, but have auxiliary modeling code to support their
assertions.

	*	Using a module/interface to package a library checker
code has many problems. This is how OVL is implemented.

		*	Modules cannot get sequences/properties as their
arguments/parameters
		*	Modules have different syntax for ports and
parameters
		*	Modules cannot be instantiated inside procedural
code
		*	Modules instantiation is not context sensitive:
they keep no information about clocks, resets and enabling conditions in
their instantiation context
		*	Modules are synthesized into silicon. The
library checkers should not be synthesized into silicon (of course, they
may if wanted, but this should not be done automatically). To prevent
library checker synthesis into silicon different ad hoc solutions are
used. These solutions are not standard. Also, though library checkers
are not usually synthesized into silicon, but they are synthesized for
formal verification and for HW acceleration.
		*	Module argument types are fixed, while library
checkers are used in different contexts - 2 and 4-value arguments,
different bit vector length, etc. To make modules generic, explicit
parameterization has to be used. This leads to clumsy syntax and to poor
readability.

*	Provide support for assertion and formal verification modeling.
This includes ability to represent the transition relation. to build
abstract, and possibly nondeterministic models. These requirements are
addressed mostly by introducing checker variables, that may be
considered as an independent feature (see the note below), but checkers
as such are also important here, since the abstract models have to be
modular, and using modules is problematic for this purpose, because
modules cannot get sequences and properties as their arguments, and we
also have a synthesis issue here.

 

The question was raised whether the checker variables (including free
variables) are an independent feature, or should they be allowed in the
checker context only. The quick answer is that the checker variables do
not require the checker construct and can be defined for modules,
interfaces, etc as well, and the issue is mostly methodological here. On
the other hand, checker variables are necessary for checkers, and using
regular SV RTL modeling in checkers would be problematic and race-prone
because of the checker instantiation semantics, and therefore they are
an integral part of the checker.

 

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