Boolean Functional Operators

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

Any 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.


In this example, let's compute the Shannon cofactors and apply the Shannon expansion to derive various representations.

  1. Compute the Shannon cofactor with respect to x for .

  2. Rewrite function in the generalized Reed-Muller form. A Reed-Muller form is an XOR sum of cubes, in which each variable is either a positive phase or a negative phase.

    1. The cofactors for are computed as follows:

      Therefore, according to Theorem 7.5, or

    2. Apply the XOR version of the Shannon expansion to successively until it is in Reed-Muller form. First apply it to variable x. We get

      Now let g be , and cofactor with respect to y. We obtain the required Reed-Muller form:

      You should verify that this Reed-Muller form is indeed functionally identical to the given function.

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.


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 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

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 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,

  1. Show that function f can be expressed as

  2. In a finite-state machine whose next-state function is given by , where a and b are input bits, and r and s are present state bits. (s, r), find an expression for all present states whose next state can be either (1, 0) or (0, 1) under some input.

    1. Let's start with the XOR version of the Shannon expansion theorem.

    2. Let's formulate the problem using the existential operator. The question in English is to find all present states such that for some input (a, b), the output of the next-state function is either (1, 0) or (0, 1). Translating it into a mathematical expression, we get

      Evaluating each cofactor gives

      Therefore, the set of present states that can be driven to 10 or 01 by an input in one cycle is , which represents present states (s, r) = {(1,0), (1,1), (0,0)}.

      Let us check our result. If the present state is (1,0), the next state is , which becomes (1, 0) if input a is 1 or b is 0. If the present state is (1,1), the next state is , which is (1,0) if a = b = 0, or is (0,1) if b = 1. Finally, if the present state is (0, 0), the next state is (a, 0), which is (1,0) if a = 1. The expression states that if the present state is (0,1), no input can drive it to (1,0) or (0,1) in one cycle. Suppose the present state is (0,1), the next state is always (0,0), as expected.

     Python   SQL   Java   php   Perl 
     game development   web development   internet   *nix   graphics   hardware 
     telecommunications   C++ 
     Flash   Active Directory   Windows