SOURCE ARCHIVE
EXTRACTED CONTENT
50,701 charsProcessor Verification using Symbolic Execution: A RISC-V Case-Study
Niklas Bruns Vladimir Herdt Rolf Drechsler
Institute of Computer Science Institute of Computer Science Institute of Computer Science University of Bremen University of Bremen University of Bremen Bremen, Germany Cyber-Physical Systems Cyber-Physical Systems nbruns@uni-bremen.de DFKI GmbH DFKI GmbH Bremen, Germany Bremen, Germany vherdt@uni-bremen.de drechsler@uni-bremen.de
Abstract—We propose to leverage state-of-the-art symbolic exe- of-the-art fuzzing-based approach is still suceptible to miss corner cution techniques from the Software (SW) domain for processor case bugs as it is an inherently incomplete testing approach. verification at the Register-Transfer Level (RTL). In particular, we Looking again for inspiration in the SW domain, the working utilize an Instruction Set Simulator (ISS) as a reference model and solution to address the issue of finding corner-case bugs efficiently integrate it with the RTL processor under test in a co-simulation setting. We then leverage the symbolic execution engine KLEE is by using the symbolic execution technique. In contrast to fuzzing, to perform a symbolic exploration that searches for functional it is a formal verification technique that allows to execute a pro- mismatches between the ISS and RTL processor. To ensure a gram using symbolic expression, that efficiently represents sets of comprehensive verification process, symbolic values are used to concrete values, and thus enables to explore large state spaces more represent the instructions and also to initialize the register values efficiently and comprehensively [11]. State-of-the-art symbolic ex- of the ISS and processor. As a case study, we present results ecution engines, such as KLEE, have been very effective in finding on the verification of the open source RISC-V based MicroRV32 numerous intricate bugs in SW programs [12]–[14]. Following the processor, using the ISS of the open source RISC-V VP as a reference model. Our results demonstrate that modern symbolic success story from the SW domain, first reaserch approaches start to execution techniques are applicable to a full scale processor co- leverage symbolic execution in the HW domain. However, the focus simulation in the embedded domain and are very effective in is mainly on test-case generation techniques to boost the obtained finding bugs in the RTL core. coverage for general RTL designs [15]–[17]. An effective processor verification methodology using symbolic execution is to the best of I. INTRODUCTION our knowledge not yet available. Verification of the processor at the Register-Transfer Level (RTL) is In this paper, we thus propose to leverage state-of-the-art symbolic crucial since the processor is a key component in every embedded execution techniques for processor verification at the RTL and de- system. Due to its ease of use and scalability, simulation-based scribe an effective open source tool flow that takes the requirements methods still form the primary backbone of the verification effort. of a modern system design flow into account. In particular, we Moreover, modern design flows for embedded systems rely on utilize an ISS, which is readily available as a C++ description in Virtual Prototypes (VPs) as a reference model for the Hardware a modern VP-based design flow, and integrate it with the RTL pro- (HW) development stage. Regarding the processor, the relevant cessor under test in a co-simulation setting using a testbench. The component of the VP is the Instruction Set Simulator (ISS), which testbench is designed to provide the same instructions to the ISS is an abstract model of the processor and thus fetches, decodes and processor, and compare the register values after execution. To and executes one instruction after another. To generate processor- ensure a comprehensive verification process, symbolic values are level input stimuli several test generation techniques have been used to represent the instructions and also to initialize the register proposed that improve upon the classical randomized instruction values of the ISS and the processor. Following a standard RTL stream generation. A notable direction is the model-based approach design flow, we assume that the processor description is available that relies on a constraint-based specification to guide the test gen- in Verilog, which is then translated into a C++ description using the eration process [1]–[3]. Further optimizations have been proposed open source verilator tool. As such the RTL processor can be inte- by propagating constraints among multiple instructions in a more grated with the C++ ISS in a combined C++ co-simulation. We then effective way [4]. However, model-based approaches require sig- leverage the open source C++ symbolic execution engine KLEE nificant effort to provide a respective input format specification. A to perform a symbolic exploration according to the co-simulation recent trend, that tries to mitigate this issue, is to leverage automated setting. We designed dedicated symbolic execution interfaces in verification techniques from the SW domain and apply them in our testbench to enable such an integration and as such we can the HW domain. A particular effective technique in this regard is benefit from the vast symbolic execution optimizations that KLEE fuzzing [5], [6]. Modern coverage-guided fuzzer work by mutating provides. As a case study, we present results on the verification randomly created data and are guided by coverage, hence they do of the open source RISC-V based MicroRV32 processor1. We use not require an input model specification [7], [8]. Fuzzing has been the ISS from the open source RISC-V VP2 as functional reference shown very effective for processor-level stimuli generation [9] and model for the MicroRV32 processor. Our results demonstrate that by using an ISS as reference model for the RTL processor under modern symbolic execution techniques are applicable to a full scale test, an effective fuzzing-based processor verification methodology 1Available at GitHub https://github.com/agra-uni-bremen/microrv32. is obtained [10]. However, while being very effective, even a state- 2 Available at GitHub https://github.com/agra-uni-bremen/riscv-vp.
processor co-simulation in the embedded domain and are very IV. PROCESSOR VERIFICATION USING SYMBOLIC effective in finding bugs in the RTL core. EXECUTION II. RELATED WORK In this section, we present our proposed processor verification As mentioned in the introduction, symbolic execution techniques, approach, which is based on co-simulation and symbolic execution. which have been very effective in the SW domain, are increasingly We start with a general overview and then describe the relevant parts leveraged to tackle problems in the HW domain. One important in more detail. research direction is to automatically generate test cases that im- A. Overview prove the coverage of the HW under test. [18] present an approach based on static analysis in combination with symbolic execution Fig. 1 shows an overview on our approach. The complete flow techniques applied on execution traces of the RTL design to sys- starts with a SpinalHDL processor description and a C++ ISS tematically drive up the branch coverage. [15] propose applying description (left side of Fig. 1). SpinalHDL is an open-source high- symbolic execution tools from the SW domain to generate test level hardware description language that is based on Scala. It aims vectors for RTL designs and evaluate their approach using a floating to give the hardware designers a tool to design a new abstraction point unit. [16] present a control flow graph assisted approach level to create reusable code [28]. Popular open source processor that enables to guide the symbolic execution engine in uncov- implementations that are based on SpinalHDL are VexRiscV [29] ering specific remaining coverage targets. [17] describe further and MicroRV32 [30]. Next, the SpinalHDL processor description optimizations to boost scalability by avoiding overlapping searches is configured based on the configuration description and translated involving multiple coverage targets. Beside test vector generation using the Scala Build Tool (SBT) into an RTL core. Likewise, to improve the coverage, another research direction that employs the C++ ISS description is configured into a C++ ISS. Because symbolic execution techniques at the RTL is the security evaluation the RTL core and the C++ ISS are configured based on the same of the design. [19] present a method for exploits generation by processor configuration description, the RTL core and the C++ using a backward symbolic execution approach based on a set of should behave in the same way at the functional level. Next, security-critical invariants. [20] describe an approach that works the RTL core is transcompiled (verilated) into a cycle-accurate by adding security-critical assertions into the RTL design and then C++ equivalent using the open source tool named verilator [31]. show that leveraging symbolic execution is effective in detecting The transcompiled RTL core (C++) and ISS (C++) are combined assertion violations. However, an effective processor verification with the co-simulation main and compiled into bytecode using the methodology using symbolic execution at the RTL in combination LLVM toolchain to create the processor co-simulation (right side with a VP-based reference model, as proposed in our paper, is to of Fig. 1). The co-simulation contains the processor and ISS bind- the best of our knowledge not yet available. ings, symbolic execution interface, instruction stream, symbolic Classic formal verification approaches targeting RTL designs rely memory & registers, and a voter that compares the functionality of on HW model checking techniques that verify the design against the ISS and the RTL core. The symbolic processor co-simulation is a set of properties specified in temporal logic, e.g. [21]–[23]. The executed on the C++ symbolic execution engine KLEE to generate most notable approach for formal RISC-V processor verification test vectors in order to find bugs and create a high coverage test set. is RISCV-formal. It is a framework for formal verification based The essential components of the co-simulation are described in the on Bounded Model Checking (BMC) [24]. For the verification, following subsection in detail. RISC-V-formal needs complex formal models as a reference, and B. Symbolic Co-Simulation our approach only requires a C++ description already used in Virtual Prototypes. Virtual Prototypes can be used for the rapid In the following, we describe the essential parts of the co- development of new functionality and debugging. Furthermore, simulation. The co-simulation main loop consists of the following RISCV-formal is incapable to find implementation mismatches parts: the initialization of the symbolic memory and sliced symbolic between an ISS and a RTL processor implementation. These mis- registers, the handling of the Data Bus (DBus) and Instruction Bus matches complicate debugging and can lead to subtle HW/SW (IBus) of the RTL Core and the connection to the symbolic memory, interaction errors that may lead to security vulnerabilities. And the monitoring of the RTL core execution behavior, including last but not least, RISCV-formal does not support Control and the determination of the complete initialization, execution of ISS Status Registers (CSRs). Consequently, our symbolic execution steps and comparison of the execution results (Voter), and the en- based approach, is complementary to classical formal verification forcement of runtime limitations (Execution Controller). Next, we approaches. describe the symbolic execution interface, the symbolic memory, III. BACKGROUND ON RISC-V and the sliced symbolic registers. Last but not least, we describe the voter and execution controller. RISC-V is an open and royalty-free Instruction Set Architecture (ISA). It has a modular design and is popular in industry and C. Symbolic Memory & Registers academia. The RISC-V specification is administered by the non- In the following, we describe our symbolic memory and registers. profit RISC-V International association, which was founded in The IBus and DBus are separated in many processor implemen- 2015 [25]. The RISC-V specification is divided into two volumes. tations to avoid performance bottlenecks. Therefore the symbolic The first part is the unprivileged specification [26]. The heart of memory consists of the symbolic instruction and the symbolic RISC-V is the instruction set I that is available in 32bit, 64bit, and data memory. The symbolic execution interface is used to con- 128bit versions. RISC-V has additional instruction set extensions nect the symbolic memory and the symbolic execution engine. like Multiply/divide (M) or Compressed instruction (C). The second The symbolic interface in our approach contains the functions volume is called the privileged architecture [27]. It contains all klee make symbolic and klee assume of the symbolic execution components needed for the hardware-software interactions like engine KLEE. The function klee make symbolic is used to mark Control and Status Registers (CSRs) for hardware identification, a variable as symbolic. The function arguments are the variable trap handling, and performance measurement. address, the variable size in bytes, and a freely choosable name
Spinal HDL Co-Simulation
Processor Description Instruction Stream Translated RTL-Core
SBT RTL Core Verilator RTL Core Symbolic Memory Regs
(Verilog) (C++) V
Symbolic o
Execution t
Co-Simulation Interface e
Processor Configuration Main / Bindings LLVM-Toolchain r Description & C++ Library Symbolic Memory Regs
Configurator ISS Instruction Stream ISS
(C++)
Testvector
C++ ISS Description Symbolic Execuction Engine Testvector (KLEE) Testvector
Fig. 1. Overview on our proposed processor verification using a symbolic co-simulation
for the variable [32]. The function klee assume(condition) is used example is the native bus interface of the RISC-V processor named
to constrain the symbolic variables and adds the condition to PicoRV32 [36]. If the RTL core wants to load data at a memory
the current path constraints [33]. Next, we describe the symbolic address, the core enables the signal DMem enable and writes the
instruction memory, the symbolic data memory and last but not least requested address into the signal DMem address. Additionally, the
the sliced symbolic registers. core sets the signal DMem wrStrobe. The strobe value identifies
1) Symbolic Instruction Memory: The symbolic instruction which of the 32-bytes at the address should be accessed. Valid
memory is the memory that provides the instructions for the co- strobe values are 0001, 0010, 0100 and 1000 to access a byte, 0011
simulation. The instruction memory is read-only and shared be- and 1100 to access a half word and 1111 to access a full word.
tween the RTL core and the ISS. It is connected via the IBus to the The symbolic co-simulation main loop redirects the request to the
RTL core and is directly connected to the ISS. If the RTL core wants strobe based interface of the symbolic data memory. The strobe
to fetch an instruction at a specific memory address, it sets the signal based interface has a load and a store function. As arguments, this
IMem address and enables the signal IMem fetchEnable. The co- two functions have a combination of memory address and strobe.
simulation main redirects the request to the symbolic instruction In opposite to the ISS binding, the strobe based interface does not
memory. The symbolic instruction memory checks if the instruction handle the signed/unsigned convertation. Next, the main loop writes
at this specific address was already generated and cached. This be- the data into the signal DMem readData and enables the signal
havior guarantees that the RTL and ISS are always supplied with the DMem dataReady. Again, the symbolic co-simulation main loop
same instructions to prevent false mismatches. A new instruction must disable the signal DMem dataReady i.e., after one clock cycle
is generated using the symbolic execution engine if the instruction to comply with the bus protocol. In the following, we describe the
was not already generated. Therefore, the new instruction variable sliced symbolic registers.
is marked as symbolic using the function klee make symbolic. 3) Sliced Symbolic Registers: For processor verification, every
Depending on the test scenario, klee assume is used to constrain instruction should be tested with arbitrary values to cover all pro-
the instruction generation. Next, the co-simulation main writes the cessor instruction functionalities. Because RISC-V is a load/store
generated instruction into the signal IMem instruction and enables architecture, most instructions receive their values exclusively from
IMem instructionReady. The symbolic co-simulation main loop the registers. Only the load and store instructions can access the
must disable the signal IMem instructionReady i.e., after one clock memory. Thus, it would be sufficient to fill only the memory with
cycle, to comply with the bus protocol. Next, we describe the symbolic values because symbolic values can be loaded from the
symbolic data memory. symbolic memory into the registers, and from there, these symbolic
2) Symbolic Data Memory: The symbolic data memory is the values can be propagated further. However, this would have the
memory that provides the data for the cross-processor verification. disadvantage that the length of the instruction trace would have
The data memory can be read and written and is separated for the to be at least two to test all instruction functionalities. A minimal
RTL core and the ISS. It is connected via the DBus to the RTL instruction trace length of two would unnecessarily increase the
core and directly to the ISS. The memory sizes of both are the same state space of the verification problem. To solve this problem, we fill
and they are initialized with the same symbolic values in order to the registers with symbolic values. However, simply filling the bank
prevent false mismatches. The data memory interface of the ISS has register would also unnecessarily increase the verification problem
dedicated functions to load byte, ubyte, half, uhalf and word, and to because the register bank in RISC-V contains 32 32bit values. In
store byte, half and word. For example, the ISS load byte function order to keep the verification state space as small as possible, we
has the goal to load a signed byte at the address of the symbolic slice the registers into three parts. The first slice of RISC-V contains
memory. It loads a signed 8bit value and sign extends it into a signed the register x0. According to the specification, the x0 register is
32bit value. The signed extension for the RTL core is handled by hardwired to zero. Thus this register cannot be symbolic in order
the RTL core itself. The DBus interface is based on a strobe logic to keep the verification approach sound. The next slice consists of
that is a known logic and used e.g: by AXI that is a ARM Bus the symbolic registers. These registers are initialized with arbitrary
standard [34] or by the open Wishbown bus standard [35]. Another values to verify every case of the processor instructions. After
the initialization, the register can be read and written like regular TABLE I registers. This part should be sufficiently large but not larger than CO-SIMULATION RESULTS (R), SHOWS THE ERRORS (E) AND MISMATCHES needed to keep the state space small. In the last slice are the regular (M) IN MICRORV32 AND THE VP (E*) registers, which can be written and read normally. For a processor Instruction & CSR Example Description R that implements RV32I, it is perfectly adequate to have only two LW LW x0, x0, 0x1 Missing alignment check M LH LH x0, x0, 0x1 Missing alignment check M symbolic registers and fill the rest of the symbolic register bank LHU LHU x0, x0, 0x1 Missing alignment check M with regular registers because no RV32I instruction has more than SW SW x0, x0, 0x1 Missing alignment check M SH SH x0, x0, 0x1 Missing alignment check M two source registers. Next, we describe the voter and the execution SHU SHU x0, x0, 0x1 Missing alignment check M WFI WFI Missing WFI instruction E controller of our symbolic co-simulation. unimpl. CSRs csrrwi x0, 0, 0x400 Missing trap at access E marchid csrrci x1, 1, marchid Missing trap at write E D. Voter & Execution Controller mvendorid csrrw x0, x0, mvendorid Missing trap at write E mhartid csrrs x1, x1, mhartid Missing trap at write E mideleg csrrw x1, x0, mideleg VP traps at mideleg read E* The voter is based on the RISC-V Formal Interface (RVFI) [37]. medeleg csrrwi x1, 0, medeleg VP traps at medeleg read E* RFVI is part of the riscv-formal [24] framework for formal verifi- mip csrrw x0, x0, mip Trap at write access E mcycle csrrw x0, x0, mcycle Trap at write access E cation of RISC-V processors, which allows to observe the execution mcycle csrrw x1, x0, mcycle Cycle Count Mismatch M state of the processor at runtime. After the RTL core has executed minstret csrrw x2, x0, minstreth Trap at write access E minstret csrrw x1, x0, minstret Cycle Count Mismatch M an instruction, the rvfi valid signal is enabled. The other signals mcycleh csrrw x0, x0, mcycleh Trap at write access E deliver the execution results as long as this signal is enabled. The minstreth csrrw x0, x0, minstreth Trap at write access E cycle csrrsi x1, 0 unimpl. Unprivileged CSR M results contain values like the actual and old PC and the value of the cycleh csrrsi x2, 0 unimpl. Unprivileged CSR M instret csrrsi x0, 0, instret unimpl. Unprivileged CSR M target register of the executed instruction. Next, the ISS follows up instreth csrrsi x0, 0, instreth unimpl. Unprivileged CSR M and executes the current instruction. After the execution, the voter time csrrsi x2, 0, time unimpl. Unprivileged CSR M timeh csrrsi x2, 0, timeh unimpl. Unprivileged CSR M compares the execution results of the RTL core and the ISS. If there mhpmcounter3-31 csrrw x0, x0, mhpmcounter16 unimpl. Privileged CSR M was an execution mismatch, the voter throws an exception and quits mhpmcounter3-31h csrrw x2, x0, mhpmcounter3h unimpl. Privileged CSR M mhpmevent3-31 csrrw x3, x2, mhpmevent16 unimpl. Privileged CSR M the simulation. If no mismatches were found, the simulation would mscratch csrrw x1, x2, mscratch unimpl. Privileged CSR M be terminated after the instruction limit or clock cycle limit was mcounteren csrrwi x1, 0, mcounteren unimpl. Privileged CSR M reached. After the simulation, the model will be cleaned up, and the memory is freed. In the following, we describe the evaluation of our execution requires more than 30 days of runtime. The results of processor verification approach. our experiment, in finding errors and mismatches, are listed in V. EVALUATION Table I. The first column of the table states the instruction or the This section presents our case study and discusses the evaluation Control and Status Register (CSR) that is responsible for the error results. Our case study aims to evaluate the applicability of sym- or mismatch (column: Instruction & CSR). The second column bolic execution in combination with a co-simulation for cross-level shows an example instruction that triggers the error or mismatch processor verification. The co-simulation for our case-study uses (column: Example). The next column contains a short description the MicroRV32 processor [30] as Device Under Test (DUT) and of the found error or mismatch (column: Description). Finally, the the ISS from the open-source RISC-V VP [38] as reference imple- last column (column: R) classifies the result as being an error in mentation. As instruction set we consider the RV32I+CSR ISA that the RTL core (E), an error in the ISS (E*), or an implementation is supported by MicroRV32. The MicroRV32 processor already has mismatch between RTL core and ISS (M) due to multiple possible been extensively tested using constrained random techniques [39] valid implementations according to the RISC-V ISA. All the results and was also verified using the RISC-V formal [24] tool, which are reported to and have been directly confirmed by the author applies a Bounded Model Checking (BMC) approach. of MicroRV32. In the following, we describe the listed errors and Our case study is structured into two parts. In the first part we report mismatches in more detail. The RV32I load and store Instructions the results we obtained on verifying the MicroRV32 core. In the LW, LH, LHU, SW, SH, and SHU are used to load and store data second part of our case study, we aim to evaluate the symbolic ver- from and to the memory. The processor has multiple permissible ification performance using a representative set of injected RV32I handling options, according to the RISC-V ISA, if the memory errors. All experiments of the two parts are conducted on a Linux address is misaligned. For example, a core can raise a trap or fully server with an Intel Xeon Gold 6240 CPU. Next, we will start with support misaligned loads and stores. The implementations of the the first part of our evaluation. ISS and the RTL core have a mismatch in handling this behavior. The RTL core fully supports misaligned loads and stores, and the A. Case Study: Symbolic Verification of MicroRV32 ISS checks for misaligned addresses and raises traps. The Wait for Interrupt instruction (WFI) is defined in the RISC-V privileged ar- In this section we present the first part of our case study that aims chitecture and is available in all privileged modes. This instruction to verify MicroRV32I using the instruction subset RV32I+CSR. aims to hint to the implementation that the current core can stop In particular we report and discuss all the mismatches and errors execution until an interrupt arrives. As the specification states, it that we have found by continously applying our co-simulation is also legal to implement the instruction as a NOP. The RTL core based approach. In this process we observed that mismatches implementation contains the error that the WFI is not implemented and errors can often be detected rather quickly (we will provide at all, and an attempted execution erroneously raises a trap. If a CSR further information on runtime results in the next section) but instruction wants to access non-existent CSRs, the implementation a more comprehensive exploration can take significantly longer must raise an illegal instruction exception. The RTL core is not runtime. An exemplary execution in this regard had a runtime of compliant to the specification, because it does not raise an exception 586905 seconds, executed 101434788 instructions, explored 848 in this case. Each core has the following read-only ID registers: paths completely and 408 paths partially, and generated a total Machine Architecture ID Register (marchid), Machine Vendor ID of 1256 test cases. Please note that the need for sliced symbolic Register (mvendorid), and Hart ID Register (mhartid). According registers is evidenced by the fact that a non-optimized symbolic to the specification, an illegal instruction exception must be raised
if a write attempt to a read-only CSR occurs. The RTL core does E6: RV32I provides multiple conditional branch operations. The not raise these mandatory illegal instruction exceptions. All traps at injected error E6 changes the behavior of Branch Not Equal (BNE) any privilege level are default handled in machine mode. In order into the behavior of Branch Equal (BEQ). to increase performance, the core implementations can provide E7: The next fault flips the endianness of the Load Byte Unsigned individual bits in the read-write CSRs medeleg (exceptions) and (LBU) memory access instruction. mideleg (interrupts) to delegate the handling to a lower privilege E8: The injected error F8 removes the sign extension from 8-bits to level. The ISS implementation is erroneous because it raises a 32-bits in the memory instruction Load Byte (LB). trap at every read attempt of medeleg and mideleg. The Machine E9: The memory instruction Load Word (LW) loads a 32-bit value. Interrupt Register mip and the Machine Counters: mcycle, minstret, With Fault E9, the LW instruction only loads the lower 16-bits from mcycleh, minstreth have one thing in common: they can be written. memory. The RTL core has the error that it raises a trap at every write access In our experiments, we use a runtime limit of 24 hours. The to the previously described CSRs. In order to enable performance processor co-simulation is configured to support RV32I. In this monitoring, the RISC-V machine mode provides machine cycle experiments, we only used assumptions that block the generation counters. Examples of these CSRs are the mcycle CSR that counts of CSR instructions (which are not a part of RV32I) to filter the the number of executed clock cycles, and the minstret CSR that known implementation mismatches that were found in the first part counts the number of retired instructions. The ISS and the RTL core of the case study. both implement these CSRs but have a deviating counting logic. Table II shows the results of our experiments in finding E0 to E9. This deviating logic is no error but only a mismatch because the The table allows the comparison between the symbolic execution detailed behavior is not specified (mismatches in the cycle count runs for the respective injected errors and also allows the compari- are actually expected due to the abstract, non-cycle accurate, timing son of the respective runs with the instruction limit of one and the model in the ISS). Other mismatches are the results of the fact, that respective runs with the instruction limit of two. The first column of the ISS implements much more performance counters than the RTL the table states the injected errors. The next five columns contain the core. The ISS additionally implements the unprivileged counter: cy- results with an instruction limit of 1. The column result describes cle, cycleh, instret, instreth, time, timeh, and the Machine Counter whether the injected error was found. The next column with the mhpmcounter3-31, mhpmcounter3-31h. Furthermore, the RTL core name executed instruction contains the counter of the executed does not implement the Machine Counter Setup CSR mhpmevent3- instructions until the error was found. The column time contains 31, Machine Scratch CSR mscratch, and the Machine Counter- the time in seconds until the error was found. The column with Enable Register mcounteren. Due to the large degree of different the name partial paths contains the number of partially completed valid implementation choices that the RISC-V ISA offers, it is im- explored symbolic execution paths by KLEE. This number contains portant to have effective methods available that detect mismatches the paths that KLEE could not complete. This can be the case in order to support the designer in providing an exactly matching because time or memory constraints were reached, or an assertion configuration of ISS and RTL core. In the following, we describe was triggered inside the voter that quit the test generation. The the second part of our evaluation. paths column contains the number of complete explored symbolic execution paths by KLEE. The following five columns contain B. Performance Evaluation with Injected Errors the results for the same experiment but with an instruction limit of 2. It is striking that our symbolic cross-processor verification In order to evaluate the performance of our verification approach we approach can find all injected errors very quickly, independent of use a error-injection methodology. In particular, we have defined the configuration. Please note, all times are given in seconds (s). a set of 10 error (E0 to E9) that cover a broad range of different The first configuration with the instruction limit of 1, executed functionality in the RTL core and represent common errors that may between 2239208 and 12367140 instructions and needed between occur during the implementation. 54s and 3237s until it found the injected error. In median, 4237517 E0: The first injected error is a fault in the decoding behavior of instructions were executed within a period of 543s and in total, the logical left shift RV32I instruction SLLI. The highest bits of the this configuration executed 53283172 instructions within 9685s. instruction encoding are 7-bits with the value 0. SLLIW is a RV64I The second configuration with the instruction limit of 2, executed instruction that has the same encoding as the RV32I instruction between 2182018 and 33959660 instructions and needed between RV32I. The RV64I specification also contains a reserved instruction 65s and 21994s until it found the injected error. In median, 4560215 that has nearly the same encoding with only the difference, that instruction were executed within a period of 790s and in total, this the 7th highest bit has the value 1. As E0 we injected a don’t care configuration executed 88712782 instructions within 37201s. As bit in the decoding table of the instruction SLLI at the 7th highest can be easily seen, the first configuration (instruction limit 1) was bit. Thus, the processor decodes the reserved RV64I erroneously to faster than the second configuration (instruction limit 2). Although SLLI. both configurations found the errors very efficiently, it is likely E1: Similar to E0, we marked the same encoding bit as don’t care that the instruction limit should be set as low as possible and only in the logical right shift instruction RV32I SRLI. increased incrementally for processor verification. E2: Also in the logical right shift instruction RV32I SRLI, we In summary, we demonstrated that symbolic cross-level processor marked the same bit as don’t care. verification is an efficient approach for bug hunting. During the E3: The next injected error is a STUCK-at-0 fault at the lowest development process we have been able to find 10 errors in the result bit in the arithmetic add immediate instruction ADDI. well-tested RTL-core MicroRV32, 2 errors in the ISS, as well as E4: In the subtraction instruction SUB we injected a STUCK-at-0 19 implementation mismatches between the RTL core and the ISS fault at the highest result bit. (as discussed in the first case study part in Section V-A). Our error- E5: The next fault is injected into the unconditional jump instruc- injection based performance evaluation in this section confirms the tion Jump And Link (JAL). The injected error F5 prevents that JAL strong bug hunting capabilities of our approach. does change the PC.
TABLE II
INJECTED ERROR RESULTS
Instruction Limit: 1 Instruction Limit: 2
Error Result # Exec. Instr. Time [s] Partial Paths Paths Result # Exec. Instr. Time [s] Partial Paths Paths E0 3 2239482 54 63 0 3 2182018 65 64 0 E1 3 2239208 93 63 0 3 2182192 66 63 0 E2 3 2239208 55 63 0 3 2182416 66 63 0 E3 3 3122286 303 77 1 3 2957146 400 98 0 E4 3 3178044 311 78 0 3 2568932 247 68 0 E5 3 10754876 2960 72 55 3 22948714 10527 2321 16 E6 3 5296990 775 98 8 3 6163284 1179 609 4 E7 3 5912722 947 92 15 3 6792846 1325 729 5 E8 3 5933216 950 92 15 3 6775574 1332 727 5 E9 3 12367140 3237 60 72 3 33959660 21994 2876 27 Sum: 10 3 53283172 9685 758 166 10 3 88712782 37201 7618 57 Median: 4237517 543 75 5 4560215 790 354 2
VI. CONCLUSION AND FUTURE WORK [16] A. Ahmed, F. Farahmandi, and P. Mishra, “Directed test generation using
Our symbolic verification methodology revealed 10 bugs in the well [17] concolic testing on rtl models,” in DATE, 2018, pp. 1538–1543.
tested RTL-core MicroRV32 and found 2 errors in the reference Y. Lyu and P. Mishra, “Scalable concolic testing of rtl models,” IEEE
Transactions on Computers, vol. 70, no. 7, pp. 979–991, 2021.
ISS. Moreover, our error-injection methodology further underlines [18] L. Liu and S. Vasudevan, “Efficient validation input generation in rtl by
the effective bug hunting capabilities of our approach. Thus, the hybridized source code analysis,” in DATE, 2011, pp. 1–6.
results demonstrate the applicability of symbolic execution in full [19] R. Zhang, C. Deutschbein, P. Huang, and C. Sturton, “End-to-end
scale processor co-simulation. For future work we plan to focus automated exploit generation for validating the security of processor
designs,” in 2018 51st Annual IEEE/ACM International Symposium on
on hybrid techniques combining symbolic execution with fuzzing Microarchitecture (MICRO), 2018, pp. 815–827.
to provide a scalable and comprehensive verification methodology. [20] R. Zhang and C. Sturton, “A recursive strategy for symbolic execution
Moreover, we want to investigate the specification of induction- to find exploits in hardware designs,” in Proceedings of the 2018 ACM
SIGPLAN International Workshop on Formal Methods and Security, 2018,
based symbolic constraints to enable a complete processor verifica- p. 1–9.
tion that is not relying on a bounded model checking methodology. [21] P. Bavonparadon and P. Chongstitvatana, “Rtl formal verification of em-
Acknowledgments: This work was supported in part by the German Federal bedded processors,” in 2002 IEEE International Conference on Industrial
Ministry of Education and Research (BMBF) within the project Scale4Edge [22] Technology, 2002. IEEE ICIT ’02., 2002, pp. 667–672 vol.1.
under contract no. 16ME0127, within the project VerSys under contract no. S. Deng, W. Wu, and J. Bian, “Bounded model checking for rtl circuits
01IW1900, and within the project ECXL no. 01IW22002. based on algorithm abstraction refinement,” in 2006 8th International Conference on Solid-State and Integrated Circuit Technology Proceedings, REFERENCES [23] 2006, pp. 2082–2084. [1] A. Adir, E. Almog, L. Fournier, E. Marcus, M. Rimon, M. Vinov, A. Goel and K. Sakallah, “Model checking of verilog rtl using ic3 with and A. Ziv, “Genesys-pro: innovations in test program generation for syntax-guided abstraction,” in NASA Formal Methods, J. M. Badger and functional processor verification,” D&T, pp. 84–93, 2004. [24] K. Y. Rozier, Eds., 2019, pp. 166–185. [2] B. Campbell and I. Stark, “Randomised testing of a microprocessor model “RISC-V formal verification framework,” https://github.com/YosysHQ/ using SMT-solver state generation,” in Formal Methods for Industrial [25] riscv-formal, 2020. Critical Systems, F. Lang and F. Flammini, Eds., 2014, pp. 185–199. “About risc-v,” 2022, accessed: 2022-07-14. [Online]. Available: [3] R. Emek, I. Jaeger, Y. Naveh, G. Bergman, G. Aloni, Y. Katz, M. Farkash, [26] https://riscv.org/about/ I. Dozoretz, and A. Goldin, “X-gen: a random test-case generator for A. Waterman and K. Asanovi´c, Eds., The RISC-V Instruction Set Manual; systems and socs,” in HLDVT, 2002, pp. 145–150. [27] Volume I: Unprivileged ISA, 2019. [4] Y. Katz, M. Rimon, and A. Ziv, “Generating instruction streams using ——, The RISC-V Instruction Set Manual; Volume II: Privileged Archi- abstract CSP,” in DATE, 2012, pp. 15–20. [28] tecture, 2019. [5] “Microsoft security development lifecycle,” https://www.microsoft.com/ “Welcome to spinalhdl’s documentation! — spinalhdl documentation,” en-us/sdl/process/verification.aspx, 2018. 2022, accessed: 2022-07-14. [Online]. Available: https://spinalhdl.github. [6] “Oss-fuzz - continuous fuzzing for open source software,” https://github. [29] io/SpinalDoc-RTD/v1.3.1/index.html com/google/oss-fuzz, 2018. “Vexriscv,” 2018, accessed: 2022-07-14. [Online]. Available: https: [7] “libFuzzer - a library for coverage-guided fuzz testing,” https://llvm.org/ [30] //github.com/SpinalHDL/VexRiscv docs/LibFuzzer.html, 2018. S. Ahmadi-Pour, V. Herdt, and R. Drechsler, “Mircorv32: an open source [8] “american fuzzy lop,” http://lcamtuf.coredump.cx/afl/, 2018. risc-v cross-level platform for education and research,” in Proceedings of [9] L. Martignoni, R. Paleari, G. F. Roglia, and D. Bruschi, “Testing CPU [31] the Workshop on Design Automation for CPS and IoT, 2021, pp. 30–35. emulators,” in ISSTA, 2009, pp. 261–272. “verilator,” 1994, accessed: 2022-07-14. [Online]. Available: https: [10] N. Bruns, V. Herdt, D. Große, and R. Drechsler, “Efficient cross-level [32] //www.veripool.org/verilator/ processor verification using coverage-guided fuzzing,” in GLSVLSI, 2012. “Tutorial one: Testing a small function,” 2014, accessed: 2022-07-14. [11] R. Baldoni, E. Coppa, D. C. D’elia, C. Demetrescu, and I. Finocchi, “A [33] [Online]. Available: https://klee.github.io/tutorials/testing-function/ survey of symbolic execution techniques,” ACM Comput. Surv., 2018. “Overview of the main klee intrinsic functions,” 2014, accessed: [12] C. Cadar, D. Dunbar, and D. R. Engler, “KLEE: unassisted and automatic [34] 2022-07-14. [Online]. Available: https://klee.github.io/docs/intrinsics/ generation of high-coverage tests for complex systems programs,” in “Amba axi protocol specification version c: Write strobes,” 2003, OSDI, 2008, pp. 209–224. accessed: 2022-07-14. [Online]. Available: https://developer.arm.com/ [13] V. Chipounov, V. Kuznetsov, and G. Candea, “S2E: a platform for in-vivo [35] documentation/ihi0022/c/Data-Buses/Write-strobes multi-path analysis of software systems,” in ASPLOS, 2011, pp. 265–278. A. Cicuttin, “Introduction to the wishbone bus interface,” 2012, [14] Y. Shoshitaishvili, R. Wang, C. Salls, N. Stephens, M. Polino, A. Dutcher, accessed: 2022-07-14. [Online]. Available: https://indico.ictp.it/event/ J. Grosen, S. Feng, C. Hauser, C. Kr¨ugel, and G. Vigna, “SOK: (state of) [36] a11204/session/35/contribution/22/material/0/0.pdf the art of war: Offensive techniques in binary analysis,” in IEEE S & P, “Picorv32 - a size-optimized risc-v cpu,” 2019, accessed: 2022-07-14. 2016, pp. 138–157. [37] [Online]. Available: https://github.com/YosysHQ/picorv32 [15] Y. Zhang, W. Feng, and M. Huang, “Automatic generation of high- “RISC-V formal interface (rvfi),” https://github.com/SymbioticEDA/ coverage tests for rtl designs using software techniques and tools,” in [38] riscv-formal/blob/master/docs/rvfi.md, 2020. 2016 IEEE 11th Conference on Industrial Electronics and Applications V. Herdt, D. Große, H. M. Le, and R. Drechsler, “Extensible and (ICIEA), 2016, pp. 856–861. [39] configurable RISC-V based virtual prototype,” in FDL, 2018. “RISCV-DV,” https://github.com/google/riscv-dv, 2020.