Formal Verification and Models - SVA: The Power of Assertions in SystemVerilog - page 455

It is possible to represent each state as a Boolean function that has the value 1 in
this state and 0 in all other states. Such a function identifying a single state from 2 V
can be written as a conjunction of literals, one for each variable: if a variable is false
in the state then the corresponding literal is the negation of the variable; otherwise
the corresponding literal is the variable itself. A conjunction of this form is called
a minterm over V . It is easy to see that the minterms over V are in one-to-one
correspondence with the elements of 2 V .

Example 21.9. The states ; ; f i g ; f o g , and f i; o g from Example 21.8 may be repre-
sented by the minterms : i ^: o; i ^: o; : i ^ o, and i ^ o, respectively. t

Boolean functions may also be used to represent sets of states. Given a set
S 2 V , each element of S can be represented symbolically by its corresponding
minterm, and the Boolean function representing S itself is then just the disjunction
of these minterms. This function returns the value 1 on the elements of S and the
value 0 on elements not in S . For this reason, the function is called the characteristic
function of the set S , and it is denoted as S .
Example 21.10. The set of states S Dff o g ; f i; o gg from Example 21.8 has the
characteristic function S D . : i ^ o/ _ .i ^ o/ D o. The empty set has the
characteristic function ; D 0, while the set of all states has the characteristic
function Q D 1. t

The same principle may be applied to symbolically represent transition relations
with their characteristic functions. Recall that the transition relation R is a binary
relation, that is, a set of pairs (sect. 21.1.1 ): R Q Q. To build the characteristic
function of a pair, it is necessary to distinguish between the variables describing
the first state of the pair and those describing the second state. This is achieved by
duplicating the set of variables for the second set and distinguishing the variables
with a prime. We call the original variables current state variables and the primed
variables next state variables . We also expand this notation to variable expressions:
if e is an expression built from the current state variables, then e 0 is the expression
obtained from e by replacing each current state variable by the corresponding next
state variable.
If a pair p 2 R, then p D .c.p/; n.p//. c.p/ is the current state of p, and n.p/
is the next state of p.Let c.p/ and n.p/ be the characteristic functions of c.p/
and n.p/, respectively. Using our convention of primes for next state variables, the
characteristic function of p is c.p/ ^ 0 n.p/

and the characteristic function of the

transition relation R as a whole is
_

c.p/ ^ 0 n.p/ :

p 2 R

Example 21.11. The symbolic representation of the transition relation R from
Example 21.7 ,Fig. 21.3 is