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

Permalink: http://www.nusl.cz/ntk/nusl-413219


The record appears in these collections:
Universities and colleges > Public universities > Brno University of Technology
Academic theses (ETDs) > Master’s theses