应对硬件设计符号执行中的路径爆炸问题
密码学与安全
2023-04-13 v1
摘要
符号执行是硬件设计的一种强大验证工具，但受路径爆炸问题困扰。我们引入一种新方法——分段组合(piecewise composition)，其利用硬件的模块化结构将路径探索的工作转移给 SMT 求解器。我们给出了实现该技术的符号执行引擎。该引擎直接作用于寄存器传输级(RTL) Verilog 设计，无需翻译为网表或进行软件仿真。在我们的评估中，分段组合将探索的路径数量减少一个数量级，并将运行时间减少 97%。利用文献中的 84 条属性，我们在包括 SoC 和 CPU 在内的 5 个开源设计中发现了断言违例。
引用
@article{arxiv.2304.05445,
title = {Countering the Path Explosion Problem in the Symbolic Execution of Hardware Designs},
author = {Kaki Ryan and Cynthia Sturton},
journal= {arXiv preprint arXiv:2304.05445},
year = {2023}
}