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.
|