Randomized Testing of RISC-V CPUs using Direct Instruction Injection
| العنوان: | Randomized Testing of RISC-V CPUs using Direct Instruction Injection |
|---|---|
| المؤلفون: | Alexandre Joannou, Peter Rugg, Jonathan Woodruff, Franz A. Fuchs, Marno Van der Maas, Matthew Naylor, Michael Roe, Robert N. M. Watson, Peter G. Neumann, Simon W. Moore |
| المساهمون: | Woodruff, Jonathan [0000-0003-3971-2681], Fuchs, Franz A [0000-0002-1402-7138], Moore, Simon W [0000-0002-2806-495X], Apollo - University of Cambridge Repository |
| المصدر: | IEEE Design & Test. :1-1 |
| بيانات النشر: | Institute of Electrical and Electronics Engineers (IEEE), 2023. |
| سنة النشر: | 2023 |
| مصطلحات موضوعية: | 4009 Electronics, Sensors and Digital Hardware, Hardware and Architecture, Electrical and Electronic Engineering, Software, 40 Engineering |
| الوصف: | TestRIG (Testing with Random Instruction Generation) is a testing framework for RISC-V implementations. The RISC-V community has standardized a formal model of the architecture in the Sail language, giving a human-readable specification that can also be used for simulation and verification. The Sail language is designed for this purpose by allowing instruction semantics to be described conveniently (for example, by supporting variable bit-widths). Ideally, a RISC-V implementor could formally prove equivalence between their implementation and the Sail model, but proof tools are not yet sufficiently automated to be routinely used on the whole- processor level. They instead focus on equivalence between combinational logic functions, with verification of a full out-of-order microarchitecture remaining an open problem. As a pragmatic compromise, we use TestRIG to check equivalence between the model and an implementation by generating random instruction sequences, executing the same sequences on the model and the implementation under test, and comparing execution traces (tandem execution). This approach does not prove equivalence but can demonstrate divergence, and is usable in all stages of development. |
| وصف الملف: | application/pdf |
| تدمد: | 2168-2364 2168-2356 |
| URL الوصول: | https://explore.openaire.eu/search/publication?articleId=doi_dedup___::1c3df44ab2b72d1129702ce1b1f60b20 https://doi.org/10.1109/mdat.2023.3262741 |
| حقوق: | CLOSED |
| رقم الأكسشن: | edsair.doi.dedup.....1c3df44ab2b72d1129702ce1b1f60b20 |
| قاعدة البيانات: | OpenAIRE |
| تدمد: | 21682364 21682356 |
|---|