Difference between revisions of "Towards Formal Verification of the iDMA Engine (1-3S/B)"
From iis-projects
(Created page with "<!-- Creating Towards Formal Verification of the iDMA Engine (1-3S/B) --> Category:Digital Category:High Performance SoCs Category:Computer Architecture Categor...") |
|||
(One intermediate revision by the same user not shown) | |||
Line 4: | Line 4: | ||
[[Category:High Performance SoCs]] | [[Category:High Performance SoCs]] | ||
[[Category:Computer Architecture]] | [[Category:Computer Architecture]] | ||
− | [[Category: | + | [[Category:2023]] |
[[Category:Semester Thesis]] | [[Category:Semester Thesis]] | ||
+ | [[Category:Bachelor Thesis]] | ||
[[Category:Tbenz]] | [[Category:Tbenz]] | ||
[[Category:Michaero]] | [[Category:Michaero]] | ||
+ | [[Category:Paulsc]] | ||
[[Category:Available]] | [[Category:Available]] | ||
Line 20: | Line 22: | ||
** [[:User:Tbenz | Thomas Benz]]: [mailto:tbenz@iis.ee.ethz.ch tbenz@iis.ee.ethz.ch] | ** [[:User:Tbenz | Thomas Benz]]: [mailto:tbenz@iis.ee.ethz.ch tbenz@iis.ee.ethz.ch] | ||
** [[:User:Michaero | Michael Rogenmoser]]: [mailto:michaero@iis.ee.ethz.ch michaero@iis.ee.ethz.ch] | ** [[:User:Michaero | Michael Rogenmoser]]: [mailto:michaero@iis.ee.ethz.ch michaero@iis.ee.ethz.ch] | ||
+ | ** [[:User:Paulsc | Paul Scheffler]]: [mailto:paulsc@iis.ee.ethz.ch paulsc@iis.ee.ethz.ch] | ||
= Introduction = | = Introduction = |
Latest revision as of 10:21, 3 November 2023
Contents
Overview
Status: Available
- Type: Bachelor / Semester Thesis or Group Project
- Professor: Prof. Dr. L. Benini
- Supervisors:
Introduction
At IIS we have created a high-performance DMA Engine called iDMA. So far we have verified the unit's correctness using a simple file-based System-Verilog testbench.
Even though our current verification strategy works, to fully develop the iDMA we need a more capable verification strategy. One approach is formal verification, where the function of a circuit is compared against a set of mathematically formulated properties. In the case of the iDMA we could formulate e.g. deadlock-free operation and verify if the hardware has this property.
At IIS we have both industry-grade and free-and-open-source tools to do the formal verification process.
Project
In this project, you use formal verification to prove some properties of the iDMA ensuring its correct operation.
Character
- 20% Getting started with formal verification and the tools used
- 60% Implementing and verifying a given set of properties
- 20% Improving the RTL should bug(s) be present
Prerequisites
- Interest in memory systems
- Experience with digital design in SystemVerilog as taught in VLSI I
- Preferred: Knowledge of AXI4