Solution

ID: past-exam-of-the-year-1-of-the-computer-science-course-of-the-university-of-oxford/2018/digital-systems-linear-algebra-introduction-to-formal-proof/1/d/solution

Use four-variable Karnaugh maps with rows and columns , both in Gray code order. A dash denotes an unused present state. The maps for the three next-state bits are
For , join its sole one with the dash directly below it. For , use the four-cell groups and , and the two-cell group ; the last group wraps between the top and bottom rows. For , join the one at row , column to the dash below it; the one at row , column is isolated. These prime implicants give
Here products mean Boolean conjunction and sums mean Boolean disjunction. The inputs are the desired next-state bits of the three D flip-flops. The equations are independent of the unused values except for the explicitly chosen Karnaugh map groups.

New to topics? Read the docs here!