Original title:
Formalní verifikace RISC-V procesoru s využitím Questa PropCheck
Translated title:
Formal verification of RISC-V processor with Questa PropCheck
Authors:
Javor, Adrián ; Fujcik, Lukáš (referee) ; Dvořák, Vojtěch (advisor) Document type: Master’s theses
Year:
2020
Language:
slo Publisher:
Vysoké učení technické v Brně. Fakulta elektrotechniky a komunikačních technologií Abstract:
[slo][eng]
Témou tejto diplomovej práce je Formálna verifikácia RISC-V procesoru s využitím Questa PropCheck pomocou formálnych tvrdení jazyka SystemVerilog Assertions. Teoretická časť práce je venovaná architektúre RISC-V, popisu vybraných komponentov procesora Codix Berkelium 5 určených na formálnu verifikáciu, popisu komunikačného protokolu AHB-lite, formálnej verifikácii, jej metódam a nástrojom. Praktickú časť tvorí návrh verifikačného plánu vybraných komponentov, ich následná formálna verifikácia, analýza výsledkov a zhodnotenie prínosu formálnych techník.
The topic of this master thesis is Formal verification of RISC-V processor with Questa PropCheck using SystemVerilog assertions. The theoretical part writes about the RISC-V architecture, furthermore, selected components of Codix Berkelium 5 processor used for formal verification are described, communication protocol AHB-lite, formal verification and its methods and tools are also studied. Experimental part consists of verification planning of selected components, subsequent formal verification, analysing of results and evaluating a benefits of formal technics.
Keywords:
Formal verification; model checking; Questa PropCheck; RISC-V; SystemVerilog assertions
Institution: Brno University of Technology
(web)
Document availability information: Fulltext is available in the Brno University of Technology Digital Library. Original record: http://hdl.handle.net/11012/189360