Personal tools

Difference between revisions of "Towards Formal Verification of the iDMA Engine (1-3S/B)"

From iis-projects

Jump to: navigation, search
(Created page with "<!-- Creating Towards Formal Verification of the iDMA Engine (1-3S/B) --> Category:Digital Category:High Performance SoCs Category:Computer Architecture Categor...")
 
Line 6: Line 6:
 
[[Category:2022]]
 
[[Category:2022]]
 
[[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 =

Revision as of 20:07, 2 August 2022


Overview

Status: Available

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

References