Imperial College London > Talks@ee.imperial > CAS Talks > Hardware Design and Verification with Cava

Hardware Design and Verification with Cava

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact John Wickerson.

This talk describes the specification, implementation and formal verification inside the Coq theorem prover of the AES crypto accelerator component of the OpenTitan silicon roof of trust. The approach we take is inspired by Adam Chlipala in his book Certified Programming with Dependent Types. We have developed a Lava-like domain specific hardware description language called Cava in Coq’s Gallina language which is designed to help describe low level data-path style circuits with a view to having tight control over resource utilization and performance. This allows us to specify, implement and formally verify high assurance systems in one model where specifications are plain Gallina functions that specify the desired behaviour of hardware components. Our system can extract circuit descriptions from our Coq DSL to SystemVerilog for implementation on FPGA circuits.

We are also planning on building on this work to also tackle the co-design of software and hardware where we extract both C code (or RISC -V machine code) and SystemVerilog and a register or bus-interface so we can reason about the end-to-end behaviour of a system comprising hardware and software.

SPEAKER BIO : Satnam Singh works at Google Research on the Oak project that is developing technology to promote secure and private computing. Satnam Singh has worked on projects dealing with custom hardware acceleration and compiler technology at Facebook, Microsoft and Xilinx and has held academic positions at the University of Glasgow and the University of Birmingham.

This talk is part of the CAS Talks series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

Changes to Talks@imperial | Privacy and Publicity