Here’s a simple challenge-problem for model-checking Boolean functions: Suppose you want to compute some Boolean function , where represents 0 or more Boolean arguments.

Let , , , range over 2-ary Boolean functions, (of type ), and suppose that is a fixed composition of , , , . (By the way, I’m going to talk about functions, but you can think of these as combinatorial circuits, if you prefer.)

Our question is, “Do there exist instantiations of , , , such that for all inputs, ?

What is interesting to me is that our question is quantified and of the form, “exists a forall b …”, and it is “higher-order” insofar as we want to find whether there exist satisfying functions. That said, the property is easy to encode as a model-checking problem. Here, I’ll encode it into SRI’s Symbolic Analysis Laboratory (SAL) using its BDD engine. (The SAL file in its entirety is here.)

To code the problem in SAL, we’ll first define for convenience a shorthand for the built-in type, `BOOLEAN`:

B: TYPE = BOOLEAN;

And we’ll define an enumerated data type representing the 16 possible 2-ary Boolean functions:

B2ARY: TYPE = { False, Nor, NorNot, NotA, AndNot, NotB, Xor, Nand , And, Eqv, B, NandNot, A, OrNot, Or, True};

Now we need an application function that takes an element `f` from `B2ARY` and two Boolean arguments, and depending on `f`, applies the appropriate 2-ary Boolean function:

app(f: B2ARY, a: B, b: B): B = IF f = False THEN FALSE ELSIF f = Nor THEN NOT (a OR b) ELSIF f = NorNot THEN NOT a AND b ELSIF f = NotA THEN NOT a ELSIF f = AndNot THEN a AND NOT b ELSIF f = NotB THEN NOT b ELSIF f = Xor THEN a XOR b ELSIF f = Nand THEN NOT (a AND b) ELSIF f = And THEN a AND b ELSIF f = Eqv THEN NOT (a XOR b) ELSIF f = B THEN b ELSIF f = NandNot THEN NOT a OR b ELSIF f = A THEN a ELSIF f = OrNot THEN a OR NOT b ELSIF f = Or THEN a OR b ELSE TRUE ENDIF;

Let’s give a concrete definition to `f` and say that it is the composition of five 2-ary Boolean functions, `f0` through `f4`. In the language of SAL:

f(b0: B, b1: B, b2: B, b3: B, b4: B, b5: B): [[B2ARY, B2ARY, B2ARY, B2ARY, B2ARY] -> B] = LAMBDA (f0: B2ARY, f1: B2ARY, f2: B2ARY, f3: B2ARY, f4: B2ARY): app(f0, app(f1, app(f2, b0, app(f3, app(f4, b1, b2), b3)), b4), b5);

Now let’s define the `spec` function that `f` should implement:

spec(b0: B, b1: B, b2: B, b3: B, b4: B, b5: B): B = (b0 AND b1) OR (b2 AND b3) OR (b4 AND b5);

Now, we’ll define a module `m`; modules are SAL’s building blocks for defining state machines. However, in our case, we won’t define an actual state machine since we’re only modeling function composition (or combinatorial circuits). The module has variables corresponding the function inputs, function identifiers, and a Boolean stating whether `f` is equivalent to its specification (we’ll label the classes of variables `INPUT`, `LOCAL`, and `OUTPUT`, to distinguish them, but for our purposes, the distinction doesn’t matter).

m: MODULE = BEGIN INPUT b0, b1, b2, b3, b4, b5 : B LOCAL f0, f1, f2, f3, f4 : B2ARY OUTPUT equiv : B DEFINITION equiv = FORALL (b0: B, b1: B, b2: B, b3: B, b4: B, b5: B): spec(b0, b1, b2, b3, b4, b5) = f(b0, b1, b2, b3, b4, b5)(f0, f1, f2, f3, f4); END;

Notice we’ve universally quantified the free variables in `spec` and the definition of `f`.

Finally, all we have to do is state the following theorem:

instance : THEOREM m |- NOT equiv;

Asking whether `equiv` is false in module `m`. Issuing

$ sal-smc FindingBoole.sal instance

asks SAL’s BDD-based model-checker to solve theorem `instance`. In a couple of seconds, SAL says the theorem is proved. So `spec` can’t be implemented by `f`, for any instantiation of `f0` through `f4`! OK, what about

spec(b0: B, b1: B, b2: B, b3: B, b4: B, b5: B): B = TRUE;

Issuing

$ sal-smc FindingBoole.sal instance

we get a counterexample this time:

f0 = True f1 = NandNot f2 = NorNot f3 = And f4 = Xor

which is an assignment to the function symbols. Obviously, to compute the constant `TRUE`, only the outermost function, `f0`, matters, and as we see, it is defined to be `TRUE`.

By the way, the purpose of defining the enumerated type `B2ARY` should be clear now—if we hadn’t, SAL would just return a mess in which the value of each function `f0` through `f4` is enumerated:

f0(false, false) = true f0(true, false) = true f0(false, true) = true f0(true, true) = true f1(false, false) = true f1(true, false) = true f1(false, true) = false f1(true, true) = true f2(false, false) = false f2(true, false) = true f2(false, true) = false f2(true, true) = false f3(false, false) = false f3(true, false) = false f3(false, true) = false f3(true, true) = true f4(false, false) = false f4(true, false) = true f4(false, true) = true f4(true, true) = false

OK, let’s conclude with one more spec:

spec(b0: B, b1: B, b2: B, b3: B, b4: B, b5: B): B = (NOT (b0 AND ((b1 OR b2) XOR b3)) AND b4) XOR b5;

This is implementable by `f`, and SAL returns

f0 = Eqv f1 = OrNot f2 = And f3 = Eqv f4 = Nor

Although these assignments compute the same function, they differ from those in our specification. Just to double-check, we can ask SAL if they’re equivalent:

spec1(b0: B, b1: B, b2: B, b3: B, b4: B, b5: B): B = ((b0 AND ((NOT (b1 OR b2)) b3)) OR NOT b4) b5;

specifies the assignments returned, and

eq: THEOREM m |- spec(b0, b1, b2, b3, b4, b5) = spec1(b0, b1, b2, b3, b4, b5);

asks if the two specifications are equivalent. They are.

Tags: model checking, SAL

## Leave a Reply