Boot code execution

Concept

Boot code execution refers to the initial software that runs on a hardware circuit immediately after reset, typically responsible for initializing and clearing microarchitectural state. In the context of formal hardware verification, modeling many cycles of boot code execution is essential for proving security properties such as deterministic start and output determinism, but the large number of cycles involved poses significant challenges for traditional bounded model checking tools, which scale exponentially with the number of execution cycles.

First seen 6/9/2026

Last seen 6/9/2026

Evidence 7 chunks

Wiki v1

WIKI

Boot code execution

Definition and purpose

Boot code execution refers to the cycle-accurate execution of the initial software that a hardware circuit runs after reset. In a typical system-on-chip (SoC), this boot code is responsible for clearing uninitialized microarchitectural state and bringing the hardware into a known, deterministic configuration before any application software is loaded. For example, in the MicroTitan RISC-V SoC (a subset of OpenTitan), boot code takes 24,516 cycles to clear the chip's uninitialized state, compared to only 104 cycles for the simpler PicoRV32 CPU [chunk: 91532559-482e-4d7c-96dd-390c79237ffc, 8f0d2e8d-6757-4786-b035-ece765fac6f1].

READ FULL ARTICLE →

NEIGHBORHOOD

1 nodes · 0 edges

graph · boot code execution · depth=1

LINKED ENTITIES

4 links

deterministic start verified_property Deterministic start is a security property whose verification is the primary motivating example for modeling boot code execution in the evidence.

output determinism verified_property Output determinism is the security property verified in the MicroTitan case study and is directly tied to modeling boot code execution.

bounded model checking verification_technique BMC is the technique used by SymbiYosys's Yosys-SMTBMC backend that scales poorly with the number of boot code execution cycles.

Symbolic Execution verification_technique Hybrid symbolic execution is rtlv's primary technique for efficiently handling many cycles of boot code execution.

CITATIONS

15 sources

15 citations — click to expand

[1] Boot code takes 104 cycles for the PicoRV32 CPU to clear uninitialized state. rtlv: push-button verification of software on hardware

[2] Boot code takes 24,516 cycles for MicroTitan to clear uninitialized state, compared to 104 for PicoRV32. rtlv: push-button verification of software on hardware

[3] Deterministic start requires that a circuit's internal state, including microarchitectural state, is fully cleared to deterministic values by boot code that runs on reset. rtlv: push-button verification of software on hardware

[4] Output determinism allows state to depend on input data, and verification requires tracking a set of 'allowed dependencies' to verify that the circuit's state post-boot code execution only relies on these allowed dependencies. rtlv: push-button verification of software on hardware

[5] Some systems such as MicroTitan cannot satisfy output determinism or SEQX without boot code. rtlv: push-button verification of software on hardware

[6] rtlv can model 104 cycles of PicoRV32 boot code execution and verify the deterministic start property in 1.3 seconds. rtlv: push-button verification of software on hardware

[7] SymbiYosys is unable to finish within 12 hours when verifying 104 cycles of boot code execution for PicoRV32, scaling exponentially with the number of cycles. rtlv: push-button verification of software on hardware

[8] rtlv scales linearly with the number of boot code execution cycles by using symbolic execution and an imperative step function instead of a transition relation in the SMT encoding. rtlv: push-button verification of software on hardware

[9] Rosette's hybrid symbolic execution performs type-driven state merging to avoid path explosion, and its rewrite rules simplify symbolic expressions on the fly. rtlv: push-button verification of software on hardware

[10] rtlv/shiva provides performance hints (abstract, overapproximate, abstract-or-overapproximate-vector) for transforming circuit state during boot code execution verification without affecting proof soundness. rtlv: push-button verification of software on hardware

[11] MicroTitan is a RISC-V SoC based on a subset of the OpenTitan project containing an Ibex CPU, 8KB ROM, 8KB RAM, UART, SPI, and USB peripherals. rtlv: push-button verification of software on hardware

[12] rtlv is expected to verify properties requiring executing several hundred lines of C on microcontroller-level hardware, but is not designed for larger applications. rtlv: push-button verification of software on hardware

[13] Prior frameworks AVR and Averroes do not support the modeling of code execution, similar to limitations discussed for rtlv in certain contexts. rtlv: push-button verification of software on hardware

[14] End-to-end software/hardware verification has a long history beginning with the CLI Stack in 1989, and includes Verisoft and the CakeML project's end-to-end verified system, which prove deep end-to-end correctness theorems using heavyweight interactive theorem provers. rtlv: push-button verification of software on hardware

[15] rtlv does not have a machine-checked, end-to-end proof that the individually verified properties of MicroTitan's clock domains imply a top-level output determinism property. rtlv: push-button verification of software on hardware