rtlv: push-button verification of software on hardware

                                                                    Noah Moroze*, Anish Athalye, M. Frans Kaashoek, and Nickolai Zeldovich
                                                                                                  MIT CSAIL
                                                                                            moroze@csail.mit.edu*

ABSTRACT This paper presents rtlv, an approach for push-button formal veri- Circuit [.v] Hints [.rkt] fication of properties that involve software running on hardware for many cycles. For example, rtlv can be used to prove that executing by Yosys boot code resets a processor’s microarchitectural state to known SMT-LIB model [.smt2] deterministic values, while existing tools time out when attempting by #lang yosys to verify such a property. Rosee model [.rkt] Two key ideas enable rtlv to handle reasoning about many cy- cles of circuit execution. First, rtlv uses hybrid symbolic execution to reason about a circuit with symbolic values while minimizing the Checker Verification Result complexity of symbolic expressions; this is achieved by compiling (such as rtlv/shiva) ✔ OK / ❌ Fail circuits to programs in the Rosette solver-aided language. Second, rtlv rtlv enables the development of reusable circuit-agnostic property Racket Rosee Z3 checkers that have a performance hint interface, allowing developers to optimize verification performance while maintaining confidence Figure 1: The rtlv workflow. A user develops a circuit- that the proof is correct. agnostic property checker (yellow) that takes in a circuit Using rtlv, formally verifying a state-clearing property for a model and performance hints that suggest optimizations. small (1,300 flip-flop) RISC-V SoC takes only 1.3 seconds, while The user then inputs a particular circuit’s Verilog code SymbiYosys, a popular open-source verification tool, is unable to (white), mechanically transformed into a Rosette model finish within 12 hours. In another case study, rtlv scales to a larger by rtlv’s compiler, along with circuit/property-specific per- 4,300 flip-flop RISC-V SoC where verifying this state-clearing prop- formance hints (purple) that suggest optimizations. The erty requires modeling over 20,000 cycles of software executing checker returns “OK” if it is able to verify that the property on hardware. Formal verification with rtlv helped us find and fix holds. violations of the property in the baseline hardware, demonstrating that rtlv is useful for finding bugs.

1 INTRODUCTION state that remains concrete and minimizing the complexity of sym- Formally verifying digital hardware allows developers to increase bolic expressions in the circuit state. rtlv accomplishes this through their confidence in a system’s security and correctness. Many ex- a verification workflow, shown in Figure 1, based on two key ideas. ample uses of popular hardware verification tools involve checking First, the developer uses rtlv to compile the circuit to Rosette [15], a properties that can be verified after executing for a small number domain specific language for solver-aided programming embedded of cycles [16]. However, these tools are unable to efficiently verify in Racket. This lets developers verify the circuit using Rosette and properties that require executing for many cycles, making it diffi- take advantage of Rosette’s unique symbolic execution approach cult to use the tools for reasoning in a cycle-accurate manner about and rewrite rules. Second, the developer builds a circuit-agnostic software running on the hardware. property checker that has an interface for supplying performance For example, suppose a developer wants to verify that boot code hints. These hints suggest certain optimizing transformations of executing after reset clears all microarchitectural state in a CPU. the circuit state. The property checker is responsible for ensuring This requires modeling the complete execution of this boot code that these optimizations do not affect the correctness of the proof, from an initially unconstrained circuit state and performing a solver resulting in a smaller core of trusted code. To verify the circuit, the query on the final state. For the PicoRV32 [17], a simple RISC-V developer invokes the property checker with the extracted circuit CPU, verifying this property requires executing 104 cycles of boot model as well as a list of performance hints. Overall, Rosette’s sym- code. Using SymbiYosys [14], a popular open-source hardware veri- bolic execution system and performance hint optimizations result fication tool, the solver query resulting from unrolling 104 cycles in simpler solver queries compared to those produced by tools like of circuit execution is unable to finish within 12 hours. SymbiYosys, which improves verification performance. This paper presents rtlv, an approach for verifying circuits that This paper provides an overview of rtlv, and contributes the enables efficient cycle-accurate reasoning about software executing following: on hardware. With rtlv, modeling 104 cycles of boot code execution • A description of rtlv’s Verilog to Rosette compiler. and verifying that all state is cleared in the PicoRV32 takes only 1.3 • An example circuit-agnostic property checker, rtlv/shiva, seconds. that can be used for verifying a security property similar rtlv efficiently handles many cycles of execution by symboli- to the microarchitectural state clearing property described cally executing the circuit while maximizing the amount of circuit above.

                                                                                            N. Moroze, A. Athalye, M. F. Kaashoek, N. Zeldovich

picorv32 cpu1(...);                                                       is_deterministic(state):
picorv32 cpu2(...);                                                         # extract all symbolic variables in state
                                                                            sym_vars = symbolics(state)
if (cycle_count == 104) begin
  assert(cpu1.reg1 == cpu2.reg1);                                           # generate mapping of sym_vars to one possible
  assert(cpu2.reg2 == cpu2.reg2);                                           # set of concrete values
  // ... repeat for each register in picorv32                               solution = solve(sym_vars)

Figure 2: Verification pseudocode using SymbiYosys. This                    # evaluate state under this mapping
tool requires an encoding with two copies of the CPU that                   # to generate concrete state
are initially unrelated, along with an assertion that their                 concrete_state = evaluate(state, solution)
state must be equal after the boot code runs.
                                                                            # assert that state must equal the concrete
                                                                            # solution, i.e. if state is deterministic, it
   •        A case study using rtlv/shiva to verify a real-world RISC-V     # *must* equal the solution 'concrete_state'
                  SoC based on the OpenTitan, demonstrating that rtlv’s     verify(assert(state == concrete_state))
                  approach can be scaled to complex hardware and can be
     used for finding bugs in practice.                                   Figure 3: Verification pseudocode using rtlv, verifying the
2  EXAMPLE: DETERMINISTIC START                                           property without instantiating two circuit states. The code
                                                                          first calls the solver to generate some possible concrete state
Deterministic start is an example of a property where verification        and then verifies that the symbolic state must always equal
involves cycle-accurate reasoning over many cycles, often about           this concrete state.
software running on hardware. If a circuit satisfies deterministic
start, then its internal state, including microarchitectural state, is
fully cleared to deterministic values by boot code that runs on              104        rtlv
reset [2].                                                                       SymbiYosys
rtlvWe use deterministic start as a motivating example for using             102
            over existing tools for verifying circuits. We performed an
experiment where we set up both rtlv and SymbiYosys, a popular
open-source hardware verification tool, to prove deterministic start         100
for the PicoRV32 CPU. As shown in Figure 2, we encoded this                      0     20     40     60     80     100
property in SymbiYosys by instantiating two copies of the PicoRV32               Cycles
and adding assertions that each register in the one copy is equal to
the corresponding register in the other copy (i.e., there is only one     Figure 4: Scalability of verifying deterministic start. Symbi-
possible value that the register can take on) after the boot code runs.   Yosys scales exponentially; results truncated after 32 cycles.
We then configure SymbiYosys to use its Yosys-SMTBMC backend              rtlv scales linearly and takes 1.3 seconds to verify the prop-
to model all 104 cycles of boot code execution and verify that these      erty for 104 cycles.
assertions hold.
    Using rtlv, instead of writing verification code in Verilog, devel-
opers write code in Rosette, a solver-aided programming language
embedded in Racket. rtlv provides a system for compiling cir-             of cycles, showing that a subset of registers were cleared after the
cuits into a Rosette model. In order to verify deterministic start        appropriate number of cycles. Figure 4 shows the runtime of verify-
for the PicoRV32, a developer can instantiate a fully unconstrained       ing each property against the number of cycles it took to verify that
PicoRV32 circuit state, call the circuit’s step function 104 times,       property. This plot illustrates how SymbiYosys’s runtime increases
and then check the resulting circuit state to verify that it must be      exponentially with the number of cycles, while rtlv’s runtime
deterministic. Because Rosette provides solver-aided queries (effec-      is relatively flat: in this particular case, rtlv’s time is linear in
tively, direct access to the SMT solver), the rtlv-based approach         the number of cycles. Code for this experiment can be found at
can verify this property without instantiating two instances of the       https://github.com/anishathalye/deterministic-start-benchmark.
circuit and comparing them. As shown in Figure 3, the verification                This example shows that in order to verify properties such as
code can instead invoke the SMT solver once to find one concrete          deterministic start, rtlv’s approach doesn’t suffer from the same
state that the circuit can be in after the boot code runs, and then       scaling bottlenecks as SymbiYosys. The next section describes what
invoke the solver again to prove that the state must be equal to that     these bottlenecks are and how rtlv eliminates them.
single concrete state. This more efficient check is enabled by the        3  VERIFICATION APPROACH
ability to make intermediate solver queries to build up a final solver
query, which is not possible in SymbiYosys.                               rtlv verifies circuits using the Rosette solver-aided programming
         With these setups, the SymbiYosys proof does not finish within   language, taking advantage of Rosette’s symbolic execution ap-
a 12-hour timeout, while the rtlv proof finishes within 1.3 sec-          proach in order to generate a more efficient low-level encoding
onds. To demonstrate how SymbiYosys’s verification time scales,           of the property being verified as compared to existing tools like
        we proved a related state-clearing property for varying numbers   SymbiYosys.

Time (s)

rtlv: push-button verification of software on hardware

3.1 SMT-based verification by rtlv’s #lang yosys DSL, which transforms Yosys’s SMT-LIB Formal verification differs from traditional hardware verification: it encoding of the circuit into Rosette code, producing a shallow em- involves proving that certain properties always hold, rather than bedding in Rosette through the use of Racket macros. The code checking that a circuit behaves as expected over a concrete (and defines: often hand-designed) set of test vectors. • A Rosette struct that represents circuit state, which includes SMT-based formal verification, a popular approach for verify- fields for all registers, memories, and current input values. ing hardware, works by encoding a model of the circuit and the • The step function, which takes a circuit state and returns property being proven into a boolean expression called an SMT a new circuit state representing the result of running the query. Verification queries are expressed in the negative, meaning circuit for one clock cycle. the query evaluates to true if the property is violated. In order to • Functions for setting the inputs to a circuit and functions for verify the property, the tool passes the query into an SMT solver getting the outputs from a circuit. like Z3 [5], which attempts to determine whether there is an assign- These definitions let us use Rosette to execute the circuit instead ment of values to the variables in the query that makes the query of encoding execution into the SMT query itself. At the very end of evaluate to true. If the solver determines the query is unsatisfiable, the execution, Rosette is able to construct a solver query that only this proves the property, because there is no possible assignment considers the final circuit state, regardless of execution length, in that makes the query evaluate to true (i.e. violates the property). contrast with the SymbiYosys encoding. Complex SMT queries result in bad performance or solver time- The example above would be encoded as follows. Let step(s) be outs, so in order for a verification tool to efficiently prove a property, the step function. rtlv initializes s0 to be a fresh symbolic variable, it must produce a “good” SMT encoding. In the case of properties and then performs the following computation: that require executing for many cycles, rtlv’s approach, building on Rosette’s symbolic execution, generally produces better SMT s1 = step(s0) (Symbolic execution) encodings than existing work. s2 = step(s1) 3.2 Symbolic execution with Rosette sn . . . To enable reasoning about circuits using Rosette, rtlv includes a = step(sn−1) Verilog to Rosette compiler, which works as follows. First, a cir- cuit’s Verilog source is passed into the Yosys [18] synthesis tool, which generates an SMT-LIB representation of the circuit. A domain- assert(I(s0) ∧ ¬P (sn )) (Solver query) specific language (DSL) provided by rtlv, called #lang yosys, then In contrast to SymbiYosys’s approach, the final query size does transforms Yosys’s SMT-LIB output into Rosette code. Yosys’s front- not inherently scale with the number of cycles of execution, and the end only supports Verilog, so if the circuit is written in a different query does not directly require the SMT solver to reason about the HDL, it must be converted into an equivalent Verilog representation. circuit’s execution. Instead, the circuit’s execution is computed in We use sv2v [13] for converting circuits written in SystemVerilog. Racket/Rosette, which can take advantage of performing concrete Both rtlv and SymbiYosys rely on Yosys’s SMT-LIB backend for computations directly in Racket as opposed to building up large producing a circuit model for verification. The key distinction be- terms for the solver to reason about. Thanks to Rosette’s rewrite tween the two approaches is how this model is used. As-is, Yosys’s rules and rtlv’s performance hints (described in Section 4.1), such output describes the behavior of the circuit on each clock cycle as opportunities occur often and result in significant speedup. a transition relation. This is a function that takes in two circuit rtlv’s approach is well suited to applications where much of states—a current state and a next state—and returns a boolean indi- the circuit state is concrete—for instance, applications modeling cating whether or not the next state can be reached by stepping the the execution of known software with concrete control flow. If the current state. Expressing the circuit transition as a relation allows circuit state is primarily symbolic, each step will result in rapidly SymbiYosys’s Yosys-SMTBMC backend to encode execution into growing complexity in the circuit state’s symbolic expressions, ul- the solver query directly. timately leading to a large final solver query (in this case, neither For example, suppose we want to prove that a circuit satisfying an the SymbiYosys encoding nor the rtlv encoding will give good initial predicate I, after n cycles, satisfies some predicate P . Suppose performance). that the transition relation between circuit states si and sj is written Deterministic start is a good example of a property well-suited as T (si , sj ). For this task, SymbiYosys will produce an SMT query to rtlv’s approach. The boot code is known, and its control flow with variables s0, s1, . . . , sn and the following assertion: is not dependent on unconstrained values, so the program counter assert(I(s0) ∧ T (s0, s1) ∧ T (s1, s2) ∧ · · · ∧ T (sn−1, sn ) ∧ ¬P (sn )) is concrete on each cycle. In addition, by the nature of what the boot code does, the final circuit state will likely contain mostly or Empirically, SMT solvers exhibit poor performance when rea- even solely concrete terms, because the entire circuit state becomes soning about long chains of T (s0, s1) ∧ · · · ∧ T (sn−1, sn ). deterministic. Therefore, the verification runtime is dominated by Instead of using the transition relation directly in the SMT encod- symbolic execution time rather than the final solver query. ing, rtlv transforms the transition relation into an imperative step rtlv benefits from several design features in Rosette. The first is function that allows for symbolic execution. This is always possible Rosette’s hybrid symbolic execution model, which performs “type- because we operate on a circuit with a single clock domain with driven state merging” [15] to merge values at control-flow joins, all nondeterminism (such as don’t-cares) resolved, so the behavior avoiding problems with path explosion found in traditional sym- of the circuit is a total function. This transformation is performed bolic execution. In addition, Rosette has “rewrite rules”, which are

                                                                               N. Moroze, A. Athalye, M. F. Kaashoek, N. Zeldovich

heuristics to simplify symbolic expressions on the fly before they reach the solver. Core Clock Domain As an example of how these two features can simplify sym- Ibex CPU ROM RAM bolic execution, suppose a circuit has a 2-to-1 multiplexer, and (8 KB) (8 KB) consider a situation where each input is a concrete zero, but the select input is symbolic. A multiplexer represents the equivalent xbar of a branch in software — a traditional symbolic execution sys- tem would separately evaluate a path for each possible value of SPI USB the select input. However, Rosette’s state-merging explores both UART branches and then merges their results into a single symbolic ex- pression such as (ite select 0 0). While SymbiYosys would have the solver reason directly about this term, Rosette’s rewrite rules further simplifies this to 0, since both branches are zero. Figure 5: A block diagram of MicroTitan, with its core clock Another example of a rewrite rule simplification would be in domain highlighted. instances where a circuit extracts a concrete bit from a concatenated concrete and symbolic value. For example, given a 5-bit symbolic foo, the expression (extract 7 7 (concat 000 foo)) will be to execute. The bulk of this additional execution time comes from simplified by Rosette to 0. the uninitialized memories in MicroTitan that must be explicitly Rewrite rules give rtlv more efficient symbolic execution that reset by loops in the boot code. Clearing the MicroTitan’s uninitial- results in smaller symbolic expressions in the final circuit state, ized state takes 24,516 cycles of boot code execution, compared to resulting in smaller SMT queries. only 104 for the PicoRV32. In addition, the MicroTitan circuit itself is more complex, consisting of around 4,300 flip-flops as compared 4 CASE STUDY to around 1,300 flip-flops in the PicoRV32. This means that solver queries about MicroTitan’s state are likely to be more complex than As a case study, we used rtlv to verify a security property called queries about the PicoRV32. output determinism for a complex SoC based on a subset of Google and lowRISC’s OpenTitan [8]. This case study demonstrates how 4.1 Performance hints we applied rtlv to a more complex verification task by creating a In this case study, Rosette’s symbolic execution system alone couldn’t circuit-agnostic property checker called rtlv/shiva that allowed provide sufficient performance, since MicroTitan’s state contains us to implement peephole optimizations in a disciplined way. In ad- symbolic terms that grow rapidly over time and cannot be simpli- dition, this case study shows that rtlv can be used to find violations fied by rewrite rules, which are heuristics and cannot be “complete.” of security properties in practice. Therefore, we had to implement circuit-specific optimizations to If a circuit satisfies output determinism, its outputs must not make verification feasible. To do so in a disciplined way, we built a depend on data present in the circuit state prior to reset. Output circuit-agnostic property checker called rtlv/shiva which takes determinism is implied by deterministic start: one way to ensure a in the Rosette circuit model (which includes components such as circuit satisfies output determinism is by clearing all circuit state on the step function and register names), executes the circuit based on reset, so that no data that was present in the circuit prior to reset the model provided, and returns whether or not the circuit satisfies remains in the circuit anymore. Therefore, both properties can be output determinism. In addition, rtlv/shiva has a performance proven by modeling the execution of boot code and verifying that hint interface that allows a developer to suggest that the checker uninitialized data has been cleared from the circuit state. However, transform the circuit state in a certain way, generally to reduce the output determinism does not require that all circuit state is reset size of symbolic expressions and therefore simplify both symbolic to deterministic values: it allows state to depend on input data. execution and the final solver query. This makes checking this property more complex, since it involves A key idea is that rtlv/shiva is sound, and the hints are un- tracking a set of “allowed dependencies” (i.e. all inputs received trusted, meaning that no matter what hints a developer specifies, over the course of execution), and verifying that the circuit’s state the tool will not erroneously say that a property holds when it does post-boot code execution only relies on these allowed dependencies. not. Supplying inadequate or incorrect hints can only harm per- We prove this property for a RISC-V SoC we call MicroTitan, formance or make the tool fail to prove the property. Performance which is based on a subset of an existing project called OpenTitan. hints cannot be misused to make the tool erroneously report “OK”. Figure 5 shows a block diagram of the circuit. It includes the Ibex This enables a workflow where the developer can freely experiment CPU, 8KB of ROM, 8KB of RAM, and UART, SPI device, and USB with performance hints without worrying about invalidating the device peripherals. MicroTitan includes multiple clock domains that proof. we verified separately, but this case study focuses on the “core clock The verification tool itself is considered trusted since we assume domain.” The core clock domain contains the Ibex CPU, memories, it enforces this property. By encapsulating the trusted code for trans- UART, and slices of the SPI and USB peripherals. To satisfy output forming circuit state in a non-circuit-specific tool, the developer determinism, the hardware in this clock domain must execute boot can apply performance hints as needed while maintaining high code to clear certain state, and to verify this property, we must confidence in the proof’s correctness. In addition, this separation model this boot code execution. allowed us to reuse rtlv/shiva for multiple circuits: we used this MicroTitan’s core clock domain is more complex than the Pi- checker to verify output determinism for the MicroTitan as well as coRV32 CPU, and its boot code takes a correspondingly longer time the PicoRV32.

rtlv: push-button verification of software on hardware

Hint Description memory where it can be consumed by software. Since output deter- abstract Checks if field only depends on allowed minism doesn’t assume anything about SoC inputs while boot code [field-name] dependencies—if so, replaces it with a fresh is executing, all SPI inputs are represented as symbolic data. These symbolic (added to allowed dependencies). inputs affect state transitions in the SPI state machine, resulting in the state machine control register itself becoming a symbolic overapproximate Replaces field with a fresh symbolic. term. In addition, since the new state on each cycle depends on the [field-name] previous state, the size of the symbolic term representing this state abstract-or- For each entry of a memory field, abstracts it grows rapidly each cycle if left unchecked. overappprox-vector if it only depends on allowed dependencies, However, it turns out that independent of inputs, after 150 cycles [field-name] and otherwise overapproximates it. of boot code execution, this state machine returns to an idle state, collect-garbage Forces GC run. and it does not leave this state for the remainder of the execution. We take advantage of this fact by applying a concretize hint to the state concretize Determines using a solver query if field only machine control register on cycle 150, which causes rtlv/shiva to [field-name] evaluates to a single concrete value—if so, verify that the register must be idle and then replace the symbolic replaces it with this concrete term. term with a concrete term. Once back to the concrete idle state, the run-and-replace Re-runs verification from initial state to cur- register is able to remain concrete for the rest of the execution. [list-of-field-names rent cycle, using the provided list of hints. In addition to performance hints, rtlv/shiva supports a gen- list-of-hints] At the end of this sub-execution, replaces eral interface called unsafe-custom-hint for user code to directly the given fields in the main execution with implement transformations of the circuit state. This was useful for their values from the secondary execution. this case study, since it allowed us to implement a complex trans- formation on each cycle based on the relationship between two Table 1: Performance hints [arguments in brackets] imple- registers. The exact transformation was circuit-specific and could mented by rtlv/shiva. not be easily generalized, so it was best implemented in user verifi- cation code. Like a performance hint, the code that implemented the transformation performed auxiliary solver queries to ensure One of rtlv/shiva’s performance hints is concretize. This that the transformation was correct. hint takes in the name of a field in the circuit state, checks if the By taking advantage of rtlv/shiva’s performance hints, verifi- field can only evaluate to a single concrete value by issuing a solver cation of output determinism for MicroTitan finishes in under 100 query, and replaces it with that concrete value if so. The solver minutes on a machine with an Intel Core i7-5930K. The verification query ensures that this hint cannot be misused to transform the code is single-threaded. circuit state in an incorrect way. Relying on the solver allows a 4.2 Bugs found hint like concretize to be more powerful than rewrite rules. As an example, consider the symbolic expression (ite a 0 a) 1. This The verification process helped us find and fix four violations of expression is always equal to 0, since it returns 0 when a equals output determinism in MicroTitan across all its clock domains: 1, and a when a equals 0 itself. However, Rosette has no built-in (1) The possibility of leaking data that was previously sent via rewrite rule for this. If rtlv/shiva is told to apply concretize to SPI prior to reset. a field containing this expression, it will set the field to 0. (2) The possibility of leaking data that was previously received Performance hints are also useful since they can take advan- via SPI prior to reset. tage of the specific property being verified, and therefore be more (3) The possibility of leaking memory that was stored in the specific than general optimizations such as Rosette’s rewrite rules. USB transmit/receive buffer prior to reset (it is unclear if this For example, rtlv/shiva supports a hint called abstract that de- issue is exploitable, but we patched it anyways to simplify termines if a field only depends on allowed dependencies, and, if verification). so, replaces that field with a fresh symbolic value that itself gets (4) The possibility of leaking data about the reset line’s previous added to the set of allowed dependencies. This is sound since we values. can always overapproximate a value (i.e., set it to a completely This demonstrates that rtlv can successfully be used for bug- unconstrained fresh symbolic) and the dependency check main- finding. In addition, this work resulted in an upstream contribution tains the invariant that values in the allowed dependencies set only to OpenTitan [10]. depend on previous inputs. However, a symbolic value being an Overall, this case study shows that rtlv can be used to write “allowed dependency” is only meaningful in the context of output performant verification code for complex circuits and successfully determinism, so this hint is inherently property-specific. In addition catch violations of a sophisticated security property. More informa- to concretize and abstract, rtlv/shiva supports several more tion about this case study can be found in [11], and the verification hints, described in Table 1. code can be found at https://github.com/nmoroze/kronos. Without performance hints, verification of MicroTitan would time out. One example of a critical performance hint is the use of 5 concretize on the state register controlling the SPI peripheral’s RELATED WORK RX FIFO state machine. This hardware state machine is responsible Much prior work has been done on hardware formal verification for gathering data the SoC receives via SPI and writing it into a tools, and a lot of this work uses similar ideas to the ones used in rtlv. However, none of this prior work has fully tackled the 1In actual Rosette code: (if (bveq x (bv #b1 1)) (bv #b0 1) x) problem of performantly verifying software execution on hardware,

    N. Moroze, A. Athalye, M. F. Kaashoek, N. Zeldovich

which requires reasoning about many cycles of execution, using a 41 bits of un-reset state. Proving the property in our case requires push-button approach. modeling execution of state-clearing boot code, while their work did not address code execution. Therefore, their framework is in- 5.1 End-to-end software/hardware verification sufficient for systems such as MicroTitan that cannot satisfy output There is a long line of work in the end-to-end verification of sys- determinism or SEQX without boot code. tems, beginning in 1989 with the CLI Stack [3]. Other notable works Goel and Sakallah [6] presents another formal verification frame- include Verisoft [1] and the CakeML project’s end-to-end verified work called AVR, which is descended from prior work on Averroes. system [9]. These works prove deep end-to-end correctness theo- However, Averroes shares AVR’s limitation of not supporting the rems (i.e. full functional correctness) about software running on modeling of code execution. hardware, but they rely on heavyweight techniques using interac- tive theorem provers. In contrast, rtlv proves simpler properties, 6 but in a push-button style. rtlvLIMITATIONS is an effective approach for verifying hardware, but it has 5.2 SymbiYosys several limitations. rtlv has no way to bridge results proven with SymbiYosys [14] is a popular open-source hardware verification Rosette to verification tools like Coq for end-to-end proofs that tool that can verify safety and liveness properties, but it has several require proving metatheory. For example, the case study described limitations. Like many commercial tools, SymbiYosys verifies prop- in Section 4 proves a property about an individual clock domain in erties written using SystemVerilog Assertions, making it difficult MicroTitan, and while we have verified MicroTitan’s other clock to express complex properties. domains, we do not have a machine-checked, end-to-end proof that SymbiYosys supports many solver backends, each with their own these individual properties imply a top-level output determinism capabilities and trade-offs. Several of the backends, including the property. Although we show this was adequate for catching viola- built-in Yosys-SMTBMC, verify properties using bounded model tions, we cannot claim that the property was fully machine-verified. checking (BMC) [4], which involves unrolling a bounded number There are also restrictions on the types of circuits that can be of circuit steps into one large SMT query. This query is then passed verified using rtlv. The first restriction is that the circuit may not into an SMT solver such as Z3 to determine satisfiability. contain combinational latches. We find this is not limiting for verify- Like rtlv, SymbiYosys uses the Yosys synthesis tool. However, as ing designs that target FPGAs, since latches are generally considered discussed in Section 3, SymbiYosys encodes execution directly into bad practice in such designs and are therefore avoided [12]. In addi- the solver query, making it less effective for reasoning about many tion, rtlv does not support asynchronous resets or clocks that are cycles of execution than our Rosette-based symbolic execution derived from logic in Verilog—these features can either be removed approach. or transformed into equivalent representations, or the circuit can be preprocessed using the Yosys clk2fflogic pass (which makes the 5.3 Symbolic execution for finding exploits circuit’s Rosette model, and hence the resulting verification code, Zhang and Sturton [19] describes a system for finding exploits of more complex). security vulnerabilities in hardware. Their system generates input A final limitation is that while rtlv can be used to verify prop- traces that will take a processor from its reset state to an error state erties by modeling software execution on hardware, this is lim- that violates a developer-defined security property. It recursively ited to simple embedded applications. We expect rtlv can verify searches from a given error state backwards to reset, generating properties that require executing several hundred lines of C on the input trace in reverse. microcontroller-level hardware, but we do not expect that the cur- Like rtlv, this tool is based on symbolic execution. However, rent design can verify code running on a full operating system with a downside of traditional symbolic execution is that it results in complex hardware. path explosion, since it involves forking execution at every possible branching point. In order to narrow the search space, Zhang and 7 CONCLUSION Sturton employ application-specific heuristics to help the search This paper describes an approach called rtlv for reasoning about converge on the reset state. This works in this case, but Rosette’s hardware using the Rosette solver-aided programming language. symbolic execution uses “type-driven state merging” to prevent path Our design choices and Rosette’s capabilities lend rtlv the ability explosion in general [15], making it useful for efficiently verifying to performantly verify properties that require executing software a wide range of properties. In addition, this work is limited to bug- on hardware for many cycles. hunting for violations of safety properties, and cannot be used to In addition, rtlv’s approach encourages the development of prove that properties hold. reusable circuit-agnostic property checkers that implement per- 5.4 Self-equivalence with don’t-cares formance hints, which are critical for scaling verification to more complicated systems. Existing tools such as SymbiYosys do not Lee and Sakallah [7] presents a hardware verification framework allow for the use of this technique, since they do not provide direct called Averroes. As a case study, this work verifies a property called access to the underlying SMT solver. “self-equivalence with don’t-cares” (or “SEQX”) for a Cortex M0+ rtlv’s symbolic execution-based verification and performance processor. SEQX is equivalent to output determinism as defined hints enabled us to verify that a large hardware system, MicroTitan, in Section 4, showing that Averroes can be used to verify such a satisfies a sophisticated security property, output determinism. This property. However, our case study’s target, the MicroTitan SoC, verification case study successfully found bugs, and demonstrates is more complex than the Cortex M0+ CPU, which contains only that rtlv is an effective approach for verifying such properties.

rtlv: push-button verification of software on hardware

REFERENCES [9] A. Lööw, R. Kumar, Y. K. Tan, M. O. Myreen, M. Norrish, O. Abrahamsson, and [1] E. Alkassar, M. A. Hillebrand, D. Leinenbach, N. W. Schirmer, and A. Starostin. The A. Fox. Verified compilation on a verified processor. In Proceedings of the 40th ACM Verisoft approach to systems verification. In Proceedings of the 2nd International SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Conference on Verified Software: Theories, Tools, Experiments (VSTTE), Toronto, page 1041–1053, Phoenix, AZ, June 2019. Ontario, Canada, Oct. 2008. [10] N. Moroze. [prim_fifo_sync] Make FIFO output zero when empty. https://github. [2] A. Athalye, A. Belay, M. F. Kaashoek, R. Morris, and N. Zeldovich. Notary: A com/lowRISC/opentitan/pull/2420. device for secure transaction approval. In Proceedings of the 27th ACM Symposium [11] N. Moroze. Kronos: Verifying leak-free reset for a system-on-chip with multiple on Operating Systems Principles (SOSP), page 97–113, Huntsville, Ontario, Canada, clock domains. Master’s thesis, Massachusetts Institute of Technology, Jan. 2021. Oct. 2019. [12] Nandland. Tutorial - what is a latch in an FPGA? https://www.nandland.com/ [3] W. R. Bevier, W. A. Hunt Jr., J. S. Moore, and W. D. Young. An approach to systems articles/what-is-a-latch-fpga.html. verification. Journal of Automated Reasoning, 5(4):411–428, Dec. 1989. [13] Z. Snow. sv2v: SystemVerilog to Verilog. https://github.com/zachjs/sv2v, 2020. [4] A. Biere. Bounded model checking. In Handbook of Satisfiability, volume 185 of [14] Symbiotic EDA. SymbiYosys (sby) documentation. https://symbiyosys. Frontiers in Artificial Intelligence and Applications, pages 457–481. 2009. readthedocs.io/en/latest/index.html, 2020. [5] L. de Moura and N. Bjørner. Z3: An efficient SMT solver. In Proceedings of the [15] E. Torlak and R. Bodik. A lightweight symbolic virtual machine for solver-aided 14th International Conference on Tools and Algorithms for the Construction and host languages. In Proceedings of the 35th ACM SIGPLAN Conference on Program- Analysis of Systems (TACAS), pages 337–340, Budapest, Hungary, Mar.–Apr. 2008. ming Language Design and Implementation (PLDI), pages 530–541, Edinburgh, [6] A. Goel and K. Sakallah. AVR: Abstractly verifying reachability. In Proceedings of United Kingdom, June 2014. the 26th International Conference on Tools and Algorithms for the Construction and [16] C. Wolf. Formal verification with SymbiYosys and Yosys-SMTBMC. URL http: Analysis of Systems (TACAS), pages 413–422, Apr. 2020. //www.clifford.at/papers/2017/smtbmc-sby/slides.pdf. [7] S. Lee and K. Sakallah. Unbounded scalable verification based on approximate [17] C. Wolf. PicoRV32 – a size-optimized RISC-V CPU. https://github.com/ property-directed reachability and datapath abstraction. In Proceedings of the 26th cliffordwolf/picorv32, 2020. International Conference on Computer Aided Verification (CAV), pages 849–865, [18] C. Wolf. Yosys Open SYnthesis Suite. http://www.clifford.at/yosys/, 2020. Vienna, Austria, July 2014. [19] R. Zhang and C. Sturton. A recursive strategy for symbolic execution to find [8] lowRISC contributors. Open source silicon root of trust (RoT) | OpenTitan. exploits in hardware designs. In Proceedings of the 2018 ACM SIGPLAN Interna- https://opentitan.org/, 2019. tional Workshop on Formal Methods and Security (FMS), page 1–9, Philadelphia, PA, 2018.