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/。