List view
Silver Oak Phase 2 will widen the scope of the design and verification effort. The planning is currently under way and some of the topics we are considering include: * Specifying hardware and software in Coq and extracting both and verifying HW/SW in concert. For example, specify and extract the software that runs on the OpenTitan RISC-V core for coordinating the AES peripheral. * Consider starting work on some aspects of "compiler verification" i.e. formally specifying or verifying the chain of transformations that map the DSL-level hardware descriptions to a circuit netlist. * Write a paper to submit to CAV 2022.
Overdue by 3 year(s)•Due by August 27, 2021•70/78 issues closedSilver Oak Phase 1 is focused on the development of a prototype system for formally specifying, implementing and verifying digital circuits using the Coq theorem prover, with extraction to SystemSystem Verilog for FPGA implementation. The goal for this milestone are: * Design and develop a proto-type DSLi in Coq for low level digital hardware design (distinct from other DSLs like Kami). * Formally specify, implement and verify the OpenTitan AES core using this framework. * Substitute the original AES core (at some level) in the OpenTitan design with our an implementation of our core and ensure all tests passes and the OpenTitan FPGA board still operates correctly with using the AES core. * Verification is of the AES Cava Coq DSL implementation against a formal specification we will also write in Coq. Verification of the compiler infrastructure we develop is not in scope for this milestone. * Write a paper for ICFP 2021 which described the design and use of our Cava DSL.
Overdue by 4 year(s)•Due by February 26, 2021•156/157 issues closed