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

mutex: assume final (rst || $onehot0({read, write}))
else $error("read/write contention");
Or alternately as a concurrent assumption

mutex: assume property (@( posedge clk) disable iff (rst)
$onehot0({read, write})) else $error("read/write contention");
This assumption reads that at all times signals read and write are mutually
exclusive, that is, they cannot have value 1 simultaneously. To express this, we use
the system function $onehot0 (Sect. 7.1.1 ) returning true when at most one bit of a
vector is 1.
Assumptions are an important part of a design specification. Although we illus-
trated a design specification in Sect. 1.2.1 ,Fig. 1.6 only with assertions, a real design
specification should have assumptions as well. Assumptions are also important for
ABV, as they document the conditions that guarantee proper functioning of the
module. It is difficult to underestimate the importance of assumptions in system
integration: if each module clearly specifies its interface, most integration errors are
discovered early as assumption violations.

4.5.2 Assumption Definition

The goal of assumptions is to constrain a system behavior . A system is composed
of the DUT (model) and its environment (see Sect. 4.1 ,Fig. 4.1 ). The system
behavior may be constrained either by constraining the DUT or by constraining
its environment. If the DUT is deterministic, as normally happens when it is
implemented in RTL, 7 there is not much sense in constraining its behavior.
Therefore, assumptions are used to constrain the behavior of the environment.
Assertions and assumptions play dual roles—assertions specify the behavior of the
DUT and assumptions specify the behavior of its environment.
Syntactically assumptions are similar to assertions, but they use the keyword
assume instead of assert .

assumption ::= name : assume_keyword ( assumption_body ) action_block

Similar to assertions, assumptions may be immediate (keyword assume ), deferred
(keyword assume #0 and assume final ), and concurrent (keyword

assume property ).

Immediate Assumptions. Figure 4.14 shows a typical example of an immediate
assumption:

7 In this section, we limit our discussion to deterministic models; study of nondeterministic models
is postponed to Chap. 23 .