Nirav Dave
Nirav Dave
32 Vassar St
Cambridge, MA 02139
I've graduated and am now a Computer Scientist in CSL at SRI International. Before I was a graduate student at Computer Science & Artificial Intelligence Laboratory(CSAIL) and part of the Computational Structures Group working with Professor Arvind.

My main interests are embedded systems, computer architecture and digital design, functional languages and compilation, and formal verification and program analysis.

My thesis research is on the design of a mixed substrate embedded systems and overcoming issues of integration, verification, and design flexibility without compromising on expressiveness or the quality of the resulting hardware or software. This entails the introduction of a unified model of computation based on Guarded Atomic Actions, a notion of computational domains with associated typing discipline to allow designs to be partitioned across various hardware and software components, a hardware-software compiler to partition and implement each component in the system, and a verification tool to help designers do safe action-level refinement of a design.


Hardware-Software Codesign

Embedded Systems often require a design be partitioned between specialized hardware components which have good power and parallel performance and software which is more flexible and requires lower additional hardware costs.

Current industrial practice is to have hardware and software designers agree on an initial design partition and work out an interface between hardware and software. Each set of designers build their part of the design, and when the final hardware is back they attempt to integrate it. Unfortunately, initial interface designs are often incomplete, unrealizable, or just need to be changed for implementation reasons. As a result the the model the software designers have does not match the actual hardware must be reworked. This causes significant problems for time to market and/or functionality. There are other significant problems with this approach; partitioning must be done well before designers have a full understanding of the design tradeoffs, we cannot migrate already developed designs to different platforms where different design tradeoffs exist.

One major aspect on my research is representing heterogenous substrate system in a single unified language based on Guarded Atomic Actions(GAAs) which exposes the interface between computational substrates explicitly. This not only isolates the complex communication channel components, but also enhances design modularity,allows easy repartitioning of designs, and makes whole system verification easier. To highlight this idea, we developed Bluespec CoDesign Language (BCL) and associated hardware-software compiler.

Improving Hardware Design

Current hardware design is done at the level of gates and wires making designs difficult to debug. I have spent a significant amount of effort refining and developing Bluespec, a hardware design language of Guarded Atomic Actions. This involved the improvement of compilation and scheduling schemes, determining how to embed highly concurrent structures naturally in the abstraction, and the development of methodologies and patterns to exploit the new senses of modularity and semantic improvements for verification. To show the viability of this approach I have done significant designs showing not only the quality of final hardware, but high reuse and design flexibility, creating significant design frameworks for multimedia and communication spaces.

Formal Verification

Despite the great strides that formal methods have made in over the last many decades, we have seen very little adoption by the design community at large. In general, formal verification in industry is done only by PhDs who's theses were on formal methods. The notable exception to this comes in the form of type checking or FSM equivalence checkers, both of which offer extremely fast if incomplete or overconstrained answers. These, though not a full completeness check give useful information to designers fast enough to have a positive impact on the design process. I strongly believe this is the only way that formal methods can be moved from the periphery of the field. To this end, I have built a equivalence checker which operates at the base one-rule-at-a-time level of our underlying GAA model. Since nondeterminism in this model regularizes the behavior space, we can establish equivalence of different designs very rapidly; showing a 7 stage MIPS processor has the same behavior as a 6-stage processor where two of the stages have been folded together can be done in a matter of machine-minutes. This can be done repeatedly in a matter of minutes to show that a fully pipeline pipeline is equal to an ISA-level description of the machine, a significant result.

Satisfiability Modulo Theories (SMT) Solvers

Satisfiability (SAT) engines which check for a satisfying assignment of variables in an equation have been getting better year after year. Often the best practical solution for solving a hard problem is translating it into a SAT query and translating the result back. Recently, much work has been done in augmenting SAT with theories like the theory of bit-vectors or arrays, effectively adding data types to the query language; these are called satistifiabilty-modulo-theories~(SMT). Casting one's problem to SMT has many issues. First, casting a problem into an SMT-level query can be difficult, especially when one want to capture higher-order sharing. This translation is made harder if one needs to reverse it and interpret the results of a query back in the language of the original question. Second, having done a translation one is locked into selecting a set of theories to exploit which effectively locks one into a single solver (or a small set of them). Third, optimizations between tools based on SMT do not benefits from the optimizations between; the only sharing of htat sort is held in the SMT solver. As a result I developed HaskSAT, an Embedded Domain-Specific Language in Haskell. HaskSAT allows the user to write queries using Haskell-level abstract data types, functions, and pattern matching. This is then automatically tranformed in a modular way to the SMT backend of choice, the result interpreted and lifted back to a Haskell-level value. This allows designers to separate the language description from the language of optimization, allowing greater translation flexibility and better choice of backend. Future work will allow us to build more efficient and expressive hybrid SMT solvers using the Nelson Oppen approach.


Conference and Journal Publications

  • Modular Deductive Verification of Multiprocessor Hardware Designs
    Muralidaran Vijayaraghavan, Adam Chlipala, Arvind, Nirav Dave
    Computer Aided Verification (CAV 2015)
    San Francisco CA USA, July 2015

  • Smten with Satisfiability-based Search
    Richard Uhler, Nirav Dave
    Systems, Programming, Languages and Applications: Software for Humanity 2014 (SPLASH 2014)
    Portland, OR, USA. October, 2014 [pdf]

  • Modular Compilation of Guarded Atomic Actions
    Muralidaran Vijayaraghavan, Nirav Dave, Arvind
    Formal Methods and Models for Codesign (MEMOCODE 2013)
    Portland, OR, USA. October, 2013

  • Smten: Automatic Translation of High-Level Symbolic Computations into SMT Queries
    Richard Uhler, Nirav Dave
    Computer Aided Verification (CAV 2013)
    St. Peterburg, Russia, July 2013

  • Enabling Hardware Exploration in Software-Defined Networking: A Flexible, Portable OpenFlow Switch
    Asif Khan, Nirav Dave
    Field-Programmable Custom Computing Machines (FCCM 2013)
    Seattle, WA, USA, April, 2013

  • CHERI: a Research Platform Deconflating Hardware Virtualization and Protection
    Robert N.M. Watson, Peter G. Neumann Jonathan Woodruff, Jonathan Anderson, Ross Anderson, Nirav Dave, Ben Laurie, Simon W. Moore, Steven J. Murdoch, Philip Paeps, Michael Roe, and Hassen Saidi.
    Runtime Environments, Systems, Layering and Virtualized Environments (RESoLVE 2012)
    London, UK March, 2012

  • Automatic Generation of Hardware/Software Interfaces
    Myron, King, Nirav Dave, Arvind
    Architectural Support for Programming Languages and Operating Systems (ASPLOS 2012)
    London, UK. March 2012

  • Verification of Microarchitectural Refinements in Rule-based Systems
    Nirav Dave, Michael Katelman, Myron King, Arvind, José Mesegeur
    Formal Methods and Models for Codesign (MEMOCODE 2011)
    Cambridge, UK. July 2011

  • BCL: A Language for Hardware-Software Codesign
    Nirav Dave, Myron King, Arvind
    Programming Language Design and Implementation (PLDI 2011)
    San Jose, CA USA. June 2011 (Submitted)

  • 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

  • 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

  • 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

  • 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

  • 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

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

  • 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

  • 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

  • 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

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

  • 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

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


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

  • 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

  • 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

Other Papers

  • HaskSAT: an Embedded DSL for SMT Queries
    Nirav Dave

() Last Modified: Fri Aug 7 17:28:39 2015   Valid HTML 4.01! Valid CSS!