About Us Technology Products Partnerships And Affiliations News and Events Support
 
Challenge
Technology Overview
Other Approaches

Key Selections of Research

 

University Courses

• MIT Course: 6.375 - Complex Digital Systems

• MIT Course: 6.827 - Multithreaded Parallelism: Languages and Compilers

• MIT Course: 6.884 - Complex Digital Systems   (MIT OpenCourseWare version)


• CMU Course: 18-744 - Hardware Systems Engineering

• LUND University Course: EDA385 - Embedded System Design

 

Applications of Bluespec

• Nirav Dave, Man Cheuk Ng, Arvind. “Automatic Synthesis of Cache-Coherence Protocol Processors Using Bluespec”, Formal Methods and Models for Codesign (MEMOCODE'2005), Verona, Italy, July 11-14, 2005.


• Nirav Dave. “Designing a Processor in Bluespec” – MS Thesis, January 2005.

• Arvind, Rishiyur S. Nikhil, Daniel Rosenband, Nirav Dave. “High-Level Synthesis: An Essential Ingredient for Designing Complex ASICs”, International Conference on Computer Aided Design (ICCAD 2004), San Jose, CA, November 6-10, 2004.

• Roland E. Wunderlich, James C. Hoe. “In-System FPGA Prototyping of an Itanium Microarchitecture”, International Conference on Computer Aided Design (ICCAD), October 2004.

• Nirav Dave. “Designing a Reorder Buffer in Bluespec”, MIT Computer Science and Artificial Intelligence Lab, International Conference on Formal Methods and Models for Codesign (MEMOCODE 2004), San Diego, CA, June 22-25, 2004.

• Rishiyur S. Nikhil. “Future Programming of FPGAs”, FPGA 2004 Panel, February 23, 2004.

• Arvind. “Why Chip Design Can’t Be Left to EEs”, MIT Computer Science and Artificial Intelligence Lab, 2004.

• Joydeep Ray, James C. Hoe. “High-Level Modeling and FPGA Prototyping of Microprocessors”, International Symposium on Field Programmable Gate Arrays (FPGA), February 2003.


• Joseph Stoy, Arvind, Xiaowei Shen. “Proofs of Correctness of
Cache-Coherence Protocols”, Formal Methods for Increasing Software Productivity, International Symposium of Formal Methods Europe (FME 2001) Springer-Verlag Lecture Notes in Computer Science 2021, pp. 43-71, Berlin, Germany, March 12-16, 2001.

• Xiaowei Shen. “Design and Verification of Adaptive Cache Coherence Protocols" – Ph.D. Thesis, MIT Computer Science and Artificial Intelligence Lab, January 2000.

• Arvind, Xiaowei Shen. “Using Term Rewriting Systems to Design and Verify Processors”, IEEE Micro, 19:3, pp 36-46, May 1999.

• Lisa Poyneer, James C. Hoe, Arvind. “A TRS Model for a Modern Microprocessor”, MIT Computer Science and Artificial Intelligence Lab, June 1998.

 

Core Technology

• Michael Pellauer, Massachusetts Institute of Technology, Mieszko Lis, Don Baltus, and Rishiyur Nikhil, Bluespec. “Synthesis of Synchronous Assertions with Guarded Atomic Actions”, Formal Methods and Models for Codesign (MEMOCODE'2005), Verona, Italy, July 11-14, 2005.

• James C. Hoe, Arvind. “Operation-Centric Hardware Description and Synthesis”, IEEE TRANSACTIONS on Computer-Aided Design of Integrated Circuits and Systems, Volume 23, Issue 9, September 2004.

• Grace Nordin, James C. Hoe. “Synchronous Extensions to Operation-Centric Hardware Description Languages”, International Conference on Formal Methods and Models for Codesign (MEMOCODE), San Diego, CA, June 22-25, 2004.

• Daniel Rosenbrand. “The Ephemeral History Register: Flexible Scheduling for Rule-Based Designs”, MIT Computer Science and Artificial Intelligence Lab, International Conference on Formal Methods and Models for Codesign (MEMOCODE 2004), San Diego, CA, June 22-25, 2004.

• Daniel Rosenband, Arvind. “Modular Scheduling of Guarded Atomic Actions”, 41st Design Automation Conference (DAC), San Diego, CA, June 2004.

• Arvind, Daniel Rosenband, Jacob Schwartz. “Modular Scheduling of Atomic Actions”, MIT Computer Science and Artificial Intelligence Lab, April 2004.

• Arvind. “Bluespec: A Language for hardware design, simulation, synthesis and verification”, Extended Abstract, Proceedings of MEMOCODE, ACM, June 2003.


• Arvind, Daniel Rosenband, Jacob Schwartz. “Computer Architecture Modeling, Synthesis, and Verification”, MIT Computer Science and Artificial Intelligence Lab, March 2003.

• James C. Hoe, Arvind. “Synthesis of Operation-Centric Hardware Descriptions”, International Conference on Computer Aided Design (ICCAD), San Jose, California, November 2000.

• James C. Hoe. “Operation-Centric Hardware Description and Synthesis”, PhD Thesis, MIT, June 2000.

• James C. Hoe, Arvind. “Hardware Synthesis from Term Rewriting Systems”, IFIP International Conference on VLSI, December 1999.

• Xiaowei Shen, Arvind, Larry Rudolph. “CACHET: An Adaptive Cache Coherence Protocol for Distributed Shared-Memory Systems”, Proceedings of the 26th International Symposium on Computer Architecture, Atlanta, Georgia, May 1999.

• Xiaowei Shen, Arvind, Larry Rudolph. “Commit-Reconcile and Fences (CRF): A New Memory Model for Architects and Compiler Writers ”, Proceedings of the 26th International Symposium on Computer Architecture, Atlanta, Georgia, May 1999.

• Xiaowei Shen, Arvind. “Design and Verification of Speculative Processors”, Proceedings of the Workshop on Formal Techniques for Hardware and Hardware-like Systems Architecture, Marstrand, Sweden, June 1998.

• Xiaowei Shen, Arvind. “A Methodology for Designing Correct Cache Coherence for DSM Systems”, MIT Computer Science and Artificial Intelligence Lab, March 1998.

• Xiaowei Shen, Arvind. “Modeling and Verification of ISA Implementations”, Proceedings of the Australasian Computer Architecture Conference, Perth, Australia Architecture, February 1998.

• Xiaowei Shen, Arvind. “An Adaptive Cache Coherence Protocol That Implements Sequential Consistency for DSM Systems with Multi-level Caches”, MIT Computer Science and Artificial Intelligence Lab, December 1997.

• Xiaowei Shen, Arvind. “Specification of Memory Models and Design of Provably Correct Cache Coherence Protocols”, MIT Computer Science and Artificial Intelligence Lab, January 1997.

 

Download Bluespec technical white papers