|
|
SystemVerilog-assertioiden formaali tarkastus |
|---|---|
| Author: | Helminen, Joonatan1 |
| Organizations: |
1University of Oulu, Faculty of Information Technology and Electrical Engineering, Electrical Engineering |
| Format: | ebook |
| Version: | published version |
| Access: | open |
| Online Access: | PDF Full Text (PDF, 2.6 MB) |
| Pages: | 25 |
| Persistent link: | http://urn.fi/URN:NBN:fi:oulu-202304191444 |
| Language: | Finnish |
| Published: |
Oulu : J. Helminen,
2023
|
| Publish Date: | 2023-04-20 |
| Thesis type: | Bachelor's thesis |
| Tutor: |
Lahti, Jukka |
| Description: |
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. Formal verification of SystemVerilog assertions Abstract 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. see all
|
| Subjects: | |
| Copyright information: |
© Joonatan Helminen, 2023. Except otherwise noted, the reuse of this document is authorised under a Creative Commons Attribution 4.0 International (CC-BY 4.0) licence (https://creativecommons.org/licenses/by/4.0/). This means that reuse is allowed provided appropriate credit is given and any changes are indicated. For any use or reproduction of elements that are not owned by the author(s), permission may need to be directly from the respective right holders. |
|
https://creativecommons.org/licenses/by/4.0/ |