Název:
Formalní verifikace RISC-V procesoru s využitím Questa PropCheck
Překlad názvu:
Formal verification of RISC-V processor with Questa PropCheck
Autoři:
Javor, Adrián ; Fujcik, Lukáš (oponent) ; Dvořák, Vojtěch (vedoucí práce) Typ dokumentu: Diplomové práce
Rok:
2020
Jazyk:
slo
Nakladatel: Vysoké učení technické v Brně. Fakulta elektrotechniky a komunikačních technologií
Abstrakt: [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.
Klíčová slova:
Formal verification; model checking; Questa PropCheck; RISC-V; SystemVerilog assertions
Instituce: Vysoké učení technické v Brně
(web)
Informace o dostupnosti dokumentu:
Plný text je dostupný v Digitální knihovně VUT. Původní záznam: http://hdl.handle.net/11012/189360