Jan. 14, 2011, 7:08 a.m.
posted by nfrank
Boolean Functional OperatorsIn 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 f_{x} and respectively. Cofactor f_{x} is computed by setting variable x to 1, whereas is computed by setting x to 0. Therefore, f_{x} and are functions without variable x. Functions f_{x} and can be further cofactored with respect to other variables. For example, cofactoring with respect to variable y gives (f_{x})_{y}, which is written as f_{xy}. It can be shown that f_{xy} = f_{yx}. Function f is related to its cofactors through the following Shannon theorem (Theorem 7.5). Theorem 7.5. Shannon Expansion TheoremAny Boolean function f can be expressed in the following forms, where x is a variable of f: 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. 11.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 f_{c} is cube. The generalized cofactor function of a vector Boolean function f, f_{g}, allows g to be any Boolean function and is defined as
where * denotes a don'tcare value. It is tempting to assume that f_{g} is equal to fg, which gives f when g = 1. The following exercise shows that they are not the same. 12.Express the generalized cofactor function using a characteristic function. From the definition, the characteristic function is
where variable y is the value of the cofactor, and x_{1} through x_{n} 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'tcare), 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 f_{g}, 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'tcare, 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 stuckat fault at node x, the decision procedure is equivalent to determining whether there is an input vector v such that
where f is the function of the circuit with the fault site x made as a primary input. 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 f_{m}(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, 13.

 Comment