Basic Properties - SVA: The Power of Assertions in SystemVerilog - page 91

Chapter 5
Basic Properties
Where there is no property there is no injustice.
— John Locke
Properties play a central role in SVA because they form the bodies of concurrent
assertions. A property is a temporal formula that can be either true or false on a given
trace. 1 As explained in Sect. 4.5.3 , by trace we understand a series of all DUT signal
values in time. Properties are interpreted over traces. In this chapter, we assume that
each point on the trace corresponds to a tick of the clock on which the property
is evaluated. This definition will not work for multiply clocked properties, but we
currently limit our consideration to singly clocked properties only. The more general
case is described in Chaps. 12 , 13 , and 22 . Also, in formal verification (FV) we
may assume that all the traces are infinite, which corresponds to the case when the
property clock ticks infinitely many times. Of course, simulation traces are always
finite. We informally describe the property semantics here, and defer the formal
semantics of properties until Chap. 22 .
This chapter is one of the central chapters of the topic, and a good grasp of the
material described here will be instrumental in understanding the rest of the topic
and in writing basic temporal assertions. Its contents are addressed both to users of
simulation and to users of FV. FV issues are always commented so that the reader
interested in only assertion simulation can skip them. However, we would like to
stress that understanding FV issues may provide a deeper insight into the nature of
temporal assertions, even for those who are not planning to use FV.
1 An exception is disabled status of a property when the disable iff operator is used. See
Sect. 13.1.1 .