SOURCE ARCHIVE
EXTRACTED CONTENT
62,650 chars Minimally Invasive Generation of RISC-V
Instruction Set Simulators from Formal ISA Models
S¨oren Tempel1 Tobias Brandt Christoph L¨uth1,2 Rolf Drechsler1,2
1Institute of Computer Science, University of Bremen, Bremen, Germany
2Cyber-Physical Systems, DFKI GmbH, Bremen, Germany
tempel@uni-bremen.de, tobbra91@gmail.com, christoph.lueth@dfki.de, drechsler@uni-bremen.de
Abstract—The development process for new embedded systems VP, it is advantageous to derive its central part—the ISS—
relies increasingly on simulation, e.g. to develop hardware and from a formal model of the ISA rather than implement it
software components in parallel using virtual prototyping. The manually. A formal model describes ISA semantics using a
central component of a virtual prototype is the instruction set
simulator (ISS) which implements instruction execution for a well-defined formal language, instead of relying on natural
specific instruction set architecture (ISA). To avoid erroneous language, thus achieving exactness and avoiding ambiguities
behavior during software simulation, it is paramount to ensure in the specification. Instead of manually implementing an
that the provided ISS implements the ISA exactly as specified, ISS from a specification in natural language, it is possible
i.e. that there are no discrepancies between the hardware and the to automatically generate it from such a formal model, thus
VP. In order to increase confidence in the correctness of the VP’s
ISS, it is advantageous to generate it automatically from a formal reducing the margin for errors.
model of the ISA instead of implementing it manually. While a While several formal ISA models have been presented in
variety of formal ISA models have been proposed in prior work, prior work [2, 3, 4, 5, 6], they are presently not utilized they are presently not widely used in the VP domain. We attempt in the VP domain. We attribute this to the fact that VPs to ease employment of formal models for ISS generation in this domain. To this end, we reduce the integration effort through a are tightly integrated with vendor-supplied components (e.g. simulator-agnostic ISS generation approach that integrates well memory implementations, bus systems, or models of hard- with existing simulators and existing vendor-supplied VP com- ware peripherals). These components are often modeled in ponents. Our approach leverages a formal RISC-V ISA model SystemC, a C++ library for hardware modeling [7]. When which exclusively describes instruction semantics and abstracts generating an ISS for a VP from a formal model, it must interactions with hardware components through an interface model, thus encapsulating interactions with simulator-specific be ensured that the generated ISS integrates well with these code. As part of our experiments, we were able to generate an vendor-supplied SystemC components and does not require ISS for the popular RISC-V implementations Spike and RISC-V replacing or changing them. For this reason, we propose a VP, thereby replacing their manually written implementations. novel approach for generating an ISS from a formal model Performed benchmarks indicate that the generated ISS offers the which—contrary to prior work—is designed to be minimally same simulation performance as a manually written one, while still passing the official RISC-V tests. invasive (i.e. allows re-using existing vendor-supplied com- Index Terms—Embedded Systems, Formal ISA Models, Sim- ponents). This is achieved by leveraging a minimal formal ulation, RISC-V, Virtual Prototyping model which focuses exclusively on formally describing the I. INTRODUCTION instruction semantics and by abstracting interactions with As embedded systems consist of both hardware and soft- hardware components through a generic interface model. That ware components, it is vital to be able to begin software is, we only generate the code implementing the instruction development before the hardware is available to reduce the semantics, which is where prior work has found most bugs [8], time-to-market. In order to do so, a simulator for the hardware leaving other components (e.g. those modeling the memory) is required. Nowadays, hardware and software components as-is to ease the integration. While our proposed approach are typically developed in parallel using virtual prototypes [1, is applicable to different ISAs, we focus on the modular Sect. 1.3]. A virtual prototype (VP) provides a simulator for RISC-V [9, 10] architecture in this publication. Due to an an entire hardware platform. A central component of a VP ever-growing set of ISA extensions, simulators for this ISA is the instruction set simulator (ISS) which is responsible for benefit significantly from formal models as the specification simulating instruction execution for a chosen instruction set is constantly expanding, requiring simulators to “catch up” by architecture (ISA). For a VP-based development flow, it is implementing new extensions, which is a laborious error-prone paramount to ensure that the VP implements the ISA exactly process. as specified. Otherwise, the software may exhibit erroneous The goal of our work is therefore to reduce the effort behavior when executed on the physical hardware, thereby required to integrate existing RISC-V simulators with formal negatively impacting the time-to-market of an embedded sys- ISA models. Our contributions towards this goal are: (1) An tem. In order to increase confidence in the correctness of the enhanced version of an existing formal model for the RISC-V This work was supported by the German Federal Ministry of Education ISA, (2) a new simulator-agnostic C/C++ code generator for and Research (BMBF) within projects Scale4Edge under grant no. 16ME0127, this formal model, and (3) a modified version of the popular ECXL under grant no. 01IW22002, and VE-HEP under grant no. 16KIS1342. Spike [11] and RISC-V VP [12] simulators which use a
generated ISS (instead of a manually written one). To the best program counter). In total, the LIBRISCV EDSL consists of of our knowledge, the ISS generation approach presented here 26 primitives for formally describing instruction semantics. is the first which is easily applicable to a variety of existing Formal descriptions using this EDSL can be further processed RISC-V simulators. The experiments we have conducted with in Haskell, e.g. for the purpose of code generation by mapping Spike and RISC-V VP confirm the feasibility of our approach the 26 primitives and the expression language to C/C++ code for this purpose. Furthermore, performed benchmarks indicate (see Subsect. III-D). Internally, the LIBRISCV EDSL is that an ISS generated using our tooling achieves similar implemented in Haskell using free monads [13]. More details simulation speed compared to a manually written one while regarding the utilization of free monads and LIBRISCV itself still passing the official RISC-V ISA tests. are provided in an existing publication by Tempel et al. [6]. II. PRELIMINARIES B. Virtual Prototypes In the following, we provide background information on VPs provide an executable model of an entire hardware formal ISA models and VPs as prerequisites for our research. platform, including peripherals provided by this platform. A. Formal ISA Model They are a popular tool for the development of embedded systems as the early creation of VPs enables developing The ISA is the interface between the hardware and the both—hardware and software components—for an embedded software of a system; it is therefore of central importance system in parallel, thereby reducing the time-to-market [1, to the system architecture. An ISA description has many Sect. 1.3]. This is achieved by utilizing the VP to simulate aspects: instruction semantics, memory and register behavior, the behavior of the targeted hardware platform, thus allowing interrupts, decoding, et cetera. In this publication, we are software development to begin before the physical hardware focusing exclusively on instruction semantics. These semantics is available. For software simulation, a VP therefore provides have traditionally been specified in natural language. However, an ISS for the architecture used by the targeted hardware natural language specifications can be ambiguous, incomplete, platform. Our work is concerned with the generation of this and are not easy to work with. For this reason, we base our component from a formal ISA model. Apart from an ISS, a VP work on a formal ISA model: one which has unambiguous also provides models for peripherals provided by the hardware semantics and can be processed by electronic means (e.g. for platform. Hardware peripherals are commonly modeled using the purpose of code generation). SystemC [7], a C++ class library for describing hardware Formal models come in a variety of languages (and we give components. More specifically, VPs often utilize SystemC a more comprehensive overview in Sect. V), but for our work TLM [7, Sect. 9], where hardware behavior is described we leverage an existing formal model in the general-purpose based on a high-level bus abstraction. Our ISS generation functional programming language Haskell. This model is approach is specifically designed to integrate well with existing called LIBRISCV [6] and provides formal semantics for the SystemC components. In order to evaluate our approach, we 32-bit base instruction set of the RISC-V architecture [10, use RISC-V VP, an existing open source SystemC-based VP Sect. 2]. Contrary to prior work (e.g. Sail [3]), LIBRISCV for the RISC-V architecture [14]. focuses exclusively on describing the user-level instruction semantics in isolation, e.g. without formally describing other III. APPROACH aspects (such as the memory). Furthermore, LIBRISCV does In the following, we present our approach for minimally not capture microarchitecture details such as pipelining or invasive generation of instruction set simulators from formal timing. This property makes LIBRISCV well suited for our ISA models. approach as it eases the integration with existing simulators by allowing re-use of existing (vendor-supplied) components A. Overview such as memory implementations, instead of also generating Fig. 1 provides an overview of our approach and includes these components from the formal model. an illustration of the software architecture of an ISS with The semantics of an individual RISC-V instruction are de- some VP-specific components (e.g. a SystemC TLM bus). scribed formally in LIBRISCV through an embedded domain- Components added for the application of our approach are specific language (EDSL) in Haskell. Conceptually, the EDSL highlighted using a dashed box. The ISS in Fig. 1 consists of consists of two components: (1) primitives for describing inter- different internal components and is responsible for executing actions with architectural state components (e.g. the memory) a firmware image as faithful to a real processor as possible. Re- and (2) an expression language for performing operations garding the internal ISS components, we differentiate between on memory/register values. Using these components (i.e. the the instruction execution unit (which is responsible for the exe- EDSL), LIBRISCV provides a formal description for each cution part of the fetch-decode-execute cycle) and architectural RISC-V instruction (analog to the natural language specifi- state components (e.g. the register file) which are required for cation in the RISC-V standard). For example, the ADD in- instruction execution but conceptually separate components. struction is described through the primitive readRegister As motivated in Sect. I, architectural state components are (to obtain the register operands), the addition operation of commonly supplied by hardware vendors and therefore often the expression language, and the writeRegister primitive modeled using the SystemC standard. For example, in Fig. 1 (for storing the result). Similar primitives are available for the memory component is modeled using SystemC TLM and other operations (e.g. interactions with the memory or the therefore attached to a TLM bus which is accessed by the
1 semantics LBInst{rd=dest, rs1=reg, imm=off} = do
Peripherals Memory 2 base <- readRegister reg
3 byte <- loadByte (base ‘Add‘ off)
4 writeRegister dest (SExtByte byte)
SystemC TLM Bus Fig. 2. Simplified description of LB instruction semantics in LIBRISCV.
Instruction Set Simulator B. ISA Model
MemIf LIBAs discussed in Subsect. II-A, we are using the existing
RISCV formal ISA model for our approach [6]. We
Instruction choose this model because—in contrast to prior work—it
Execution RegFile describes instructions semantics in isolation without providing
Unit a formal description of other ISA aspects such as memory
behavior or decoding. This allows us to only generate the
ExecState code implementing instruction semantics (the instruction ex-
ecution unit) from the formal specification while retaining
other parts as-is, thereby making our approach minimally
generates requires executes invasive and easing the integration with existing simulators.
Code As per Subsect. II-A, LIBRISCV leverages a Haskell EDSL
Generator Firmware for the formal description of RISC-V instruction semantics.
utilizes This EDSL consists of two components: (1) primitives for de-
scribing interactions with architectural state components (e.g.
ISA Model the memory) and (2) an expression language for performing
operations on memory/register values. As an example, the
Fig. 1. Overview of our minimally invasive ISS generation approach. formal description of the RISC-V LB instruction in this EDSL
is provided in Fig. 2. The semantics of this instruction are de-
scribed in terms of the readRegister (Line 2), loadByte
(Line 3), and writeRegister (Line 4) primitives which
execution unit over a memory interface (MemIf). Our proposed correspond to changes of the architectural state. Furthermore, ISS generation approach is specifically designed to integrate operations on retrieved register/memory values are modeled well with existing vendor-supplied components. Therefore, we using the aforementioned expression language, i.e. the Add focus on generating the execution unit of an ISS from a formal and SExtByte constructors in Fig. 2. For the purpose of code ISA model. The execution unit implements the instruction generation, we need to map constructors of the LIBRISCV semantics and is the component in which prior work on expression language to C/C++ expressions. Additionally, we automated testing has found the most implementation errors in need to map the readRegister, writeRegister, etc. existing simulators [8]. In order to generate this component, primitives to functions provided by our interface model. the code generation tool needs to be able to emit code that In order to do so, we further enhanced the existing ISA interacts with the architectural state components to generate model for code generation purposes. The original version of code which implements the instruction semantics (e.g. to write LIBRISCV as presented by Tempel et al. [6] was intended a register). Since the API of these components is highly for building custom ISA interpreters directly in Haskell. For simulator- and vendor-specific, we leverage a custom inter- this reason, it separates instruction decoding from instruction face model for our approach. This interface model provides execution (i.e. the decoding is not part of the formal model). a generic API for common operations (e.g. writing/reading This can be illustrated by considering the formal semantics registers or accessing memory). The generic API itself is for the LB instruction in Fig. 2 again. The semantics of a set of C function prototypes which define a simulator- this instruction are defined over a record type constructor agnostic interface for performing these common operations (LBInst) in Line 1 which represents a decoded LB instruc- (see Subsect. III-C). These functions need to be implemented tion. The different members of this record type are assigned on a per-simulator basis by mapping them to the internal to variables; the values of these variables correspond directly interfaces provided by the simulator. Since simulator-specific to integer values (e.g. 15 for accessing register x15) and are code is abstracted through the generic API, the code generation hence not captured by the formal description. To overcome tool is itself applicable to different RISC-V simulators (see this limitation, we added additional primitives to LIBRISCV Subsect. IV-A). While we believe the outlined approach to to express decoding operations as part of the instruction be practical for different ISAs, we focus on the RISC-V semantics descriptions. The resulting, enhanced description architecture in this publication as it is highly modular and of the LB instruction is shown in Fig. 3. Contrary to the therefore well suited for an application of our approach. In the description from Fig. 2, this version is only parameterized next subsection, we therefore present a significantly enhanced over the instruction opcode (LBOpcode) and then uses the version of an existing formal RISC-V ISA model which has new primitives decodeRD, decodeRS1, and decodeImmI been tailored to our use case. to obtain additional information about the current instruction
Interface Model
1 semantics LBOpcode = do 1 /* Register file */
2 dest <- decodeRD 2 uint32_t read_register(void *core, unsigned idx);
3 base <- decodeRS1 >>= readRegister 3 void write_register(void *core,
4 off <- decodeImmI 4 unsigned idx,
5 5 uint32_t value);
6 byte <- loadByte (base ‘Add‘ off) 6
7 writeRegister dest (SExtByte byte) 7 /* Byte-addressable memory */
8 uint8_t load_byte(void *core, uint32_t addr);
Fig. 3. Description of the LB instruction with our LIBRISCV changes. 9 uint16_t load_half(void *core, uint32_t addr);
10 uint32_t load_word(void *core, uint32_t addr);
1 semantics LBOpcode = do 11 /* ... */
2 (dest, base, off) <- decodeAndReadIType
3 byte <- loadByte (base ‘Add‘ off) Fig. 5. Excerpt of the generic API provided by the interface model.
4 writeRegister dest (SExtByte byte)
Fig. 4. Final refinement of LB instruction semantics in LIBRISCV. will further discuss the interface model implementation for
Spike and RISC-V VP in Subsect. IV-A. In the following, we
(Line 2 - 4). Since the description is now more verbose, will introduce our simulator-agnostic code generation tool and
we added an abstraction to define the instruction type, as illustrate how this tool interacts with the interface model.
mandated by the RISC-V specification [9, Sect. 2.2], as part D. Code Generation
of the formal description. The actual description of the LB
instruction—using our enhanced version of LIBRISCV—is We use the previously described ISA and interface models
therefore less verbose and depicted in Fig. 4. Notably, it has to implement a simulator-agnostic code generation tool. As
the same length as the original description. depicted in Fig. 1, the tool generates a simulator-agnostic
The new instruction decoding primitives that we have added instruction execution unit, i.e. the code implementing the
to the existing LIBRISCV ISA model allow us to map these RISC-V instruction semantics. For this purpose, we build
to decoding functions provided by RISC-V simulators using on the formal description of these semantics provided by
our interface model. More details on interface modeling will LIBRISCV. As discussed in Subsect. II-A, the formal ISA
be provided in the next subsection. model consists conceptually of two components: primitives for
describing interactions with the architectural state components
C. Interface Model and an expression language for describing operations on
The interface model is the central perquisite for generating register/memory values which were obtained through these a simulator-agnostic ISS as the generated implementation primitives. All instruction semantics are formally described of instruction semantics will need to interface with existing using these components. In order to automatically generate components of a simulator (e.g. the register file). Since the code from this formal description, we need to build a code C/C++ code—emitted by our code generation tool—should be generator in Haskell which receives these EDSL components simulator-agnostic, we introduce the interface model as an as inputs. As discussed in the original LIBRISCV paper, additional abstraction layer within the simulator. The inter- the code generator then acts as an interpreter for the EDSL face model provides a generic C/C++ API for accessing the transforming its components into the desired representation [6, aforementioned components, this API is used by the code Sect. 4.3]. As part of this transformation, we generate C/C++ generator tool and needs to be implemented manually once code for all 26 primitives of the EDSL, e.g. mapping the for each targeted simulator. An excerpt of the generic API readRegister primitive to C/C++ code retrieving a register is shown in Fig. 5, the full API description is available value through the interface model. Therefore, the desired separately.1 As illustrated in this figure, the API consists of representation is a C/C++ abstract syntax tree (AST) in our a set of C functions which are parameterized over a void case. The creation of this AST from the formal ISA model is pointer. These void pointers are converted to simulator-specific illustrated in Fig. 6. types internally in the implementation of these functions. We As depicted in Fig. 6, C/C++ code implementing instruction decided against utilizing C++ abstractions (such as abstract semantics is created from this generated AST using an un- classes) for this purpose to also support RISC-V simulators parser (also called a pretty printer). Conceptually, an unparser that are purely written in C. Presently, the generic API consists is the opposite of a parser, as shown in Fig. 6: it serializes a of 19 C functions and provides an interface for the register given AST to a chosen output format, C/C++ source code in file, the program counter, the memory, and the decoder of a our case [15, 16, 17]. By employing an unparser we can ensure RISC-V simulator. Relying solely on a functional abstraction the syntactic correctness of the generated code, compared eases implementing this generic API as an implementation to—for example—generating the code directly through string is essentially a mapping of the defined generic functions to concatenation. This enables straightforward adjustments of the simulator-specific ones. Therefore, these functions will be generated code and eases the application of our approach inlined by the C/C++ compiler in the common case and hence to simulators written in other programming languages. The the additional interface model abstraction has minimal to no implementation of the unparser (i.e. the translation from the impact on simulation performance (see Subsect. IV-C). We AST to the C code) makes use of the existing language-c2
1https://github.com/agra-uni-bremen/formal-iss/tree/fdl-2023#readme 2
https://hackage.haskell.org/package/language-c
Unparser for C/C++ 1 static inline void exec_lb(void * core,
2 uint32_t instrPC,
3 void * instr)
AST creates C/C++ Code 4 { write_register(core, instr_rd(instr),
5
6 (int32_t)(int8_t)load_byte(core,
7 read_register(core,
generates 8 } instr_rs1(instr))+instr_immI(instr)));
9
Code Fig. 7. Automatically generated C/C++ code for the LB instruction.
Generator
passed to passed to standalone Haskell binary written in roughly 750 LOC which
depends on the LIBRISCV Haskell library (for the formal
RISC-V model) and the language-c library (for C/C++
Architectural Expression unparsing). In the next section, we illustrate that we can
State Primitives Language easily employ this tool—and our general approach—for au-
tomatically generating an execution unit for different existing
LibRISCV ISA Model RISC-V simulators, thereby demonstrating that a minimally
Fig. 6. Interaction between the code generator and the LIBRISCV ISA model. invasive ISS generation is feasible.
IV. EVALUATION
Haskell library. As shown in Fig. 6, our code generation tool is In the following, we evaluate our approach in terms of
in this context responsible for generating an AST that is passed generalizability, conformance, and simulation performance. In
to the unparser provided by language-c. The generation of this regard, we have concerned ourselves with the following
this AST is based on the formal instruction semantics obtained research questions:
from LIBRISCV. RQ1 Is the approach generalizable in the sense that it can
As part of the AST generation, we create one C function RQ2 be applied to different RISC-V simulators?
for each formally described RISC-V instruction. As an ex- Does the generated ISS conform to the instruction
ample, the C function which implements the LB instruction RQ3 semantics mandated by the RISC-V specification?
is shown in Fig. 7. Each generated function receives a void Does the original, manually written, ISS have better
pointer to a simulator-specific processor abstraction (core), simulation performance than the generated one?
the program counter of the current instruction (instrPC), and A. Generalizability
a void pointer to a simulator-specific instruction abstraction Our proposed ISS generation approach is specifically de-
(instr) as function arguments. Naturally, since the code is signed to be easily applicable to a variety of different RISC-V automatically generated, it heavily nests function calls and simulators. In order to evaluate the suitability of our approach is not optimized for human readability. Nonetheless, it is for this purpose, we have employed it to generate a new ISS possible to illustrate the interaction with the aforementioned for the popular Spike [11] and RISC-V VP [12] simulators. generic API of the interface model using this example. The The existing ISS of these simulators was manually written by function body shown in Line 5 - 8 of Fig. 7 uses the the developers in C++ and was not generated from a formal write_register, read_register, and load_byte specification. In the following, we provide more background functions from the generic API (see Fig. 5) to interact with information on these two simulators and describe the changes the register file and memory implementation. These functions that were necessary in order to integrate them with our ISS receive the processor abstraction (core) as a void pointer generation approach. function argument and cast this pointer to a simulation-specific Spike was one of the first simulators for the RISC-V type internally to implement the operation.3 Furthermore, the architecture and was initially developed by the University of generated code in Fig. 7 also obtains information about the California. Similar to RISC-V VP, it simulates the execution instruction (register and immediate) using the instr_rs1 of RISC-V machine code on a host system. In this regard, and instr_immI functions of the interface model. Arith- it focuses on achieving a high simulation speed at the cost metic operations are performed on these values by mapping the of simulation accuracy. For this reason, it does not use a Add operation from LIBRISCV’s expression language (see hardware modeling language like SystemC and therefore only Fig. 4) to the + operator provided by C/C++. Similarly, the has limited support for additional hardware peripherals. Con- sign-extension from Fig. 4 (SExtByte) is implemented in trary to Spike, RISC-V VP provides a full virtual prototype of Fig. 7 using integer type casts. common RISC-V hardware platforms, e.g. the SiFive HiFive14 By leveraging the interface model, the code generation or the SiFive HiFive Unleashed5. As such, RISC-V VP focuses tool itself remains entirely simulator-agnostic. The tool is a on simulation accuracy and therefore also uses the SystemC
3Refer to Subsect. IV-A for more information on the simulator-specific 4https://www.sifive.com/boards/hifive1
5https://www.sifive.com/boards/hifive-unleashed
implementation of the interface model for Spike and RISC-V VP.
1 // ... lines for the same purpose.6 The integration process took a
2
3 static inline uint32_t programmer with domain knowledge less than a day. As such,
4 read_register(void *c, unsigned idx) the experiments demonstrate that minimal effort is required to
5 { apply our approach to different RISC-V simulators, thereby
6 return ((struct rv32::ISS*)c)->regs[idx];
7 } illustrating its generalizability.
8
9 static inline void B. Conformance
1011 write_register(void *c,{ unsigned idx, uint32_t v) With the modifications outlined in the previous section, our
12 ((struct rv32::ISS*)c)->regs[idx] = v; enhanced versions of Spike and RISC-V VP use an ISS that
13 } has been automatically generated from the formal LIBRISCV
1415 static inline uint8_t ISA model, instead of a manually written one. Naturally, it
16 load_byte(void *c, uint32_t addr) is possible that the ISA model does not correctly capture the
17 { RISC-V instruction semantics or that our code generation tool
1819 auto mem = ((struct rv32::ISS*)c)->mem; or interface model implementations contain bugs. Therefore,
20 } return mem->load_byte(addr); it is paramount to ensure that the generated ISS still conforms
21 to the RISC-V specification. In order to test conformance to
22 // ... the specification, we utilize the official RISC-V ISA tests for
Fig. 8. Excerpt of the interface model implementation for RISC-V VP. the 32-bit base instruction set.7 These tests include several test
programs (one per instruction) which validate the behavior of
RISC-V instruction implementations using manually written
hardware modeling language. The entire execution of RISC-V test cases. Both our modified version of Spike and RISC-V machine code is performed within a SystemC simulation, VP pass the RISC-V ISA tests for rv32i. This indicates which eases reasoning about low-level details (e.g. timing). that our enhanced version of the LIBRISCV ISA model still RISC-V VP is further described in a publication by Herdt et conforms to the RISC-V ISA tests and that our code generator al. [12]. We choose Spike and RISC-V VP for our experi- and interface model do not introduce any severe bugs. In ments, because they represent two ends of a spectrum (Spike future work, we would like to expand our conformance tests focuses on simulation performance while RISC-V VP focuses by showing equivalence between the generated ISS and the on simulation accuracy) and their implementations therefore manually written one. differ significantly. This demonstrates that our approach is C. Performance applicable to a variety of existing simulators, from full VPs Since our approach replaces a manually written ISS with to performance-oriented simulators like Spike. an automatically generated one, there is the possibility that In order to employ our ISS generation approach for these the code generation tool does not account for optimizations simulators, we first had to manually implement an interface included in the manually written code. Simulation speed is model for each simulator (see Subsect. III-C). As part of this of importance for RISC-V simulators in order to be able to implementation, we need to map the simulator-agnostic API execute and test complex RISC-V software in a reasonable for interacting with simulator components (e.g. the register time span. In order to evaluate the impact of our approach file) to the internal simulator-specific API. An excerpt of the on simulation speed, we use our modified version of RISC-V interface model implementation for RISC-V VP is shown VP (see Subsect. IV-A) and perform a simulation speed com- in Fig. 8. As illustrated in this figure, the interface model parison with the original unmodified version of this simulator casts a provided void pointer to a simulator-specific type (referred to as the baseline version in the following). In prior for representing a RISC-V processor (struct rv32::ISS) work, performance benchmarks for RISC-V VP have been and afterward calls methods of this type to implement the se- conducted using the Embench benchmark suite [14]; therefore mantics of the interface model. The implementation presented we also use Embench for our experiments. Embench is an open in Fig. 8 is specific to RISC-V but the Spike interface model source benchmark suite which is specifically tailored to the has a similar complexity. The complete implementation of both embedded domain, it consists of several benchmark programs interface models is available as part of the publication artifacts. which perform computation intensive tasks (such as checksum Apart from the interface model, we also had to connect calculation) [18]. We conduct our experiments with Embench the generated functions which implement the semantics of 1.0 on a Linux system with an Intel i7-8565U processor. RISC-V instructions (see Fig. 7) with the existing fetch- Since benchmark results for a simulator can differ depend- decode-execute cycle implementation of Spike and RISC-V ing on the workload of the host system, we executed each VP. Spike already generates functions for the implementation benchmark application 25 times with both variants of RISC-V of RISC-V instruction using several scripts, which we have VP. Benchmark results are presented as a grouped bar chart in adjusted accordingly. RISC-V VP uses a switch/case statement Fig. 9. The absolute execution time in seconds is given on the to execute decoded instructions, which—similar to Spike—we y-axis of Fig. 9 while the x-axis lists the benchmark programs now generate using a script. In total, we modified roughly 6Naturally, automatically generated lines are not included in this metric, 150 lines in RISC-V VP to implement the interface model and the build system changes. In Spike, we modified 200 since they do not correspond to any manual integration effort. 7 https://github.com/riscv/riscv-tests
100
baseline generated 86.9 84.8
80
60
46.2 44.7
40
31.9 30.8
26.626.4
22.6 22.2
20 14.9 14.6 15.4 15.2 13.613.3 17.817.3 15.0 14.8
8.9 8.9 8.9 8.7 9.3 9.1 7.1 7.0 4.5 4.3 8.4 8.1 7.2 7.0 2.1 2.1 8.1 7.8
0
aha-mont64 crc32 cubic edn huffbench matmult-int minver nbody nettle-aes nettle-sha256 nsichneu picojpeg qrduino sglib-combined slre st statemate ud wikisort
Fig. 9. Execution time benchmarks performed for an unmodified version of RISC-V VP and a version generated using our approach. Each benchmark
application has been executed 25 times. The bars represent the arithmetic mean over all executions (lower is better); error bars indicate the standard derivation.
of the Embench suite. For each benchmark program, two bar RISC-V board—is provided in Sail [3], but models in the Coq
charts are presented: the left bar chart (blue) represents the theorem prover or the Haskell programming language exist
results for the baseline version, the right bar chart (orange) as well. The Coq model uses the embedded Kami DSL [21]
represents our modified version of RISC-V VP (i.e. uses an and allows reasoning about correctness—in particular, about
ISS generated using our approach). Both bar charts specify the correctness of microarchitecture implementations of the ISA,
arithmetic mean for the execution time of a given benchmark or about software running on the ISA—but as Coq is an in-
application over 25 executions. The error bars in Fig. 9 specify teractive theorem prover rather than a programming platform,
the standard derivation. it is less convenient to work with in aspects other than proof
In total, 19 benchmark applications have been tested with (e.g. code generation). Apart from the LIBRISCV model used both variants of RISC-V VP. Comparing the results for in this publication, additional RISC-V models in Haskell are each benchmark application, execution time for the generated GRIFT [4] and Forvis [5]. All of these have different design RISC-V VP variant is either sightly lower or the same as goals. While Forvis was meant as an executable formal model the execution time of the baseline version. This indicates that implemented in a deliberately restricted subset of Haskell, an ISS generated using our approach does not have worse GRIFT attempted to capture the ISA as precise as possible simulation performance than a manually written one. Since the in Haskell’s type system, and LIBRISCV was designed with generated instruction semantics are the same for both Spike a focus on instruction semantics to ease building custom ISA and RISC-V VP and only the interface model differs, we do interpreters. From these, the design goals of LIBRISCV best not provide a comparison of Spike variants in this publication. aligned with ours as it enabled us to focus on generating the V. RELATED WORK code implementing instruction semantics while retaining other Due to their numerous advantages, formal ISA models parts, thereby easing the integration with existing simulators. have been subject of intense research for a while now. ARM Related work in the electronic design automation domain technologies introduced a custom domain-specific language leverages architecture description languages (ADLs) for pro- (DSL) with a formal semantics, to describe the ISA of their at cessor descriptions [22, 23, 24]. Compared to formal ISA that time new ARM-v8 architecture [2]. The formal language models, these ADLs focus more on microarchitectural details allowed deriving test suites and Verilog code, for example. (such as pipelining or caching). For this reason, it is chal- Following on from this, the Sail language was developed, a lenging to integrate them with existing simulators and vendor- DSL designed to describe ISA semantics [19]. From the Sail supplied components. Therefore, these languages are primarily model of an ISA, formal descriptions in different programming used to generate new simulators instead of aiming for an and theorem proving languages can be generated (such as C, integration with existing ones. To the best of our knowledge, OCaml, Coq, Isabelle, or HOL4). Sail has been used in prior the generation approach presented here is the first which is work to model the RISC-V, ARM-v8 and MIPS ISAs, amongst easily applicable to a variety of existing simulators, from full others [3]. However, such versatility comes at a price: the VPs like RISC-V VP to performance-focused simulators like generated models are not as concise or convenient to work with Spike. as native ones. Moreover, Sail focuses on completeness and VI. D ISCUSSION & FUTURE WORK therefore goes beyond the description of instruction semantics and also includes formalization of additional ISA details such In this publication, we focused on a minimally invasive as address translation algorithms or instruction decoding. This integration of formal ISA models with existing RISC-V sim- contributes to the complexity of Sail and makes it difficult to ulators. Especially in the VP domain, formal models have not integrate it into an existing RISC-V simulator. Therefore, Sail yet been used to their full potential. In order to ease usage of instead generates a new standalone ISA simulator [3, Sect. 5]. formal ISA models for VP generation, we focused on mini- Specifically for RISC-V, a variety of formal ISA models mizing the integration effort. Therefore, we only employed a exist [20]. The definitive formal model—approved by the formal model for the 32-bit RISC-V base instruction set [10,
Average execution time (s)
Sect. 2]. In future work, it would be possible to focus more [3] A. Armstrong, T. Bauereiss, B. Campbell, et al., “ISA semantics for
on modeling aspects and expand the underlying LIBRISCV ARMv8-a, RISC-V, and CHERI-MIPS,” Proc. ACM Program. Lang.,
ISA model to cover additional RISC-V extensions and RISC-V [4] vol. 3, no. POPL, Jan. 2019. DOI: 10.1145/3290384.
variants (e.g. 64-bit RISC-V). In this context, it would be B. Selfridge, “GRIFT: A richly-typed, deeply-embedded RISC-V se-
mantics written in Haskell,” in SpISA 2019: Workshop on Instruction
especially interesting to also support parts of the RISC-V Set Architecture Specification, Portland, Oregon, Sep. 2019. [Online].
privileged architecture specification [10], instead of focusing [5] Available: https://www.cl.cam.ac.uk/∼jrh13/spisa19/paper 10.pdf.
on the user-level ISA [9]. Such modeling aspects are also Bluespec, Inc., Forvis: A formal RISC-V ISA specification, GitHub.
[Online]. Available: https://github.com/rsnikhil/Forvis RISCV- ISA-
discussed in the original LIBRISCV paper [6], extending the Spec.
formal model to cover more parts of the ISA (e.g. decod- [6] S. Tempel, T. Brandt, and C. L¨uth, “Versatile and flexible modelling
ing) would allow our code generation approach to be more of the RISC-V instruction set architecture,” in Trends in Functional
Programming, S. Chang, Ed., Boston, MA, USA: Springer Interna-
comprehensive. However, in this regard, there is a trade-off tional Publishing, 2023, ISBN: 978-3-031-21314-4.
between comprehensiveness of the formal model and the effort [7] System C Standardization Working Group, “IEEE standard for stan-
required to integrate it with existing simulators. The premise dard SystemC language reference manual,” Tech. Rep., 2012, pp. 1–
638. DOI: 10.1109/IEEESTD.2012.6134619.
of our work is that by focusing on code implementing the [8] V. Herdt, D. Große, H. M. Le, and R. Drechsler, “Verifying instruc-
actual instruction semantics—where in accordance with prior tion set simulators using coverage-guided fuzzing,” in 2019 Design,
work we assume most bugs to occur [8]—we can more easily Automation & Test in Europe Conference & Exhibition (DATE), 2019,
pp. 360–365. DOI: 10.23919/DATE.2019.8714912.
integrate the formal model with existing simulators. If we were [9] RISC-V Foundation, The RISC-V instruction set manual, volume I:
to capture additional parts of an ISA (e.g. memory behavior) in User-level ISA, ed. by A. Waterman and K. Asanovi´c, Document
the formal model as well, it would complicate the integration [10] Version 20191213, Dec. 2019.
RISC-V Foundation, The RISC-V instruction set manual, volume
with existing simulators. In terms of comprehensiveness, it II: Privileged architecture, ed. by A. Waterman and K. Asanovi´c,
is possible to cover the semantics of additional RISC-V [11] Document Version 20190608-Priv-MSU-Ratified, Jun. 2019. extensions using our approach in future work [6, Sect. 7]. University of California, Spike, a RISC-V ISA simulator, GitHub. [Online]. Available: https://github.com/riscv/riscv-isa-sim. VII. CONCLUSION [12] V. Herdt, D. Große, P. Pieper, and R. Drechsler, “RISC-V based virtual prototype: An extensible and configurable platform for the In this paper, we have presented a novel approach for system-level,” Journal of Systems Architecture, vol. 109, p. 13, 2020, generating the ISS of RISC-V simulators from a formal ISA [13] ISSN: 1383-7621. DOI: 10.1016/j.sysarc.2020.101756. O. Kiselyov and H. Ishii, “Freer monads, more extensible effects,” model. Contrary to prior work, our approach is designed to SIGPLAN Notices, vol. 50, no. 12, pp. 94–105, Aug. 2015, ISSN: be as minimally invasive as possible through a simulator- 0362-1340. DOI: 10.1145/2887747.2804319. agnostic interface model (Subsect. III-C), a self-contained [14] V. Herdt, D. Große, and R. Drechsler, “Fast and accurate performance evaluation for RISC-V using virtual prototypes,” in 2020 Design, formal ISA model (Subsect. III-B), and a code generator for Automation & Test in Europe Conference & Exhibition (DATE), 2020, this model (Subsect. III-D). By focusing exclusively on the pp. 618–621. DOI: 10.23919/DATE48585.2020.9116522. code implementing the actual instruction semantics, we ease [15] J. Hughes, “The design of a pretty-printing library,” in Advanced Functional Programming, J. Jeuring and E. Meijer, Eds., Berlin, the integration with existing vendor-supplied components and Heidelberg: Springer Berlin Heidelberg, 1995, pp. 53–96, ISBN: 978- increases the confidence in the correctness of the utilized ISS. 3-540-49270-2. DOI: 10.1007/3-540-59451-5 3. Conducted experiments confirm that our approach is applica- [16] P. Wadler, “A prettier printer,” in The Fun of Programming. Palgrave, Mar. 2003, ISBN: 0-3339-9285-7. ble to different RISC-V simulators (Spike and RISC-V VP) [17] L. Hermerschmidt, S. Kugelmann, and B. Rumpe, “Towards more with minimal effort (Subsect. IV-A). Furthermore, we were security in data exchange: Defining unparsers with context-sensitive able to show that an ISS—generated using our approach— encoders for context-free grammars,” in 2015 IEEE Security and Privacy Workshops, 2015, pp. 134–141. DOI: 10.1109/SPW.2015.29. still passes the RISC-V ISA tests (Subsect. IV-B) and offers [18] Free and Open Source Silicon Foundation, Embench: A modern similar simulation speed performance as a manually written embedded benchmark suite. [Online]. Available: https : / / www . one (Subsect. IV-C). In future work, we want to investigate [19] embench.org/ (visited on 01/24/2023). A. Armstrong, T. Bauereiss, B. Campbell, et al., “The state of sail,” in correctness proofs (for both the formal model and the gener- SpISA 2019: Workshop on Instruction Set Architecture Specification, ated ISS), expand our ISA model to support additional RISC-V M. Fernandez, Ed., 2019. [Online]. Available: https://www.cl.cam.ac. extensions, and consider its application to VP-based software [20] uk/∼jrh13/spisa19/paper 04.pdf. RISC-V Foundation, ISA Formal Spec Public Review, GitHub, Ac- analysis tasks. To stimulate further research in this direction, cessed 2023-03-23, 2019. [Online]. Available: https : / / github. com / we have released our code generation tool8 as well as our riscvarchive/ISA Formal Spec Public Review. modified versions of Spike9 and RISC-V VP10 as open source [21] J. Choi, M. Vijayaraghavan, B. Sherman, A. Chlipala, and Arvind, “Kami: A platform for high-level parametric hardware specification software. and its modular verification,” Proc. ACM Program. Lang., vol. 1, no. ICFP, Aug. 2017. DOI: 10.1145/3110268. REFERENCES [22] S. Rigo, G. Araujo, M. Bartholomeu, and R. Azevedo, “ArchC: A SystemC-based architecture description language,” in 16th Symposium [1] T. D. Schutter, Better Software. Faster!: Best Practices in Virtual on Computer Architecture and High Performance Computing, 2004, Prototyping. Synopsys Press, Mar. 2014, ISBN: 978-1-61-730013-4. pp. 66–73. DOI: 10.1109/SBAC-PAD.2004.8. [2] A. Reid, “Trustworthy specifications of ARM® v8-A and v8-M [23] A. Fauth, J. Van Praet, and M. Freericks, “Describing instruction set system level architecture,” in 2016 Formal Methods in Computer- processors using nML,” in Proceedings the European Design and Test Aided Design (FMCAD), Oct. 2016, pp. 161–168. DOI: 10 . 1109 / Conference. ED&TC 1995, 1995, pp. 503–507. DOI: 10.1109/EDTC. FMCAD.2016.7886675. 1995.470354. [24] V. Zivojnovic, S. Pees, and H. Meyr, “LISA-machine description 8https://github.com/agra-uni-bremen/formal-iss language and generic machine model for HW/SW co-design,” in VLSI 9https://github.com/agra-uni-bremen/spike-libriscv Signal Processing, IX, 1996, pp. 127–136. DOI: 10 . 1109 / VLSISP. 10https://github.com/agra-uni-bremen/libriscv-vp 1996.558311.