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

4.5 Assumptions

We have mentioned the existence and general meaning of assumptions in previous
chapters, here we provide a more detailed examination of assumptions.

4.5.1 Motivation

Figure 4.13 shows a module implementing a simple RAM.
When read is asserted, out is assigned the contents of the memory at address
addr . When write is asserted, data is written at address addr . This module also
contains assertion stable_when_write checking that when write is asserted the
module output out does not change. The system function $stable (Sect. 7.2.1.4 )
returns true when the current value of the signal is identical to its value at the
previous clock tick, and false, otherwise.
It looks like our design should satisfy this assertion, but if you try to formally
verify the model, you will discover that the assertion fails. Why? The answer
may be surprising: when read and write are asserted together, the value of out
may change. But how can it be? We know that read and write cannot be asserted
together, otherwise the design would not function properly. But how should formal
verification tools guess that this input condition is impossible?
As we can see from this example, to make the design work properly its inputs
should be appropriately constrained. These constraints are called assumptions , and
there is a special notation for assumptions in SVA. In our example, the following
assumption is missing:

Fig. 4.13 Simple RAM