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.
(p ∧ ¬q) ∨ (¬p ∧ q) ⇔ o
r ∧ o ⇔ a
p ∧ q ⇔ b
(o ∧ ¬r) ∨ (¬o ∧ r) ⇔ s
a ∨ b ⇔ c
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.
