Assertion Statements - SVA: The Power of Assertions in SystemVerilog - page 84

4.5.3.2 Assumptions in Formal Verification

Any specific DUT behavior may be described by a corresponding signal trace, a
sequence of all DUT signal values in time. This is what we see in simulation if we
request the dump of all DUT signals. 8
In FV, assumptions are used to constrain the set of legal traces of a DUT,
that is, the assumptions are not checked in FV. The role of assumptions and
assertions in FV is absolutely different: assertion satisfaction is checked provided
that all assumptions hold .
Thus, in the example from Sect. 4.5.1 , assumption mutex is used to keep
only those traces where read and write are not 1 at the same time. Assertion
stable_when_write holds for those traces, while it fails without this mutex
constraint.

4.5.3.3 Assumptions in Random Simulation

In the case where randomization is done only in the environment, for example, using
constraint solving SystemVerilog Testbench (SVTB), there is no difference between
random and deterministic simulation as far as checking assumptions is concerned.
However, when the DUT input stimuli are generated directly, the assumptions in
random simulation may act as constraints. Therefore, the role of assumptions in
random simulation is similar to their role in FV—to limit the legal traces of DUT.
But if in FV we consider all legal traces simultaneously, in random simulation we
generate only one legal trace.
Tools may eventually provide means for constraining simulations using assump-
tions, but it involves several difficult issues to be resolved and may imply some
restrictions on the form of the assumptions. See also the discussion on free variables
and assumptions in checkers used in random simulation in Sect. 23.3 .
A distribution operator dist in SystemVerilog can be used in assumptions for
tuning them for random simulation. It is best to explain its usage on the following
example.
The assumption

m1: assume property (@clk a dist {1 := 2, 3 := 1, 4 := 5});
means that a may only get values 1, 3, or 4. If this assumption is used as a constraint
in a random testbench, the specified weights, or frequencies are taken into account.
In our example, a assumes values 1, 3, and 4 with the respective weights of 2, 1,
and 5.
If the distribution weight is omitted, 1 is assumed by default.

8 In simulation all traces are, of course, finite. In FV, we can also consider infinite traces. This is
discussed in Chap. 21 .