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
Structures Group working
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.
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 DesignCurrent 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 VerificationDespite 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) SolversSatisfiability (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
|() Last Modified: Fri Aug 7 17:28:39 2015|