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