rdf-syntax-grammar
mods:
  schema location: http://www.loc.gov/mods/v3 http://www.loc.gov/standards/mods/v3/mods-3-2.xsd
  title info:
    non sort: A
    title: Pipelined Multi-core MIPS Machine
    sub title: Hardware Implementation and Correctness Proof
  name:
    name part: Kovalev, Mikhail.
    role:
      role term: creator
    role:
      role term: author.
  name:
    name part: Müller, Silvia M.
    role:
      role term: author.
  name:
    name part: Paul, Wolfgang J.
    role:
      role term: author.
  name:
    name part: SpringerLink (Online service)
  type of resource: text
  origin info:
    place:
      place term: gw
    date issued: 2014
    issuance: monographic
  language:
    language term: eng
  physical description:
    form: electronic
    form: electronic resource
    reformatting quality: access
    form: remote
    extent: XII, 352 p. 147 illus. online resource.
  abstract: 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.
  table of contents: 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 …
  note: by Mikhail Kovalev, Silvia M. Müller, Wolfgang J. Paul.
  subject:
    topic: Computer science
  subject:
    topic: Computer hardware
  subject:
    topic: Microprocessors
  subject:
    topic: Computer communication systems
  subject:
    topic: Software engineering
  subject:
    topic: Programming languages (Electronic computers)
  subject:
    topic: Algorithms
  subject:
    topic: Computer Science
  subject:
    topic: Algorithm Analysis and Problem Complexity
  subject:
    topic: Software Engineering
  subject:
    topic: Computer Hardware
  subject:
    topic: Processor Architectures
  subject:
    topic: Computer Communication Networks
  subject:
    topic: Programming Languages, Compilers, Interpreters
  classification: QA76.9.A43
  classification: 005.1
  related item:
    title info:
      title: Springer eBooks
  related item:
    title info:
      title: Lecture Notes in Computer Science, 9000
  identifier: 9783319139067
  identifier: http://dx.doi.org/10.1007/978-3-319-13906-7
  record info:
    record creation date: 141124
    record change date: 20151123142153.0
    record identifier: 978-3-319-13906-7