Research Interests

My chief research interest can be summarized as computational optimization. This can be either by-hand or machine-automated techniques, and they are equally, interesting in hardware, software, or elsewhere. However, in general, the more parallel as system the more challenges and solutions are possible, so I tend to focus on hardware.

Certain fundamental problems crop up again and again when trying to optimize: What exactly does a particular algorithm or design mean and more importantly what was actually desired.

From my desire to answer these questions I derive by other research interests: language semantics, design verification, automated proving, and high-performance emulation.


Current Research Projects

These are research projects with which to greater or lesser extent, I am currently affiliated.
  • Bluespec SystemVerilog: Most of the work I do now is phrased in the context of Bluespec SystemVerilog a hardware description language which is based on the underlying semantic model of Guarded Atomic Actions. I believe that this sort of operation-centric representation will provide a natural, modular framework to reason about highly parallel designs, while at the same time raising the level of discourse from signals and wires, to something closer to how architect think. This proides the dual benefit of adding more inherent flexibility and reuse in designs, as well as motiviating the mechanization of a whole swath of optimizations which were previously always forced upon the RTL designers.

  • UNUM: UNUM is a highly generalized, modular, RTL-level multi-processor system written in Bluespec SystemVerilog. The goal of this project is to provide a way to gather low-level charcteristics (area, power, etc.) characteristics of a microarchitectural technique. Because the design is generalized and modular, it is possible to generate a variety of different RTL systems with about the same level of effort as doing the design in a software simulator. Since these designs are in RTL, we expect much more reasonable low-level numbers and may even get execution speedup by use of FPGAs.

    Currently UNUM has a fairly general model of an out-of-order PowerPC design. However, it is on hold while we improve some aspects of our language and compiler.

  • UT FAST:FAST is a very clever simulator (heading by Derek Chiou from University of Texas) much in the style of UNUM, but only concerns itself with modelling the cycle-level performance of a micro-architecture, but promises to be much easier to use.

    At a high-level the goal is to quickly model a microarchitecture to observe it's performance. The simplest solution would be to use a software simulator, but they tend to be far too slow to get reasonable performance AND be fully faithful to the micro-architecture. Functionally all of them, ignore many possibly important micro-architecture occurances (such as the implmentation of the handling of a TLB miss).

    FAST's solution relies on the fact that a micro-architectural simulators can be divided into two partitions to vastly simplify their complexities: a functional model which just takes care of executing the instruction stream correctly, and a timing model which deals with where instructions are in the pipeline and the relative timings. The former is very naturally expressed in software and is relatively simple and the later is easy to represent in hardware (i.e. an FPGA) and is computationally expensive in software. FAST uses these natural implementations as a basis for simulation and is aiming at around a 100-1000x improvement in simulation times.

  • HASim: HASim is project very much in line with UT FAST. It also has a partitioned simulator environment. The main difference is that it hopes to achieve further speedups by implementing the functional partition in hardware as well. As a result it can be a little more precise in when individual aspects of execution are done. However, it has a heavier burden in fitting the whole design into an FPGA with a good performance.

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
    [pdf]

  • 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
    [pdf]

  • Checking Modular Refinements of Bluespec
    Nirav Dave, Michael Katelman Designing Correct Circuits (DCC 2010)
    Paphos, Cyprus, 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
    [pdf]

  • 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
    [pdf]

  • H.264 Decoder: A Case Study in Multiple Design Points
    Kermin Fleming, Chun-Chieh Lin, Nirav Dave, Gopal Raghavan, Jamey Hicks, Arvind
    Formal Methods and Models for Codesign (MEMOCODE 2008)
    Anaheim, CA, USA. Jun 2008
    [pdf]

  • Getting Formal Verification into Design Flow
    Arvind, Nirav Dave, Michael Katelman
    Lecture Notes in Computer Science, FM 2008: Formal Methods
    Volume 5014/2008 pp.12-32
    Formal Methods (FM 2008)
    Turku, Finland. May 2008
    [pdf]

  • 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
    [pdf]

  • Scheduling as Rule Composition
    Nirav Dave, Arvind, Michael Pellauer
    Formal Methods and Models for Codesign (MEMOCODE 2007)
    Nice, France. May 2007
    [pdf]

  • From WiFi to WiMAX: Techniques for IP Reuse Across Different OFDM Protocols
    Man Cheuk Ng, Muralidaran Vijayaraghavan, Gopal Raghavan, Nirav Dave, Jamey Hicks, Arvind
    Formal Methods and Models for Codesign (MEMOCODE 2007)
    Nice, France. May 2007
    [pdf]

  • 802.11a Transmitter: A Case Study in Microarchitectural Exploration
    Nirav Dave, Michael Pellauer, Steve Gerding, Arvind
    Formal Methods and Models for Codesign (MEMOCODE 2006)
    Napa Valley, CA, USA. July 2006
    [pdf]

  • Automatic Synthesis of Cache-Coherence Protocol Processors Using Bluespec
    Nirav Dave, Man Cheuk Ng, Arvind
    Formal Methods and Models for Codesign (MEMOCODE 2005)
    Verona, Italy, July 2005
    [pdf]

  • Designing a Processor in Bluespec
    Nirav Dave
    S.M. Massachusetts Institute of Technology
    Jan 2005
    [pdf]

  • High-Level Synthesis: An Essential Ingredient for Designing Complex ASICs
    Arvind, Rishikur Nikhil, Daniel L. Rosenband, Nirav Dave
    International Conference on Computer-Aided Design (ICCAD-2004)
    San Diego, California, USA. November 2004
    [pdf]

  • Designing a Reorder Buffer in Bluespec
    Nirav Dave
    Formal Methods and Models for Codesign (MEMOCODE 2004)
    San Diego, California, USA. June 2004
    [pdf]

Workshops/Posters

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

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

  • 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
    [pdf]

  • 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
    [pdf]

  • 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
    [pdf]