A pipelined multi-core MIPS machine. Hardware implementation and correctness proof (Q481104)

Proponents of software verification hold up complete end-to-end verification, from hardware, through ISA, assembly, programming language, operating system, to application, as a tenable, but yet unrealized, goal. This monograph contributes the crucial first link in this chain, viz., the first complete (but not yet formally verified) ``correctness proof for both the gate level implementation of a multi-core processor and of a cache-based sequentially consistent shared memory''. This book is a welcome contribution to the increasingly important field of verified multi-core hardware.