Checkers in Formal Verification - SVA: The Power of Assertions in SystemVerilog - page 530

23.4.3 Rigid and Free Variables Versus Local Variables

Rigid variables are typically used for latching: they effectively store a value at the
beginning of a transaction, and then check it at the transaction end, as shown in
Example 23.29 . This usage is also common for local variables. The advantage of
rigid variables is their straightforward implementation in FV, while not all assertions
with local variables are supported by FV tools. On the contrary, local variables
have full support in simulation, while the rigid variable support is rather poor. Both
assertion implementations look very similar.

It is recommended to use local variables rather than rigid variables, unless
there is a restriction on local variables imposed by an FV tool.

Efficiency Tip. Rigid variables are expensive in FV, but they are significantly less
expensive than the free variables of the same size. When rigid variables may be used
interchangeably with local variables, the efficiency of the rigid variables and of the
local variables in FV is about the same, provided that the FV tool can handle local
variables efficiently.
Sometimes it is possible to achieve the same goal by using local variables instead
of free variables. As opposed to rigid variables, here we are talking about free
variables of a smaller size than corresponding local variables. For instance, the
checker described in Example 23.18 can be implemented as an assertion with local
variables, as discussed in Exercise 23.3 , but in this case one-bit free variable start
would be replaced by local variables of a larger size. Both approaches have their
own advantages and drawbacks:

￿ Processing of unconstrained free variables is straightforward for FV tools.
Although free variables impose a heavy burden on FV, they are efficiently
synthesized. Sophisticated assertions with local variables may be difficult to
synthesize, and their synthesis may introduce substantial penalty in addition to
the penalty introduced by free variables.
￿ If an abstract model requires complex modeling, it is difficult to keep assertions
with local variables of manageable size. Some modularity may be achieved by
partitioning complex properties into subproperties. Splitting these assertions into
several smaller assertions is problematic, since different assertions cannot share
their local variables, and one will have to duplicate many common parts of
the modeling in different assertions. On the contrary, when using free variables
the modeling can be shared.
￿ For manageable models, using local variables is more intuitive and readable than
using free variables.
￿ Local variables can easily be checked in simulation, whereas free variables have
only partial simulation support.