Muutke küpsiste eelistusi

Pipelined Multi-core MIPS Machine: Hardware Implementation and Correctness Proof 2014 ed. [Pehme köide]

, ,
  • Formaat: Paperback / softback, 352 pages, kõrgus x laius: 235x155 mm, kaal: 5504 g, 147 Illustrations, black and white; XII, 352 p. 147 illus., 1 Paperback / softback
  • Sari: Lecture Notes in Computer Science 9000
  • Ilmumisaeg: 01-Dec-2014
  • Kirjastus: Springer International Publishing AG
  • ISBN-10: 3319139053
  • ISBN-13: 9783319139050
Teised raamatud teemal:
  • Pehme köide
  • Hind: 48,70 €*
  • * hind on lõplik, st. muud allahindlused enam ei rakendu
  • Tavahind: 57,29 €
  • Säästad 15%
  • Raamatu kohalejõudmiseks kirjastusest kulub orienteeruvalt 2-4 nädalat
  • Kogus:
  • Lisa ostukorvi
  • Tasuta tarne
  • Tellimisaeg 2-4 nädalat
  • Lisa soovinimekirja
Pipelined Multi-core MIPS Machine: Hardware Implementation and Correctness Proof 2014 ed.Suurem pilt
  • Formaat: Paperback / softback, 352 pages, kõrgus x laius: 235x155 mm, kaal: 5504 g, 147 Illustrations, black and white; XII, 352 p. 147 illus., 1 Paperback / softback
  • Sari: Lecture Notes in Computer Science 9000
  • Ilmumisaeg: 01-Dec-2014
  • Kirjastus: Springer International Publishing AG
  • ISBN-10: 3319139053
  • ISBN-13: 9783319139050
Teised raamatud teemal:
Püsilink: https://www.kriso.ee/db/9783319139050.html
Märksõnad:
This monograph is based on the third author's lectures on computer architecture, given in the summer semester 2013 at Saarland University, Germany. It contains a gate level construction of a multi-core machine with pipelined MIPS processor cores and a sequentially consistent shared memory.

The book contains the first correctness proofs for both the gate level implementation of a multi-core processor and also of a cache based sequentially consistent shared memory. This opens the way to the formal verification of synthesizable hardware for multi-core processors in the future.

Constructions are in a gate level hardware model and thus deterministic. In contrast the reference models against which correctness is shown are nondeterministic. The development of the additional machinery for these proofs and the correctness proof of the shared memory at the gate level are the main technical contributions of this work.
1 Introduction
1(6)
1.1 Motivation
1(4)
1.2 Overview
5(2)
2 Number Formats and Boolean Algebra
7(22)
2.1 Basics
8(4)
2.1.1 Numbers, Sets, and Logical Connectives
8(1)
2.1.2 Sequences and Bit-Strings
9(3)
2.2 Modulo Computation
12(2)
2.3 Geometric Sums
14(1)
2.4 Binary Numbers
15(3)
2.5 Two's Complement Numbers
18(2)
2.6 Boolean Algebra
20(9)
2.6.1 Identities
23(2)
2.6.2 Solving Equations
25(1)
2.6.3 Disjunctive Normal Form
26(3)
3 Hardware
29(54)
3.1 Digital Gates and Circuits
30(3)
3.2 Some Basic Circuits
33(8)
3.3 Clocked Circuits
41(13)
3.3.1 Digital Clocked Circuits
41(3)
3.3.2 The Detailed Hardware Model
44(5)
3.3.3 Timing Analysis
49(5)
3.4 Registers
54(1)
3.5 Drivers and Main Memory
54(21)
3.5.1 Open Collector Drivers and Active Low Signal
55(1)
3.5.2 Tristate Drivers and Bus Contention
56(4)
3.5.3 The Incomplete Digital Model for Drivers
60(1)
3.5.4 Self Destructing Hardware
61(3)
3.5.5 Clean Operation of Tristate Buses
64(5)
3.5.6 Specification of Main Memory
69(3)
3.5.7 Operation of Main Memory via a Tristate Bus
72(3)
3.6 Finite State Transducers
75(8)
3.6.1 Realization of Moore Automata
76(2)
3.6.2 Precomputing Outputs of Moore Automata
78(2)
3.6.3 Realization of Mealy Automata
80(1)
3.6.4 Precomputing Outputs of Mealy Automata
81(2)
4 Nine Shades of RAM
83(16)
4.1 Basic Random Access Memory
83(2)
4.2 Single-Port RAM Designs
85(7)
4.2.1 Read Only Memory (ROM)
85(1)
4.2.2 Multi-bank RAM
86(3)
4.2.3 Cache State RAM
89(1)
4.2.4 SPR RAM
90(2)
4.3 Multi-port RAM Designs
92(7)
4.3.1 3-port RAM for General Purpose Registers
92(2)
4.3.2 General 2-port RAM
94(1)
4.3.3 2-port Multi-bank RAM-ROM
95(2)
4.3.4 2-port Cache State RAM
97(2)
5 Arithmetic Circuits
99(18)
5.1 Adder and Incrementer
99(2)
5.2 Arithmetic Unit
101(5)
5.3 Arithmetic Logic Unit (ALU)
106(2)
5.4 Shift Unit
108(5)
5.5 Branch Condition Evaluation Unit
113(4)
6 A Basic Sequential MIPS Machine
117(44)
6.1 Tables
118(2)
6.1.1 I-type
118(1)
6.1.2 R-type
119(1)
6.1.3 J-type
119(1)
6.2 MIPS ISA
120(13)
6.2.1 Configuration and Instruction Fields
120(3)
6.2.2 Instruction Decoding
123(1)
6.2.3 ALU-Operations
124(2)
6.2.4 Shift Unit Operations
126(1)
6.2.5 Branch and Jump
127(2)
6.2.6 Sequences of Consecutive Memory Bytes
129(1)
6.2.7 Loads and Stores
130(2)
6.2.8 ISA Summary
132(1)
6.3 A Sequential Processor Design
133(28)
6.3.1 Software Conditions
133(1)
6.3.2 Hardware Configurations and Computations
134(1)
6.3.3 Memory Embedding
135(3)
6.3.4 Defining Correctness for the Processor Design
138(2)
6.3.5 Stages of Instruction Execution
140(1)
6.3.6 Initialization
141(1)
6.3.7 Instruction Fetch
142(1)
6.3.8 Instruction Decoder
143(4)
6.3.9 Reading from General Purpose Registers
147(1)
6.3.10 Next PC Environment
147(3)
6.3.11 ALU Environment
150(1)
6.3.12 Shift Unit Environment
151(1)
6.3.13 Jump and Link
152(1)
6.3.14 Collecting Results
153(1)
6.3.15 Effective Address
153(1)
6.3.16 Shift for Store Environment
154(2)
6.3.17 Memory Stage
156(2)
6.3.18 Shifter for Load
158(1)
6.3.19 Writing to the General Purpose Register File
159(2)
7 Pipelining
161(46)
7.1 MIPS ISA and Basic Implementation Revisited
162(5)
7.1.1 Delayed PC
162(1)
7.1.2 Implementing the Delayed PC
163(1)
7.1.3 Pipeline Stages and Visible Registers
164(3)
7.2 Basic Pipelined Processor Design
167(23)
7.2.1 Transforming the Sequential Design
167(5)
7.2.2 Scheduling Functions
172(3)
7.2.3 Use of Invisible Registers
175(1)
7.2.4 Software Condition SC-1
176(1)
7.2.5 Correctness Statement
177(1)
7.2.6 Correctness Proof of the Basic Pipelined Design
178(12)
7.3 Forwarding
190(6)
7.3.1 Hits
190(1)
7.3.2 Forwarding Circuits
190(1)
7.3.3 Software Condition SC-2
191(1)
7.3.4 Scheduling Functions Revisited
192(1)
7.3.5 Correctness Proof
193(3)
7.4 Stalling
196(11)
7.4.1 Stall Engine
196(1)
7.4.2 Hazard Signals
197(1)
7.4.3 Correctness Statement
198(1)
7.4.4 Scheduling Functions
198(5)
7.4.5 Correctness Proof
203(2)
7.4.6 Liveness
205(2)
8 Caches and Shared Memory
207(104)
8.1 Concrete and Abstract Caches
209(10)
8.1.1 Abstract Caches and Cache Coherence
210(2)
8.1.2 Direct Mapped Caches
212(2)
8.1.3 k-way Associative Caches
214(2)
8.1.4 Fully Associative Caches
216(3)
8.2 Notation
219(5)
8.2.1 Parameters
219(1)
8.2.2 Memory and Memory Systems
219(1)
8.2.3 Accesses and Access Sequences
220(1)
8.2.4 Sequential Memory Semantics
221(1)
8.2.5 Sequentially Consistent Memory Systems
222(1)
8.2.6 Memory System Hardware Configurations
223(1)
8.3 Atomic MOESI Protocol
224(11)
8.3.1 Invariants
224(2)
8.3.2 Defining the Protocol by Tables
226(2)
8.3.3 Translating the Tables into Switching Functions
228(2)
8.3.4 Algebraic Specification
230(4)
8.3.5 Properties of the Atomic Protocol
234(1)
8.4 Gate Level Design of a Shared Memory System
235(26)
8.4.1 Specification of Interfaces
236(4)
8.4.2 Data Paths of Caches
240(7)
8.4.3 Cache Protocol Automata
247(2)
8.4.4 Automata Transitions and Control Signals
249(8)
8.4.5 Bus Arbiter
257(3)
8.4.6 Initialization
260(1)
8.5 Correctness Proof
261(50)
8.5.1 Arbitration
261(2)
8.5.2 Silent Slaves and Silent Masters
263(1)
8.5.3 Automata Synchronization
264(5)
8.5.4 Control of Tristate Drivers
269(5)
8.5.5 Protocol Data Transmission
274(3)
8.5.6 Data Transmission
277(2)
8.5.7 Accesses of the Hardware Computation
279(22)
8.5.8 Relation with the Atomic Protocol
301(4)
8.5.9 Ordering Hardware Accesses Sequentially
305(3)
8.5.10 Sequential Consistency
308(2)
8.5.11 Liveness
310(1)
9 A Multi-core Processor
311(34)
9.1 Compare-and-Swap Instruction
312(5)
9.1.1 Introducing CAS to the ISA
312(1)
9.1.2 Introducing CAS to the Sequential Processor
313(4)
9.2 Multi-core ISA and Reference Implementation
317(9)
9.2.1 Multi-core ISA Specification
317(1)
9.2.2 Sequential Reference Implementation
318(3)
9.2.3 Simulation Relation
321(2)
9.2.4 Local Configurations and Computations
323(2)
9.2.5 Accesses of the Reference Computation
325(1)
9.3 Shared Memory in the Multi-core System
326(19)
9.3.1 Notation
326(1)
9.3.2 Invisible Registers and Hazard Signals
327(2)
9.3.3 Connecting Interfaces
329(1)
9.3.4 Stability of Inputs of Accesses
330(1)
9.3.5 Relating Update Enable Signals and Ends of Accesses
331(3)
9.3.6 Scheduling Functions
334(1)
9.3.7 Stepping Function
334(2)
9.3.8 Correctness Proof
336(5)
9.3.9 Liveness
341(4)
References 345(2)
Index 347