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].

Role in hardware security properties

Boot code execution is central to several hardware security properties:

• Deterministic start: A circuit satisfies this property if its internal state, including microarchitectural state, is fully cleared to deterministic values by boot code that runs on reset [chunk: e01eb2bc-af07-4f83-a991-8c44179dcede].
• Output determinism: A circuit satisfies this property if its outputs do not depend on data present in the circuit state prior to reset. Unlike deterministic start, output determinism does not require that all circuit state is reset to deterministic values — it allows state to depend on input data. This makes checking the property more complex, since it involves tracking a set of "allowed dependencies" (i.e. all inputs received over the course of execution) and verifying that the circuit's state post-boot code execution only relies on these allowed dependencies [chunk: 100a4c6b-a946-4379-a410-c1a6a76b0c78].

Some systems, such as MicroTitan, cannot satisfy output determinism or SEQX without boot code execution [chunk: 91532559-482e-4d7c-96dd-390c79237ffc].

Verification challenges

Verifying properties about boot code execution requires modeling the complete execution of the boot code from an initially unconstrained (symbolic) circuit state and performing a solver query on the final state. This poses difficulties for traditional hardware verification tools:

• Bounded model checking (BMC): Tools like SymbiYosys use BMC to unroll a bounded number of circuit steps into one large SMT query. Empirically, SMT solvers exhibit poor performance when reasoning about long chains of transition relations [chunk: da13564e-2b08-4a7e-b7f8-9409cf1c1d13]. SymbiYosys's runtime increases exponentially with the number of boot code cycles [chunk: e01eb2bc-af07-4f83-a991-8c44179dcede].
• Two-copy encoding: A common workaround in SymbiYosys is to instantiate two copies of the CPU that are initially unrelated, and add assertions that their state must be equal after the boot code runs. However, this encoding has poor scalability [chunk: e01eb2bc-af07-4f83-a991-8c44179dcede].
• Memory state complexity: In complex SoCs like MicroTitan, symbolic terms representing state (e.g., SPI state machine registers) can grow rapidly each cycle during boot code execution if left unchecked, because the new state on each cycle depends on the previous state [chunk: 100a4c6b-a946-4379-a410-c1a6a76b0c78].

rtlv's approach to verifying boot code execution

The rtlv verification approach is specifically designed to handle many cycles of boot code execution efficiently. Its key techniques include:

• Hybrid symbolic execution: rtlv compiles Verilog circuits into a Rosette model and uses Rosette's hybrid symbolic execution, which performs type-driven state merging to merge values at control-flow joins, avoiding path explosion [chunk: da13564e-2b08-4a7e-b7f8-9409cf1c1d13].
• Rewrite rules: Rosette's rewrite rules act as heuristics to simplify symbolic expressions on the fly before they reach the solver, resulting in smaller SMT queries [chunk: 8f0d2e8d-6757-4786-b035-ece765fac6f1].
• Imperative step function: Instead of using a transition relation directly in the SMT encoding, rtlv transforms the transition relation into an imperative step function that allows for symbolic execution, which scales linearly with the number of cycles [chunk: da13564e-2b08-4a7e-b7f8-9409cf1c1d13].
• Performance hints: For complex SoCs, rtlv/shiva provides a performance hint interface (e.g., abstract, overapproximate, abstract-or-overapproximate-vector) that allows developers to suggest state transformations to reduce the size of symbolic expressions while maintaining soundness [chunk: 100a4c6b-a946-4379-a410-c1a6a76b0c78, 8f0d2e8d-6757-4786-b035-ece765fac6f1].

Case study results

Table: rtlv can verify boot code execution for a small RISC-V SoC in 1.3 seconds, while SymbiYosys is unable to finish within 12 hours for the same 104 cycles [chunk: e01eb2bc-af07-4f83-a991-8c44179dcede, ab47b904-296b-461d-8987-9bce0df2787b]. For the more complex MicroTitan, rtlv scales to over 20,000 cycles of boot code execution, and the verification effort helped find and fix violations of the state-clearing property in the baseline hardware [chunk: ab47b904-296b-461d-8987-9bce0df2787b].

Limitations

The rtlv approach to verifying boot code execution has several limitations:

• Simple embedded applications only: rtlv is currently expected to verify properties that require executing several hundred lines of C on microcontroller-level hardware, and is not designed for larger applications [chunk: 91532559-482e-4d7c-96dd-390c79237ffc].
• End-to-end proof gap: rtlv does not bridge results proven with Rosette to verification tools like Coq for end-to-end proofs requiring metatheory. The case study proves properties about individual clock domains in MicroTitan, but there is no machine-checked proof that these imply a top-level output determinism property [chunk: 91532559-482e-4d7c-96dd-390c79237ffc].
• Boot code must have known control flow: The approach works best when the boot code is known and its control flow is not dependent on unconstrained values, so that the program counter is concrete on each cycle. The final circuit state should also contain mostly or solely concrete terms, because this means the verification runtime is dominated by symbolic execution time rather than the final solver query [chunk: da13564e-2b08-4a7e-b7f8-9409cf1c1d13].

Related verification approaches

Several prior works have addressed end-to-end verification of systems, including:

• The CLI Stack (beginning in 1989) [chunk: 91532559-482e-4d7c-96dd-390c79237ffc]
• Verisoft [chunk: 91532559-482e-4d7c-96dd-390c79237ffc]
• The CakeML project's end-to-end verified system [chunk: 91532559-482e-4d7c-96dd-390c79237ffc]

These works prove deep end-to-end correctness theorems about software running on hardware, but rely on heavyweight techniques using interactive theorem provers. The rtlv framework shares a limitation with prior systems like AVR and Averroes: neither supports the modeling of code execution [chunk: 91532559-482e-4d7c-96dd-390c79237ffc].