Author Topic: (book) Pipelined Multi-core MIPS, Implementation and Correctness  (Read 5576 times)

0 Members and 1 Guest are viewing this topic.

Offline DiTBhoTopic starter

  • Super Contributor
  • ***
  • Posts: 4436
  • Country: gb
  • A Pipelined Multi-core MIPS Machine: Hardware Implementation and Correctness Proof (Theoretical Computer Science and General Issues) 2014th Edition
    by Mikhail Kovalev (Author), Silvia M. Müller (Author), Wolfgang J. Paul (Author)
See here, on Amaozn dot com

Not yet bought, it sounds *very* interesting  :o :o :o
The opposite of courage is not cowardice, it is conformity. Even a dead fish can go with the flow
 

Offline rstofer

  • Super Contributor
  • ***
  • Posts: 9972
  • Country: us
Re: (book) Pipelined Multi-core MIPS, Implementation and Correctness
« Reply #1 on: August 02, 2024, 01:57:44 pm »
Bought it!  It should be an interesting read and perhaps it might be fun to synthesize on an FPGA.

Thanks for pointing it out!
 
The following users thanked this post: DiTBho

Offline ZaneKaminski

  • Contributor
  • Posts: 34
  • Country: us
Re: (book) Pipelined Multi-core MIPS, Implementation and Correctness
« Reply #2 on: August 09, 2024, 10:18:46 am »
Quite interested as well. If only formal proof was the currently accepted verification methodology and there were tools, etc. around it, then maybe we would be spending a lot less effort in verification. Very tempted to buy but it's a bit pricey and there is probably still a lot of work required to verify a real design in the way the title suggests
 

Offline DiTBhoTopic starter

  • Super Contributor
  • ***
  • Posts: 4436
  • Country: gb
Re: (book) Pipelined Multi-core MIPS, Implementation and Correctness
« Reply #3 on: August 11, 2024, 03:39:42 pm »
Quite interested as well. If only formal proof was the currently accepted verification methodology and there were tools, etc. around it, then maybe we would be spending a lot less effort in verification. Very tempted to buy but it's a bit pricey and there is probably still a lot of work required to verify a real design in the way the title suggests

I have the same doubts: a bit pricey, will it say something really useful, and therefore worth it, or will it just be an educational but sterile reading on a practical level?

Who knows ...  :-//

I designed and implemented  a toy-ISA, which has nothing interesting except for the C-like compiler I wrote, as it facilitates the machine level.
Now I am adding multi-processing and I need a way to validate things better, or rather, to spend less time than I have used so far.

The implementation I made has been carried forward and tested rigorously for modules, so, specific test-bench-units for each ALU circuit, COP0, COP1, load/store, register file (which has particular properties), etc.

Finally, the system integration test-benches.

I need to spend less effort in verification, so probably a better verification methodology.
The opposite of courage is not cowardice, it is conformity. Even a dead fish can go with the flow
 

Offline DiTBhoTopic starter

  • Super Contributor
  • ***
  • Posts: 4436
  • Country: gb
Re: (book) Pipelined Multi-core MIPS, Implementation and Correctness
« Reply #4 on: December 04, 2024, 01:33:24 pm »
Bought it!  It should be an interesting read and perhaps it might be fun to synthesize on an FPGA.

Thanks for pointing it out!

any comment about the book?  :D
The opposite of courage is not cowardice, it is conformity. Even a dead fish can go with the flow
 

Offline kk2009

  • Newbie
  • Posts: 1
  • Country: us
Re: (book) Pipelined Multi-core MIPS, Implementation and Correctness
« Reply #5 on: December 04, 2024, 07:56:09 pm »
I recommend this book. As you know, now RISC-V is more attracitve......

https://www.amazon.com/Digital-Design-Computer-Architecture-RISC-V/dp/0128200642
 

Offline radiogeek381

  • Regular Contributor
  • *
  • Posts: 133
  • Country: us
    • SoDaRadio
Re: (book) Pipelined Multi-core MIPS, Implementation and Correctness
« Reply #6 on: December 14, 2024, 04:22:01 pm »
I've designed a multi-core MIPS SOC (with a team) around the R5KF, a clean slate MIPS core, and worked on Alpha and VAX implementations.

I am not sure how the authors could have "proven" correctness. Are they claiming to have proven correctness of the MIPS implementation?  Given that MIPS and SGI never actually produced a formal definition of the ISA (at least not prior to 2007 when I last worked on a MIPS) the definition of "correct" would be hard to discern. MIPS had an architectural validation suite of programs, but it was by no means exhaustive -- there are just too many cross-products, especially when we add in interrupts, faults, and traps.

Alternatively, they may have proven equivalence between two different representations -- say a high level behavioral model and the logic design.

Can anybody who read the book comment?
 
The following users thanked this post: pardo-bsso


Share me

Digg  Facebook  SlashDot  Delicious  Technorati  Twitter  Google  Yahoo
Smf