Designing a RISC-V Reference Model for Open Source Processor Cores

Abstract

Nøye verifikasjon er avgjørende ved utviklig av prosessorkjerner og tar en betydelig del av den totale utviklingstiden. Asynkrone hendelser som "interrupts" er en stor utfordring i prosessorverifisering, som ofte fører til vanskelige feil. Instruksjonssettsimulatorer (ISS) brukes ofte som referansemodell for å verifisere prosessorkjerner, og er ofte tilstrekkelig for normal gjennomkjøring av prosessoren. På grunn av deres høye abstraksjonsnivå kan imidlertid ikke ISS-er nøyaktig simulere timingen og virkningen av asynkrone hendelser på samme måte som en prosessorkjerne. Det er derfor behov for en mer avansert referansemodell som nøyaktig simulerer timingen og korrektheten av asynkrone hendelser.

I denne masteroppgaven utforsker og sammenligner vi ulike tilnærminger til implementeringen av en referansemodell for åpne RISC-V prosessorkjerner som kan simulere asynkrone hendelser på syklusnivå. Vi foreslår og implementerer en referansemodellarkitektur som kombinerer et “Pipeline-Skall” og en eksisterende ISS. Pipeline-skallet er ansvarlig for å modellere timingen til pipelinen og asynkrone hendelser, mens ISSen er ansvarlig for den funksjonelle utførelsen av instruksjonene. Referansemodellen er implementert i SystemVerilog og integrert i OpenHW Groups verifiseringsmiljø for CV32E40S-kjernen til Silicon Labs. Spike er valgt som den eksisterende ISSen, og de nødvendige modifikajonene blir diskutert. I tillegg fokuserer vi på å gjøre referansemodellen kompatibel med formell verifisering.

Resultatene viser at referansemodellen kan simulere asynkrone hendelser korrekt i mange ulike scenarier. Den har et mindre verifikasjonsgap sammenlignet med å bruke en tradisjonell ISS som referansemodell, og kan sannsynligvis finne feil som andre referansemodelløsninger ikke kan. ISSen som brukes er ikke kompatibel med formell verifikasjon, men resten av designet antas å være kompatibelt med formell verifikasjon dersom ISSen erstattes med en syntetiserbar ISS. Imidlertid har de nåværende implementeringen noen begrensninger. Den implementerte referansemodellen er avhengig av signaler fra prosessorkjernen for noen detaljer i pipelinetimingen, og kompleksiteten til pipeline-skallet har ført til flere hittil uløste feil.

Processor verification is a crucial aspect of processor development, consuming a significant portion of the overall development time. Asynchronous events, like interrupts and debug requests, pose a significant challenge in processor verification and often lead to elusive bugs. Instruction Set Simulators (ISS) are often used as a Reference Model to verify the correctness of a processor’s execution and are often sufficient in normal execution. However, due to their instruction-level abstraction level, ISSs can not accurately simulate the timing of asynchronous events and side effects compared to the processor core. Therefore, a more advanced Reference Model that accurately simulates the timing and correctness of asynchronous events is needed.

This thesis explores and compares different approaches to implementing a reference model for open-source RISC-V processor cores that can accurately simulate asynchronous events at the cycle level. We propose and implement a reference model architecture combining a "Pipeline Shell" and an existing ISS. The pipeline shell is responsible for modeling the timing of the pipeline and the behavior of asynchronous events, while the ISS is responsible for the functional execution of the instructions. The reference model is implemented in SystemVerilog and integrated into the OpenHW Group’s verification environment for the CV32E40S core by Silicon Labs. Spike is chosen as the existing ISS, and the necessary modifications are discussed. We also focus on making the reference model compatible with formal verification.

The results show that the reference model can correctly simulate asynchronous events in many different scenarios. It has a smaller verification gap compared to using a traditional ISS as a reference model and is likely to find bugs that other reference model solutions can not. The ISS used is not compatible with formal verification. Still, the rest of the design is believed to be compatible with formal verification if the ISS is replaced with a synthesizable ISS. However, the current implementation has some limitations. The reference model is currently dependent on the DUT core for some pipeline timing details, and the complexity of the pipeline shell has led to multiple unresolved bugs.