A digital circuit is a collection of interconnected digital components called gates. Gates have inputs and outputs. When Boolean signals (on or off) are applied to the inputs of a gate, the circuit produces a corresponding output depending on the type of the gate. The output of an and-gate is on if and only if both inputs are on. The output of an or-gate is on if and only if at least one of the inputs is on. The output of an xor-gate is on if and only if the inputs disagree.

The following illustration is a schematic diagram for a digital circuit called a full adder. There are three input nodes (the boxes labelled x, y, and z), three internal nodes (the boxes labelled a, b, and o), and two output nodes (the boxes labelled s and c). There are two xor-gates (the components at the top), two and-gates (the components on the lower left), and one or-gate (the component on the lower right).

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 a node is on if the constant is true and off if the constant if false. With this convention, we can capture the behavior of gates by writing sentences relating the values of the inputs nodes and the output nodes of the gates.

The sentences shown below express the behavior of the five gates in the circuit shown above. Node o must be on if and only if nodes x and y disagree. Node a must be on if and only if nodes z and o are both on. Node b must be on if and only if nodes x and y are both on. Node s must be on if and only if nodes o and z disagree. Node c must be on if and only if one of the nodes a and b is on. In what follows, we use the symbol Δ to refer to these five sentences.

Once we have done this, we can use our formalization to analyze the circuit - to simulate it, to configure its inputs to achieve desired outputs, to verify that it meets it specification, to diagnose failures in physical instances, and to test whether particular instances are operating correctly.

Simulation is the process of determining the outputs of a circuit for given inputs. To simulate a circuit, we start with the sentences describing the behavior of the gates in the circuit, and we add ground atoms expressing the given input signals (x and y and z). Given these premises, we then derive statements about the outputs (s and c).

As an example, suppose we know that x is on and y is off and z is on, and we want to know whether outputs s and c are on or off. We are asking whether our design Δ together with our input data logically entails s or ¬s and whether it entails c or ¬c. In this case, we have the following results.

Configuration is the opposite of simulation. We start with desired values for the outputs of a circuit and try to find one or more combinations of inputs that produce those outputs. Unlike simulation, there can be multiple answers.

As an example, suppose we want to find values for x and y and z such that output s is on and output c is off. We are trying to find inputs such that Δ together with these inputs logically entails (s ∧ ¬c). In this case, we find three possibilities.

Of course, to be meaningful, we need to be sure that the inputs are consistent. If we were to choose x and ¬x, the conclusion would follow (since an inconsistent set of sentences logically entails everything). However, the inputs would not be realizable.

The specification of a circuit is a characterization of the desired behavior of the circuit under all possible inputs. The design of a circuit is a characterization of its components and connectivity. The specification expresses the circuit's purpose, whereas the design expresses how it is built. Verification is the process of determining whether a circuit's design meets its specification.

The purpose of a full-adder is to do one slice of binary addition. Given two input bits (x and y) and a carry bit from another slice (z), it produces a sum bit (s) and a carry bit (c) to be passed on to the next slice. We can summarize the desired behavior as shown below. We use the symbol Ω to refer to these two sentences.

We can verify a circuit by starting with its design (the sentences we saw earlier) and using them to confirm that each of the sentences in the specification is logically entailed. If so, the circuit is correct. If Δ is the set of sentences comprising our design (the sentences we saw earlier) and if Ω is our specification (the sentences above), we are asking whether our design logically entails our specification.

In our discussion thus far, we have assumed that all of the components in our circuit are behaving correctly. This is not always the case. Sometimes, components fail and as a result they change their behavior. Diagnosis is the process of finding the malfunctioning component(s) in a circuit that are responsible for the observed symptoms.

The sentences in our design are true only if the corresponding components are behaving correctly. We can allow for the possibility of failure by adorning each of our sentences with a condition stating that the corresponding component is working correctly. See below. The first sentence here says that if component on the upper left (named x1) is working correctly, then it behaves like an xor-gate. The other sentences are analogous. In what follows, we refer to these sentences as Δ'.

One advantage of doing things this way is that we can use logical tools to diagnosis hardware failures and to generate tests to see whether an instance of our circuit is working correctly, as described in the following sections.

Suppose that x is on, y is off, and z is on; and suppose that as a result we observe that the sum bit s is on and the carry bit c is off. This is not what we expected. Something must be broken. The good news is that, from this data and the enhanced model of our circuit, we can diagnose the problem.

To do this, we use our logical tools to derive conclusions written in terms of x1, x2, a1, a2, o1 and nothing else. In this case, we can derive the following conclusions. The first conclusion below comes from the erroneous sum bit, and the second comes from the erroneous carry bit.

A common assumption in hardware diagnosis is that at most one component is failing. This is often called the single fault assumption, and it is reasonable in the vast majority of cases. In this case, from our first conclusion, we know that one of x1 or x2 must be broken; and, from our second conclusion, we know that one of x1 and a1 anda2 and o1 must be broken. If we intersect these two sets of possibilities, we see that x1 is the culprit. Of course, more than one component might be bad, but this is relatively rare.

Note that we can express the single fault assumption for our circuit as shown below. In what follows, we use the symbol Σ to refer to these five sentences.

Given out modified design Δ' and our single fault sentences Σ, we can use our logical tools to determine the failing component responsible for our observations.

Test Generation is the process of devising a set of tests to confirm that a physical instance of a circuit is working correctly. If the circuit passes the tests, then we know it is okay. If not, we can diagnose the problem to find the malfunctioning components(s).

In principle, test generation is easy. We can just apply all possible input combinations and, for each combination, check that the circuit produces the correct outputs. This technique is simple and works well for small circuits. However, it is impractical for large circuits because the number of possible input combinations can be very large. For example, a circuit that adds two 64 bit numbers would have 128 inputs, and for this circuit there would be 2¹²⁸ input combinations.

The good news is that it is often possible to guarantee that circuits are working correctly with only a subset of the possible input combinations. The trick to achieving this economy is to exploit the structure of the circuit - we validate each of the components. Assuming the design is correct, this means that the circuit as a whole must work as well.

One practical problem with this approach is that we usually cannot directly set the inputs or directly observe the outputs of every component. In most cases, all we can do is to set the overall inputs of the circuit and observe the overall outputs; and from such tests we must deduce whether or not the internal components are working correctly. Luckily, this is possible much of the time.

As with diagnosis, we start with a modified description of the design. Test generation requires more detail than diagnosis. Instead of saying whether a component is working or not, we must talk about each of the behaviors of each component. Every gate with two inputs has four behaviors - one for each combination of input values. In what follows, we name these four behaviors by appending the input combinations to the name of the component, e.g. the four behaviors of gate x1 are x111, x110, x101, and x100. The following sentences capture the behavior of gate x1 using this vocabulary. In what follows, we use the symbol Δ'' to denote the set of behaviors for all five gates in our circuit.

A gate is working correctly if and only if all of its behaviors are correct. The following sentences capture this definition for our five gates. In what follows, we use the symbol Π to refer to these sentences.

As before, we make the assumption that at most one gate is failing. The sentences Σ work just fine here. Note that a gate may have multiple failing behaviors. However, in making the single fault assumption, we are assuming that all failing behaviors are confined to one gate.

With these preliminaries, we can now address the problem of test generation. Taking our design description Δ'' together with our gate definitions Π and our single fault assumption Σ, we can show which gates are validated when we apply a set of inputs and observe the outputs. For example, we can show that, if we apply inputs x and y and z to the circuit and observe s and ¬c, then we know that x111 behavior is okay.

Continuing in this fashion, we can show the behaviors validated by other input combinations together with their corresponding outputs. We can validate each of these cases by taking the appropriate sentences from Δ'' and Π and Σ, building a truth table with those sentences as premises, and noticing that, whenever these premises are true, our conclusion is true.

Looking at these tests, we see that every behavior of every gate appears on the right hand side of at least one test (with the exception of o111). Thus, if the circuit passes all of these tests we know that all behaviors are correct (with the exception of o111). And the exception of o111 does not matter since that behavior is not used in this circuit for any combination of inputs, so it does not matter,

One oddity here is that four of the rules have only four conclusions. For example, the first rule allows us to conclude that all relevant behaviors are okay except for a210. The reason that this case is excluded is that the output of a1 in this case is 1, and hence the output of o1 must be 1 no matter what the output of a2. So, by looking at only the overall outputs in this case, we do not know whether a2 is functioning correctly. There are three other examples of this in the rules as shown.

Our main objective now is to explain why we do not need all of these input combinations to test our circuit. Rather than do this exhaustively, let us consider just one case. If we have the tests 2 and 4, then the first test in this list is unnecessary. To see this, notice that the second test allows us to conclude x111, a111, and o101 and the fourth test gives us a201. Consequently, we can get all of the same results without performing the first test. In similar fashion, we can dispense with the third test.

The upshot is that we can test our full adder completely with just six tests, viz. tests 2, 4, 5, 6, 7, 8. Not much saving here, but for large circuits the savings can be much more dramatic. For example, in the case of the 64 bit adder mentioned earlier, we can get away with fewer than 400 tests instead of 2¹²⁸ tests.

One way to do the sorts of analysis described here is to use truth tables for the propositions in our circuit description. The other approach is to use one of our proof methods. For small circuits, the truth table method is certainly the best approach, while for large circuits symbolic reasoning is more practical. In any case, it is worthwhile to work through the examples shown here. They exemplify many of the concepts of Propositional Logic, and producing the answers in each case is a good way if understanding the different methods for determining logical entailment.

Suggested Exercises. Simulate the circuit for inputs x and y and ¬z. Find all configurations that lead to s and ¬c. Build a truth table with 8 rows; use Δ to compute all outputs; repeat with Ω; and compare. Show that Δ' ∪ {x, ¬y, z, s, ¬c} ∪ Σ |= ¬x1. Show that x ∧ y ∧ z ∧ s ∧ c ⇒ x111. Do all five kinds of analysis for a different circuit.