This repository contains code for my MEng thesis, "Kronos: Verifying leak-free reset for a system-on-chip with multiple clock domains". Kronos consists of a SoC based on a subset of OpenTitan, with a security property called "output determinism" verified using Racket/Rosette.

For more information, see the thesis!

• sv2v (tested on commit 8e1f2bb, newer versions may break)
• Yosys (custom fork)
• rtlv (custom fork)
  • This fork adds additional performance hints as well as special support for interpreting SMT-LIB generated by Yosys's clk2fflogic extraction.
• Racket
• Rosette
• RISC-V toolchain
• bin2coe

Once dependencies are installed, run make verify in the top-level to run the build flow and all top-level verification scripts.

Contains verified boot code for resetting SoC's state.

Contains all of our HDL code. This directory contains a fork of OpenTitan as a Git submodule, and the top level and crossbar implementations for our subset. The OpenTitan fork contains two types of modifications: some to let it work nicely with our toolchain, and some to fix violations of our output determinism property. The fork's commit messages provide a bit of detail about each change.

Contains Racket verification code. The following files are top-level entry points:

• verify/core/main.rkt - proof of core output determinism
• verify/peripheral/spi-in.rkt - proof of peripheral output determinism for SPI-in clock domain
• verify/peripheral/spi-out.rkt - proof of peripheral output determinism for SPI-out clock domain
• verify/peripheral/usb.rkt - proof of peripheral output determinism for USB clock domain
• verify/fifo/main.rkt - FIFO auxiliary proof for all verified sizes of sync and async FIFO

This project is based on Notary, which also uses Racket/Rosette to verify a security property for an open-source RISC-V SoC (based on the PicoRV32).