PRECISE Seminar: Formal Methods for Computer Architecture: Reducing the Barriers to Entry

In this talk, I will present recent work with my students and collaborators that reduces the barriers to entry for computer architects to use formal methods. First, I will discuss our work on automatically generating formal microarchitectural models of hardware. These models are necessary for microarchitectural verification, and generally need to be written by hand by formal methods experts. In contrast, our work can automatically generate such models from accessible inputs like test programs and execution traces or from hardware RTL implementations. These models can then be used for formal verification of memory consistency and hardware security using known automated verification techniques. I will also speak briefly on our technique for automated verification of cyber-physical systems written in the Lingua Franca coordination language.

Meanwhile, we also need to develop formal models and verification techniques for emerging architectures that significantly change the hardware-software interface. As an example, I will discuss our ongoing work on developing a verified programming model for a recent non-traditional memory hierarchy. I will conclude with our work on automatically converting axiomatic formal models to their operational equivalents, enabling each type of model to be used for the tasks it handles best.