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

... // sequence of statements 2
v <= expr2;

end
3. Uniformize all conditionals to be of the form if ... else by adding trivial
else begin end to any if statement with no else clause. Further uniformize
so that if v is assigned in a conditional statement, then v is assigned in both the
then and the else clauses. Do this by adding the trivial assignment v<=v; to
any clause where assignment to v is missing but needed.
4. If v is assigned in both clauses of a conditional statement
if (cond) begin
... // sequence of statements 1
v <= expr1;
... // sequence of statements 2

end
else begin
... // sequence of statements 3
v <= expr2;
... // sequence of statements 4

end
extract it out of the scope of the conditional operator as follows:
v <= cond ? expr1 : expr2;
if (cond) begin
... // sequence of statements 1
... // sequence of statements 2

end
else begin
... // sequence of statements 3
... // sequence of statements 4

end
The semantic soundness of this extraction follows from the fact that only NBA
can be written in a checker always_ff , and so the statements preceding the NBA
in the conditional do not affect the value of its RHS.

23.2.2.3 Fully Assigned Free Variables

As we have seen, assignment to a free variable leaves it little freedom: only its
initial value contributes nondeterminism. 6 If we also initialize it, there remains no
freedom introduced by this variable. Such a free variable is said to be fully assigned .
Essentially, there is no difference between a fully assigned free variable and a
regular checker variable.

6 If we assign one free variable to a second free variable, the second one may still be completely
nondeterministic by virtue of the nondeterminism of the first. The point is that a free variable that
is assigned loses its “own” nondeterminism. See also Sect. 23.2.2.4 .