Computer Engineering Cider Seminars

Upcoming Seminar

Tsunami Simulation on FPGA and its Analysis Based on Statistical Model Checking

Masahiro Fujita
University of Tokyo
Friday, March 23, 2012
1-2pm, GB244

Cider Seminar HomePage

Abstract

In the first part of the talk, techniques by which Tsunami simulation can be accelerated with FPGA and GPU are presented. Both approaches have realized similar speed up of around 30 times over single core processors. They are based on stream based processing and the original C programs have been transformed to work with streams which are sequences of values of variables for partial differential equations at each time step. In FPGA based acceleration, streams are constructed for each variable among different time steps, whereas in GPU implementation, steams are constructed for each time step among variables for different geographical locations. These difference come from the different memory architectures used in FPGA and GPU. In the second part of the talk, by utilizing FPGA/GPU based acceleration Tsunami simulation, various bounded properties on the accuracy of Tsunami predictions based on Tsunami simulations are statistically model checked. The statistical model checker is the one being developed by Ed Clarke's group at CMU, and our Tsunami simulation results are analyzed. Finally we will discuss about FPGA based implementation on bounded model checking for Tsunami simulations results for further speed up.

Biography

Masahiro Fujita received his Ph.D. degree in Engineering from the University of Tokyo in 1985 and shortly after joined Fujitsu Laboratories Ltd. From 1993 to 2000, he had been assigned to Fujitsu's US research office and directed the CAD research group. In March 2000, he joined the department of Electronic Engineering in the University of Tokyo as a professor. He has written over 100 technical papers on all aspects of logic design CAD. He has received several awards from Japanese major scientific societies on his works in formal verification and logic synthesis. His doctor degree thesis was written in early 80's and on model checking. Since then he has been involved in many research projects on various aspects of formal verification.