Skip to main content
Home

Main navigation

  • Home
  • Series
  • People
  • Depts & Colleges
  • Open Education

Main navigation

  • Home
  • Series
  • People
  • Depts & Colleges
  • Open Education

Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification

Series
International Conference on Functional Programming 2017
Video Embed
Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification
Co-written by Joonwon Choi, Benjamin Sherman, Adam Chlipala, Arvind (Massachusetts Institute of Technology, USA).

It has become fairly standard in the programming-languages research world to verify functional programs in proof assistants using induction, algebraic simplification, and rewriting. In this paper, we introduce Kami, a Coq library that enables similar expressive and modular reasoning for hardware designs expressed in the style of the Bluespec language. We can specify, implement, and verify realistic designs entirely within Coq, ending with automatic extraction into a pipeline that bottoms out in FPGAs. Our methodology, using labeled transition systems, has been evaluated in a case study verifying an infinite family of multicore systems, with cache-coherent shared memory and pipelined cores implementing (the base integer subset of) the RISC-V instruction set.

More in this series

View Series
International Conference on Functional Programming 2017

No-Brainer CPS Conversion

Milo Davis (Northeastern University, USA) gives the fourth talk in the second panel, Foundations of Higher-Order Programming, on the 2nd day of the ICFP.
Previous
International Conference on Functional Programming 2017

SpaceSearch: A Library for Building and Verifying Solver-Aided Tools

Konstantin Weitz (University of Washington, USA) gives the second talk in the second panel, Tools for Verification, on the 2nd day of the ICFP conference.
Next
Licence
Creative Commons Attribution-Non-Commercial-Share Alike 2.0 UK: England & Wales; http://creativecommons.org/licenses/by-nc-sa/2.0/uk/

Episode Information

Series
International Conference on Functional Programming 2017
People
Muralidaran Vijayaraghavan
Keywords
technology
computing
programming
Department: Department of Computer Science
Date Added: 15/01/2018
Duration: 00:19:30

Subscribe

Apple Podcast Video Video RSS Feed

Download

Download Video

Footer

  • About
  • Accessibility
  • Contribute
  • Copyright
  • Contact
  • Privacy
'Oxford Podcasts' Twitter Account @oxfordpodcasts | MediaPub Publishing Portal for Oxford Podcast Contributors | Upcoming Talks in Oxford | © 2011-2022 The University of Oxford