Title:片上系统的模块化规范与形式化验证

Speaker:张弘策（香港科技大学广州校区）

Time: 4月27日（周三）下午2:00-3:30

Venue:线上报告，腾讯会议号 154-839-179

Abstract:复杂的片上系统，尤其是专用硬件加速器的广泛应用，给硬件验证带来了更多挑战。指令集规范作为一种模块化的规范，可以推广到非处理器组件的验证中，从而一定程度上缓解验证的可伸缩性问题。在应用基于指令集的模块化验证方法时，需要对指令的执行环境进行建模，以往这项工作依赖验证人员手工完成。本次报告将介绍一种基于反例引导抽象精化的自动环境不变量合成方法，它利用了电路结构信息，从而能够更高效地合成特定应用场景下的不变量。

Bio:张弘策，香港科技大学（广州）功能枢纽微电子学域助理教授。2021年在普林斯顿大学电子与计算机系取得博士学位，主要从事硬件领域的形式化验证应用的研究，相关研究工作获得ACM TODAES（Transactions on Design Automation of Electronic Systems）最佳文章奖，曾担任第59届电子设计自动化会议DAC的技术程序委员会成员。更多信息请访问 https://hongcezh.people.ust.hk/。