Digital Circuits

Now let's consider the use of Propositional Logic in modeling a portion of the physical world, in this case, a digital circuit like the ones used in building computers.

The diagram below is a pictorial representation of such a circuit. There are three input nodes, some internal nodes, and two output nodes. There are five gates connecting these nodes to each other - two xor gates (the gates on the top), two and gates (the gates on the lower left), and one or gate (the gate on the lower right).

At a given point in time, a node in a circuit can be either on or off. The input nodes are set from outside the circuit. A gate sets its output either on or off based on the type of gate and the values of its input nodes. The output of an and gate is on if and only if both of its inputs are on. The value of an or node is on if and only if at least one of its inputs is on. The output of an xor gate is on if and only if its inputs disagree with each other.

Given the Boolean nature of signals on nodes and the deterministic character of gates, it is quite natural to model digital circuits in Propositional Logic. We can represent each node of a circuit as a proposition constant, with the idea that the node is on if and only if the constant is true. Using the language of Propositional Logic, we can capture the behavior of gates by writing sentences relating the values of the inputs nodes and out nodes of the gates.

The sentences shown below capture the five gates in the circuit shown above. Node o must be on if and only if nodes p and q disagree.

Once we have done this, we can use our formalization to analyze the circuit - to determine if it meets it specification, to test whether a particular instance is operating correctly, and to diagnose the problem in cases here it is not. In the remainder of this chapter, we describe some methods that facilitate this sort of analysis.