中文 英语
首页
技术论文

使用形式化验证优化hls生产的电路(苏黎世联邦理工学院)

受欢迎程度

苏黎世联邦理工学院的研究人员发表了一篇题为“使用模型检查消除数据流电路的过度动态”的新技术论文。

摘要
“最近HLS的努力探索了从高级代码生成动态调度的数据流电路;它们在运行时根据特定数据和控制结果调整调度的能力保证了比标准的静态调度HLS解决方案更好的性能。然而,数据流电路是出了名的资源昂贵:它们的分布式握手机制在某些情况下带来了性能优势,但当不需要一般动态时,会导致不必要的资源开销。在这项工作中,我们提出了一个基于模型检查的验证框架,系统地降低了数据流电路的硬件复杂性。我们设计了一系列形式化的证明来识别特定行为场景的缺失,并使用这些信息用更简单和更便宜的控制结构取代通用的数据流逻辑。在从高级代码中获得的一组基准测试中,我们证明了我们的技术显著降低了数据流电路的资源需求(即,它导致LUT和FF分别减少高达51%和53%),同时仍然获得了动态调度的所有性能优势。”

找到开放获取技术纸在这里.2023年2月出版。

徐佳慧,Emmet Murphy, Jordi Cortadella和Lana josipoviic。2023.使用模型检查消除数据流电路的过度动态。在
2023 ACM/SIGDA现场可编程门阵列(FPGA ' 23)国际研讨会论文集,2023年2月12日至14日,美国加州蒙特利。
ACM,纽约,纽约,美国,11页。https://doi.org/10.1145/3543622.3573196



留下回复


(注:此名称将公开显示)

Baidu