A The following illustration is a schematic diagram for a digital circuit called a Click on
x, y, z to toggle their values.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 The sentences shown below express the behavior of the five gates in the circuit shown above. Node
Once we have done this, we can use our formalization to analyze the circuit - to
As an example, suppose we know that
As an example, suppose we want to find values for
Of course, to be meaningful, we need to be sure that the inputs are consistent. If we were to choose The The purpose of a full-adder is to do one slice of binary addition. Given two input bits (
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. 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
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 To do this, we use our logical tools to derive conclusions written in terms of
A common assumption in hardware diagnosis is that at most one component is failing. This is often called the 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. x, ¬y, z, s, ¬c} ∪ Σ |= ¬x1
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 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
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 ∧ y ∧ z ∧ s ∧ ¬c ⇒ x111
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 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 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 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 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 |