This book presents a formal model for evaluating the cost effectiveness of computer architectures. It is formally proved that the interrupt mechanism proposed for the DLX architecture handles nested interrupts correctly.
In an appendix all programs to compute the cost and cycle time of the designs described are listed in C code.