Jan. 14, 2011, 7:08 a.m.
posted by nfrank
Boolean Functional Operators
In this section, we will study some common operators encountered in formal verification. Cofactor operation on function f with respect to a variable x has two phasesa positive and negative phasedenoted by fx and respectively. Cofactor fx is computed by setting variable x to 1, whereas is computed by setting x to 0. Therefore, fx and are functions without variable x. Functions fx and can be further cofactored with respect to other variables. For example, cofactoring with respect to variable y gives (fx)y, which is written as fxy. It can be shown that fxy = fyx. Function f is related to its cofactors through the following Shannon theorem (Theorem 7.5).
Theorem 7.5. Shannon Expansion Theorem
The Shannon cofactor can be applied successively to all variables in a function. For example, a function with two variables, x and y, can be expressed as
This last equation is a minterm expansion of the function. Because the function has only two variables, the cofactors, , and , are either 1 or 0. Therefore, Shannon expansion can be regarded as a partial evaluation.
In this example, let's compute the Shannon cofactors and apply the Shannon expansion to derive various representations.
This cofactor definition, sometimes called the classic cofactor, is based on a cube; that is, the c in cofactor fc is cube. The generalized cofactor function of a vector Boolean function f, fg, allows g to be any Boolean function and is defined as
where * denotes a don't-care value. It is tempting to assume that fg is equal to fg, which gives f when g = 1. The following exercise shows that they are not the same.
where variable y is the value of the cofactor, and x1 through xn are the variables in f and g. The function is 1 if y has the same value as f when g is 1 or y can be any value (such as don't-care), when g is 0, which is exactly the definition of generalized cofactor.
Let's apply this technique to computing the generalized cofactor and . Using a characteristic function to represent fg, we have
To check, let a = b = c = d = 0. Then, g = 1 and , which means the value of the cofactor is 0, consistent with the value of f because g = 1. Let a = 1 and c = 0. Then g = 0. So the cofactor is a don't-care, meaning the characteristic function should be 1 independent of y. l(y, 1, b, 0, d) = 1, as expected.
The Boolean difference of function f with respect to variable x, , is defined to be
If the Boolean difference of a function with respect to variable x is identically equal to 0, then the function is independent of x, because the cofactors with respect to x are equal, meaning the function remains the same whether x takes on the value of 1 or 0. Therefore, x is in the minimum support of a function if and only if its Boolean difference is not identically equal to 0.
The concept of Boolean difference is used widely in practice. For example, to determine whether a circuit can detect a stuck-at fault at node x, the decision procedure is equivalent to determining whether there is an input vector v such that
The problem of deciding whether a value v exists such that function f(v, w) evaluates to a specific function g(w) is called the existential problem, and is often denoted by the existential operation as vf(v,w)g(w), To compute an existential problem, we simply enumerate all possible values of input v, evaluate the function on each of them, and OR together all outputs. If the result is equal to g(w), then such an input value exists. This procedure of computing existential operation in mathematical form is
where fm(v, w) is a cofactor with respect to minterm m. For instance, if the existential operator is on two variables, x and y, then all minterms are . This summation can be regarded as a Boolean operation for evaluating the existential operation. This operator, called the smooth operator, is
A special case is when the existential operator is on a single variable, say x. Then the equation becomes
The counteroperator of the existential operator is the universal operator. An example of an application of a universal operator is deciding whether function f(v, w) is always equal to some specific function g(w) for all values of v. This is denoted by vf(v,w)g(w). To compute this universal operation, we can evaluate f(v, w) for each of possible values of v and AND the outputs. If the result is g(w), the answer is yes. Mathematically, the computation is
If the function has a single variable x,