Past exam of the year 1 of the computer science course of the University of Oxford / 2015 / Digital systems, linear algebra, introduction to formal proof (resit) / 3 / b / ii / Solution

A writing MIPS instruction distinguishes a line stuck at zero. With $t0=7, $t1=5, $t2=99, executeA healthy line or a line stuck at one produces $t2=12; a line stuck at zero leaves $t2=99.

To distinguish normal operation from stuck at one, execute a normally nonwriting MIPS instruction. The following functional test uses the usual concrete controller choice MemToReg=0 during sw, selecting the ALU result on the write-data bus. Prepare $t0=37 and $s0=L-16384, for an aligned writable address $L\ne 37$, then executeThe ALU computes $L$. Here rt is register 8 ($t0), and immediate $16384=0x4000$ also puts 8 into bits $15\dots 11$. Thus either value of the otherwise irrelevant RegDst selects $t0. With a healthy RegWrite, $t0 remains 37. With RegWrite stuck at one and the specified write-data selection, the unwanted register file write changes $t0 to $L$. Combining the two independent observations gives

Controller qualification. The source diagram does not specify values of otherwise irrelevant control outputs during a store. MemToReg is a don't-care condition when RegWrite=0; its chosen implementation matters when that enable line is faulty. The functional test above explicitly fixes this convention instead of assuming that all implementations resolve it identically. A manufacturing fixture can also observe the register file write-enable directly while executing add followed by sw: the expected pairs are $(1,0)$ normally, $(0,0)$ stuck at zero, and $(1,1)$ stuck at one. This second observation does not depend on unused write-data controls or on whether an unwanted write happens to repeat an old value.