. s% j+ w- v) G& J演講主題(Title): % e. j" I* C$ n* dAchieving Ultra Dependable VLSI through Collaboration of Formal Verification and Architectural Technologies . _ z) U' y1 G; W 7 g# ~$ P1 g% M主講人(Speaker): 4 [+ a7 a: j2 c+ ~4 c! v" m( }Prof. Masahiro Fujita VLSI Design and Education Center (VDEC), University of Tokyo4 `/ D* d; w9 C# F
8 }5 q4 v4 H7 v6 Q演講摘要(Abstract): Y/ O) C) {1 d b$ t% r
Under JST/CREST funding mechanism, there are 11 research groups being funded as “Dependable VLSI Systems”. In the first part of the talk, we briefly review the research activities performed by Prof. Sakai’s group which try to enhance dependability of VLSI systems through collaboration of formal verification and architectural technologies. The research of formal verification includes formal verifiers for C-based designs, pre-/post-silicon verification and debugging with high-level designs descriptions, and formal verification of high performance processor designs. The research of architectural technologies includes timing-fault-tolerant circuit/architecture against random variation, highly dependable, and dependable and high performance many-core architecture. The architectures developed are the target of the formal verification in order to ensure highly dependable systems. In the second part of the talk, we show details of the research in formal verification part as well ! industrial evaluation of the formal verifier for C-based design descriptions and the tool development for post-silicon verification and debugging.