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 determinismverify/peripheral/spi-in.rkt- proof of peripheral output determinism for SPI-in clock domainverify/peripheral/spi-out.rkt- proof of peripheral output determinism for SPI-out clock domainverify/peripheral/usb.rkt- proof of peripheral output determinism for USB clock domainverify/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).