• Mikhail Kovalev
  • Silvia M. Müller
  • Wolfgang J. Paul
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9000)


Building on [12] and [6], we present at the gate level the construction of a multi-core MIPS machine with “basic” pipelined processors and prove that it works. “Basic” means that the processors only implement the part of the instruction set architecture (ISA) that is visible in user mode; we call it ISA-u. Extending it to the full architecture ISA-sp, that is visible in system programmers mode, we would have to add among other things the following mechanisms: i) local and inter processor interrupts, ii) store buffers, and iii) memory management units (MMUs). We plan to do this as future work. In Sect. 1.1 we present reasons why we think the results might be of interest. In Sect. 1.2 we give a short overview of the book.


Formal Verification Cache Line Proof Obligation Correctness Proof Shared Memory System 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Mikhail Kovalev
    • 1
  • Silvia M. Müller
    • 2
  • Wolfgang J. Paul
    • 3
  1. 1.Sirrix AGSaarbrückenGermany
  2. 2.IBM Germany Research and Development GmbHBöblingenGermany
  3. 3.Saarland UniversitySaarbrückenGermany

Personalised recommendations