Nowadays, a majority of System-on-Chips (SoCs) make use of Intellectual Property (IP) in order to shorten development cycles. When such IPs are developed, one of the main focuses lies in the high configurability of the design. This flexibility on the design side introduces the challenge of covering a huge state space of IP configurations on the verification side to ensure the functional correctness under every possible parameter setting. The vast number of possibilities does not allow a brute-force approach, and therefore, only a selected number of settings based on typical and extreme assumptions are usually verified. Especially in automotive applications, which need to follow the ISO 26262 functional safety standard, the requirement of covering all significant variants needs to be fulfilled in any case. State-of-the-Art existing verification techniques such as simulation-based verification and formal verification have challenges such as time-space explosion and state-space explosion respectively and therefore, lack behind in verifying highly configurable digital designs efficiently. This paper is focused on a semi-formal verification methodology for efficient configuration coverage of highly configurable digital designs. The methodology focuses on reduced runtime based on simulative and formal methods that allow high configuration coverage. The paper also presents the results when the developed methodology was applied on a highly configurable microprocessor IP and discusses the gained benefits.

翻译：如今，大多数片上系统（SoC）都采用知识产权（IP）核以缩短开发周期。在开发此类IP核时，主要关注点之一在于设计的高度可配置性。这种设计端的灵活性给验证端带来了挑战——需要覆盖IP配置的庞大状态空间，以确保在每种可能的参数设置下功能正确性。由于组合数量过于庞大，无法采用暴力验证方法，因此通常仅基于典型和极端假设选择有限数量的配置进行验证。尤其在需要遵循ISO 26262功能安全标准的汽车应用中，必须满足覆盖所有关键变体的要求。现有的仿真验证与形式化验证等先进技术分别面临时间-空间爆炸和状态空间爆炸的挑战，难以高效验证高度可配置的数字设计。本文聚焦于一种面向高可配置数字设计的半形式化验证方法，旨在实现高效的配置覆盖。该方法基于仿真与形式化方法的结合，通过降低运行时间实现高配置覆盖。文中还展示了将该方法应用于高度可配置的微处理器IP核的实验结果，并讨论了其优势。