Extend the vocabulary from
Section circuits-section to define addition for $n$-bit
binary numbers. Then encode the description of the four-bit adder in
Figure 4bit-adder-figure, and pose the queries needed
to verify that it is in fact correct.
A four-bit adder. Each ${Ad}_i$ is a one-bit adder, as in figure adder-figure on page <a href=""#">adder-figure</a>
Extend the vocabulary from
Section circuits-section to define addition for $n$-bit
binary numbers. Then encode the description of the four-bit adder in
Figure 4bit-adder-figure, and pose the queries needed
to verify that it is in fact correct.
A four-bit adder. Each ${Ad}_i$ is a one-bit adder, as in figure adder-figure on page adder-figure
