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.