随着现代数字设计复杂度的增加,设计师趋向于从高级语言开始设计探索,并使用高层次综合或手动转换生成寄存器传输级(RTL)设计。不幸的是,这一翻译过程非常复杂,可能会在生成的设计中引入错误。本文提出了一种新颖的SLM和RTL顺序等效性检查方法。该方法基于有限状态机数据路径(FSMD)等效性检查方法。提出的方法使用机器学习(ML)技术从所有路径中识别FSMD对应的路径对。然后它通过符号仿真比较相应的路径对。我们方法的优势在于它从所有路径中分离出相应的路径对,避免了盲目的路径对比较。我们的方法可以处理大不相同的SLM和RTL设计,并显著降低基于路径的FSMD等效性检查问题的复杂度。有前途的实验结果显示了所提出方法的效率和有效性。
关键词包括等效性检查、FSMD、机器学习、系统级建模和形式化验证。在引言部分,作者指出系统级芯片(SoC)的尺寸和复杂性的增加使得设计师开始从系统级别使用高级语言设计。例如,可以使用C/C++和SystemC通过行为综合进行设计。不幸的是,翻译过程复杂且容易出错。因此,保持SLM和RTL设计之间的一致性成为了一个重要问题。由于SLM和RTL设计之间存在巨大的时间性和结构性差异,所以保证两者之间的等效性成为一个艰难的任务。所提出的基于模拟的等效性检查技术和基于形式化的等效性检查技术可以被分类为两种类型的方法。例如,Bombieri等人[1]提出了基于模拟的等效性检查方法[2]和属性测量方法。
在讨论等效性检查时,SLM和RTL设计的等效性通常涉及到对设计功能的重要一致性问题。SLM到RTL的转换可能是一个错误滋生的过程,因为它通常包括多个复杂转换的步骤。机器学习技术在这个过程中提供了辅助,能够从大量的数据中识别出可能的等效性路径对,这一过程需要对数据进行有效筛选。通过符号模拟比较路径对,可以减少人工干预,并提高等效性检查的自动化程度。
基于FSMD的等效性检查方法是现代设计验证中的一个重要方向。FSMD模型能够同时描述系统的有限状态机行为和数据路径操作,因而它在表示硬件设计时可以涵盖更多的细节。传统的方法可能会遍历所有可能的路径,进行直接比较,这不仅效率低下,而且在许多情况下无法有效处理设计之间的差异。提出的方法在进行路径对比较之前,先使用机器学习技术识别对应的路径对,这样可以减少比较的范围,提高检查的效率。
在等效性检查的实践中,传统手工检查方法依赖于设计师的经验和直觉,而基于机器学习的方法能够提供更加客观和一致的检查结果。通过学习历史的等效性检查案例,机器学习模型能够逐渐提高识别路径对的准确率,从而在设计的验证阶段发挥关键作用。此外,使用符号仿真而不是数值仿真可以在许多情况下避免由于数值误差导致的误报或漏报问题。
值得注意的是,等效性检查并不仅仅局限于设计转换的验证。在高层次综合、逻辑综合,以及后端设计流程中的各个阶段,等效性检查都是保证设计转换正确性的重要手段。随着硬件设计自动化水平的提高,等效性检查方法需要适应更加复杂的设计环境和不同的设计阶段需求。机器学习作为一种强大的辅助工具,在提高等效性检查的智能水平和效率方面具有重要的应用前景。