EPEX: Processor Verification by Equivalent Program Execution

    Lucas Klemmer                                                                                  Daniel Große

Institute for Complex Systems Institute for Complex Systems Johannes Kepler University Johannes Kepler University Linz, Austria Linz, Austria lucas.klemmer@jku.at daniel.grosse@jku.at ABSTRACT 1 INTRODUCTION Verifying processors has been and still is a major challenge. There- With the advent of the RISC-V Instruction-Set Architecture (ISA) [29, fore, intensive research has led to advanced verification solutions 30] and the principles of open-source arriving in the semiconductor ranging from ISS-based reference models, (cross-level) simulation industry, teams started to design their own processor or accelera- down to formal verification at the RTL. During the verification of tor as RISC-V is a free and open ISA. The RISC-V ISA standard is the processor implementation at the Instruction Set Architecture maintained by the non-profit RISC-V foundation. Moreover, con- (ISA) level, test stimuli, i.e. test programs are needed. They are figurability and extendability were important design factors of the either created manually or with the aid of sophisticated test pro- RISC-V ISA. However, while this opens up a lot of opportunities, gram generators. However, significant effort is required to produce two major issues occur: (1) there is not much field-proven verifi- thorough test programs. cation experience for RISC-V processors and (2) the flexibility of In this paper, we devise a novel approach for processor verifi- the RISC-V ISA wrt. ISA extensions results in significant additional cation by Equivalent Program EXecution (EPEX). Our approach is verification effort. During processor design, effective verification of based on a new form of equivalence checking: Instead of compar- the Register Transfer Level (RTL) implementation at the ISA level is ing the architectural states of two models which execute the same a mandatory task. Here, instructions are checked on the complete program 𝑃 , we derive a second, but equivalent program ˆ𝑃 from 𝑃 processor and this also includes initialization code/boot code, pe- (wrt. to a formal ISA model), and check that executing 𝑃 and ˆ𝑃 will ripheral access etc. Hence, at the ISA level test programs (binaries) produce equal architectural states on the same design. We show are needed which are simulated on the design. While they are still that EPEX can easily be used in a simulation-based verification very often created manually, also methods for automatic generation environment and broadens existing tests automatically. In a RISC-V of test programs have been proposed to allow for thorough verifi- case study using different core configurations of the well-known cation. Prominent examples include approaches using constraint VexRiscv core, we demonstrate the bug-finding capabilities of EPEX. solving techniques, guided random generation, or approaches such as quick error detection. We provide more details in the discussion CCS CONCEPTS on related work. Overall, however, significant effort is required to • Hardware → Integrated circuits; Equivalence checking; Sim- produce thorough test programs. ulation and emulation; • Computer systems organization → In this paper, we devise a novel approach for processor verifica- Architectures. tion by Equivalent Program EXecution (EPEX). Our approach is based on a new form of equivalence checking: Instead of com- KEYWORDS paring the architectural states of two models which execute the same program 𝑃 , we iteratively perform two integrated steps for Processor Verification, Formal ISA model, RISC-V, Equivalence verification: (1) We replace a single instruction of 𝑃 by one or more Checking, Functional Verification, Simulation instructions; more formally, we locally determine for the next to be executed instruction 𝑃𝑖 of 𝑃 an equivalent instruction sequence ACM Reference Format: 𝑃ˆ𝑖 𝑗 of length 𝑗 . For this task, we have created a formal ISA model1 Lucas Klemmer and Daniel Große. 2021. EPEX: Processor Verification by for which we constrain the current architectural state and next Equivalent Program Execution. In Proceedings of the Great Lakes Symposium architectural state when executing 𝑃𝑖 , and eventually make use of on VLSI 2021 (GLSVLSI ’21), June 22–25, 2021, Virtual Event, USA. ACM, New an Satisfiability Modulo Theories (SMT) solver. (2) we check that York, NY, USA, 6 pages. https://doi.org/10.1145/3453688.3461497 executing 𝑃ˆ𝑖 𝑗 and 𝑃𝑖 will produce equal architectural states on the same design. This general procedure of EPEX provides improved processor Permission to make digital or hard copies of all or part of this work for personal or verification which is further strengthened by exploiting two major classroom use is granted without fee provided that copies are not made or distributed degrees of freedom coming with the EPEX principle: (1) we can for profit or commercial advantage and that copies bear this notice and the full citation substitute the next instruction with exactly one other instruction, on the first page. Copyrights for components of this work owned by others than ACM or we can insert longer linked instructions sequences which will must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a increase the variety of instructions influencing the test result. (2) fee. Request permissions from permissions@acm.org. when searching for an instruction replacement we can guide the GLSVLSI ’21, June 22–25, 2021, Virtual Event, USA © 2021 Association for Computing Machinery. 1Our formal ISA model is available at https://github.com/ics-jku/epex-formal-rv32- ACM ISBN 978-1-4503-8393-6/21/06. . . $15.00 https://doi.org/10.1145/3453688.3461497 model.

SMT-solver such that 𝑃 and ˆ𝑃 will activate very different control based on advanced model checking techniques. However, for using and data paths of the processor implementation and hence enabling riscv-formal the user has to implement the RISC-V formal interface, to compare typically unrelated logic/operations against each other. and OneSpin 360 DV is only commercially available. Beyond this, In total, EPEX broadens a given test program automatically. EPEX initially proposed for post-silicon verification only, Quick Error De- increases the chance in detecting bugs as for example the result of a tection (QED) has been enhanced and recently a symbolic form has compute-instruction is now compared to the result of a jump which been proposed, i.e. Symbolic Quick Error Detection (SQED). SQED has to be identical per construction on the architectural states but targets pre-silicon verification of processors [28] and has been ex- obviously checks very different micro-architectural states. tended and applied to RISC-V processors [16]. As such it checks We show that EPEX can easily be used in a simulation-based whether the outputs produced by executing a particular instruction verification environment. In a RISC-V case study using different core sequence match if the sequence is executed twice, assuming the in- configurations of the well-known VexRiscv core, we demonstrate puts to the two sequences also match. For this check SQED leverages the bug-finding capabilities of EPEX. bounded model checking. While SQED offer several advantages as a This paper is structured as follows: Section 2 discusses related formal technique, there are also some limitations: Single instruction work. Our EPEX approach is introduced in Section 3. The exper- checks have to be performed for each instruction, i.e. each instruc- imental evaluation is presented in Section 4. Finally, the paper is tion has to be completely formally verified on the core. In contrast, concluded in Section 5. EPEX can uncover bugs even in a basic data path operation, as a comparison to other unrelated logic is possible. Moreover, SQED 2 RELATED WORK involves splitting the register file in half and using one half for the original instructions and the second half for a duplicated sequence For processor verification various approaches aiming at the gen- of instructions. This however imposes practical restrictions, as for eration of test programs have been proposed. A strong focus was example tests cannot use the full register range. Overall, while put on the separation of the test generator from the architecture formal approaches can provide correctness guarantees, they are description. This includes for instance approaches using constraint significantly more difficult to use than simulation-based methods solving techniques [9, 12]. [24] presented an optimized test gen- and, due to their complexity and potential scalability issues, should eration framework which propagates constraints among multiple be complemented by simulation-based methods. instructions effectively. The test program generator of [13] uses Also in the formal context solutions to formalize the RISC-V a constraint-based coverage model describing execution paths of ISA semantics have been introduced, for example [8, 27]. They individual instructions. Alternative approaches integrate coverage- allow leveraging theorem proving to reason about the RISC-V ISA guided test generation via Bayesian networks [17] and other ma- semantics and generate simulation back ends. Unfortunately, even if chine learning techniques [11, 23] as well as fuzzing [26]. However, mentioned, no formal ISA model in propositional logic is generated these approaches are either not designed for RTL verification, re- or available which we would have integrated in EPEX. Therefore, quire a lot of effort until thorough tests are generated, or do not we created our own model. target the RISC-V ISA. 3 EPEX Recently, several RISC-V specific verification approaches emerged. In [3, 5], the RISC-V foundation provides official hand-written test- In this section, we first describe the basic idea of our approach suites. They are typically used as a starting point when implement- in Section 3.1. Then, we describe the EPEX flow in Section 3.2. ing a RISC-V processor. A model-based test generation approach is Afterwards, we detail the core ingredients in the remaining sections. the RISC-V Torture Test [6] framework. It uses Scala and generates 3.1 Basic Idea tests based on randomized instruction sequence templates. [20] is another model-based approach that employs a constraint-based When verifying a processor implementation at the ISA level, test specification for test generation. For verification at the Instruction programs (binaries) are needed. As the ISA of a processor defines Set Simulator (ISS) level, approaches leveraging coverage-guided the interface between the hardware and the software, processing fuzzing have been proposed recently [19, 22]. Googles’ RISC-V an instruction of a test program transforms the architectural state DV [7] is another test generation approach that leverages Sys- 𝑠, i.e. the state visible to the programmer, to a new architectural temVerilog in combination with the Universal Verification Method- state 𝑠 ′. We leverage this programmers view abstraction at the ISA ology (UVM) to continuously generate RISC-V instruction streams level as follows: We take an instruction of a test program 𝑃 starting based on constrained-random specifications. In [21] an efficient in 𝑠 leading to the successor architectural state 𝑠 ′. Now we use a cross-level testing approach for processor verification has been formal ISA model and automated reasoning (SMT) to determine proposed which generates an endless instruction stream on-the-fly a different instruction, which, when executed on 𝑠, results in the during simulation. While all these approaches are very sophisti- same successor architectural state 𝑠 ′ as the original instruction. cated and aim for closing the remaining coverage gap after decent This process is repeated for every instruction of 𝑃 . By this, we have verification progress, EPEX is complementary as existing tests can transformed 𝑃 to ˆ𝑃 according to the ISA specification and know that be broadened automatically and the verification check is extended the behavior of both programs is equivalent on the architectural across different data and control paths. states. Hence, instead of classical equivalence checking where two Besides methods for test generation, also formal approaches aim- models are compared on identical input, we now consider one ing at RISC-V have been developed. Notable are riscv-formal [4] processor implementation (which is instantiated twice), simulate and the OneSpin 360 DV RISC-V verification app [2] which are the equivalent programs 𝑃 and ˆ𝑃 , respectively, and compare the

                                                                     0996:  ...
                                                                     #    assume   t1 =  2,  t2  =   2046 ,  t3  =  0                          Test Program
                                                                     1000:  add    t3 ,  t1 ,  t2  #   t3 =  t1  +  t2   =  2048                    |                                             Testbench
                                                                     1004:  ...          (a) Excerpt of test program P                             BE —_—P,                                   Queue   i                         Compare
                                                                     0996:  ...                                                                                                       .                   Succ. States
                                                                     #    assume   t1 =  2,  t2  =   2046 ,  t3  =  0                              SES
                                                                     1000:  slli    t3 ,  t1 ,  10   # shift    left    t1  by    10           EPEX     Lib
                                                                     1004:  ...                                                                    Fa                                         Queue
                                                                                   (b) Excerpt of equivalent test program P1ˆ                                                             B   =u      it   [=]
                                                                     0996:  ...
                                                                     #    assume   t1 =  2,  t2  =   2046 ,  t3  =  0
                                                                     1000:  j     1044 #   set  pc   to 2044                                                               0
                                                                     1004:  ...                                                                                            P Trace                        Error
                                                                     2044:  jal    t3 ,  -1040   #   jump   back   and    link    t3 =                                                    Figure 2: EPEX flow
                                                                         2044      + 4 =   2048
                                                                                   (c) Excerpt of equivalent test program   ˆ
                                                                                                                            P2                     Example 2.                        Again, we consider the same test program P of Fig-
                                                                                    Figure 1: Example for broadening of a test program         ure 1a. However, this time we search for an instruction replacement
                                                                                                                                               consisting of two instructions. The result using EPEX is shown in

architectural states along the execution. Consequently, we denote Figure 1c. The determined test program uses two jump instructions our novel approach for processor verification as Equivalent Program and a free memory location. In detail, from address 1000 a relative EXecution (EPEX). jump (j) to address 2044 is performed. For this location a jump-and- Taking the idea further, EPEX can be extended naturally to search link instruction (jal) has been generated which performs a relative for instruction sequences instead of only a single instruction used jump to 1004 (the next instruction after the original add) and sets as replacement to form ˆ𝑃 . In general, EPEX offers the following the target register 𝑡3 as sum of the current program counter and 4, advantages: (a) existing tests can be broadened automatically, (b) resulting in the needed value 2048. This new test program shows that the search can be guided to activate different control and data an equivalent test program can be determined which now relates a paths when determining an instruction replacement, and (c) general compute-instruction with two instructions from a completely differ- purpose software can be converted into enhanced test programs. ent instruction class, i.e. control flow operations. These kinds of test We now provide two concrete examples to illustrate EPEX and programs will neither be created manually, nor random generators in particular the broadening of test programs. First, we consider are able to produce them. the replacement of the current instruction with a single instruction. As both examples have demonstrated, EPEX opens up a novel Thereafter, we provide an example using two instructions for the approach for the verification of processors by broadening test pro- equivalent program transformation. grams. We introduce the EPEX flow in the next section. Example 1. Figure 1a shows an excerpt of the test program P to- 3.2 EPEX Flow gether with the memory addresses where the instructions of P are The EPEX flow is depicted in Figure 2. EPEX is split into two compo- located. Let us consider the add instruction to be processed in a given nents: (1) The (processor) testbench controls the iterative execution architectural state. This architectural state has been reached by exe- of the original test program and drives the simulation of the two cuting all instructions up to and including address 0996. We only list processor instances, denoted as 𝐼1 and 𝐼2 in Figure 2, respectively. 𝑡the relevant subset of this architectural state, i.e. the registers2 = 𝑡1 = 2, (2) The generation of equivalent instructions with the formal ISA 2046 and 𝑡3 = 0. After the execution of add, the target register 𝑡3 model is performed via the EPEX library. This library is not tied has been set to 2048. In Figure 1b an equivalent program, as found by to any particular processor implementation and can be easily con- EPEX employing formal methods, is shown where the add instruction nected to other cores. has been replaced by the shift left logical immediate. More precisely, EPEX starts with a user-supplied test program as input (top in the execution of slli shifts 𝑡1 by 10 and stores the result of 2048 Figure 2). From the formal ISA model we have also derived an ISS. into 𝑡3. By this, both architectural states, after executing up to and including add of P and up to and including slli of P1, respectively,ˆ Into this ISS, the test program is loaded by the testbench. Then, the are identical. This example demonstrates that the compute-instruction ISS starts to execute the program step by step. For each step, the add can be replaced by another compute-instruction (here slli) in 𝑃architectural states𝑖 𝑠 and 𝑠 ′, and the executed original instruction this particular scenario/architectural state. By this, EPEX broadens are saved. an existing test program P in the sense that typically unrelated logic, The formal ISA model is constrained such that the initial state of i.e. in particular different control and data path operations are exe- the model matches 𝑠 and the final state matches 𝑠 ′. This constrained cuted and their results are finally compared. model is then given to the Z3 SMT-solver which finds assignments for the unconstrained instruction variables that lead from 𝑠 to 𝑠 ′. We now look at a more complex example. The values of the instruction variables form an instruction sequence

𝑃ˆ𝑖 𝑗 which is equivalent to the original instruction 𝑃𝑖 . The instruc- form of guidance is necessary since many possible sequences even tion sequence 𝑃ˆ𝑖 𝑗 consists, depending on additional constraints (see contain “uninteresting” instructions (e.g. different de-facto NOP Section 3.4), of either a single instruction or multiple linked in- variations like or x0, x0, x0). To guide the formal search towards structions. Both, 𝑃𝑖 and 𝑃ˆ𝑖 𝑗 are pushed to instruction queues which generating interesting instructions we propose the following two are connected to the corresponding processor instances I1 and I2, constraints: The effect constraint specifies that the value of the respectively. Also, 𝑃𝑖 and 𝑃ˆ𝑖 𝑗 are dumped into separate trace files by destination register 𝑠 ′[𝑟𝑑] in the successor architectural state 𝑠 ′ the EPEX library. This enables later testing via a cache mechanism is different from the value of the same register in the predecessor without the cost of querying the formal model again. state 𝑠 and by this reduces the number of de-facto NOPs. Since The processor instances fetch their instructions not from mem- not every instruction produces a result in a destination register ory but from the queues (gray in the center of Figure 2). This allows (e.g. branches), the effect constraint is not always required. Overall controlling the instructions that are fetched and executed by I1 and we get formally: I2. After I1 has finished the execution of 𝑃𝑖 and I2 has finished the Definition 1 (Effect Constraint). execution of 𝑃ˆ𝑖 𝑗 , the architectural states of I1, I2 and the ISS are ℎ𝑎𝑠_𝑟𝑒𝑠𝑢𝑙𝑡 (𝑐𝑢𝑟𝑟𝑒𝑛𝑡 _𝑖𝑛𝑠𝑡𝑟𝑝 ) → 𝑠 ′[𝑟𝑑] ≠ 𝑠 [𝑟𝑑]. compared. If the architectural states do not match, a bug either in I1 or I2 has been discovered, and the EPEX test is terminated and If instruction sequences are generated, the chain constraint guides marked as failed. Recall that the ISS has been derived from the for- the search to produce sequences with instructions that build on mal ISA model and is therefore correct by construction. However, each other’s results. This is reflected by relating the variables repre- I1 and I2 (instances of the processor at hand) execute different, but senting the registers along the generated instruction sequence 𝑃𝑖 𝑗 on the architectural states equivalent, programs as generated by with the index position 𝑝 . Essentially, we formulate that consecu- EPEX. Therefore in this case the mismatch has to result from the tive instructions of the instructions sequence must use the result activation of different control and/or data paths of the processor of the previous one, if one is produced: via the programs 𝑃𝑖 and 𝑃ˆ𝑖 𝑗 , respectively. Definition 2 (Chain Constraint). In the following we detail the core components, i.e. the formal ℎ𝑎𝑠_𝑟𝑒𝑠𝑢𝑙𝑡 (𝑐𝑢𝑟𝑟𝑒𝑛𝑡 _𝑖𝑛𝑠𝑡𝑟𝑝 ) → (𝑟𝑠1𝑝+1 = 𝑟𝑑𝑝 ∨ 𝑟𝑠2𝑝+1 = 𝑟𝑑𝑝 ) ISA model and constraints for guidance of the search. Finally, the Besides this essential constraints, there are several options to major implementation aspects are summarized. drive the search in certain directions. We also did some experiments 3.3 Formal ISA Model for this, but a thorough investigation is left for future work. In this section, we introduce the formal ISA model which we have 3.5 Implementation developed and which is used for the generation of equivalent pro- As already shown in Figure 2, EPEX consists of the EPEX library grams. (containing the formal ISA model) and the processor testbench Finding equivalent instruction sequences is a special case of the composed of the ISS, the processor instances, and the component program synthesis problem [25] which is up to today a challenging for comparison of the architectural states. This separation makes task. Formal methods, such as SMT-solving, are commonly used in the EPEX approach easily portable. The testbench needs to provide program synthesis, see for example [18]. certain functionality to support EPEX. Explicit control over the While multiple projects of formal RISC-V ISA specifications em- fetched instructions is necessary. Moreover, it is essential that the erged, nothing is available which is suitable for automated reason- exact time point a processor commits an instruction can be obtained, ing. To minimize the effort for the creation of the formal ISA model an common requirement for many verification approaches (e.g. [4, we decided to create it in C. This additionally allows to directly 21]). derive the ISS needed for EPEX. To integrate our formal model into EPEX, we use CBMC [14] to transform the C description into 4 RESULTS an SMT-lib v2.0 [10] instance. Hence, efficient reasoning becomes In this section, we present the experimental evaluation of our possible via the well known SMT-solver Z3 [15]. proposed EPEX approach. For the experiments we use a modu- To save run-time in the EPEX generation phase the SMT-lib in- lar RISC-V implementation for FPGAs which is provided by the stance produced by CBMC is post-processed to include placeholders VexRiscv project [1]. The VexRiscv cores are built in SpinalHDL. for the architectural states 𝑠 and 𝑠 ′, respectively. During an EPEX SpinalHDL is a domain specific language in Scala which allows de- run, these placeholders are replaced by the actual values of 𝑠 and 𝑠 ′. scribing RTL by using object-oriented and functional programming. Depending on the number of instructions that are to be generated, The VexRiscv cores are completely configurable from a bare-bone the model is unrolled. Each unwinding generates a new free 32-bit minimal CPU to a full-fledged Linux capable processor using a very variable that encodes the instruction to be executed. Moreover, flexible plugin concept. Finally, for a concrete core configuration additional constraints to guide the search in case of generating Verilog is generated. an instruction sequence longer than one are necessary which we In the first part of the experiments (Section 4.1), we reconsider the discuss in the following section. basic examples from Section 3. Afterwards, we demonstrate the bug- 3.4 Guidance Constraints finding capabilities of EPEX in a set of mutation-based experiments (Section 4.2). Finally, we show for multiple examples that executing If one instruction is replaced by an instruction sequence, the num- 𝑃 and ˆ𝑃 on the VexRiscv processor leads to a significant variation ber of possible instruction sequences grows rapidly. Thus, some in the control paths.

4.1 Basic EPEX Examples                                                       Table 1: Results for VexRiscv Tests
We come back to the test program excerpt described in Example 1.                 Test case     #Instrs  Orig          EPEX
For this experiment we selected a minimal VexRiscv configuration,
but the goal was to speed up shifting of the core. During the design             ADDI              263    81            87
and integration of a barrel shifter in the RISC-V core, the shifting             SRAI              234    84            88
was split in three operations: In case of a left shift operation, it             JALR              218    84            93
first reverses the input. Then, it performs a right shift with vari-
able number of steps. Finally, in case of a left shift operation, it
reverses the output again. Additionally, a configuration option was      1           J                   B    S     U     I  R
integrated to define the location of the final reverse operation to
be either in the execute stage (reduces the logic depth) or in the
memory stage of the pipeline. This has been modeled very nicely
in SpinalHDL, however, due to a copy and paste error the operation       0.5
was not reversed correctly. Running our test program ˆ
                                                  P1 (Figure 1b),
which has been generated by EPEX, easily revealed this bug. Please
note, that it was immediately clear that the bug was not caused by
the add instruction of the original program P (Figure 1a) executed       0
on instance I1: The comparison of the add result to the ISS gave              J      B     S             U     I      R
the same output; the mismatch could be seen on the incorrectly
computed register value 𝑡3 of the equivalent program ˆ
which executed the slli instruction on instance    P1 (Figure 1b)       Figure 3: Exemplary distribution of instruction class replace-
                                              I2. Of course, also       ments for ADDI test (cf. Table 1)
dedicated shift tests would have found this bug. However, the ad-
vantage of EPEX is that existing tests are automatically broadened      minutes to generate an equivalent program. The obtained results
and hence serve as an additional test.                                  for our approach are summarized in Table 1. The first column re-
Looking at the test program excerpt from Example 2 (add re-             ports the name of the test. The second column gives the number
placed by a jump and a jal), and one of the first VexRiscv cores        of instructions. In the third column the number of mutants are re-
from the GitHub repository, we first observed no problem when
using EPEX and comparing the execution of P and ˆ                       ported which have been found by the original test. The last column
                                                P2, respectively.       reports the number of mutants identified with EPEX. As can be
However, we instructed EPEX to generate more test programs. An          seen, EPEX is able to find nearly 8% more of the mutants than the
alternative test program ˆ
    P3 contained:                                                       original test on average. To achieve this result, we configured EPEX
    1000: jalr zero, 2045(zero).                                        to replace each instruction with up to three alternative instructions
For this program EPEX reported an error. The reason is that the         for the generation of the equivalent test program.
jalr instruction adds an immediate to its source register, then has
to clear the LSB of the sum, and then jumps to the resulting address.    EPEX Test Broadening Result.                    We found a very interesting mutant,
In the VexRiscv implementation however, the LSB was not set to          which was not detected even with extended cross-level testing
zero and hence the program counters differed. The problem occurs        (includes full compliance test-suite, Dhrystone and CoreMark). In
when odd addresses are generated via EPEX. This bug is nowa-            contrast to this, EPEX was able to discover the mutant by using the
days well-known in the RISC-V community and has been found              three EPEX tests shown Table 1. This demonstrates that broadening
by riscv-formal [4] on the VexRiscv core at hand. Nonetheless, this     given tests using EPEX already increases the test quality even when
demonstrates that EPEX can be used to generate relevant tests via       using a few basic tests only.
relating a compute-instruction with two instructions from a com-                         EPEX Test Diversity. To illustrate the diversity resulting from the
pletely different instruction class, namely control flow operations     EPEX test programs, we look on the RISC-V instruction format. It is
in this example.                                                        divided into six classes2: Register/register, Immediate, Upper im-
4.2 Mutation Experiments                                                mediate, Store, Branch, and Jump. The instruction format has been
                                                                        carefully designed to share and save logic. Moreover, it is important
To evaluate the bug-finding capabilities of EPEX we performed a         to note that all instructions of a class share most of the data path
set of mutation experiments which we describe in the following.         and have an almost identical control; this is because the instructions
Experimental Setup. For the experiments we used an area efficient       within a class use the same number of registers, immediates etc. but
VexRiscv configuration. We automatically created mutations of           of course differ in the specific operation. Based on this classification
the Verilog code of the core. Mutants were created by toggling          we now illustrate the effect of EPEX when generating an equivalent
bit constants and modifying comparison operators (e.g. replacing        test program. For each class, the percentage of replacements into
greater than by greater than or equal). Overall this resulted in 275    other classes for the ADDI test is shown in Figure 3.
mutants.                                                                 For example, consider the class U (on the x-axis the fourth in-
                                                                        struction format class): As can be seen an instruction from this
  EPEX Generation and Results. We now consider three tests of the       2
VexRiscv test-suite. For each test EPEX needs on average about five     See page 16, Figure 2.3 of “The RISC-V Instruction Set Manual Volume I: Unprivileged
                                                                        ISA V20191213” [29]

Instr. Class Replacement in %

   Table 2: EPEX Control Path Variation on VexRiscv                                       instructions which activate different control and data paths has

Test EPEX #Instrs Gen Ratio Avg. Δ Max. Δ great potential. For future work we will investigate the replacement of longer instruction sequences in more detail. Furthermore, we Compliance 1 8,834 100% 7.2% 36.0% will devise new guidance constraints in combination with novel Compliance 1-4 12,923 100% 15.1% 45.3% coverage metrics to measure the difference in logic activity when Dhrystone 1 38,798 10% 10.8% 33.0% running both programs on the two processor instances. Dhrystone 1-4 41,931 10% 13.4% 38.0% REFERENCES class is replaced in 10% with an instruction from J, in 15% with [1] 2021. GitHub - VexRiscv: A FPGA friendly 32 bit RISC-V CPU implementation. an instruction from B, in 0% of the cases with an instruction from https://github.com/SpinalHDL/VexRiscv. S, in 17% of the cases with another instruction within this class, [2] 2021. OneSpin 360 DV RISC-V Verification App. https://www.onespin.com/ in 58% with an instruction from I, and in 0% of the cases with an solutions/risc-v. instruction from R. Please note that instructions from the class S [3] 2021. RISC-V Compliance Task Group. https://github.com/riscv/riscv- compliance. are intentionally never replaced as integrating a memory model [4] 2021. RISC-V Formal Verification Framework. https://github.com/YosysHQ/riscv- into the formal model would make it much harder to solve for the formal. [5] 2021. RISC-V ISA Tests. https://github.com/riscv/riscv-tests. SMT-solver. Also, the ADDI test does not contain any instructions [6] 2021. RISC-V Torture Test Generator. https://github.com/ucb-bar/riscv-torture. of class R. Overall, this plot demonstrates that a good diversity [7] 2021. RISCV-DV. https://github.com/google/riscv-dv. in the sense of replacing an instruction with an instruction from [8] 2021. RISCV Sail Model. https://github.com/rems-project/sail-riscv. [9] Allon Adir, Eli Almog, Laurent Fournier, Eitan Marcus, Michal Rimon, Michael another class can be achieved. Therefore, independent of a RISC-V Vinov, and Avi Ziv. 2004. Genesys-Pro: innovations in test program generation core implementation, diverse testing becomes possible using EPEX. for functional processor verification. D&T (2004), 84–93. [10] Clark Barrett, Aaron Stump, and Cesare Tinelli. 2010. The SMT-LIB Standard: 4.3 Control Path Variation Version 2.0. In SMT Workshop. [11] Niklas Bruns, Daniel Große, and Rolf Drechsler. 2020. Early Verification of Finally, we consider the control path variation produced by EPEX. ISA Extension Specifications Using Deep Reinforcement Learning. In GLSVLSI. 297–302. We used the same experimental setup as in the previous section. [12] Brian Campbell and Ian Stark. 2014. Randomised Testing of a Microprocessor As tests, we utilized the compliance test-suite and the Dhrystone Model Using SMT-Solver State Generation. In Formal Methods for Industrial Critical Systems. 185–199. benchmark. Table 2 lists the obtained results. The first column [13] Mikhail Chupilko, Alexander Kamkin, Artem Kotsynyak, and Andrei Tatarnikov. lists the name of the test. Column EPEX reports the number of 2017. MicroTESK: Specification-Based Tool for Constructing Test Program Gen- instructions we configured to be replaced during equivalent pro- erators. In HVC. [14] Edmund Clarke, Daniel Kroening, and Flavio Lerda. 2004. A Tool for Checking gram generation via the formal ISA model for an instruction. The ANSI-C Programs. In TACAS. 168–176. column #Instrs shows the number of executed instructions. Then, [15] Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In column Gen Ratio gives the ratio of instructions of 𝑃 that where TACAS. 337–340. Available at https://github.com/Z3Prover/z3. [16] Keerthikumara Devarajegowda, Mohammad Rahmani Fadiheh, Eshan Singh, selected for EPEX replacement. The next column Avg. Δ reports Clark W. Barrett, Subhasish Mitra, Wolfgang Ecker, Dominik Stoffel, and Wolf- the average control path variation (stated in percent) triggered gang Kunz. 2020. Gap-free Processor Verification by S2QED and Property Gener- ation. In DATE. 526–531. by ˆ𝑃 in comparison to 𝑃 . For this, we carefully identified the se- [17] Shai Fine and Avi Ziv. 2003. Coverage directed test generation for functional lect signals of the multiplexers which control the data path in the verification using Bayesian networks. In DAC. 286–291. VexRiscv implementation along the pipeline stages. In the last col- [18] Sumit Gulwani, Susmit Jha, Ashish Tiwari, and Ramarathnam Venkatesan. 2011. Synthesis of Loop-Free Programs. SIGPLAN Not. 46, 6 (June 2011), 62–73. umn Max. Δ, the maximum delta found is provided, respectively. [19] Vladimir Herdt, Daniel Große, and Rolf Drechsler. 2020. Closing the RISC-V As can be seen EPEX causes a strong variation of the control paths Compliance Gap: Looking from the Negative Testing Side. In DAC. 1–6. of up to 45%. The obtained percentage values clearly demonstrate [20] Vladimir Herdt, Daniel Große, and Rolf Drechsler. 2020. Towards Specification and Testing of RISC-V ISA Compliance. In DATE. 995–998. that large parts of the control paths differ during the execution [21] Vladimir Herdt, Daniel Große, Eyck Jentzsch, and Rolf Drechsler. 2020. Efficient of 𝑃 on instance I1 and ˆ𝑃 on instance I2, respectively. Overall, the Cross-Level Testing for Processor Verification: A RISC-V Case-Study. In FDL. 1–7. strong control path variation shows that EPEX compares typically [22] Vladimir Herdt, Daniel Große, Hoang M. Le, and Rolf Drechsler. 2019. Verifying unrelated logic/operations against each other which enables a wide Instruction Set Simulators using Coverage-guided Fuzzing. In DATE. 360–365. testing. [23] Charalambos Ioannides, Geoff Barrett, and Kerstin Eder. 2011. Feedback-Based Coverage Directed Test Generation: An Industrial Evaluation. In HVC. 112–128. [24] Yoav Katz, Michal Rimon, and Avi Ziv. 2012. Generating instruction streams 5 CONCLUSIONS using abstract CSP. In DATE. 15–20. [25] Zohar Manna and Richard J. Waldinger. 1971. Toward Automatic Program EPEX is a novel approach for processor verification that automat- Synthesis. Commun. ACM 14, 3 (March 1971), 151–165. ically broadens existing test programs. For this task a formal ISA [26] Lorenzo Martignoni, Roberto Paleari, Giampaolo Fresi Roglia, and Danilo Bruschi. model and SMT-reasoning is utilized to generate an equivalent test 2009. Testing CPU Emulators. In ISSTA. 261–272. [27] SiFive. 2021. Formal Specification of RISC-V ISA in Kami. https://github.com/ program. EPEX is based on a new form of equivalence checking: sifive/RiscvSpecFormal. Executing both programs, i.e. original and equivalent, iteratively [28] Eshan Singh, David Lin, Clark W. Barrett, and Subhasish Mitra. 2018. Logic Bug Detection and Localization Using Symbolic Quick Error Detection. TCAD (2018). on two instances of the same processor design has to always re- [29] Andrew Waterman and Krste Asanović. 2019. The RISC-V Instruction Set Manual; sult in equal architectural states. We demonstrated the bug-finding Volume I: Unprivileged ISA. SiFive Inc. and CS Division, EECS Department, capabilities of EPEX on the VexRiscv processor. Broadening a few University of California, Berkeley. [30] Andrew Waterman and Krste Asanović. 2019. The RISC-V Instruction Set Manual; tests already resulted in the detection of more bugs. Volume II: Privileged Architecture. SiFive Inc. and CS Division, EECS Department, In conclusion, EPEX is a promising new approach to processor University of California, Berkeley. verification. In particular the feature of relating the execution of