印度技术学院(IIT)的五位研究人员最近提出一种形式特性验证(FPV)的新方法。他们建议以直观的方式针对形式分析编写明确的测试方案。这些研究人员提出的方法还包含特性测试方案覆盖(test plan coverage by properties)的观念,以及识别测试方案的哪一部分被形式特性所覆盖的方法。研究人员表示:“我们相信,我们的方法将通过削减测试计划而缩短设计验证时间,有助于显著减少仿真费用。”
传统的形式验证方法尝试按照形式规范,采用诸如模型校验的技术验证给定的RTL实现。但纯粹的验证形式方法还仍然没有被设计流程所接纳。微架构编写设计的测试方案,这种结构化的方式用于检查设计在不同的时间点是否满足特性,并且在不同的输入序列下是否符合协议要求。但目前仍没有正式的明确的方式来编写测试方案,因此,设计师难以发现测试方案的哪一部分被形式特性验证(FPV)的结果所覆盖。
IIT的研究人员提出的测试方案可由FPV所覆盖。所提出的语法结构称为测试方案描述语言Test Plan Description Language(TDPL)。该语言的核心部分是使用简单的语法。
据研究人员发布的论文称,“在FPV中,由于缺乏足够的行为覆盖准则,设计人员并不明确知道FPV是否覆盖了测试计划中涉及的所有情形。”而他们则在论文中提出了构建测试计划的初步设想,并指出了测试计划中的部分内容如何使用FPV进行覆盖。研究人员建议,应该与设计架构师协同工作,共同改进编写测试计划的语法。他们称,采用ARM AMBA APB协议的一个具体案例实施效果良好。
京公网安备 11011202001138号
