Type of Work:
In this work timed Petri net descriptions of different DRAM standards (DDR3, DDR4, LPDDR4 etc.) shall be auto-translated into sets of properties (SVA) for formal hardware verification. Afterwards these properties shall be applied to the RTL description of an available DDR3 memory controller in order to formally verify its functional correctness.
This work will be jointly supervised by the chairs of Prof. Kunz and Prof. Wehn, and Dr. Jung at Fraunhofer IESE.
- SystemVerilog Assertions
- DRAM basics (optional)
- Petri Net basics (optional)
DRAM controllers are advanced hardware systems that have to satisfy a complex timing protocol. The validation of their behavior is tedious and intensive since test data has to ensure the coverage of all internal states. Formal verification is a technique to guarantee the functional correctness of hardware systems by exact mathematical proofs instead of handwritten test benches. Since DRAM is becoming more and more present in safety-critical environments (e.g. autonomous driving), the need for formally verified controller hardware is growing rapidly.