Self-Explaining Digital Hardware using Temporal Specifications

Lead-Supervisor:

• Prof. Görschwin Fey
  Hamburg University of Technology

Co-Supervisors:

• Prof. Heike Wehrheim,
• Prof. Sebastian Lehnhoff

Can digital hardware be self-explaining? How would that be achieved?

Explaining all hardware behaviour at any time during runtime is infeasible due to overhead, processing speed, and limited data bandwidth. Instead, we assume a decision and/or analysis at design time
fixing what is to be explained. By this, we can pre-calculate the model for explaining past and future behaviour online. Behaviour to be explained is specified by temporal logic at design time.

We will consider mainly designs in Register Transfer Level (RTL) descriptions, e.g., in Verilog, and temporal logic using SystemVerilog Assertions. Within the project we will develop algorithms that can turn a RTL design into self-explaining hardware.

Desirable background and expertise: Knowledge in temporal logic or other computational logics, and interest in methods for formal reasoning (e.g., model checking). Basic knowledge in hardware description languages.