View source for Towards Formal Verification of the iDMA Engine (1-3S/B)

<!-- Creating Towards Formal Verification of the iDMA Engine (1-3S/B) -->

[[Category:Digital]]
[[Category:High Performance SoCs]]
[[Category:Computer Architecture]]
[[Category:2023]]
[[Category:Semester Thesis]]
[[Category:Bachelor Thesis]]
[[Category:Tbenz]]
[[Category:Michaero]]
[[Category:Paulsc]]
[[Category:Available]]


= Overview =

== Status: Available ==

* Type: Bachelor / Semester Thesis or Group Project
* Professor: Prof. Dr. L. Benini
* Supervisors:
** [[: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:Paulsc | Paul Scheffler]]: [mailto:paulsc@iis.ee.ethz.ch paulsc@iis.ee.ethz.ch]

= 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 [https://en.wikipedia.org/wiki/Formal_verification  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

= References =