line
csg   
line

Site Contents

Home

Courses

People

Projects

Publications

Seminars

Bluespec Related Publications

A Design Flow Based on Modular Refinement
Nirav Dave, Man Cheuk Ng, Michael Pellauer, Arvind Formal Methods and Models for Codesign (MEMOCODE 2010)
Grenoble, France. June 2010

Debugging Bluespec Designs via Equivalence Checking
Nirav Dave, Michael Katelman
Designing Correct Circuits (DCC 2010)
Paphos, Cyprus. March 2010

Implementing a Fast Matrix Cartesian-Polar Matrix Interpolator
Abhinav Agarwal, Nirav Dave, Kermin Fleming, Asif Khan, Myron King, Man Cheuk Ng, Muralidaran Vijayaraghavan
Formal Methods and Models for Codesign (MEMOCODE 2009)
Cambridge, MA USA. June 2009

802.15.3 Transmitter: A Fast Design Cycle Using the OFDM Framework in Bluespec
Teemu Pitkänen , Vesa-Matti Hartikainen, Nirav Dave, Gopal Raghavan
Lecture Notes in Computer Science, Embedded Computer Systems: Architectures, Modeling, and Simulation
Volume 5114/2008 pp.65-74
International Symposium on Systems, Architectures, Modeling and Simulation (SAMOS 2008)
Samos, Greece. Jul 2008

Hardware Accelleration of Matrix Multiplication on a Xilinx FPGA
Nirav Dave, Kermin Fleming, Myron King, Michael Pellauer, Muralidaran Vijayaraghavan
Formal Methods and Models for Codesign (MEMOCODE 2007)
Nice, France. May 2007

Implementation of a Parallel Language with Guarded Interfaces
Arvind, Nirav Dave, Michael Pellauer
Hardware Design and Functional Languages (HFL 2007)
Braga, Portugal. March 2007

802.11a Transmitter: A Case Study in Michroarchitectural Exploration
Nirav Dave, Michael Pellauer, Steve Gerding, and Arvind
In the proceedings of Formal Methods and Models for Codesign (MEMOCODE'2006) , Napa, CA, July 26-30, 2006

Implementing a Functional/Timing Partitioned Microprocessor Simulator with an FPGA
Nirav Dave, Michael Pellauer, Joel Emer
2nd Workshop on Architecture Research using FPGA Platforms(WARFP 2006)
Austin, Texas, USA. February 2006

Hardware Synthesis from Guarded Atomic Actions with Performanc Specifications
Daniel L. Rosenband and Arvind
In the proceedings of International Conference on Computer Aided Design (ICCAD) - San Jose, CA
Nov. 6-10, 2005

UNUM: A General Microprocessor Framework Using Guarded Atomic Actions
Nirav Dave, Michael Pellauer
1st Workshop on Architecture Research using FPGA Platforms(WARFP 2005)
San Francisco, CA, USA. February 2005


UNUM: A General Microprocessor Framework Using Guarded Atomic Actions
Nirav Dave, Michael Pellauer, Joel Emer
Boston Area Architecture Workshop (BARC 2005)
Providence, RI, USA. January 2005


A Performance Driven Approach for Hardware Synthesis of Guarded Atomic Actions
Daniel L. Rosenband
PhD Thesis, MIT
August, 2005


Automatic Synthesis of Cache-Coherence Protocol Processors Using Bluespec(10 pages)
Nirav Dave, Man Cheuk Ng, Arvind
In the proceedings of Formal Methods and Models for Codesign (MEMOCODE'2005) , Verona, Italy, July 11-14, 2005
Architecture, 2005

Synthesis of Synchronous Assertions with Guarded Atomic Actions
Michael Pellauer, Mieszko Lis, Donald Baltus, Rishiyur Nikhil
In the proceedings of Formal Methods and Models for Codesign (MEMOCODE'2005) , Verona, Italy, July 11-14, 2005
Architecture, 2005


Designing a Processor in Bluespec (67 pages)
Nirav Dave
Masters Thesis, EECS, MIT , January  2005

6.884 - Complex Digital Systems

Spring, 2005 - MIT

Instructors: Professor Arvind and Professor Krste Asanovic

 

Operation-Centric Hardware Descriptions and Synthesis

James Hoe and Arvind,

IEEE TCAD, September 2004.


The Ephemeral History Register: Flexible Scheduling for Rule-Based Designs
Daniel Rosenband
In the proceedings of Formal Methods and Models for Codesign (MEMOCODE'2004) , San Diego, California, June 22-25, 2004


Designing a Reorder Buffer in Bluespec (11 pages)
Nirav Dave
In the proceedings of Formal Methods and Models for Codesign (MEMOCODE'2004) , San Diego , California , June 22-25, 2004

 

Bluespec: Why chip design can't be left to EE's.

Arvind

University of California, Irvine

March 22, 2004


High-level synthesis: An Essential Ingredient for Designing Complex ASICs (10 pages)
Arvind, Nirav Dave, Rishiyur Nikhil, Daniel Rosenband,
In the proceedings of the International Conference on Computer Aided Design (ICCAD 2004), San Jose, California, November 6-10, 2004.

 

Computer Architecture Modeling, Synthesis, and Verification

Arvind, Daniel L. Rosenband, and Jacob B. Schwartz

March, 2003

 


Modular Scheduling of Guarded Atomic Actions (8  pages)
Daniel Rosenband, Arvind
In the proceedings of the 41st Design Automation Conference (DAC),
San Diego, CA, June 2004


Modular scheduling of atomic actions
Daniel L. Rosenband, Jacob B. Schwartz, Arvind
September, 2003

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

Proofs of Correctness of Cache-Coherence Protocols (29 pages)
Joseph Stoy, Xiaowei Shen, Arvind
In Proceedings of the Formal Methods Europe: Formal Methods for Increasing Software Productivity,
Berlin, Germany, March 2001. (LNCS 2001)


Scheduling and Synthesis of Operation-Centric Hardware Descriptions (10 pages)
James C. Hoe, Arvind
 In proceedings of ICCAD-2000 (International Conference on ComputerAided Design, pages 511--518. IEEE/ACM, 2000), San Jose , CA , November 2000.

Operation-Centric Hardware Description and Synthesis

James Hoe, PhD Thesis

June 2000

 

Design and Verification of Adaptive Cache Coherence Protocols
Xiaowei Shen

Doctoral Dissertation, EECS, MIT,  February 2000


Deriving Superscalar Microarchitectures from Pipelined Microarchitectures
James C. Hoe, Arvind
November, 1999


Hardware Synthesis from Term Rewriting Systems (27 pages)
James C. Hoe, Arvind
In proceedings of VLSI'99
Lisbon , Portugal , December 1999


Using Term Rewriting Systems to Design and Verify Processors (17 pages)
Arvind, Xiaowei Shen
In IEEE Micro Special Issue on Modeling and Validation of Microprocessors, May, 1999


CACHET: An Adaptive Cache Coherence Protocol for Distributed Shared-Memory Systems (14 pages)
Xiaowei Shen, Arvind, Larry Rudolph
In proceedings of the 13th ACM SIGARCH International Conference on Supercomputing,
Rhodes , Greece . June 1999


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


A TRS Model for a Modern Microprocessor (14 pages)
Lisa Poyneer, James C. Hoe, Arvind
Jun, 1998

Design and Verification of Speculative Processors (20 pages)
Xiaowei Shen, Arvind
In Proceedings of the Workshop on Formal Techniques for Hardware and Hardware-like Systems Architecture,
Marstrand, Sweden, June 1998


Modeling and Verification of ISA Implementations (14 pages)
Xiaowei Shen, Arvind
In Proceedings of the Australasian Computer Architecture Conference,
Perth , Australia Architecture,  February 1998,


A Methodology for Designing Correct Cache Coherence for DSM Systems (39 pages)
Xiaowei Shen, Arvind , March 1998


An Adaptive Cache Coherence Protocol That Implements Sequential Consistency for DSM Systems with Multi-level Caches
Arvind, Xiaowei Shen
December 1997


Specification of Memory Models and Design of Provably Correct Cache Coherence Protocols(39 pages)
Xiaowei Shen, Arvind
January,  1997


James Hoe papers link.


Bluespec papers link.


For more publications, click here.



line


C S A I L
Computer Science and Artificial Intelligence Laboratory
Massachusetts Institute of Technology
32 Vassar Street, 32-G846
Cambridge, MA 02139
v: 617.253.6837, f: 617.253.6652


Copyright © 2003 by Massachusetts Institute of Technology. All rights reserved.