SpinalHDL是一种基于Scala语言的敏捷硬件逻辑描述库，它能够提供更高级别的参数化和抽象能力，具有工程化能力强的特点。新发布的SpinalHDL-1.7.0版本中增加了与SymbiYosys协同进行形式化验证的能力，为数字设计开发者提供了有别于UVM的验证方法。本次分享将从形式化验证的目的和思维方式入手，通过案例介绍使用SpinalHDL进行形式化验证的流程和方法，降低数字设计工程师利用SpinalHDL这一敏捷开发工具实现高可靠IP核的难度。
内容大纲
肖寅东，电子科技大学副教授
研究方向为以计算机技术为核心平台的网络测试及同步技术、高速数据发生技术、测试系统集成技术（包括集成电路测试、网络设备测试等）。作为负责人或主研先后承担过型号项目，基础科研项目、国家自然科学基金面上项目等十余项国家级项目，以及各类省部级和横向合作科研项目；获省部级科技进步一等奖1项；1项研究成果经四川省科技成果鉴定为国际先进水平；发表学术论文十余篇。担任国际知名学术杂志《ISA Transaction》审稿人。作为SpinalHDL的主要贡献者之一，研究下一代软硬件结合的HDL描述语言及相关应用。
扫码加入技术讨论微信群进行更多技术交流。如失效，请添加极术小姐姐微信（aijishu20)备注“spinalhdl”加入。
