SystemVerilog-assertioiden formaali tarkastus
Helminen, Joonatan (2023-04-19)
Helminen, Joonatan
J. Helminen
19.04.2023
© 2023 Joonatan Helminen. Ellei toisin mainita, uudelleenkäyttö on sallittu Creative Commons Attribution 4.0 International (CC-BY 4.0) -lisenssillä (https://creativecommons.org/licenses/by/4.0/). Uudelleenkäyttö on sallittua edellyttäen, että lähde mainitaan asianmukaisesti ja mahdolliset muutokset merkitään. Sellaisten osien käyttö tai jäljentäminen, jotka eivät ole tekijän tai tekijöiden omaisuutta, saattaa edellyttää lupaa suoraan asianomaisilta oikeudenhaltijoilta.
Julkaisun pysyvä osoite on
https://urn.fi/URN:NBN:fi:oulu-202304191444
https://urn.fi/URN:NBN:fi:oulu-202304191444
Tiivistelmä
Tässä kandidaatin työssä perehdytään, miten SystemVerilog-laitteistokuvauskielessä väitteiden formaali tarkastus toimii käyttämällä automaattista formaali tarkastustyökalu OneSpin 360 Design Verification (DV)-ohjelmaa. Työn sisällössä perehdytään aluksi teoriapuolella SystemVerilog -laitteistokuvauskieleen ja siinä esiintyviin väitteisiin, sekä formaaliseen tarkastukseen ja sen käyttämiseen väitteiden tarkastuksessa. Käytännön puolessa käyttämällä OneSpin 360 DV-ohjelmaa apuna tutkitaan, miten väitteiden formaali tarkastus toimii. Lopuksi käsitellään aihetta sekä pohditaan ohjelmasta saatuja tuloksia. In this bachelor’s thesis, the formal verification of assertions in the SystemVerilog Hardware Description Language is explained and verified using the automatic formal verification tool OneSpin 360 Design Verification (DV) program. At first, the theory about SystemVerilog Hardware Description Language, assertions in it, formal verification, and its use for verification of assertions are explained. Then in the practical side, using the OneSpin 360 DV program as an aid, formal verification of assertions is verified. In the end, the topic is covered, and the results obtained from the program are discussed.
Kokoelmat
- Avoin saatavuus [32013]