Motivation For Checkers

Key Motivation: 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.

Related Issues

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.

-- ErikSeligman - 11 Apr 2008