A Pipelined Multi-core MIPS Machine [electronic resource] : Hardware Implementation and Correctness Proof / by Mikhail Kovalev, Silvia M. Müller, Wolfgang J. Paul.

Introduction -- Motivation -- Overview -- Number Formats and Boolean Algebra -- Basics -- Numbers, Sets and Logical Connectives -- Sequences and Bit-Strings -- Modulo Computation -- Geometric Sums -- Binary Numbers -- Two's Complement Numbers -- Boolean Algebra -- Identities -- Solving Equations -- Disjunctive Normal Form -- Hardware -- Digital Gates and Circuits -- Some Basic Circuits -- Clocked Circuits -- Digital Clocked Circuits -- The Detailed Hardware Model -- Timing Analysis -- Registers -- Drivers and Main Memory -- Open Collector Drivers and Active Low Signal -- Tristate Drivers and Bus Contention -- The Incomplete Digital Model for Drivers -- Self Destructing Hardware -- Clean Operation of Tristate Buses -- Specification of Main Memory -- Operation of Main Memory via a Tristate Bus -- Finite State Transducers -- Realization of Moore Automata -- Precomputing Outputs of Moore Automata -- Realization of Mealy Automata -- Precomputing Outputs of Mealy Automata -- Nine Shades of RAM -- Basic Random Access Memory -- Single-Port RAM Designs -- Read Only Memory (ROM) -- Multi-bank RAM -- Cache State RAM -- SPR RAM -- Multi-port RAM Designs -- 3-port RAM for General Purpose Registers -- General 2-port RAM -- 2-port Multi-bank RAM-ROM -- 2-port Cache State RAM -- Arithmetic Circuits -- Adder and Incrementer -- Arithmetic Unit -- Arithmetic Logic Unit (ALU) -- Shift Unit -- Branch Condition Evaluation Unit -- A Basic Sequential MIPS Machine -- Tables -- I-type -- R-type -- J-type -- MIPS ISA -- Configuration and Instruction Fields -- Instruction Decoding -- ALU-Operations -- Shift Unit Operations -- Branch and Jump -- Sequences of Consecutive Memory Bytes -- Loads and Stores -- ISA Summary -- A Sequential Processor Design -- Software Conditions -- Hardware Configurations and Computations -- Memory Embedding -- Defining Correctness for the Processor Design -- Stages of Instruction Execution -- Initialization -- Instruction Fetch -- Instruction Decoder -- Reading from General Purpose Registers -- Next PC Environment -- ALU Environment -- Shift Unit Environment -- Jump and Link -- Collecting Results -- Effective Address -- Shift for Store Environment -- Memory Stage -- Shifter for Load -- Writing to the General Purpose Register File -- Pipelining.-MIPS ISA and Basic Implementation Revisited -- Delayed PC -- Implementing the Delayed PC -- Pipeline Stages and Visible Registers -- Basic Pipelined Processor Design -- Transforming the Sequential Design -- Scheduling Functions -- Use of Invisible Registers -- Software Condition SC-1 -- Correctness Statement -- Correctness Proof of the Basic Pipelined Design -- Forwarding -- Hits -- Forwarding Circuits -- Software Condition SC-2 -- Scheduling Functions Revisited -- Correctness Proof -- Stalling Stall Engine -- Hazard Signals -- Correctness Statement -- Scheduling Functions -- Correctness Proof -- Liveness -- Caches and Shared Memory -- Concrete and Abstract Caches -- Abstract Caches and Cache Coherence -- Direct Mapped Caches -- k-way Associative Caches -- Fully Associative Caches -- Notation -- Parameters -- Memory and Memory Systems -- Accesses and Access Sequences -- Sequential Memory Semantics -- Sequentially Consistent Memory Systems -- Memory System Hardware Configurations -- Atomic MOESI Protocol -- Invariants -- Defining the Protocol by Tables -- Translating the Tables into Switching Functions -- Algebraic Specification -- Properties of the Atomic Protocol -- Gate Level Design of a Shared Memory System -- Specification of Interfaces -- Data Paths of Caches -- Cache Protocol Automata -- Automata Transitions and Control Signals -- Bus Arbiter -- Initialization -- Correctness Proof -- Arbitration -- Silent Slaves and Silent Masters -- Automata Synchronization -- Control of Tristate Drivers -- Protocol Data Transmission -- Data Transmission -- Accesses of the Hardware Computation -- Relation with the Atomic Protocol -- Ordering Hardware Accesses Sequentially -- Sequential Consistency -- Liveness -- A Multi-core Processor -- Compare-and-Swap Instruction -- Introducing CAS to the ISA -- Introducing CAS to the Sequential Processor -- Multi-core ISA and Reference Implementation -- Multi-core ISA Specification -- Sequential Reference Implementation -- Simulation Relation -- Local Configurations and Computations -- Accesses of the Reference Computation -- Shared Memory in the Multi-core System -- Notation -- Invisible Registers and Hazard Signals -- Connecting Interfaces -- Stability of Inputs of Accesses -- Relating Update Enable Signals and Ends of Accesses -- Scheduling Functions -- Stepping Function -- Correctness Proof -- Liveness -- References -- Index.