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.
| Identifer | oai:union.ndltd.org:nusl.cz/oai:invenio.nusl.cz:413219 |
| Date | January 2020 |
| Creators | Javor, Adrin |
| Contributors | Fujcik, Lukáš, Dvořák, Vojtěch |
| Publisher | Vysoké učení technické v Brně. Fakulta elektrotechniky a komunikačních technologií |
| Source Sets | Czech ETDs |
| Language | Slovak |
| Detected Language | English |
| Type | info:eu-repo/semantics/masterThesis |
| Rights | info:eu-repo/semantics/restrictedAccess |
Page generated in 0.0023 seconds